# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# 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 \<longrightarrow> P2 x3 x4) \<and> 
          ((x5 :: TRM) = x6 \<longrightarrow> 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