# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264790527 -3600
# Node ID 333c24bd595d25ff10dc905dab2a3e6d750cb3cd
# Parent  5c0d9a507bcbac163e6afbe466200f398543a807
More in the LF example in the new nominal way, all is clear until support.

diff -r 5c0d9a507bcb -r 333c24bd595d Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Fri Jan 29 13:47:05 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Fri Jan 29 19:42:07 2010 +0100
@@ -26,13 +26,14 @@
 where
   "rfv_kind (Type) = {}"
 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {}"
+| "rfv_ty (TConst i) = {atom i}"
 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
-| "rfv_trm (Const i) = {}"
+| "rfv_trm (Const i) = {atom i}"
 | "rfv_trm (Var x) = {atom x}"
 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
+print_theorems
 
 instantiation kind and ty and trm :: pt
 begin
@@ -111,7 +112,7 @@
 by (size_change)
 *)
 
-lemma akind_aty_artm_inj:
+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')))"
   "(TConst i) \<approx>ty (TConst j) = (i = j)"
@@ -377,6 +378,29 @@
 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
 by (lifting kind_ty_trm.induct)
 
+thm kind_ty_trm.inducts
+
+lemma KIND_TY_TRM_inducts: 
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P10 kind"
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P20 ty"
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P30 trm"
+by (lifting kind_ty_trm.inducts)
+
 instantiation KIND and TY and TRM :: pt
 begin
 
@@ -395,9 +419,7 @@
 as
   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
 
-term "permute_TRM"
-thm permute_kind_permute_ty_permute_trm.simps
-lemma [simp]:
+lemma permute_ktt[simp]:
 shows "pi \<bullet> TYP = TYP"
 and   "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
 and   "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"
@@ -415,13 +437,13 @@
 apply simp_all
 done
 
-lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"
-apply(rule KIND_TY_TRM_induct[of 
-"\<lambda>x1. ((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> x1))"
-"\<lambda>x2. ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2)"
-"\<lambda>x3. ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"])
+lemma perm_add_ok: 
+  "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
+  "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
+  "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
+apply(induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
 apply (simp_all)
-sorry
+done
 
 instance
 apply default
@@ -452,8 +474,156 @@
     \<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)"
-apply (lifting akind_aty_atrm.induct)
-done
+by (lifting akind_aty_atrm.induct)
+
+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)
+
+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')))"
+  "(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'))"
+  "(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)
+
+lemma fv_kind_ty_trm:
+ "fv_kind TYP = {}"
+ "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"
+ "fv_ty (TCONST i) = {atom 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 - {atom x})"
+ "fv_trm (CONS i) = {atom i}"
+ "fv_trm (VAR x) = {atom 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 - {atom x})"
+by(lifting rfv_kind_rfv_ty_rfv_trm.simps)
+
+lemma fv_eqvt:
+ "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)"
+ "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)"
+ "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"
+by(lifting rfv_eqvt)
+
+lemma supp_fv:
+ "fv_kind t1 = supp t1"
+ "fv_ty t2 = supp t2"
+ "fv_trm t3 = supp t3"
+apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
+apply (simp_all add: fv_kind_ty_trm)
+apply (simp_all add: supp_def)
+sorry
+
+lemma
+"(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow>
+(a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) =
+(supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and>
+(\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)"
+apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A")
+apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}")
+apply simp_all
+sorry
+
+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 KIND_TY_TRM_INJECT)
+apply(simp only: supp_fv)
+apply simp
+apply (unfold supp_def)
+sorry
+
+lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+apply(subst supp_kpi_pre)
+thm supp_Abs
+(*apply(simp add: supp_Abs)*)
+sorry
+
+lemma supp_kind_ty_trm:
+ "supp TYP = {}"
+ "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+ "supp (TCONST i) = {atom i}"
+ "supp (TAPP A M) = supp A \<union> supp M"
+ "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
+ "supp (CONS i) = {atom i}"
+ "supp (VAR x) = {atom x}"
+ "supp (APP M N) = supp M \<union> supp N"
+ "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
+apply -
+apply (simp add: supp_def)
+apply (simp add: supp_kpi)
+apply (simp add: supp_def) (* need ty.distinct lifted *)
+sorry
+
 
 end