175 end |
175 end |
176 *} |
176 *} |
177 |
177 |
178 ML {* |
178 ML {* |
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) lthy = |
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
181 let |
181 let |
182 val rep_thm = #Rep typedef_info |
182 val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} |
|
183 val rep_thm = #Rep typedef_info |> unfold_mem |
183 val rep_inv = #Rep_inverse typedef_info |
184 val rep_inv = #Rep_inverse typedef_info |
184 val abs_inv = #Abs_inverse typedef_info |
185 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
185 val rep_inj = #Rep_inject typedef_info |
186 val rep_inj = #Rep_inject typedef_info |
186 |
|
187 val ss = HOL_basic_ss addsimps @{thms mem_def} |
|
188 val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm |
|
189 val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv |
|
190 in |
187 in |
191 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
188 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
192 rtac equiv_thm, |
189 rtac equiv_thm, |
193 rtac rep_thm_simpd, |
190 rtac rep_thm, |
194 rtac rep_inv, |
191 rtac rep_inv, |
195 rtac abs_inv_simpd, |
192 rtac abs_inv, |
196 rtac @{thm exI}, |
193 rtac @{thm exI}, |
197 rtac @{thm refl}, |
194 rtac @{thm refl}, |
198 rtac rep_inj] |
195 rtac rep_inj] |
199 end |
196 end |
200 |
197 *} |
|
198 |
|
199 ML {* |
201 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 = |
202 let |
201 let |
203 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
202 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
204 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
203 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
205 |> Syntax.check_term lthy |
204 |> Syntax.check_term lthy |
206 val _ = goal |> Syntax.string_of_term lthy |> tracing |
205 val _ = goal |> Syntax.string_of_term lthy |> tracing |
207 in |
206 in |
208 Goal.prove lthy [] [] goal |
207 Goal.prove lthy [] [] goal |
209 (K (typedef_quot_type_tac equiv_thm typedef_info lthy)) |
208 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
210 end |
209 end |
211 |
210 |
212 |
211 |
213 (* proves the quotient theorem *) |
212 (* proves the quotient theorem *) |
214 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 = |