equal
deleted
inserted
replaced
154 (HOLogic.exists_const ty $ |
154 (HOLogic.exists_const ty $ |
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 |
|
160 ML {* |
|
161 typedef_term @{term "x::nat\<Rightarrow>nat\<Rightarrow>bool"} @{typ nat} @{context} |
|
162 |> Syntax.string_of_term @{context} |
|
163 |> writeln |
|
164 *} |
|
165 |
|
166 |
|
167 ML {* |
159 ML {* |
168 (* makes the new type definitions and proves non-emptyness*) |
160 (* makes the new type definitions and proves non-emptyness*) |
169 fun typedef_make (qty_name, rel, ty) lthy = |
161 fun typedef_make (qty_name, rel, ty) lthy = |
170 let |
162 let |
171 val typedef_tac = |
163 val typedef_tac = |
181 NONE typedef_tac) lthy |
173 NONE typedef_tac) lthy |
182 end |
174 end |
183 *} |
175 *} |
184 |
176 |
185 ML {* |
177 ML {* |
186 (* proves the QUOT_TYPE theorem for the new type *) |
178 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
187 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
179 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
188 let |
180 let |
189 val rep_thm = #Rep typedef_info |
181 val rep_thm = #Rep typedef_info |
190 val rep_inv = #Rep_inverse typedef_info |
182 val rep_inv = #Rep_inverse typedef_info |
191 val abs_inv = #Abs_inverse typedef_info |
183 val abs_inv = #Abs_inverse typedef_info |
213 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
205 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
214 end |
206 end |
215 *} |
207 *} |
216 |
208 |
217 ML {* |
209 ML {* |
|
210 (* proves the quotient theorem *) |
218 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
211 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
219 let |
212 let |
220 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
213 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
221 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
214 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
222 |> Syntax.check_term lthy |
215 |> Syntax.check_term lthy |
709 shows "(z # xs) \<approx> (z # ys)" |
702 shows "(z # xs) \<approx> (z # ys)" |
710 using a by (rule QuotMain.list_eq.intros(5)) |
703 using a by (rule QuotMain.list_eq.intros(5)) |
711 |
704 |
712 |
705 |
713 text {* |
706 text {* |
714 unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)' |
707 Unlam_def converts a definition given as |
715 to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left. |
708 |
|
709 c \<equiv> %x. %y. f x y |
|
710 |
|
711 to a theorem of the form |
|
712 |
|
713 c x y \<equiv> f x y |
|
714 |
|
715 This function is needed to rewrite the right-hand |
|
716 side to the left-hand side. |
716 *} |
717 *} |
717 |
718 |
718 ML {* |
719 ML {* |
719 fun unlam_def_aux orig_ctxt ctxt t = |
720 fun unlam_def_aux orig_ctxt ctxt t = |
720 let val rhs = Thm.rhs_of t in |
721 let val rhs = Thm.rhs_of t in |
851 val concl2 = term_of (#prop (crep_thm thm)) |
852 val concl2 = term_of (#prop (crep_thm thm)) |
852 in |
853 in |
853 Logic.mk_equals ((build_aux concl2), concl2) |
854 Logic.mk_equals ((build_aux concl2), concl2) |
854 end *} |
855 end *} |
855 |
856 |
|
857 thm EMPTY_def IN_def UNION_def |
|
858 |
856 ML {* val emptyt = symmetric (unlam_def @{context} @{thm EMPTY_def}) *} |
859 ML {* val emptyt = symmetric (unlam_def @{context} @{thm EMPTY_def}) *} |
857 ML {* val in_t = symmetric (unlam_def @{context} @{thm IN_def}) *} |
860 ML {* val in_t = symmetric (unlam_def @{context} @{thm IN_def}) *} |
858 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
861 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
859 ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} |
862 ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} |
860 ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} |
863 ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} |