equal
deleted
inserted
replaced
37 in |
37 in |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
39 end |
39 end |
40 |
40 |
41 |
41 |
|
42 (********************************) |
42 (* definition of quotient types *) |
43 (* definition of quotient types *) |
43 (********************************) |
44 (********************************) |
44 |
45 |
45 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
46 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
46 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
47 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
50 let |
51 let |
51 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
52 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
52 |> Variable.variant_frees lthy [rel] |
53 |> Variable.variant_frees lthy [rel] |
53 |> map Free |
54 |> map Free |
54 in |
55 in |
55 lambda c |
56 lambda c (HOLogic.exists_const rty $ |
56 (HOLogic.exists_const rty $ |
57 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
57 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
58 end |
58 end |
59 |
59 |
60 |
60 (* makes the new type definitions and proves non-emptyness *) |
61 (* makes the new type definitions and proves non-emptyness *) |
61 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
62 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
62 let |
63 let |
63 val typedef_tac = |
64 val typedef_tac = |
67 rtac @{thm refl}] |
68 rtac @{thm refl}] |
68 in |
69 in |
69 Local_Theory.theory_result |
70 Local_Theory.theory_result |
70 (Typedef.add_typedef false NONE |
71 (Typedef.add_typedef false NONE |
71 (qty_name, vs, mx) |
72 (qty_name, vs, mx) |
72 (typedef_term rel rty lthy) |
73 (typedef_term rel rty lthy) |
73 NONE typedef_tac) lthy |
74 NONE typedef_tac) lthy |
74 end |
75 end |
|
76 |
75 |
77 |
76 (* tactic to prove the Quot_Type theorem for the new type *) |
78 (* tactic to prove the Quot_Type theorem for the new type *) |
77 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
79 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
78 let |
80 let |
79 val rep_thm = (#Rep typedef_info) RS mem_def1 |
81 val rep_thm = (#Rep typedef_info) RS mem_def1 |
87 rtac rep_inv, |
89 rtac rep_inv, |
88 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
90 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
89 rtac rep_inj]) 1 |
91 rtac rep_inj]) 1 |
90 end |
92 end |
91 |
93 |
|
94 |
92 (* proves the Quot_Type theorem *) |
95 (* proves the Quot_Type theorem *) |
93 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
96 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
94 let |
97 let |
95 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
98 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
96 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
99 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
113 rtac quot_type_thm] |
116 rtac quot_type_thm] |
114 in |
117 in |
115 Goal.prove lthy [] [] goal |
118 Goal.prove lthy [] [] goal |
116 (K typedef_quotient_thm_tac) |
119 (K typedef_quotient_thm_tac) |
117 end |
120 end |
|
121 |
118 |
122 |
119 (* main function for constructing a quotient type *) |
123 (* main function for constructing a quotient type *) |
120 fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
124 fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
121 let |
125 let |
122 (* generates the typedef *) |
126 (* generates the typedef *) |
161 in |
165 in |
162 lthy4 |
166 lthy4 |
163 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
167 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
164 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
168 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
165 end |
169 end |
|
170 |
166 |
171 |
167 (* sanity checks of the quotient type specifications *) |
172 (* sanity checks of the quotient type specifications *) |
168 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
173 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
169 let |
174 let |
170 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
175 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
201 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
206 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
202 in |
207 in |
203 if null errs then () else error (cat_lines errs) |
208 if null errs then () else error (cat_lines errs) |
204 end |
209 end |
205 |
210 |
|
211 |
|
212 (******************************) |
206 (* interface and syntax setup *) |
213 (* interface and syntax setup *) |
|
214 (******************************) |
207 |
215 |
208 (* the ML-interface takes a list of 5-tuples consisting of *) |
216 (* the ML-interface takes a list of 5-tuples consisting of *) |
209 (* *) |
217 (* *) |
210 (* - the name of the quotient type *) |
218 (* - the name of the quotient type *) |
211 (* - its free type variables (first argument) *) |
219 (* - its free type variables (first argument) *) |