# HG changeset patch # User Cezary Kaliszyk # Date 1260054047 -3600 # Node ID 5dffcd087e306cc1135caa7799beb92ec9261765 # Parent 4eca2c3e59f7107eca1261c97ed1a6c5ea9dbe80 Definitions folded first. diff -r 4eca2c3e59f7 -r 5dffcd087e30 LFex.thy --- a/LFex.thy Sat Dec 05 23:35:09 2009 +0100 +++ b/LFex.thy Sun Dec 06 00:00:47 2009 +0100 @@ -220,6 +220,7 @@ val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot *} lemma @@ -256,12 +257,11 @@ ((x5 :: TRM) = x6 \ P3 x5 x6)" using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 apply - -apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *}) -(*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) +apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) +apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) +apply(fold perm_kind_def perm_ty_def perm_trm_def FV_ty_def[simplified id_simps] FV_kind_def[simplified id_simps] FV_trm_def[simplified id_simps]) apply(tactic {* clean_tac @{context} 1 *}) -*) -(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) (* Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} @@ -270,8 +270,6 @@ ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) -apply(unfold perm_kind_def perm_ty_def perm_trm_def) -apply(tactic {* clean_tac @{context} 1 *}) done (* Does not work: diff -r 4eca2c3e59f7 -r 5dffcd087e30 LamEx.thy --- a/LamEx.thy Sat Dec 05 23:35:09 2009 +0100 +++ b/LamEx.thy Sun Dec 06 00:00:47 2009 +0100 @@ -190,14 +190,20 @@ lemma fv_var: "fv (Var (a\name)) = {a}" apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma a1: "(a\name) = (b\name) \ Var a = Var b" @@ -210,6 +216,8 @@ lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; @@ -217,6 +225,8 @@ \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); @@ -225,6 +235,8 @@ \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ \ qxb qx qxa" apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma var_inject: "(Var a = Var b) = (a = b)" diff -r 4eca2c3e59f7 -r 5dffcd087e30 QuotMain.thy --- a/QuotMain.thy Sat Dec 05 23:35:09 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 00:00:47 2009 +0100 @@ -1105,10 +1105,9 @@ let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - val thms1 = @{thms all_prs ex_prs} + val thms1 = @{thms all_prs ex_prs} @ defs val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} - @ defs fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver (* FIXME: use of someting smaller than HOL_basic_ss *) in