# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273405139 -3600
# Node ID 9568f9f31822d72396264a213be45329400abb91
# Parent  0854af516f14bc6e6fe626e6db9c6420fb8de188
tuned file names for examples

diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/CoreHaskell.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CoreHaskell.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,673 @@
+theory CoreHaskell
+imports "../NewParser"
+begin
+
+(* core haskell *)
+
+atom_decl var
+atom_decl cvar
+atom_decl tvar
+
+nominal_datatype tkind =
+  KStar
+| KFun "tkind" "tkind"
+and ckind =
+  CKEq "ty" "ty"
+and ty =
+  TVar "tvar"
+| TC "string"
+| TApp "ty" "ty"
+| TFun "string" "ty_lst"
+| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TEq "ckind" "ty"
+and ty_lst =
+  TsNil
+| TsCons "ty" "ty_lst"
+and co =
+  CVar "cvar"
+| CConst "string"
+| CApp "co" "co"
+| CFun "string" "co_lst"
+| CAll cv::"cvar" "ckind" C::"co"  bind cv in C
+| CEq "ckind" "co"
+| CRefl "ty"
+| CSym "co"
+| CCir "co" "co"
+| CAt "co" "ty"
+| CLeft "co"
+| CRight "co"
+| CSim "co" "co"
+| CRightc "co"
+| CLeftc "co"
+| CCoe "co" "co"
+and co_lst =
+  CsNil
+| CsCons "co" "co_lst"
+and trm =
+  Var "var"
+| K "string"
+| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
+| AppT "trm" "ty"
+| AppC "trm" "co"
+| Lam v::"var" "ty" t::"trm"       bind v in t
+| App "trm" "trm"
+| Let x::"var" "ty" "trm" t::"trm" bind x in t
+| Case "trm" "assoc_lst"
+| Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
+and assoc_lst =
+  ANil
+| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
+and pat =
+  Kpat "string" "tvars" "cvars" "vars"
+and vars =
+  VsNil
+| VsCons "var" "ty" "vars"
+and tvars =
+  TvsNil
+| TvsCons "tvar" "tkind" "tvars"
+and cvars =
+  CvsNil
+| CvsCons "cvar" "ckind" "cvars"
+binder
+    bv :: "pat \<Rightarrow> atom list"
+and bv_vs :: "vars \<Rightarrow> atom list"
+and bv_tvs :: "tvars \<Rightarrow> atom list"
+and bv_cvs :: "cvars \<Rightarrow> atom list"
+where
+  "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
+| "bv_vs VsNil = []"
+| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
+| "bv_tvs TvsNil = []"
+| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
+| "bv_cvs CvsNil = []"
+| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+
+lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
+lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
+lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
+lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
+lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
+
+lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
+lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
+
+lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
+  unfolding fresh_star_def Ball_def
+  by auto (simp_all add: fresh_minus_perm)
+
+primrec permute_bv_vs_raw
+where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
+|     "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
+primrec permute_bv_cvs_raw
+where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
+|     "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
+primrec permute_bv_tvs_raw
+where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
+|     "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
+primrec permute_bv_raw
+where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
+     Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
+
+quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
+is "permute_bv_vs_raw"
+quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
+is "permute_bv_cvs_raw"
+quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
+is "permute_bv_tvs_raw"
+quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
+is "permute_bv_raw"
+
+lemma rsp_pre:
+ "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
+ "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
+ "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
+ apply (erule_tac [!] alpha_inducts)
+ apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
+ done
+
+lemma [quot_respect]:
+ "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
+ "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
+ "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
+ "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
+ apply (simp_all add: rsp_pre)
+ apply clarify
+ apply (erule_tac alpha_inducts)
+ apply (simp_all)
+ apply (rule alpha_intros)
+ apply (simp_all add: rsp_pre)
+ done
+
+thm permute_bv_raw.simps[no_vars]
+ permute_bv_vs_raw.simps[quot_lifted]
+ permute_bv_cvs_raw.simps[quot_lifted]
+ permute_bv_tvs_raw.simps[quot_lifted]
+
+lemma permute_bv_pre:
+  "permute_bv p (Kpat c l1 l2 l3) =
+   Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
+  by (lifting permute_bv_raw.simps)
+
+lemmas permute_bv[simp] =
+ permute_bv_pre
+ permute_bv_vs_raw.simps[quot_lifted]
+ permute_bv_cvs_raw.simps[quot_lifted]
+ permute_bv_tvs_raw.simps[quot_lifted]
+
+lemma perm_bv1:
+  "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
+  "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
+  "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
+  apply(induct b rule: inducts(12))
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct c rule: inducts(11))
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct d rule: inducts(10))
+  apply(simp_all add:permute_bv eqvts)
+  done
+
+lemma perm_bv2:
+  "p \<bullet> bv l = bv (permute_bv p l)"
+  apply(induct l rule: inducts(9))
+  apply(simp_all add:permute_bv)
+  apply(simp add: perm_bv1[symmetric])
+  apply(simp add: eqvts)
+  done
+
+lemma alpha_perm_bn1:
+ "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
+ "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
+ "alpha_bv_vs vars (permute_bv_vs q vars)"
+  apply(induct tvars rule: inducts(11))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  apply(induct cvars rule: inducts(12))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  apply(induct vars rule: inducts(10))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  done
+
+lemma alpha_perm_bn:
+  "alpha_bv pat (permute_bv q pat)"
+  apply(induct pat rule: inducts(9))
+  apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
+  done
+
+lemma ACons_subst:
+  "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
+  apply (simp only: eq_iff)
+  apply (simp add: alpha_perm_bn)
+  apply (rule_tac x="q" in exI)
+  apply (simp add: alphas)
+  apply (simp add: perm_bv2[symmetric])
+  apply (simp add: eqvts[symmetric])
+  apply (simp add: supp_abs)
+  apply (simp add: fv_supp)
+  apply (rule supp_perm_eq[symmetric])
+  apply (subst supp_finite_atom_set)
+  apply (rule finite_Diff)
+  apply (simp add: finite_supp)
+  apply (assumption)
+  done
+
+lemma permute_bv_zero1:
+  "permute_bv_cvs 0 b = b"
+  "permute_bv_tvs 0 c = c"
+  "permute_bv_vs 0 d = d"
+  apply(induct b rule: inducts(12))
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct c rule: inducts(11))
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct d rule: inducts(10))
+  apply(simp_all add:permute_bv eqvts)
+  done
+
+lemma permute_bv_zero2:
+  "permute_bv 0 a = a"
+  apply(induct a rule: inducts(9))
+  apply(simp_all add:permute_bv eqvts permute_bv_zero1)
+  done
+
+lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
+  apply (induct x rule: inducts(11))
+  apply (simp_all add: eq_iff fresh_star_union)
+  done
+
+lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
+apply (induct x rule: inducts(12))
+apply (rule TrueI)+
+apply (simp_all add: eq_iff fresh_star_union)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
+apply (induct x rule: inducts(10))
+apply (rule TrueI)+
+apply (simp_all add: fresh_star_union eq_iff)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
+apply (induct x rule: inducts(9))
+apply (rule TrueI)+
+apply (simp_all add: eq_iff fresh_star_union)
+apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fin1: "finite (fv_bv_tvs x)"
+apply (induct x rule: inducts(11))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin2: "finite (fv_bv_cvs x)"
+apply (induct x rule: inducts(12))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin3: "finite (fv_bv_vs x)"
+apply (induct x rule: inducts(10))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_fv_bv: "finite (fv_bv x)"
+apply (induct x rule: inducts(9))
+apply (rule TrueI)+
+defer
+apply (rule TrueI)+
+apply (simp add: fin1 fin2 fin3)
+apply (rule finite_supp)
+done
+
+lemma finb1: "finite (set (bv_tvs x))"
+apply (induct x rule: inducts(11))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb2: "finite (set (bv_cvs x))"
+apply (induct x rule: inducts(12))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb3: "finite (set (bv_vs x))"
+apply (induct x rule: inducts(10))
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_bv: "finite (set (bv x))"
+apply (induct x rule: inducts(9))
+apply (simp_all add: finb1 finb2 finb3)
+done
+
+lemma strong_induction_principle:
+  assumes a01: "\<And>b. P1 b KStar"
+  and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
+  and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
+  and a04: "\<And>tvar b. P3 b (TVar tvar)"
+  and a05: "\<And>string b. P3 b (TC string)"
+  and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
+  and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
+  and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
+    \<Longrightarrow> P3 b (TAll tvar tkind ty)"
+  and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"
+  and a10: "\<And>b. P4 b TsNil"
+  and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
+  and a12: "\<And>string b. P5 b (CVar string)"
+  and a12a:"\<And>str b. P5 b (CConst str)"
+  and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
+  and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
+  and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
+    \<Longrightarrow> P5 b (CAll tvar ckind co)"
+  and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"
+  and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"
+  and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
+  and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
+  and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"
+  and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
+  and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
+  and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"
+  and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
+  and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
+  and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
+  and a25: "\<And>b. P6 b CsNil"
+  and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
+  and a27: "\<And>var b. P7 b (Var var)"
+  and a28: "\<And>string b. P7 b (K string)"
+  and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
+    \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
+  and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
+    \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
+  and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"
+  and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"
+  and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
+  and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
+  and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>
+    \<Longrightarrow> P7 b (Let var ty trm1 trm2)"
+  and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
+  and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
+  and a37: "\<And>b. P8 b ANil"
+  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
+    \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
+  and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
+    \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
+  and a40: "\<And>b. P10 b VsNil"
+  and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"
+  and a42: "\<And>b. P11 b TvsNil"
+  and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>
+    \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"
+  and a44: "\<And>b. P12 b CvsNil"
+  and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
+    \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
+  shows "P1 (a :: 'a :: pt) tkind \<and>
+         P2 (b :: 'b :: pt) ckind \<and>
+         P3 (c :: 'c :: {pt,fs}) ty \<and>
+         P4 (d :: 'd :: pt) ty_lst \<and>
+         P5 (e :: 'e :: {pt,fs}) co \<and>
+         P6 (f :: 'f :: pt) co_lst \<and>
+         P7 (g :: 'g :: {pt,fs}) trm \<and>
+         P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
+         P9 (i :: 'i :: pt) pat \<and>
+         P10 (j :: 'j :: pt) vars \<and>
+         P11 (k :: 'k :: pt) tvars \<and>
+         P12 (l :: 'l :: pt) cvars"
+proof -
+  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
+    apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
+    apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
+    apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
+
+(* GOAL1 *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
+                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
+               and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
+                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a08)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+(* GOAL2 *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
+                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
+               and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
+                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a15)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+
+(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
+               and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
+                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a29)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+(* GOAL4 a copy-and-paste *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
+               and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
+                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a30)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+
+(* GOAL5 a copy-and-paste *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
+               and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
+                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a32)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+
+(* GOAL6 a copy-and-paste *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
+               and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
+    apply (simp add: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
+                and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
+    apply (rule a34)
+    apply simp
+    apply simp
+    apply(rotate_tac 2)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_abs eqvts)
+    apply blast
+
+(* MAIN ACons Goal *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
+                       supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm eqvts)
+    apply (subst ACons_subst)
+    apply assumption
+    apply (rule a38)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply simp
+    apply (simp add: perm_bv2[symmetric])
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2)
+    apply (simp add: fin_bv)
+    apply (simp add: finite_supp)
+    apply (simp add: supp_abs)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
+    done
+  then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
+  moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
+  ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
+qed
+
+section {* test about equivariance for alpha *}
+
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
+
+(*declare permute_pure[eqvt]*)
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
+end
+
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,675 +0,0 @@
-theory ExCoreHaskell
-imports "../NewParser"
-begin
-
-(* core haskell *)
-
-atom_decl var
-atom_decl cvar
-atom_decl tvar
-
-(* there are types, coercion types and regular types list-data-structure *)
-
-nominal_datatype tkind =
-  KStar
-| KFun "tkind" "tkind"
-and ckind =
-  CKEq "ty" "ty"
-and ty =
-  TVar "tvar"
-| TC "string"
-| TApp "ty" "ty"
-| TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
-| TEq "ckind" "ty"
-and ty_lst =
-  TsNil
-| TsCons "ty" "ty_lst"
-and co =
-  CVar "cvar"
-| CConst "string"
-| CApp "co" "co"
-| CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
-| CEq "ckind" "co"
-| CRefl "ty"
-| CSym "co"
-| CCir "co" "co"
-| CAt "co" "ty"
-| CLeft "co"
-| CRight "co"
-| CSim "co" "co"
-| CRightc "co"
-| CLeftc "co"
-| CCoe "co" "co"
-and co_lst =
-  CsNil
-| CsCons "co" "co_lst"
-and trm =
-  Var "var"
-| K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
-| AppT "trm" "ty"
-| AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm"       bind_set v in t
-| App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind_set x in t
-| Case "trm" "assoc_lst"
-| Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
-and assoc_lst =
-  ANil
-| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
-and pat =
-  Kpat "string" "tvars" "cvars" "vars"
-and vars =
-  VsNil
-| VsCons "var" "ty" "vars"
-and tvars =
-  TvsNil
-| TvsCons "tvar" "tkind" "tvars"
-and cvars =
-  CvsNil
-| CvsCons "cvar" "ckind" "cvars"
-binder
-    bv :: "pat \<Rightarrow> atom list"
-and bv_vs :: "vars \<Rightarrow> atom list"
-and bv_tvs :: "tvars \<Rightarrow> atom list"
-and bv_cvs :: "cvars \<Rightarrow> atom list"
-where
-  "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
-| "bv_vs VsNil = []"
-| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
-| "bv_tvs TvsNil = []"
-| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
-| "bv_cvs CvsNil = []"
-| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
-
-lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
-lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
-lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
-lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
-lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
-
-lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
-lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
-
-lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
-  unfolding fresh_star_def Ball_def
-  by auto (simp_all add: fresh_minus_perm)
-
-primrec permute_bv_vs_raw
-where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
-|     "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
-primrec permute_bv_cvs_raw
-where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
-|     "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
-primrec permute_bv_tvs_raw
-where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
-|     "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
-primrec permute_bv_raw
-where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
-     Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
-
-quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
-is "permute_bv_vs_raw"
-quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
-is "permute_bv_cvs_raw"
-quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
-is "permute_bv_tvs_raw"
-quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
-is "permute_bv_raw"
-
-lemma rsp_pre:
- "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
- "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
- "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
- apply (erule_tac [!] alpha_inducts)
- apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
- done
-
-lemma [quot_respect]:
- "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
- "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
- "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
- "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
- apply (simp_all add: rsp_pre)
- apply clarify
- apply (erule_tac alpha_inducts)
- apply (simp_all)
- apply (rule alpha_intros)
- apply (simp_all add: rsp_pre)
- done
-
-thm permute_bv_raw.simps[no_vars]
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma permute_bv_pre:
-  "permute_bv p (Kpat c l1 l2 l3) =
-   Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
-  by (lifting permute_bv_raw.simps)
-
-lemmas permute_bv[simp] =
- permute_bv_pre
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma perm_bv1:
-  "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
-  "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
-  "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
-  apply(induct b rule: inducts(12))
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct c rule: inducts(11))
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct d rule: inducts(10))
-  apply(simp_all add:permute_bv eqvts)
-  done
-
-lemma perm_bv2:
-  "p \<bullet> bv l = bv (permute_bv p l)"
-  apply(induct l rule: inducts(9))
-  apply(simp_all add:permute_bv)
-  apply(simp add: perm_bv1[symmetric])
-  apply(simp add: eqvts)
-  done
-
-lemma alpha_perm_bn1:
- "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
- "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
- "alpha_bv_vs vars (permute_bv_vs q vars)"
-  apply(induct tvars rule: inducts(11))
-  apply(simp_all add:permute_bv eqvts eq_iff)
-  apply(induct cvars rule: inducts(12))
-  apply(simp_all add:permute_bv eqvts eq_iff)
-  apply(induct vars rule: inducts(10))
-  apply(simp_all add:permute_bv eqvts eq_iff)
-  done
-
-lemma alpha_perm_bn:
-  "alpha_bv pat (permute_bv q pat)"
-  apply(induct pat rule: inducts(9))
-  apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
-  done
-
-lemma ACons_subst:
-  "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
-  apply (simp only: eq_iff)
-  apply (simp add: alpha_perm_bn)
-  apply (rule_tac x="q" in exI)
-  apply (simp add: alphas)
-  apply (simp add: perm_bv2[symmetric])
-  apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_abs)
-  apply (simp add: fv_supp)
-  apply (rule supp_perm_eq[symmetric])
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (simp add: finite_supp)
-  apply (assumption)
-  done
-
-lemma permute_bv_zero1:
-  "permute_bv_cvs 0 b = b"
-  "permute_bv_tvs 0 c = c"
-  "permute_bv_vs 0 d = d"
-  apply(induct b rule: inducts(12))
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct c rule: inducts(11))
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct d rule: inducts(10))
-  apply(simp_all add:permute_bv eqvts)
-  done
-
-lemma permute_bv_zero2:
-  "permute_bv 0 a = a"
-  apply(induct a rule: inducts(9))
-  apply(simp_all add:permute_bv eqvts permute_bv_zero1)
-  done
-
-lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
-  apply (induct x rule: inducts(11))
-  apply (simp_all add: eq_iff fresh_star_union)
-  done
-
-lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
-apply (induct x rule: inducts(12))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
-apply (induct x rule: inducts(10))
-apply (rule TrueI)+
-apply (simp_all add: fresh_star_union eq_iff)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fin1: "finite (fv_bv_tvs x)"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin2: "finite (fv_bv_cvs x)"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin3: "finite (fv_bv_vs x)"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_fv_bv: "finite (fv_bv x)"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-defer
-apply (rule TrueI)+
-apply (simp add: fin1 fin2 fin3)
-apply (rule finite_supp)
-done
-
-lemma finb1: "finite (set (bv_tvs x))"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb2: "finite (set (bv_cvs x))"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb3: "finite (set (bv_vs x))"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_bv: "finite (set (bv x))"
-apply (induct x rule: inducts(9))
-apply (simp_all add: finb1 finb2 finb3)
-done
-
-lemma strong_induction_principle:
-  assumes a01: "\<And>b. P1 b KStar"
-  and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
-  and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
-  and a04: "\<And>tvar b. P3 b (TVar tvar)"
-  and a05: "\<And>string b. P3 b (TC string)"
-  and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
-  and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
-  and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
-    \<Longrightarrow> P3 b (TAll tvar tkind ty)"
-  and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"
-  and a10: "\<And>b. P4 b TsNil"
-  and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
-  and a12: "\<And>string b. P5 b (CVar string)"
-  and a12a:"\<And>str b. P5 b (CConst str)"
-  and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
-  and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
-  and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
-    \<Longrightarrow> P5 b (CAll tvar ckind co)"
-  and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"
-  and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"
-  and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
-  and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
-  and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"
-  and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
-  and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
-  and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"
-  and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
-  and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
-  and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
-  and a25: "\<And>b. P6 b CsNil"
-  and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
-  and a27: "\<And>var b. P7 b (Var var)"
-  and a28: "\<And>string b. P7 b (K string)"
-  and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
-    \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
-  and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
-    \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
-  and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"
-  and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"
-  and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
-  and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
-  and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>
-    \<Longrightarrow> P7 b (Let var ty trm1 trm2)"
-  and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
-  and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
-  and a37: "\<And>b. P8 b ANil"
-  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
-    \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
-  and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
-    \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
-  and a40: "\<And>b. P10 b VsNil"
-  and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"
-  and a42: "\<And>b. P11 b TvsNil"
-  and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>
-    \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"
-  and a44: "\<And>b. P12 b CvsNil"
-  and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
-    \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
-  shows "P1 (a :: 'a :: pt) tkind \<and>
-         P2 (b :: 'b :: pt) ckind \<and>
-         P3 (c :: 'c :: {pt,fs}) ty \<and>
-         P4 (d :: 'd :: pt) ty_lst \<and>
-         P5 (e :: 'e :: {pt,fs}) co \<and>
-         P6 (f :: 'f :: pt) co_lst \<and>
-         P7 (g :: 'g :: {pt,fs}) trm \<and>
-         P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
-         P9 (i :: 'i :: pt) pat \<and>
-         P10 (j :: 'j :: pt) vars \<and>
-         P11 (k :: 'k :: pt) tvars \<and>
-         P12 (l :: 'l :: pt) cvars"
-proof -
-  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
-    apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
-    apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
-    apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
-
-(* GOAL1 *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
-                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
-               and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
-                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a08)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-(* GOAL2 *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
-                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
-               and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
-                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a15)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-
-(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
-                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
-               and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
-                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a29)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-(* GOAL4 a copy-and-paste *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
-                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
-               and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
-                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a30)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-
-(* GOAL5 a copy-and-paste *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
-                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
-               and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
-                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a32)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-
-(* GOAL6 a copy-and-paste *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
-                       supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm)
-    apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
-               and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
-    apply (simp add: eq_iff)
-    apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
-                and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
-    apply (rule conjI)
-    apply (rule supp_perm_eq)
-    apply (simp add: eqvts)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply (simp add: eqvts)
-    apply (subst supp_perm_eq)
-    apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
-    apply assumption
-    apply (simp add: fresh_star_minus_perm)
-    apply (rule a34)
-    apply simp
-    apply simp
-    apply(rotate_tac 2)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2_atom)
-    apply (simp add: finite_supp)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_def)
-    apply (simp only: supp_abs eqvts)
-    apply blast
-
-(* MAIN ACons Goal *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
-                       supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
-    apply clarify
-    apply (simp only: perm eqvts)
-    apply (subst ACons_subst)
-    apply assumption
-    apply (rule a38)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply simp
-    apply (simp add: perm_bv2[symmetric])
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2)
-    apply (simp add: fin_bv)
-    apply (simp add: finite_supp)
-    apply (simp add: supp_abs)
-    apply (simp add: finite_supp)
-    apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
-    done
-  then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
-  moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
-  ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
-qed
-
-section {* test about equivariance for alpha *}
-
-(* this should not be an equivariance rule *)
-(* for the moment, we force it to be       *)
-
-(*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)
-
-thm eqvts
-thm eqvts_raw
-
-declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_tkind_raw
-
-thm eqvts
-thm eqvts_raw
-
-end
-
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/ExLF.thy
--- a/Nominal/Ex/ExLF.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-theory ExLF
-imports "../NewParser"
-begin
-
-atom_decl name
-atom_decl ident
-
-nominal_datatype kind =
-    Type
-  | KPi "ty" n::"name" k::"kind" bind_set n in k
-and ty =
-    TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty" bind_set n in t
-and trm =
-    Const "ident"
-  | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm" bind_set n in t
-
-thm kind_ty_trm.supp
-
-declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_trm_raw
-
-
-
-
-end
-
-
-
-
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/ExLeroy.thy
--- a/Nominal/Ex/ExLeroy.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-theory ExLeroy
-imports "../NewParser"
-begin
-
-(* example form Leroy 96 about modules; OTT *)
-
-atom_decl name
-
-nominal_datatype mexp =
-  Acc "path"
-| Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
-| FApp "mexp" "path"
-| Ascr "mexp" "sexp"
-and body =
-  Empty
-| Seq c::defn d::"body"     bind_set "cbinders c" in d
-and defn =
-  Type "name" "ty"
-| Dty "name"
-| DStru "name" "mexp"
-| Val "name" "trm"
-and sexp =
-  Sig sbody
-| SFunc "name" "sexp" "sexp"
-and sbody =
-  SEmpty
-| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
-and spec =
-  Type1 "name"
-| Type2 "name" "ty"
-| SStru "name" "sexp"
-| SVal "name" "ty"
-and ty =
-  Tyref1 "name"
-| Tyref2 "path" "ty"
-| Fun "ty" "ty"
-and path =
-  Sref1 "name"
-| Sref2 "path" "name"
-and trm =
-  Tref1 "name"
-| Tref2 "path" "name"
-| Lam' v::"name" "ty" M::"trm"  bind_set v in M
-| App' "trm" "trm"
-| Let' "body" "trm"
-binder
-    cbinders :: "defn \<Rightarrow> atom set"
-and Cbinders :: "spec \<Rightarrow> atom set"
-where
-  "cbinders (Type t T) = {atom t}"
-| "cbinders (Dty t) = {atom t}"
-| "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
-| "Cbinders (Type1 t) = {atom t}"
-| "Cbinders (Type2 t T) = {atom t}"
-| "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"
-
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
-
-declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_trm_raw
-
-
-end
-
-
-
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/ExNotRsp.thy
--- a/Nominal/Ex/ExNotRsp.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-theory ExNotRsp
-imports "../NewParser"
-begin
-
-atom_decl name
-
-(* this example binds bound names and
-   so is not respectful *)
-(*
-nominal_datatype trm =
-  Vr "name"
-| Lm x::"name" t::"trm"         bind x in t
-| Lt left::"trm" right::"trm"   bind "bv left" in right
-binder
-  bv
-where
-  "bv (Vr n) = {}"
-| "bv (Lm n t) = {atom n} \<union> bv t"
-| "bv (Lt l r) = bv l \<union> bv r"
-*)
-
-(* this example uses "-" in the binding function; 
-   at the moment this is unsupported *)
-(*
-nominal_datatype trm' =
-  Vr' "name"
-| Lm' l::"name" r::"trm'"   bind l in r
-| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
-binder
-  bv'
-where
-  "bv' (Vr' n) = {atom n}"
-| "bv' (Lm' n t) = bv' t - {atom n}"
-| "bv' (Lt' l r) = bv' l \<union> bv' r"
-*)
-
-(* this example again binds bound names  *)
-(*
-nominal_datatype trm'' =
-  Va'' "name"
-| Lm'' n::"name" l::"trm''" bind n in l
-and bla'' =
-  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
-binder
-  bv''
-where
-  "bv'' (Vm'' x) = {}"
-| "bv'' (Lm'' x b) = {atom x}"
-*)
-
-end
-
-
-
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/LF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LF.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,35 @@
+theory LF
+imports "../NewParser"
+begin
+
+atom_decl name
+atom_decl ident
+
+nominal_datatype kind =
+    Type
+  | KPi "ty" n::"name" k::"kind"  bind n in k
+and ty =
+    TConst "ident"
+  | TApp "ty" "trm"
+  | TPi "ty" n::"name" t::"ty"    bind n in t
+and trm =
+    Const "ident"
+  | Var "name"
+  | App "trm" "trm"
+  | Lam "ty" n::"name" t::"trm"   bind n in t
+
+thm kind_ty_trm.supp
+
+declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
+
+end
+
+
+
+
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/Modules.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Modules.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,80 @@
+theory Modules
+imports "../NewParser"
+begin
+
+(* example from Leroy'96 about modules; 
+   see OTT example by Owens *)
+
+atom_decl name
+
+nominal_datatype mexp =
+  Acc "path"
+| Stru "body"
+| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
+| FApp "mexp" "path"
+| Ascr "mexp" "sexp"
+and body =
+  Empty
+| Seq c::defn d::"body"     bind_set "cbinders c" in d
+and defn =
+  Type "name" "ty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trm"
+and sexp =
+  Sig sbody
+| SFunc "name" "sexp" "sexp"
+and sbody =
+  SEmpty
+| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
+and spec =
+  Type1 "name"
+| Type2 "name" "ty"
+| SStru "name" "sexp"
+| SVal "name" "ty"
+and ty =
+  Tyref1 "name"
+| Tyref2 "path" "ty"
+| Fun "ty" "ty"
+and path =
+  Sref1 "name"
+| Sref2 "path" "name"
+and trm =
+  Tref1 "name"
+| Tref2 "path" "name"
+| Lam' v::"name" "ty" M::"trm"  bind_set v in M
+| App' "trm" "trm"
+| Let' "body" "trm"
+binder
+    cbinders :: "defn \<Rightarrow> atom set"
+and Cbinders :: "spec \<Rightarrow> atom set"
+where
+  "cbinders (Type t T) = {atom t}"
+| "cbinders (Dty t) = {atom t}"
+| "cbinders (DStru x s) = {atom x}"
+| "cbinders (Val v M) = {atom v}"
+| "Cbinders (Type1 t) = {atom t}"
+| "Cbinders (Type2 t T) = {atom t}"
+| "Cbinders (SStru x S) = {atom x}"
+| "Cbinders (SVal v T) = {atom v}"
+
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
+
+declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+end
+
+
+
diff -r 0854af516f14 -r 9568f9f31822 Nominal/Ex/NoneExamples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/NoneExamples.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,54 @@
+theory NoneExamples
+imports "../NewParser"
+begin
+
+atom_decl name
+
+(* this example binds bound names and
+   so is not respectful *)
+(*
+nominal_datatype trm =
+  Vr "name"
+| Lm x::"name" t::"trm"         bind x in t
+| Lt left::"trm" right::"trm"   bind "bv left" in right
+binder
+  bv
+where
+  "bv (Vr n) = {}"
+| "bv (Lm n t) = {atom n} \<union> bv t"
+| "bv (Lt l r) = bv l \<union> bv r"
+*)
+
+(* this example uses "-" in the binding function; 
+   at the moment this is unsupported *)
+(*
+nominal_datatype trm' =
+  Vr' "name"
+| Lm' l::"name" r::"trm'"   bind l in r
+| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
+binder
+  bv'
+where
+  "bv' (Vr' n) = {atom n}"
+| "bv' (Lm' n t) = bv' t - {atom n}"
+| "bv' (Lt' l r) = bv' l \<union> bv' r"
+*)
+
+(* this example again binds bound names  *)
+(*
+nominal_datatype trm'' =
+  Va'' "name"
+| Lm'' n::"name" l::"trm''" bind n in l
+and bla'' =
+  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+binder
+  bv''
+where
+  "bv'' (Vm'' x) = {}"
+| "bv'' (Lm'' x b) = {atom x}"
+*)
+
+end
+
+
+
diff -r 0854af516f14 -r 9568f9f31822 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sun May 09 12:26:10 2010 +0100
+++ b/Nominal/ROOT.ML	Sun May 09 12:38:59 2010 +0100
@@ -2,7 +2,7 @@
 
 no_document use_thys
    ["Ex/Lambda",
-    "Ex/ExLF",
+    "Ex/LF",
     "Ex/SingleLet",
     "Ex/Ex1rec",
     "Ex/Ex2",
@@ -10,10 +10,10 @@
     "Ex/ExLet",
     "Ex/ExLetRec",
     "Ex/TypeSchemes",
-    "Ex/ExLeroy",
+    "Ex/Modules",
     "Ex/ExPS3",
     "Ex/ExPS7",
-    "Ex/ExCoreHaskell",
+    "Ex/CoreHaskell",
     "Ex/Test",
     "Manual/Term4"
     ];