# HG changeset patch # User Christian Urban # Date 1254786613 -7200 # Node ID 33d7bcfd56031e2d3b264899b3adc0aa18243100 # Parent 980c95c2bf7ff6e1785dfaba0a06928ad3b7330d simplified the unlam_def function diff -r 980c95c2bf7f -r 33d7bcfd5603 QuotMain.thy --- a/QuotMain.thy Mon Oct 05 11:54:02 2009 +0200 +++ b/QuotMain.thy Tue Oct 06 01:50:13 2009 +0200 @@ -177,7 +177,7 @@ ML {* (* tactic to prove the QUOT_TYPE theorem for the new type *) -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = +fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) lthy = let val rep_thm = #Rep typedef_info val rep_inv = #Rep_inverse typedef_info @@ -192,19 +192,21 @@ rtac equiv_thm, rtac rep_thm_simpd, rtac rep_inv, - rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl}, + rtac abs_inv_simpd, + rtac @{thm exI}, + rtac @{thm refl}, rtac rep_inj] end - fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |> Syntax.check_term lthy + val _ = goal |> Syntax.string_of_term lthy |> tracing in Goal.prove lthy [] [] goal - (K (typedef_quot_type_tac equiv_thm typedef_info)) + (K (typedef_quot_type_tac equiv_thm typedef_info lthy)) end @@ -730,21 +732,24 @@ *} ML {* -fun unlam_def_aux orig_ctxt ctxt t = - let val rhs = Thm.rhs_of t in - (case try (Thm.dest_abs NONE) rhs of - SOME (v, vt) => - let - val (vname, vt) = Term.dest_Free (Thm.term_of v) - val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt - val nv = Free(vnname, vt) - val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) - val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 - in unlam_def_aux orig_ctxt ctxt tnorm end - | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) - end; +fun unlam_def ctxt def = +let + val (lhs, rhs) = Thm.dest_equals (cprop_of def) + val xs = strip_abs_vars (term_of rhs) + val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt -fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t + fun get_lhs [] = lhs + | get_lhs (x::xs) = + let val cx = cterm_of (ProofContext.theory_of ctxt') (Free x) + in Thm.capply (get_lhs xs) cx end + + fun get_conv [] = Conv.rewr_conv def + | get_conv (x::xs) = Conv.fun_conv (get_conv xs) + +in + get_conv xs (get_lhs (rev xs)) |> + singleton (ProofContext.export ctxt' ctxt) +end *} local_setup {* @@ -754,6 +759,9 @@ term membship term IN thm IN_def +ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}*} +ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} + ML {* unlam_def @{context} @{thm IN_def} *} lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]