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