36 "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; |
36 "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; |
37 by (rtac Pow_mono 1); |
37 by (rtac Pow_mono 1); |
38 by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); |
38 by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); |
39 by (etac subset_trans 1); |
39 by (etac subset_trans 1); |
40 by (rtac (arg_subset_eclose RS univ_mono) 1); |
40 by (rtac (arg_subset_eclose RS univ_mono) 1); |
41 by (simp_tac (!simpset addsimps [Union_Pow_eq]) 1); |
41 by (simp_tac (simpset() addsimps [Union_Pow_eq]) 1); |
42 qed "MapQU_lemma"; |
42 qed "MapQU_lemma"; |
43 |
43 |
44 (* Theorems *) |
44 (* Theorems *) |
45 |
45 |
46 val prems = goalw Map.thy [PMap_def,TMap_def] |
46 val prems = goalw Map.thy [PMap_def,TMap_def] |
67 (* ############################################################ *) |
67 (* ############################################################ *) |
68 |
68 |
69 (** map_emp **) |
69 (** map_emp **) |
70 |
70 |
71 goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)"; |
71 goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)"; |
72 by (safe_tac (!claset)); |
72 by (safe_tac (claset())); |
73 by (rtac image_02 1); |
73 by (rtac image_02 1); |
74 qed "pmap_empI"; |
74 qed "pmap_empI"; |
75 |
75 |
76 (** map_owr **) |
76 (** map_owr **) |
77 |
77 |
78 |
78 |
79 goalw Map.thy [map_owr_def,PMap_def,TMap_def] |
79 goalw Map.thy [map_owr_def,PMap_def,TMap_def] |
80 "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
80 "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
81 by Safe_tac; |
81 by Safe_tac; |
82 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff]))); |
82 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff]))); |
83 by (Fast_tac 1); |
83 by (Fast_tac 1); |
84 by (Fast_tac 1); |
84 by (Fast_tac 1); |
85 by (Deepen_tac 2 1); |
85 by (Deepen_tac 2 1); |
86 (*Remaining subgoal*) |
86 (*Remaining subgoal*) |
87 by (rtac (excluded_middle RS disjE) 1); |
87 by (rtac (excluded_middle RS disjE) 1); |
88 by (etac image_Sigma1 1); |
88 by (etac image_Sigma1 1); |
89 by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1); |
89 by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1); |
90 by (asm_full_simp_tac |
90 by (asm_full_simp_tac |
91 (!simpset addsimps [qbeta] setloop split_tac [expand_if]) 1); |
91 (simpset() addsimps [qbeta] setloop split_tac [expand_if]) 1); |
92 by (safe_tac (!claset)); |
92 by (safe_tac (claset())); |
93 by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3); |
93 by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3); |
94 by (ALLGOALS Asm_full_simp_tac); |
94 by (ALLGOALS Asm_full_simp_tac); |
95 by (Fast_tac 1); |
95 by (Fast_tac 1); |
96 qed "pmap_owrI"; |
96 qed "pmap_owrI"; |
97 |
97 |
154 by (Fast_tac 1); |
154 by (Fast_tac 1); |
155 qed "map_domain_emp"; |
155 qed "map_domain_emp"; |
156 |
156 |
157 goalw Map.thy [map_owr_def] |
157 goalw Map.thy [map_owr_def] |
158 "!!a. b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; |
158 "!!a. b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; |
159 by (simp_tac (!simpset addsimps [domain_Sigma]) 1); |
159 by (simp_tac (simpset() addsimps [domain_Sigma]) 1); |
160 by (rtac equalityI 1); |
160 by (rtac equalityI 1); |
161 by (Fast_tac 1); |
161 by (Fast_tac 1); |
162 by (rtac subsetI 1); |
162 by (rtac subsetI 1); |
163 by (rtac CollectI 1); |
163 by (rtac CollectI 1); |
164 by (assume_tac 1); |
164 by (assume_tac 1); |
165 by (etac UnE' 1); |
165 by (etac UnE' 1); |
166 by (etac singletonE 1); |
166 by (etac singletonE 1); |
167 by (Asm_simp_tac 1); |
167 by (Asm_simp_tac 1); |
168 by (Fast_tac 1); |
168 by (Fast_tac 1); |
169 by (fast_tac (!claset addss (!simpset)) 1); |
169 by (fast_tac (claset() addss (simpset())) 1); |
170 qed "map_domain_owr"; |
170 qed "map_domain_owr"; |
171 |
171 |
172 (** Application **) |
172 (** Application **) |
173 |
173 |
174 goalw Map.thy [map_app_def,map_owr_def] |
174 goalw Map.thy [map_app_def,map_owr_def] |