Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LFex.thy
changeset 437 532bcd868842
parent 432 9c33c0809733
child 439 70a4b73f82a9 
--- 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*})
+
+
+
+
nominal2