141 end |
141 end |
142 |
142 |
143 section {* type definition for the quotient type *} |
143 section {* type definition for the quotient type *} |
144 |
144 |
145 ML {* |
145 ML {* |
146 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *) |
146 (* constructs the term \<lambda>(c::rty \<Rightarrow> bool). \<exists>x. c = rel x *) |
147 fun typedef_term rel ty lthy = |
147 fun typedef_term rel rty lthy = |
148 let |
148 let |
149 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
149 val [x, c] = [("x", rty), ("c", rty --> @{typ bool})] |
150 |> Variable.variant_frees lthy [rel] |
150 |> Variable.variant_frees lthy [rel] |
151 |> map Free |
151 |> map Free |
152 in |
152 in |
153 lambda c |
153 lambda c |
154 (HOLogic.exists_const ty $ |
154 (HOLogic.exists_const rty $ |
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
156 end |
156 end |
157 *} |
157 *} |
158 |
158 |
159 ML {* |
159 ML {* |
160 (* makes the new type definitions and proves non-emptyness*) |
160 (* makes the new type definitions and proves non-emptyness*) |
161 fun typedef_make (qty_name, mx, rel, ty) lthy = |
161 fun typedef_make (qty_name, mx, rel, rty) lthy = |
162 let |
162 let |
163 val typedef_tac = |
163 val typedef_tac = |
164 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
164 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
165 rtac @{thm exI}, |
165 rtac @{thm exI}, |
166 rtac @{thm exI}, |
166 rtac @{thm exI}, |
167 rtac @{thm refl}] |
167 rtac @{thm refl}] |
168 val tfrees = map fst (Term.add_tfreesT ty []) |
168 val tfrees = map fst (Term.add_tfreesT rty []) |
169 in |
169 in |
170 LocalTheory.theory_result |
170 LocalTheory.theory_result |
171 (Typedef.add_typedef false NONE |
171 (Typedef.add_typedef false NONE |
172 (qty_name, tfrees, mx) |
172 (qty_name, tfrees, mx) |
173 (typedef_term rel ty lthy) |
173 (typedef_term rel rty lthy) |
174 NONE typedef_tac) lthy |
174 NONE typedef_tac) lthy |
175 end |
175 end |
176 *} |
176 *} |
177 |
177 |
178 ML {* |
178 ML {* |
200 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
200 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
201 let |
201 let |
202 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
202 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
203 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
203 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
204 |> Syntax.check_term lthy |
204 |> Syntax.check_term lthy |
205 val _ = goal |> Syntax.string_of_term lthy |> tracing |
|
206 in |
205 in |
207 Goal.prove lthy [] [] goal |
206 Goal.prove lthy [] [] goal |
208 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
207 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
209 end |
208 end |
210 |
209 *} |
211 |
210 |
|
211 ML {* |
212 (* proves the quotient theorem *) |
212 (* proves the quotient theorem *) |
213 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
213 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
214 let |
214 let |
215 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
215 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
216 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
216 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
253 val ((_, [th']), _) = Variable.import true [th] ctxt; |
253 val ((_, [th']), _) = Variable.import true [th] ctxt; |
254 in th' end); |
254 in th' end); |
255 *} |
255 *} |
256 |
256 |
257 ML {* |
257 ML {* |
258 fun typedef_main (qty_name, mx, rel, ty, equiv_thm) lthy = |
258 fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
259 let |
259 let |
260 (* generates typedef *) |
260 (* generates typedef *) |
261 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, ty) lthy |
261 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
262 |
262 |
263 (* abs and rep functions *) |
263 (* abs and rep functions *) |
264 val abs_ty = #abs_type typedef_info |
264 val abs_ty = #abs_type typedef_info |
265 val rep_ty = #rep_type typedef_info |
265 val rep_ty = #rep_type typedef_info |
266 val abs_name = #Abs_name typedef_info |
266 val abs_name = #Abs_name typedef_info |
438 end |
438 end |
439 |
439 |
440 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
440 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
441 | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) |
441 | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) |
442 |
442 |
443 fun mk_identity ty = Abs ("x", ty, Bound 0) |
443 fun mk_identity ty = Abs ("", ty, Bound 0) |
444 |
444 |
445 in |
445 in |
446 if ty = qty |
446 if ty = qty |
447 then (get_const flag) |
447 then (get_const flag) |
448 else (case ty of |
448 else (case ty of |
1046 *} |
1046 *} |
1047 |
1047 |
1048 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1048 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1049 notation ( output) "Trueprop" ("#_" [1000] 1000) |
1049 notation ( output) "Trueprop" ("#_" [1000] 1000) |
1050 |
1050 |
1051 lemma atomize_eqv [atomize]: "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
1051 lemma atomize_eqv[atomize]: |
1052 (is "?rhs \<equiv> ?lhs") |
1052 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
1053 proof |
1053 proof |
1054 assume "PROP ?lhs" then show "PROP ?rhs" by unfold |
1054 assume "A \<equiv> B" |
|
1055 then show "Trueprop A \<equiv> Trueprop B" by unfold |
1055 next |
1056 next |
1056 assume *: "PROP ?rhs" |
1057 assume *: "Trueprop A \<equiv> Trueprop B" |
1057 have "A = B" |
1058 have "A = B" |
1058 proof (cases A) |
1059 proof (cases A) |
1059 case True |
1060 case True |
1060 with * have B by unfold |
1061 have "A" by fact |
1061 with `A` show ?thesis by simp |
1062 then show "A = B" using * by simp |
1062 next |
1063 next |
1063 case False |
1064 case False |
1064 with * have "~ B" by auto |
1065 have "\<not>A" by fact |
1065 with `~ A` show ?thesis by simp |
1066 then show "A = B" using * by auto |
1066 qed |
1067 qed |
1067 then show "PROP ?lhs" by (rule eq_reflection) |
1068 then show "A \<equiv> B" by (rule eq_reflection) |
1068 qed |
1069 qed |
1069 |
|
1070 |
1070 |
1071 prove {* (Thm.term_of cgoal2) *} |
1071 prove {* (Thm.term_of cgoal2) *} |
1072 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1072 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1073 apply (atomize(full)) |
1073 apply (atomize(full)) |
1074 apply (tactic {* foo_tac' @{context} 1 *}) |
1074 apply (tactic {* foo_tac' @{context} 1 *}) |