# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259394384 -3600
# Node ID 42e7f323913a60c12d2f2eb198a5980f9f37502a
# Parent  0af649448a11661575c4974a9e643b03ce9eb5bd
Manually finished LF induction.

diff -r 0af649448a11 -r 42e7f323913a LFex.thy
--- a/LFex.thy	Sat Nov 28 08:04:23 2009 +0100
+++ b/LFex.thy	Sat Nov 28 08:46:24 2009 +0100
@@ -181,17 +181,23 @@
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma KPi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi"
-sorry
-
-lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>"
-sorry
+lemma kpi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
+lemma tconst_rsp: "(op = ===> aty) TConst TConst" sorry
+lemma tapp_rsp: "(aty ===> atrm ===> aty) TApp TApp" sorry
+lemma tpi_rsp: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
+lemma var_rsp: "(op = ===> atrm) Var Var" sorry
+lemma app_rsp: "(atrm ===> atrm ===> atrm) App App" sorry
+lemma const_rsp: "(op = ===> atrm) Const Const" sorry
+lemma lam_rsp: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty"
-sorry
+lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
+lemma perm_ty_rsp: "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
+lemma perm_trm_rsp: "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind"
-sorry
+lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty" sorry
+lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind" sorry
+lemma fv_trm_rsp: "(atrm ===> op =) fv_trm fv_trm" sorry
+
 
 thm akind_aty_atrm.induct
 
@@ -318,7 +324,7 @@
 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 {* 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 {* 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*})
@@ -350,39 +356,113 @@
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 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 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms KPi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
-
-
-
-
-
-
-
-
-
-
-
-
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 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 @{thms tconst_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 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 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 nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 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 @{thms fv_ty_rsp}) 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 @{thms fv_ty_rsp}) 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 trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 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 {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 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 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 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 trm} quot rel_refl trans2 @{thms const_rsp}) 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 trm} quot rel_refl trans2 @{thms var_rsp}) 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 trm} quot rel_refl trans2 @{thms app_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 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 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 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 {* 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 {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_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 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 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 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 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 {* 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 {* 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 {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 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 trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 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 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 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 {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+done
 
 print_quotients
-apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*})
-
-
-ML {* val consts = lookup_quot_consts defs *}
-
-ML {*
-val rty_qty_rel =
-  [(@{typ kind}, (@{typ KIND}, @{term akind})),
-   (@{typ ty}, (@{typ TY}, @{term aty})),
-   (@{typ trm}, (@{typ TRM}, @{term atrm}))]
-*}
-
-print_quotients
-
-ML {* val rty = [@{typ }] *}
-ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
-ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}
-prove {* build_regularize_goal t_a rty rel @{context}
 
 end