--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/LFex.thy Mon Dec 07 14:09:50 2009 +0100
@@ -0,0 +1,307 @@
+theory LFex
+imports Nominal "../QuotMain"
+begin
+
+atom_decl name ident
+
+nominal_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})"
+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_equivps:
+ shows "equivp akind"
+ and "equivp aty"
+ and "equivp atrm"
+sorry
+
+quotient KIND = kind / akind
+ by (rule alpha_equivps)
+
+quotient TY = ty / aty
+ and TRM = trm / atrm
+ by (auto intro: alpha_equivps)
+
+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 :: "ident \<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 :: "ident \<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[quotient_rsp]:
+ "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
+lemma tconst_rsp[quotient_rsp]:
+ "(op = ===> aty) TConst TConst" sorry
+lemma tapp_rsp[quotient_rsp]:
+ "(aty ===> atrm ===> aty) TApp TApp" sorry
+lemma tpi_rsp[quotient_rsp]:
+ "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
+lemma var_rsp[quotient_rsp]:
+ "(op = ===> atrm) Var Var" sorry
+lemma app_rsp[quotient_rsp]:
+ "(atrm ===> atrm ===> atrm) App App" sorry
+lemma const_rsp[quotient_rsp]:
+ "(op = ===> atrm) Const Const" sorry
+lemma lam_rsp[quotient_rsp]:
+ "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
+
+lemma perm_kind_rsp[quotient_rsp]:
+ "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
+lemma perm_ty_rsp[quotient_rsp]:
+ "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
+lemma perm_trm_rsp[quotient_rsp]:
+ "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
+
+lemma fv_ty_rsp[quotient_rsp]:
+ "(aty ===> op =) fv_ty fv_ty" sorry
+lemma fv_kind_rsp[quotient_rsp]:
+ "(akind ===> op =) fv_kind fv_kind" sorry
+lemma fv_trm_rsp[quotient_rsp]:
+ "(atrm ===> op =) fv_trm fv_trm" sorry
+
+
+thm akind_aty_atrm.induct
+thm kind_ty_trm.induct
+
+ML {*
+ val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
+ val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
+ val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
+ val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot
+*}
+
+lemma
+ 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 a11
+apply -
+apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(fold perm_kind_def perm_ty_def perm_trm_def)
+apply(tactic {* clean_tac @{context} 1 *})
+(*
+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(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
+done
+
+print_quotients
+
+end
+
+
+