# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264763768 -3600
# Node ID 74e9a580448cd57e8a2251e3f8499ea4529d8aad
# Parent  928e80edf138d82bd11563f24c577f7bc9cbd5c0
equivariance of rfv and alpha.

diff -r 928e80edf138 -r 74e9a580448c Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Fri Jan 29 10:13:07 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Fri Jan 29 12:16:08 2010 +0100
@@ -1,24 +1,25 @@
 theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"  "Abs"
 begin
 
 atom_decl name
 atom_decl ident
 
-datatype kind = 
+datatype kind =
     Type
   | KPi "ty" "name" "kind"
-and ty =  
+and ty =
     TConst "ident"
   | TApp "ty" "trm"
   | TPi "ty" "name" "ty"
-and trm = 
+and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
-  | Lam "ty" "name" "trm" 
+  | Lam "ty" "name" "trm"
+print_theorems
 
-fun
+primrec
     rfv_kind :: "kind \<Rightarrow> atom set"
 and rfv_ty   :: "ty \<Rightarrow> atom set"
 and rfv_trm  :: "trm \<Rightarrow> atom set"
@@ -58,7 +59,7 @@
 instance
 apply default
 apply (simp_all only:rperm_zero_ok)
-apply(induct_tac [!] x)
+apply(induct_tac[!] x)
 apply(simp_all)
 apply(induct_tac ty)
 apply(simp_all)
@@ -110,6 +111,114 @@
 by (size_change)
 *)
 
+lemma akind_aty_artm_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)"
+  "(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'))"
+  "(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'))"
+apply -
+apply (simp add: akind_aty_atrm.intros)
+
+apply rule apply (erule akind.cases) apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply simp
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply simp
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+done
+
+(* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)
+lemma rfv_eqvt_tmp:
+  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1)) \<and>
+  ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2)) \<and>
+  ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
+thm kind_ty_trm.induct
+(*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
+apply(rule kind_ty_trm.induct[of
+  "\<lambda>t1. ((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
+  "\<lambda>t2. ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
+  "\<lambda>t3. ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"])
+apply(simp_all add:  union_eqvt Diff_eqvt)
+apply(simp_all add: permute_set_eq atom_eqvt)
+done
+
+lemma rfv_eqvt[eqvt]:
+  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
+  "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
+  "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
+(*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
+apply(simp_all only: rfv_eqvt_tmp)
+done
+
+lemma alpha_eqvt:
+  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
+  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+  "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])
+done
+
 lemma al_refl:
   fixes K::"kind" 
   and   A::"ty"
@@ -209,7 +318,6 @@
 as
   "rfv_trm"
 
-thm akind_aty_atrm.induct
 lemma alpha_rfv:
   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
@@ -222,21 +330,14 @@
   "(op = ===> akind ===> akind) permute permute"
   "(op = ===> aty ===> aty) permute permute"
   "(op = ===> atrm ===> atrm) permute permute"
-apply simp_all
-sorry (* by eqvt *)
+  by (simp_all add:alpha_eqvt)
 
-lemma kpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> akind ===> akind) KPi KPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 lemma tconst_rsp[quot_respect]: 
   "(op = ===> aty) TConst TConst"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma tapp_rsp[quot_respect]: 
   "(aty ===> atrm ===> aty) TApp TApp" 
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
-lemma tpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> aty ===> aty) TPi TPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 lemma var_rsp[quot_respect]: 
   "(op = ===> atrm) Var Var"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
@@ -246,9 +347,17 @@
 lemma const_rsp[quot_respect]: 
   "(op = ===> atrm) Const Const"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+
+lemma kpi_rsp[quot_respect]: 
+  "(aty ===> op = ===> akind ===> akind) KPi KPi"
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+lemma tpi_rsp[quot_respect]: 
+  "(aty ===> op = ===> aty ===> aty) TPi TPi"
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+
 lemma rfv_ty_rsp[quot_respect]: 
   "(aty ===> op =) rfv_ty rfv_ty"
   by (simp add: alpha_rfv)
@@ -259,9 +368,6 @@
   "(atrm ===> op =) rfv_trm rfv_trm"
   by (simp add: alpha_rfv)
 
-thm akind_aty_atrm.induct
-thm kind_ty_trm.induct
-
 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);
  \<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);