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