the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
theory LFeximports Nominal "../QuotList"beginatom_decl name identnominal_datatype kind = Type | KPi "ty" "name" "kind"and ty = TConst "ident" | TApp "ty" "trm" | TPi "ty" "name" "ty"and trm = Const "ident" | 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})"sorrytermination fv_kind sorryinductive 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) donelemma alpha_equivps: shows "equivp akind" and "equivp aty" and "equivp atrm"sorryquotient_type KIND = kind / akind by (rule alpha_equivps)quotient_type TY = ty / aty and TRM = trm / atrm by (auto intro: alpha_equivps)quotient_definition "TYP :: KIND"as "Type"quotient_definition "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"as "KPi"quotient_definition "TCONST :: ident \<Rightarrow> TY"as "TConst"quotient_definition "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"as "TApp"quotient_definition "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"as "TPi"(* FIXME: does not work with CONST *)quotient_definition "CONS :: ident \<Rightarrow> TRM"as "Const"quotient_definition "VAR :: name \<Rightarrow> TRM"as "Var"quotient_definition "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"as "App"quotient_definition "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"as "Lam"thm TYP_defthm KPI_defthm TCONST_defthm TAPP_defthm TPI_defthm VAR_defthm CONS_defthm APP_defthm LAM_def(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)quotient_definition "FV_kind :: KIND \<Rightarrow> name set"as "fv_kind"quotient_definition "FV_ty :: TY \<Rightarrow> name set"as "fv_ty"quotient_definition "FV_trm :: TRM \<Rightarrow> name set"as "fv_trm"thm FV_kind_defthm FV_ty_defthm 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) beginquotient_definition "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"as "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"quotient_definition "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"as "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"quotient_definition "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"as "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"end(* TODO/FIXME: Think whether these RSP theorems are true. *)lemma kpi_rsp[quot_respect]: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorrylemma tconst_rsp[quot_respect]: "(op = ===> aty) TConst TConst" sorrylemma tapp_rsp[quot_respect]: "(aty ===> atrm ===> aty) TApp TApp" sorrylemma tpi_rsp[quot_respect]: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorrylemma var_rsp[quot_respect]: "(op = ===> atrm) Var Var" sorrylemma app_rsp[quot_respect]: "(atrm ===> atrm ===> atrm) App App" sorrylemma const_rsp[quot_respect]: "(op = ===> atrm) Const Const" sorrylemma lam_rsp[quot_respect]: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorrylemma perm_kind_rsp[quot_respect]: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorrylemma perm_ty_rsp[quot_respect]: "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorrylemma perm_trm_rsp[quot_respect]: "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorrylemma fv_ty_rsp[quot_respect]: "(aty ===> op =) fv_ty fv_ty" sorrylemma fv_kind_rsp[quot_respect]: "(akind ===> op =) fv_kind fv_kind" sorrylemma fv_trm_rsp[quot_respect]: "(atrm ===> op =) fv_trm fv_trm" sorrythm akind_aty_atrm.inductthm kind_ty_trm.inductlemma assumes a0: "P1 TYP TYP" and a1: "\<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 a2: "\<And>A A' K K' x x'. \<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 a3: "\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)" and a4: "\<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 a5: "\<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 a6: "\<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 a7: "\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))" and a8: "\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))" and a9: "\<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 a10: "\<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 a11: "\<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')" shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11apply(lifting akind_aty_atrm.induct)(*Profiling:ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}ML_prf {* PolyML.profiling 1 *}ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}*) done(* Does not work:lemma assumes a0: "P1 TYP" and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" and a2: "\<And>id. P2 (TCONST id)" and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)" and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)" and a5: "\<And>id. P3 (CONS id)" and a6: "\<And>name. P3 (VAR name)" and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)" and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"using a0 a1 a2 a3 a4 a5 a6 a7 a8*)lemma "\<lbrakk>P TYP; \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind); \<And>id. Q (TCONST id); \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm); \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); \<And>id. R (CONS id); \<And>name. R (VAR name); \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"apply(lifting kind_ty_trm.induct)doneend