removed old inj_repabs_tac; kept only the one with (selective) debugging information
theory LFex
imports Nominal QuotMain
begin
atom_decl name id
nominal_datatype kind =
Type
| KPi "ty" "name" "kind"
and ty =
TConst "id"
| TApp "ty" "trm"
| TPi "ty" "name" "ty"
and trm =
Const "id"
| Var "name"
| App "trm" "trm"
| Lam "ty" "name" "trm"
function
fv_kind :: "kind \<Rightarrow> name set"
and fv_ty :: "ty \<Rightarrow> name set"
and fv_trm :: "trm \<Rightarrow> name set"
where
"fv_kind (Type) = {}"
| "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})"
| "fv_ty (TConst i) = {}"
| "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)"
| "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})"
| "fv_trm (Const i) = {}"
| "fv_trm (Var x) = {x}"
| "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)"
| "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})"
sorry
termination fv_kind sorry
inductive
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
where
a1: "(Type) \<approx>ki (Type)"
| a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')"
| a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk>
\<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
| a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')"
| a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk>
\<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
| a6: "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)"
| a7: "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)"
| a8: "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
| a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')"
| a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk>
\<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
lemma al_refl:
fixes K::"kind"
and A::"ty"
and M::"trm"
shows "K \<approx>ki K"
and "A \<approx>ty A"
and "M \<approx>tr M"
apply(induct K and A and M rule: kind_ty_trm.inducts)
apply(auto intro: akind_aty_atrm.intros)
done
lemma alpha_EQUIVs:
shows "EQUIV akind"
and "EQUIV aty"
and "EQUIV atrm"
sorry
quotient KIND = kind / akind
by (rule alpha_EQUIVs)
quotient TY = ty / aty
and TRM = trm / atrm
by (auto intro: alpha_EQUIVs)
print_quotients
quotient_def
TYP :: "KIND"
where
"TYP \<equiv> Type"
quotient_def
KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
where
"KPI \<equiv> KPi"
quotient_def
TCONST :: "id \<Rightarrow> TY"
where
"TCONST \<equiv> TConst"
quotient_def
TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
where
"TAPP \<equiv> TApp"
quotient_def
TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
where
"TPI \<equiv> TPi"
(* FIXME: does not work with CONST *)
quotient_def
CONS :: "id \<Rightarrow> TRM"
where
"CONS \<equiv> Const"
quotient_def
VAR :: "name \<Rightarrow> TRM"
where
"VAR \<equiv> Var"
quotient_def
APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
where
"APP \<equiv> App"
quotient_def
LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
where
"LAM \<equiv> Lam"
thm TYP_def
thm KPI_def
thm TCONST_def
thm TAPP_def
thm TPI_def
thm VAR_def
thm CONS_def
thm APP_def
thm LAM_def
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_def
FV_kind :: "KIND \<Rightarrow> name set"
where
"FV_kind \<equiv> fv_kind"
quotient_def
FV_ty :: "TY \<Rightarrow> name set"
where
"FV_ty \<equiv> fv_ty"
quotient_def
FV_trm :: "TRM \<Rightarrow> name set"
where
"FV_trm \<equiv> fv_trm"
thm FV_kind_def
thm FV_ty_def
thm FV_trm_def
(* FIXME: does not work yet *)
overloading
perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked)
perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked)
perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked)
begin
quotient_def
perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
where
"perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
quotient_def
perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
where
"perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
quotient_def
perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
where
"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 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 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_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
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}
*}
lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
\<And>A A' K x x' K'.
\<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk>
\<Longrightarrow> P1 (KPI A x K) (KPI A' x' K');
\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
\<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
\<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B');
\<And>A A' B x x' B'.
\<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk>
\<Longrightarrow> P2 (TPI A x B) (TPI A' x' B');
\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j)); \<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y));
\<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N');
\<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M');
\<And>A A' M x x' M' B'.
\<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk>
\<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk>
\<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
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 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 *})
prefer 2
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 *}
ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<longrightarrow>"]}) 1 *})
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)
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)
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)
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)
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 {* 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 trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} 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 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 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 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 trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* 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 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 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 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 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 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 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 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 kind} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp} 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 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 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 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 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 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 kind} 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 kind} 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 kind} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp} 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 @{thms tconst_rsp} 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 {* 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 @{thms fv_ty_rsp} 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 @{thms fv_ty_rsp} 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 @{thms fv_ty_rsp} 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 @{thms fv_ty_rsp} 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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp} 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 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp} 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 @{thms const_rsp} 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 @{thms var_rsp} 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 @{thms app_rsp} 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 {* 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 ty} quot rel_refl trans2 [] 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp} 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 {* 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 {* 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 @{thms perm_trm_rsp} 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 @{thms perm_trm_rsp} 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 @{thms fv_ty_rsp} 1*})
apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp} 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 {* 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