(* Title: ZF/Induct/Rmap.thy ID: $Id: Rmap.thy,v 1.4 2005/06/17 14:15:11 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) header {* An operator to ``map'' a relation over a list *} theory Rmap imports Main begin consts rmap :: "i=>i" inductive domains "rmap(r)" ⊆ "list(domain(r)) × list(range(r))" intros NilI: "<Nil,Nil> ∈ rmap(r)" ConsI: "[| <x,y>: r; <xs,ys> ∈ rmap(r) |] ==> <Cons(x,xs), Cons(y,ys)> ∈ rmap(r)" type_intros domainI rangeI list.intros lemma rmap_mono: "r ⊆ s ==> rmap(r) ⊆ rmap(s)" apply (unfold rmap.defs) apply (rule lfp_mono) apply (rule rmap.bnd_mono)+ apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+ done inductive_cases Nil_rmap_case [elim!]: "<Nil,zs> ∈ rmap(r)" and Cons_rmap_case [elim!]: "<Cons(x,xs),zs> ∈ rmap(r)" declare rmap.intros [intro] lemma rmap_rel_type: "r ⊆ A × B ==> rmap(r) ⊆ list(A) × list(B)" apply (rule rmap.dom_subset [THEN subset_trans]) apply (assumption | rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+ done lemma rmap_total: "A ⊆ domain(r) ==> list(A) ⊆ domain(rmap(r))" apply (rule subsetI) apply (erule list.induct) apply blast+ done lemma rmap_functional: "function(r) ==> function(rmap(r))" apply (unfold function_def) apply (rule impI [THEN allI, THEN allI]) apply (erule rmap.induct) apply blast+ done text {* \medskip If @{text f} is a function then @{text "rmap(f)"} behaves as expected. *} lemma rmap_fun_type: "f ∈ A->B ==> rmap(f): list(A)->list(B)" by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total) lemma rmap_Nil: "rmap(f)`Nil = Nil" by (unfold apply_def) blast lemma rmap_Cons: "[| f ∈ A->B; x ∈ A; xs: list(A) |] ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)" by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros) end
lemma rmap_mono:
r ⊆ s ==> rmap(r) ⊆ rmap(s)
lemmas Nil_rmap_case:
[| 〈[], zs〉 ∈ rmap(r); zs = [] ==> Q |] ==> Q
and Cons_rmap_case:
[| 〈Cons(x, xs), zs〉 ∈ rmap(r); !!y ys. [| 〈x, y〉 ∈ r; 〈xs, ys〉 ∈ rmap(r); zs = Cons(y, ys) |] ==> Q |] ==> Q
lemma rmap_rel_type:
r ⊆ A × B ==> rmap(r) ⊆ list(A) × list(B)
lemma rmap_total:
A ⊆ domain(r) ==> list(A) ⊆ domain(rmap(r))
lemma rmap_functional:
function(r) ==> function(rmap(r))
lemma rmap_fun_type:
f ∈ A -> B ==> rmap(f) ∈ list(A) -> list(B)
lemma rmap_Nil:
rmap(f) ` [] = []
lemma rmap_Cons:
[| f ∈ A -> B; x ∈ A; xs ∈ list(A) |] ==> rmap(f) ` Cons(x, xs) = Cons(f ` x, rmap(f) ` xs)