equal
deleted
inserted
replaced
92 in |
92 in |
93 (thm', lthy') |
93 (thm', lthy') |
94 end |
94 end |
95 |
95 |
96 (* main function for constructing the quotient type *) |
96 (* main function for constructing the quotient type *) |
97 fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
97 fun mk_typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
98 let |
98 let |
99 (* generates typedef *) |
99 (* generates typedef *) |
100 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
100 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
101 |
101 |
102 (* abs and rep functions *) |
102 (* abs and rep functions *) |
167 let |
167 let |
168 val (qty_name, _) = Term.dest_Type qty |
168 val (qty_name, _) = Term.dest_Type qty |
169 |
169 |
170 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
170 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
171 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
171 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
172 |
172 |
173 val _ = [Syntax.string_of_term lthy EQUIV_goal, |
|
174 Syntax.string_of_typ lthy (fastype_of rel_trm), |
|
175 Syntax.string_of_typ lthy EQUIV_ty] |
|
176 |> cat_lines |
|
177 |> tracing |
|
178 |
|
179 fun after_qed thms lthy = |
173 fun after_qed thms lthy = |
180 let |
174 let |
181 val thm = the_single (flat thms) |
175 val thm = the_single (flat thms) |
182 in |
176 in |
183 typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd |
177 mk_typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd |
184 end |
178 end |
185 in |
179 in |
186 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
180 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
187 end |
181 end |
188 |
182 |