diff -r 9cb45d022524 -r d925d9fa43dd LFex.thy
--- a/LFex.thy	Sun Nov 29 23:59:37 2009 +0100
+++ b/LFex.thy	Mon Nov 30 02:05:22 2009 +0100
@@ -214,13 +214,23 @@
 
 
 thm akind_aty_atrm.induct
-
+thm kind_ty_trm.induct
 
 ML {* val defs =
   @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
     FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
 *}
 
+ML {*
+  val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
+  val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
+  val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
+  val lower = flat (map (add_lower_defs @{context}) defs)
+  val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
+  val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+  val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+*}
+
 lemma 
   assumes a0:
   "P1 TYP TYP"
@@ -260,12 +270,6 @@
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-(* injecting *)
-ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
-ML_prf {*
-  val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
-  val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
-*}
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
@@ -457,14 +461,8 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
-(* cleaning *)
-ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
 (*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *)
 apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
-ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *}
-ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
-ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
@@ -494,6 +492,115 @@
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
 done
 
+lemma "\<lbrakk>P1 TYP;
+  \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind);
+  \<And>id. P2 (TCONST id);
+  \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm);
+  \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2);
+  \<And>id. P3 (CONS id); \<And>name. P3 (VAR name);
+  \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
+  \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
+  \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}
+apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} quot defs aps 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+(* LOOP! *)
+(* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *)
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+done
+
 print_quotients
 
 end