1(* Title: ZF/Coind/Map.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4 5Some sample proofs of inclusions for the final coalgebra "U" (by lcp). 6*) 7 8theory Map imports ZF begin 9 10definition 11 TMap :: "[i,i] => i" where 12 "TMap(A,B) == {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}" 13 14definition 15 PMap :: "[i,i] => i" where 16 "PMap(A,B) == TMap(A,cons(0,B))" 17 18(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *) 19 20definition 21 map_emp :: i where 22 "map_emp == 0" 23 24definition 25 map_owr :: "[i,i,i]=>i" where 26 "map_owr(m,a,b) == \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}" 27 28definition 29 map_app :: "[i,i]=>i" where 30 "map_app(m,a) == m``{a}" 31 32lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})" 33by (unfold TMap_def, blast) 34 35lemma "{0} \<union> TMap(I,1) \<subseteq> {1} \<union> TMap(I, {0} \<union> TMap(I,1))" 36by (unfold TMap_def, blast) 37 38lemma "{0,1} \<union> TMap(I,2) \<subseteq> {1} \<union> TMap(I, {0,1} \<union> TMap(I,2))" 39by (unfold TMap_def, blast) 40 41(*A bit too slow. 42lemma "{0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2) \<subseteq> 43 {1} \<union> TMap(I, {0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2))" 44by (unfold TMap_def, blast) 45*) 46 47(* ############################################################ *) 48(* Lemmas *) 49(* ############################################################ *) 50 51lemma qbeta_if: "Sigma(A,B)``{a} = (if a \<in> A then B(a) else 0)" 52by auto 53 54lemma qbeta: "a \<in> A ==> Sigma(A,B)``{a} = B(a)" 55by fast 56 57lemma qbeta_emp: "a\<notin>A ==> Sigma(A,B)``{a} = 0" 58by fast 59 60lemma image_Sigma1: "a \<notin> A ==> Sigma(A,B)``{a}=0" 61by fast 62 63 64(* ############################################################ *) 65(* Inclusion in Quine Universes *) 66(* ############################################################ *) 67 68(* Lemmas *) 69 70lemma MapQU_lemma: 71 "A \<subseteq> univ(X) ==> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)" 72apply (unfold quniv_def) 73apply (rule Pow_mono) 74apply (rule subset_trans [OF Sigma_mono product_univ]) 75apply (erule subset_trans) 76apply (rule arg_subset_eclose [THEN univ_mono]) 77apply (simp add: Union_Pow_eq) 78done 79 80(* Theorems *) 81 82lemma mapQU: 83 "[| m \<in> PMap(A,quniv(B)); !!x. x \<in> A ==> x \<in> univ(B) |] ==> m \<in> quniv(B)" 84apply (unfold PMap_def TMap_def) 85apply (blast intro!: MapQU_lemma [THEN subsetD]) 86done 87 88(* ############################################################ *) 89(* Monotonicity *) 90(* ############################################################ *) 91 92lemma PMap_mono: "B \<subseteq> C ==> PMap(A,B)<=PMap(A,C)" 93by (unfold PMap_def TMap_def, blast) 94 95 96(* ############################################################ *) 97(* Introduction Rules *) 98(* ############################################################ *) 99 100(** map_emp **) 101 102lemma pmap_empI: "map_emp \<in> PMap(A,B)" 103by (unfold map_emp_def PMap_def TMap_def, auto) 104 105(** map_owr **) 106 107lemma pmap_owrI: 108 "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |] ==> map_owr(m,a,b):PMap(A,B)" 109apply (unfold map_owr_def PMap_def TMap_def, safe) 110apply (simp_all add: if_iff, auto) 111(*Remaining subgoal*) 112apply (rule excluded_middle [THEN disjE]) 113apply (erule image_Sigma1) 114apply (drule_tac psi = "uu \<notin> B" for uu in asm_rl) 115apply (auto simp add: qbeta) 116done 117 118(** map_app **) 119 120lemma tmap_app_notempty: 121 "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a) \<noteq>0" 122by (unfold TMap_def map_app_def, blast) 123 124lemma tmap_appI: 125 "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B" 126by (unfold TMap_def map_app_def domain_def, blast) 127 128lemma pmap_appI: 129 "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B" 130apply (unfold PMap_def) 131apply (frule tmap_app_notempty, assumption) 132apply (drule tmap_appI, auto) 133done 134 135(** domain **) 136 137lemma tmap_domainD: 138 "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> a \<in> A" 139by (unfold TMap_def, blast) 140 141lemma pmap_domainD: 142 "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> a \<in> A" 143by (unfold PMap_def TMap_def, blast) 144 145 146(* ############################################################ *) 147(* Equalities *) 148(* ############################################################ *) 149 150(** Domain **) 151 152(* Lemmas *) 153 154lemma domain_UN: "domain(\<Union>x \<in> A. B(x)) = (\<Union>x \<in> A. domain(B(x)))" 155by fast 156 157 158lemma domain_Sigma: "domain(Sigma(A,B)) = {x \<in> A. \<exists>y. y \<in> B(x)}" 159by blast 160 161(* Theorems *) 162 163lemma map_domain_emp: "domain(map_emp) = 0" 164by (unfold map_emp_def, blast) 165 166lemma map_domain_owr: 167 "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} \<union> domain(f)" 168apply (unfold map_owr_def) 169apply (auto simp add: domain_Sigma) 170done 171 172(** Application **) 173 174lemma map_app_owr: 175 "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))" 176by (simp add: qbeta_if map_app_def map_owr_def, blast) 177 178lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b" 179by (simp add: map_app_owr) 180 181lemma map_app_owr2: "c \<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)" 182by (simp add: map_app_owr) 183 184end 185