# HG changeset patch # User Cezary Kaliszyk # Date 1273227004 -7200 # Node ID 1bebf8007677f9375e69220892f563c487d48b91 # Parent 85826b52fd9db073144690a9485bb605f469673f Regularize experiments diff -r 85826b52fd9d -r 1bebf8007677 Attic/Quot/Examples/LFex.thy --- a/Attic/Quot/Examples/LFex.thy Thu May 06 14:21:10 2010 +0200 +++ b/Attic/Quot/Examples/LFex.thy Fri May 07 12:10:04 2010 +0200 @@ -251,16 +251,50 @@ ((x3 ::TY) = x4 \ P2 x3 x4) \ ((x5 :: TRM) = x6 \ P3 x5 x6)" using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 -apply(lifting akind_aty_atrm.induct) -(* -Profiling: -ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} -ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} -ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} -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 ()))) *} -*) - done +apply(lifting_setup akind_aty_atrm.induct) +defer +apply injection +apply cleaning +apply (simp only: ball_reg_eqv[OF KIND_equivp] ball_reg_eqv[OF TRM_equivp] ball_reg_eqv[OF TY_equivp]) +apply (rule ball_reg_right)+ +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +defer +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +defer +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +defer +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply simp +apply simp +apply regularize+ +done (* Does not work: lemma