--- a/Quot/Nominal/LFex.thy Tue Feb 02 12:48:12 2010 +0100
+++ b/Quot/Nominal/LFex.thy Tue Feb 02 13:10:46 2010 +0100
@@ -80,50 +80,25 @@
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
where
a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
+| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b 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')"
-| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
+| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
| a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
| a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
-
-(*
-function(sequential)
- 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) = True"
-| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
-| "_ \<approx>ki _ = False"
-| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
-| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
-| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>ty _ = False"
-| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
-| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
-| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>tr _ = False"
-apply (pat_completeness)
-apply simp_all
-done
-termination
-by (size_change)
-*)
+| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
lemma akind_aty_atrm_inj:
"(Type) \<approx>ki (Type) = True"
- "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
+ "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
"(TConst i) \<approx>ty (TConst j) = (i = j)"
"(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
- "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
+ "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
"(Const i) \<approx>tr (Const j) = (i = j)"
"(Var x) \<approx>tr (Var y) = (x = y)"
"(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
- "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
+ "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
apply -
apply (simp add: akind_aty_atrm.intros)
@@ -167,45 +142,16 @@
"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
apply(induct rule: akind_aty_atrm.inducts)
apply (simp_all add: akind_aty_atrm.intros)
-apply(rule a2)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
-apply(rule a5)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
-apply(rule a9)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
+apply (simp_all add: akind_aty_atrm_inj)
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
done
lemma al_refl:
@@ -220,22 +166,85 @@
apply (rule a2)
apply auto
apply(rule_tac x="0" in exI)
- apply(simp_all add: fresh_star_def fresh_zero_perm)
+ apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
apply (rule a5)
apply auto
apply(rule_tac x="0" in exI)
- apply(simp_all add: fresh_star_def fresh_zero_perm)
+ apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
apply (rule a9)
apply auto
apply(rule_tac x="0" in exI)
- apply(simp_all add: fresh_star_def fresh_zero_perm)
+ apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
+ done
+
+lemma al_sym:
+ fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
+ shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
+ and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
+ and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
+ apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply (simp_all add: akind_aty_atrm_inj)
+ apply(rule alpha_gen_atom_sym)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
+ apply(rule alpha_gen_atom_sym)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
+ apply(rule alpha_gen_atom_sym)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
+ done
+
+lemma al_trans:
+ fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
+ shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
+ and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
+ and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
+ apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(erule akind.cases)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(simp add: akind_aty_atrm_inj)
+ apply(rule alpha_gen_atom_trans)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
+ apply(rotate_tac 4)
+ apply(erule aty.cases)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(rotate_tac 3)
+ apply(erule aty.cases)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(simp add: akind_aty_atrm_inj)
+ apply(rule alpha_gen_atom_trans)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
+ apply(rotate_tac 4)
+ apply(erule atrm.cases)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(rotate_tac 3)
+ apply(erule atrm.cases)
+ apply(simp_all add: akind_aty_atrm.intros)
+ apply(simp add: akind_aty_atrm_inj)
+ apply(rule alpha_gen_atom_trans)
+ apply(rule alpha_eqvt)
+ apply(assumption)+
done
lemma alpha_equivps:
shows "equivp akind"
and "equivp aty"
and "equivp atrm"
-sorry
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(auto intro: al_refl al_sym al_trans)
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(auto intro: al_refl al_sym al_trans)
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(auto intro: al_refl al_sym al_trans)
+ done
quotient_type KIND = kind / akind
by (rule alpha_equivps)
@@ -312,7 +321,7 @@
(t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
(t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
apply(rule akind_aty_atrm.induct)
- apply(simp_all)
+ apply(simp_all add: alpha_gen)
done
lemma perm_rsp[quot_respect]:
@@ -340,24 +349,24 @@
lemma kpi_rsp[quot_respect]:
"(aty ===> op = ===> akind ===> akind) KPi KPi"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
- apply (rule a2) apply simp
+ apply (rule a2) apply assumption
apply (rule_tac x="0" in exI)
- apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+ apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
done
lemma tpi_rsp[quot_respect]:
"(aty ===> op = ===> aty ===> aty) TPi TPi"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
- apply (rule a5) apply simp
+ apply (rule a5) apply assumption
apply (rule_tac x="0" in exI)
- apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+ apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
done
lemma lam_rsp[quot_respect]:
"(aty ===> op = ===> atrm ===> atrm) Lam Lam"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
- apply (rule a9) apply simp
+ apply (rule a9) apply assumption
apply (rule_tac x="0" in exI)
- apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+ apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
done
lemma rfv_ty_rsp[quot_respect]:
@@ -370,7 +379,12 @@
"(atrm ===> op =) rfv_trm rfv_trm"
by (simp add: alpha_rfv)
-lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
+thm kind_ty_trm.induct
+
+lemma KIND_TY_TRM_induct:
+ fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool"
+ shows
+"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
@@ -452,107 +466,108 @@
end
-lemma "\<lbrakk>P10 TYP TYP;
- \<And>A A' K x K' x'.
- \<lbrakk>(A :: TY) = A'; P20 A A';
- \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
- (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
- (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
- (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
- (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
-by (lifting akind_aty_atrm.induct)
+lemma AKIND_ATY_ATRM_inducts:
+"\<lbrakk>z1 = z2; P1 TYP TYP;
+ \<And>A A' a K b K'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ K) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+ \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+ \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+ \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+ \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+ \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+ \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ M) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+ \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P1 z1 z2"
+"\<lbrakk>z3 = z4; P1 TYP TYP;
+ \<And>A A' a K b K'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ K) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+ \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+ \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+ \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+ \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+ \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+ \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ M) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+ \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P2 z3 z4"
+"\<lbrakk>z5 = z6; P1 TYP TYP;
+ \<And>A A' a K b K'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ K) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+ \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+ \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+ \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+ \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+ \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+ \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+ \<lbrakk>A = A'; P2 A A';
+ \<exists>pi. ({atom a},
+ M) \<approx>gen (\<lambda>x1 x2.
+ x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+ \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P3 z5 z6"
+unfolding alpha_gen
+apply (lifting akind_aty_atrm.inducts[unfolded alpha_gen])
+done
-lemma AKIND_ATY_ATRM_inducts:
-"\<lbrakk>x10 = x20; P10 TYP TYP;
- \<And>A A' K x K' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
- (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
- (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
- (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> P10 x10 x20"
-"\<lbrakk>x30 = x40; P10 TYP TYP;
- \<And>A A' K x K' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
- (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
- (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
- (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
- \<Longrightarrow> P20 x30 x40"
-"\<lbrakk>x50 = x60; P10 TYP TYP;
- \<And>A A' K x K' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
- (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
- (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
- \<lbrakk>A = A'; P20 A A';
- \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
- (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
- \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> P30 x50 x60"
-by (lifting akind_aty_atrm.inducts)
-
+thm akind_aty_atrm_inj
lemma KIND_TY_TRM_INJECT:
"(TYP) = (TYP) = True"
- "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. (fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> (fv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) = K' \<and> (pi \<bullet> x) = x')))"
+ "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))"
"(TCONST i) = (TCONST j) = (i = j)"
"(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')"
- "(TPI A x B) = (TPI A' x' B') = ((A = A') \<and> (\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> (fv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) = B' \<and> (pi \<bullet> x) = x'))"
+ "(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))"
"(CONS i) = (CONS j) = (i = j)"
"(VAR x) = (VAR y) = (x = y)"
"(APP M N) = (APP M' N') = (M = M' \<and> N = N')"
- "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> (fv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) = M' \<and> (pi \<bullet> x) = x'))"
-by (lifting akind_aty_atrm_inj)
+ "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, M')))"
+unfolding alpha_gen
+by (lifting akind_aty_atrm_inj[unfolded alpha_gen])
lemma fv_kind_ty_trm:
"fv_kind TYP = {}"
@@ -631,32 +646,24 @@
apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
apply (simp_all add: supp_kind_ty_trm_easy)
apply (simp_all add: fv_kind_ty_trm)
-apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)")
-apply(simp add: supp_Abst Set.Un_commute)
+apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
+apply(simp add: supp_Abs Set.Un_commute)
apply(simp (no_asm) add: supp_def)
apply(simp add: KIND_TY_TRM_INJECT)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-apply(simp add: abs_eq alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen)
+apply(simp add: Abs_eq_iff alpha_gen)
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
-apply (fold supp_def)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
apply (rule refl)
-apply(subst Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-prefer 2
-apply(simp add: eqvts supp_eqvt atom_eqvt)
sorry (* Stuck *)
-lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
+lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
(*apply (subst supp_Pair[symmetric])*)
unfolding supp_def
apply (simp add: permute_set_eq)
-apply(subst abs_eq)
+apply(subst Abs_eq_iff)
apply(subst KIND_TY_TRM_INJECT)
-apply(simp only: supp_fv)
+apply(simp only: alpha_gen supp_fv)
apply simp
apply (simp_all add: Collect_imp_eq Collect_neg_eq)
apply(subst Set.Un_commute)
@@ -665,11 +672,16 @@
apply (rule refl)
prefer 2
apply (rule refl)
-sorry (* Stuck *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (rule refl)
+apply (simp_all)
+apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
+sorry (* should be true... *)
lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
apply(subst supp_kpi_pre)
-apply(subst supp_Abst)
+apply(subst supp_Abs)
apply (simp only: Set.Un_commute)
done