69 apply(simp add: equiv[simplified EQUIV_def]) |
69 apply(simp add: equiv[simplified EQUIV_def]) |
70 done |
70 done |
71 |
71 |
72 end |
72 end |
73 |
73 |
74 ML {* |
|
75 Variable.variant_frees |
|
76 *} |
|
77 |
|
78 |
|
79 section {* type definition for the quotient type *} |
74 section {* type definition for the quotient type *} |
80 |
75 |
81 ML {* |
76 ML {* |
82 (* constructs the term \<lambda>(c::ty\<Rightarrow>bool). \<exists>x. c = rel x *) |
77 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *) |
83 fun typedef_term rel ty lthy = |
78 fun typedef_term rel ty lthy = |
84 let |
79 let |
85 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
80 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
86 |> Variable.variant_frees lthy [rel] |
81 |> Variable.variant_frees lthy [rel] |
87 |> map Free |
82 |> map Free |
88 in |
83 in |
89 lambda c |
84 lambda c |
90 ((HOLogic.exists_const ty) $ |
85 (HOLogic.mk_exists |
91 (lambda x (HOLogic.mk_eq (c, (rel $ x))))) |
86 ("x", ty, HOLogic.mk_eq (c, (rel $ x)))) |
92 end |
87 end |
93 *} |
88 *} |
94 |
89 |
95 ML {* |
90 ML {* |
96 val typedef_tac = |
91 val typedef_tac = |
100 |
95 |
101 ML {* |
96 ML {* |
102 (* makes the new type definitions *) |
97 (* makes the new type definitions *) |
103 fun typedef_make (qty_name, rel, ty) lthy = |
98 fun typedef_make (qty_name, rel, ty) lthy = |
104 LocalTheory.theory_result |
99 LocalTheory.theory_result |
105 (TypedefPackage.add_typedef false NONE |
100 (Typedef.add_typedef false NONE |
106 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) |
101 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) |
107 (typedef_term rel ty lthy) |
102 (typedef_term rel ty lthy) |
108 NONE typedef_tac) lthy |
103 NONE typedef_tac) lthy |
109 *} |
104 *} |
110 |
105 |
111 text {* proves the QUOTIENT theorem for the new type *} |
106 text {* proves the QUOTIENT theorem for the new type *} |
112 ML {* |
107 ML {* |
113 fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = |
108 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
114 let |
109 let |
115 val rep_thm = #Rep typedef_info |
110 val rep_thm = #Rep typedef_info |
116 val rep_inv = #Rep_inverse typedef_info |
111 val rep_inv = #Rep_inverse typedef_info |
117 val abs_inv = #Abs_inverse typedef_info |
112 val abs_inv = #Abs_inverse typedef_info |
118 val rep_inj = #Rep_inject typedef_info |
113 val rep_inj = #Rep_inject typedef_info |