# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259385290 -3600
# Node ID 532bcd868842bb6b405fd17cc680e1f4460ca55a
# Parent  1c245f6911ddae9b97aa475c5d449983f24786c2
Looking at repabs proof in LF.

diff -r 1c245f6911dd -r 532bcd868842 LFex.thy
--- a/LFex.thy	Sat Nov 28 05:43:18 2009 +0100
+++ b/LFex.thy	Sat Nov 28 06:14:50 2009 +0100
@@ -180,6 +180,16 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
+(* TODO/FIXME: Think whether these are true. *)
+lemma KPi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi"
+sorry
+
+lemma perm_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>"
+sorry
+
+lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty"
+sorry
+
 thm akind_aty_atrm.induct
 
 
@@ -311,6 +321,125 @@
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+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 {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms KPi_rsp}) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_rsp}) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_rsp}) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+
+
+
+