# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267004678 -3600
# Node ID ae73578feb6466ec319f6aa243caefd20b4ba6d4
# Parent  c88159ffa7a3d2541bb2e83fb58c812c6420dbae
Use the infrastructure in LF. Much shorter :).

diff -r c88159ffa7a3 -r ae73578feb64 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:38:45 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:44:38 2010 +0100
@@ -19,49 +19,8 @@
   | Lam "rty" "name" "rtrm"
 
 
-instantiation rkind and rty and rtrm :: pt
-begin
-
-primrec
-    permute_rkind
-and permute_rty
-and permute_rtrm
-where
-  "permute_rkind pi Type = Type"
-| "permute_rkind pi (KPi t n k) = KPi (permute_rty pi t) (pi \<bullet> n) (permute_rkind pi k)"
-| "permute_rty pi (TConst i) = TConst (pi \<bullet> i)"
-| "permute_rty pi (TApp A M) = TApp (permute_rty pi A) (permute_rtrm pi M)"
-| "permute_rty pi (TPi A x B) = TPi (permute_rty pi A) (pi \<bullet> x) (permute_rty pi B)"
-| "permute_rtrm pi (Const i) = Const (pi \<bullet> i)"
-| "permute_rtrm pi (Var x) = Var (pi \<bullet> x)"
-| "permute_rtrm pi (App M N) = App (permute_rtrm pi M) (permute_rtrm pi N)"
-| "permute_rtrm pi (Lam A x M) = Lam (permute_rty pi A) (pi \<bullet> x) (permute_rtrm pi M)"
+setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
 
-lemma rperm_zero_ok:
-  "0 \<bullet> (x :: rkind) = x"
-  "0 \<bullet> (y :: rty) = y"
-  "0 \<bullet> (z :: rtrm) = z"
-apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
-apply(simp_all)
-done
-
-lemma rperm_plus_ok:
- "(p + q) \<bullet> (x :: rkind) = p \<bullet> q \<bullet> x"
- "(p + q) \<bullet> (y :: rty) = p \<bullet> q \<bullet> y"
- "(p + q) \<bullet> (z :: rtrm) = p \<bullet> q \<bullet> z"
-apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply (simp_all only:rperm_zero_ok rperm_plus_ok)
-done
-
-end
-
-(*
-setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
 local_setup {*
   snd o define_fv_alpha "LFex.rkind"
   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
@@ -75,96 +34,12 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
 thm alpha_rkind_alpha_rty_alpha_rtrm_inj
 
-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)"
-sorry
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
-  (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
-     @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 
-     @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
-     @{thms rkind.distinct rty.distinct rtrm.distinct}
-     @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
-     @{thms alpha_eqvt} ctxt)) ctxt)) *}
-thm alpha_equivps
-*)
-
-primrec
-    fv_rkind :: "rkind \<Rightarrow> atom set"
-and fv_rty   :: "rty \<Rightarrow> atom set"
-and fv_rtrm  :: "rtrm \<Rightarrow> atom set"
-where
-  "fv_rkind (Type) = {}"
-| "fv_rkind (KPi A x K) = (fv_rty A) \<union> ((fv_rkind K) - {atom x})"
-| "fv_rty (TConst i) = {atom i}"
-| "fv_rty (TApp A M) = (fv_rty A) \<union> (fv_rtrm M)"
-| "fv_rty (TPi A x B) = (fv_rty A) \<union> ((fv_rty B) - {atom x})"
-| "fv_rtrm (Const i) = {atom i}"
-| "fv_rtrm (Var x) = {atom x}"
-| "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"
-| "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
-
-inductive
-    alpha_rkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and alpha_rty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
-and alpha_rtrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
-where
-  a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen alpha_rkind fv_rkind 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. (({atom a}, B) \<approx>gen alpha_rty fv_rty 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. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
-
-lemma alpha_rkind_alpha_rty_alpha_rtrm_inj:
-  "(Type) \<approx>ki (Type) = True"
-  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen alpha_rkind fv_rkind 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 a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty 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 a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))))"
-apply -
-apply (simp add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rkind.cases) apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rty.cases) apply simp apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-
-apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-done
-
 lemma rfv_eqvt[eqvt]:
   "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
   "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
   "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"
 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
-apply(simp_all add:  union_eqvt Diff_eqvt)
+apply(simp_all add: union_eqvt Diff_eqvt)
 apply(simp_all add: permute_set_eq atom_eqvt)
 done
 
@@ -186,94 +61,14 @@
 apply assumption
 done
 
-lemma al_refl:
-  fixes K::"rkind" 
-  and   A::"rty"
-  and   M::"rtrm"
-  shows "K \<approx>ki K"
-  and   "A \<approx>ty A"
-  and   "M \<approx>tr M"
-  apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
-  apply(auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2))
-  apply auto
-  apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
-  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5))
-  apply auto
-  apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
-  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9))
-  apply auto
-  apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
-  done
-
-lemma al_sym:
-  fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
-  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: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-  apply(erule alpha_gen_compose_sym)
-  apply(erule alpha_eqvt)
-  apply(erule alpha_gen_compose_sym)
-  apply(erule alpha_eqvt)
-  apply(erule alpha_gen_compose_sym)
-  apply(erule alpha_eqvt)
-  done
-
-lemma al_trans:
-  fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
-  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: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(erule alpha_rkind.cases)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-  apply(erule alpha_gen_compose_trans)
-  apply(assumption)
-  apply(erule alpha_eqvt)
-  apply(rotate_tac 4)
-  apply(erule alpha_rty.cases)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(rotate_tac 3)
-  apply(erule alpha_rty.cases)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-  apply(erule alpha_gen_compose_trans)
-  apply(assumption)
-  apply(erule alpha_eqvt)
-  apply(rotate_tac 4)
-  apply(erule alpha_rtrm.cases)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(rotate_tac 3)
-  apply(erule alpha_rtrm.cases)
-  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
-  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-  apply(erule alpha_gen_compose_trans)
-  apply(assumption)
-  apply(erule alpha_eqvt)
-  done
-
-lemma alpha_equivps:
-  shows "equivp alpha_rkind"
-  and   "equivp alpha_rty"
-  and   "equivp alpha_rtrm"
-  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
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
+  (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
+     @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 
+     @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
+     @{thms rkind.distinct rty.distinct rtrm.distinct}
+     @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
+     @{thms alpha_eqvt} ctxt)) ctxt)) *}
+thm alpha_equivps
 
 quotient_type RKIND = rkind / alpha_rkind
   by (rule alpha_equivps)
@@ -469,7 +264,8 @@
  "supp (CONS i) = {atom i}"
  "supp (VAR x) = {atom x}"
  "supp (APP M N) = supp M \<union> supp N"
-apply (simp_all add: supp_def permute_ktt RKIND_RTY_RTRM_INJECT)
+apply (simp_all add: supp_def permute_ktt)
+apply (simp_all only: RKIND_RTY_RTRM_INJECT)
 apply (simp_all only: supp_at_base[simplified supp_def])
 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 done