# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270326671 -7200
# Node ID c0eac04ae3b467f361eba434b7bbff95e39c372a
# Parent  48c2eb84d5ce7e8c1f70a5c820b96c6f13cc9ee3
added README and moved examples into separate directory

diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Ex1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Ex1.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,36 @@
+theory Ex1
+imports "../Parser"
+begin
+
+text {* example 1, equivalent to example 2 from Terms *}
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
+and bp =
+  BP "name" "lam"
+binder
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (BP x t) = {atom x}"
+
+thm lam_bp.fv
+thm lam_bp.supp
+thm lam_bp.eq_iff
+thm lam_bp.bn
+thm lam_bp.perm
+thm lam_bp.induct
+thm lam_bp.inducts
+thm lam_bp.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+thm lam_bp.fv[simplified lam_bp.supp]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Ex1rec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Ex1rec.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,34 @@
+theory Ex1rec
+imports "../Parser" 
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaGen *}
+nominal_datatype lam' =
+  VAR' "name"
+| APP' "lam'" "lam'"
+| LAM' x::"name" t::"lam'"  bind x in t
+| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
+and bp' =
+  BP' "name" "lam'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'.fv
+thm lam'_bp'.eq_iff[no_vars]
+thm lam'_bp'.bn
+thm lam'_bp'.perm
+thm lam'_bp'.induct
+thm lam'_bp'.inducts
+thm lam'_bp'.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+thm lam'_bp'.fv[simplified lam'_bp'.supp]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Ex2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Ex2.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,37 @@
+theory Ex2
+imports "../Parser"
+begin
+
+text {* example 2 *}
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype trm' =
+  Var "name"
+| App "trm'" "trm'"
+| Lam x::"name" t::"trm'"          bind x in t
+| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
+and pat' =
+  PN
+| PS "name"
+| PD "name" "name"
+binder
+  f::"pat' \<Rightarrow> atom set"
+where
+  "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
+| "f (PS x) = {atom x}"
+
+thm trm'_pat'.fv
+thm trm'_pat'.eq_iff
+thm trm'_pat'.bn
+thm trm'_pat'.perm
+thm trm'_pat'.induct
+thm trm'_pat'.distinct
+thm trm'_pat'.fv[simplified trm'_pat'.supp]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Ex3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Ex3.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,37 @@
+theory Ex3
+imports "../Parser"
+begin
+
+(* Example 3, identical to example 1 from Terms.thy *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype trm0 =
+  Var0 "name"
+| App0 "trm0" "trm0"
+| Lam0 x::"name" t::"trm0"          bind x in t
+| Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
+and pat0 =
+  PN0
+| PS0 "name"
+| PD0 "pat0" "pat0"
+binder
+  f0::"pat0 \<Rightarrow> atom set"
+where
+  "f0 PN0 = {}"
+| "f0 (PS0 x) = {atom x}"
+| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+
+thm trm0_pat0.fv
+thm trm0_pat0.eq_iff
+thm trm0_pat0.bn
+thm trm0_pat0.perm
+thm trm0_pat0.induct
+thm trm0_pat0.distinct
+thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExCoreHaskell.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExCoreHaskell.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,677 @@
+theory ExCoreHaskell
+imports "../Parser"
+begin
+
+(* core haskell *)
+
+ML {* val _ = recursive := false *}
+
+atom_decl var
+atom_decl cvar
+atom_decl tvar
+
+(* there are types, coercion types and regular types list-data-structure *)
+
+ML {* val _ = alpha_type := AlphaLst *}
+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
+ apply (rule_tac [!] alpha_intros)
+ apply simp_all
+ 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(rule TrueI)
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct c rule: inducts(11))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct d rule: inducts(10))
+  apply(rule TrueI)
+  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(rule TrueI)
+  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 (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 (simp add: alpha_perm_bn)
+  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(rule TrueI)
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct c rule: inducts(11))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bv eqvts)
+  apply(induct d rule: inducts(10))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bv eqvts)
+  done
+
+lemma permute_bv_zero2:
+  "permute_bv 0 a = a"
+  apply(induct a rule: inducts(9))
+  apply(rule TrueI)
+  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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+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 (tactic {* ALLGOALS (TRY o rtac @{thm 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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
+apply (simp add: eqvts)
+done
+
+lemma fin1: "finite (fv_bv_tvs x)"
+apply (induct x rule: inducts(11))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin2: "finite (fv_bv_cvs x)"
+apply (induct x rule: inducts(12))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin3: "finite (fv_bv_vs x)"
+apply (induct x rule: inducts(10))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_fv_bv: "finite (fv_bv x)"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp add: fin1 fin2 fin3)
+done
+
+lemma finb1: "finite (set (bv_tvs x))"
+apply (induct x rule: inducts(11))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb2: "finite (set (bv_cvs x))"
+apply (induct x rule: inducts(12))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb3: "finite (set (bv_vs x))"
+apply (induct x rule: inducts(10))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_bv: "finite (set (bv x))"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp add: finb1 finb2 finb3)
+done
+
+thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct
+
+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 only: 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 only: 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 only: 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 only: 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 only: 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 only: 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
+
+end
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLF.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,27 @@
+theory ExLF
+imports "../Parser"
+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
+
+end
+
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLam.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLam.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,91 @@
+theory ExLam
+imports "../Parser"
+begin
+
+atom_decl name
+
+nominal_datatype lm =
+  Vr "name"
+| Ap "lm" "lm"
+| Lm x::"name" l::"lm"  bind x in l
+
+lemmas supp_fn' = lm.fv[simplified lm.supp]
+
+lemma
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  shows "P c lm"
+proof -
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
+    apply(rule a1)
+    apply(simp only: lm.perm)
+    apply(rule a2)
+    apply(blast)[1]
+    apply(assumption)
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
+    defer
+    apply(simp add: fresh_def)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(simp add: supp_Pair finite_supp)
+    apply(blast)
+    apply(erule exE)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
+    apply(simp del: lm.perm)
+    apply(subst lm.perm)
+    apply(subst (2) lm.perm)
+    apply(rule flip_fresh_fresh)
+    apply(simp add: fresh_def)
+    apply(simp only: supp_fn')
+    apply(simp)
+    apply(simp add: fresh_Pair)
+    apply(simp)
+    apply(rule a3)
+    apply(simp add: fresh_Pair)
+    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
+    apply(simp)
+    done
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+
+lemma
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  shows "P c lm"
+proof -
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
+    apply(rule a1)
+    apply(simp only: lm.perm)
+    apply(rule a2)
+    apply(blast)[1]
+    apply(assumption)
+    thm at_set_avoiding
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
+    defer
+    apply(simp add: lm.perm)
+    apply(rule a3)
+    apply(simp add: eqvts fresh_star_def)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    sorry
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLeroy.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLeroy.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,74 @@
+theory ExLeroy
+imports "../Parser"
+begin
+
+(* example form Leroy 96 about modules; OTT *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype mexp =
+  Acc "path"
+| Stru "body"
+| Funct x::"name" "sexp" m::"mexp"    bind x in m
+| FApp "mexp" "path"
+| Ascr "mexp" "sexp"
+and body =
+  Empty
+| Seq c::defn d::"body"     bind "cbinders c" in d
+and defn =
+  Type "name" "tyty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trmtrm"
+and sexp =
+  Sig sbody
+| SFunc "name" "sexp" "sexp"
+and sbody =
+  SEmpty
+| SSeq C::spec D::sbody    bind "Cbinders C" in D
+and spec =
+  Type1 "name"
+| Type2 "name" "tyty"
+| SStru "name" "sexp"
+| SVal "name" "tyty"
+and tyty =
+  Tyref1 "name"
+| Tyref2 "path" "tyty"
+| Fun "tyty" "tyty"
+and path =
+  Sref1 "name"
+| Sref2 "path" "name"
+and trmtrm =
+  Tref1 "name"
+| Tref2 "path" "name"
+| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
+| App' "trmtrm" "trmtrm"
+| Let' "body" "trmtrm"
+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_tyty_path_trmtrm.fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLet.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLet.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,236 @@
+theory ExLet
+imports "../Parser" "../../Attic/Prove"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+ML {* val _ = alpha_type := AlphaLst *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm"  bind x in t
+| Lt a::"lts" t::"trm"   bind "bn a" in t
+(*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+
+thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct[no_vars]
+thm trm_lts.inducts[no_vars]
+thm trm_lts.distinct
+(*thm trm_lts.supp*)
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
+
+
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
+| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+  apply simp_all
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma permute_bn_zero:
+  "permute_bn 0 a = a"
+  apply(induct a rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma permute_bn_add:
+  "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+  oops
+
+lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+  apply(induct lts rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
+  done
+
+lemma perm_bn:
+  "p \<bullet> bn l = bn(permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma fv_perm_bn:
+  "fv_bn l = fv_bn (permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma fv_fv_bn:
+  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  by blast
+
+lemma Lt_subst:
+  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  apply (simp only: trm_lts.eq_iff)
+  apply (rule_tac x="q" in exI)
+  apply (simp add: alphas)
+  apply (simp add: permute_bn_alpha_bn)
+  apply (simp add: perm_bn[symmetric])
+  apply (simp add: eqvts[symmetric])
+  apply (simp add: supp_abs)
+  apply (simp add: trm_lts.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 fin_bn:
+  "finite (set (bn l))"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+thm trm_lts.inducts[no_vars]
+
+lemma 
+  fixes t::trm
+  and   l::lts
+  and   c::"'a::fs"
+  assumes a1: "\<And>name c. P1 c (Vr name)"
+  and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
+  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
+  and     a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+  and     a5: "\<And>c. P2 c Lnil"
+  and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
+  shows "P1 c t" and "P2 c l"
+proof -
+  have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
+       b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
+    apply(induct rule: trm_lts.inducts)
+    apply(simp)
+    apply(rule a1)
+    apply(simp)
+    apply(rule a2)
+    apply(simp)
+    apply(simp)
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" 
+               and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+    apply(rule supp_perm_eq)
+    apply(simp)
+    apply(simp)
+    apply(rule a3)
+    apply(simp add: atom_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(rule at_set_avoiding2_atom)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_def)
+    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    apply(subst Lt_subst)
+    apply assumption
+    apply(rule a4)
+    apply(simp add:perm_bn[symmetric])
+    apply(simp add: eqvts)
+    apply (simp add: fresh_star_def fresh_def)
+    apply(rotate_tac 1)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def fresh_def supp_abs)
+    apply(simp add: eqvts permute_bn)
+    apply(rule a5)
+    apply(simp add: permute_bn)
+    apply(rule a6)
+    apply simp
+    apply simp
+    done
+  then have a: "P1 c (0 \<bullet> t)" by blast
+  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+
+
+
+lemma lets_bla:
+  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
+  by (simp add: trm_lts.eq_iff)
+
+lemma lets_ok:
+  "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+  apply (simp add: trm_lts.eq_iff)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp_all add: alphas)
+  apply (simp add: fresh_star_def eqvts)
+  done
+
+lemma lets_ok3:
+  "x \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  done
+
+
+lemma lets_not_ok1:
+  "x \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
+  done
+
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+  done
+
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLetMult.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLetMult.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,31 @@
+theory ExLetMult
+imports "../Parser"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
+ML {* val _ = cheat_equivp := true *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm" bind x in t
+| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+thm trm_lts.eq_iff
+thm trm_lts.induct
+thm trm_lts.fv[simplified trm_lts.supp]
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLetRec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLetRec.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,83 @@
+theory ExLetRec
+imports "../Parser"
+begin
+
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm"  bind x in t
+| Lt a::"lts" t::"trm"   bind "bn a" in t
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct
+thm trm_lts.distinct
+thm trm_lts.supp
+thm trm_lts.fv[simplified trm_lts.supp]
+
+(* why is this not in HOL simpset? *)
+lemma set_sub: "{a, b} - {b} = {a} - {b}"
+by auto
+
+lemma lets_bla:
+  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
+  by (simp add: trm_lts.eq_iff alphas2 set_sub)
+
+lemma lets_ok:
+  "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+  apply (simp add: trm_lts.eq_iff)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp_all add: alphas2 fresh_star_def eqvts)
+  done
+
+lemma lets_ok3:
+  "x \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  done
+
+
+lemma lets_not_ok1:
+  "x \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  done
+
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+  done
+
+lemma lets_ok4:
+  "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp add: atom_eqvt fresh_star_def)
+  done
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExNotRsp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExNotRsp.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,48 @@
+theory ExNotRsp
+imports "../Parser"
+begin
+
+atom_decl name
+
+(* example 6 from Terms.thy *)
+
+nominal_datatype trm6 =
+  Vr6 "name"
+| Lm6 x::"name" t::"trm6"         bind x in t
+| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+binder
+  bv6
+where
+  "bv6 (Vr6 n) = {}"
+| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
+
+(* example 7 from Terms.thy *)
+nominal_datatype trm7 =
+  Vr7 "name"
+| Lm7 l::"name" r::"trm7"   bind l in r
+| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
+binder
+  bv7
+where
+  "bv7 (Vr7 n) = {atom n}"
+| "bv7 (Lm7 n t) = bv7 t - {atom n}"
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+*)
+
+(* example 9 from Terms.thy *)
+nominal_datatype lam9 =
+  Var9 "name"
+| Lam9 n::"name" l::"lam9" bind n in l
+and bla9 =
+  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+binder
+  bv9
+where
+  "bv9 (Var9 x) = {}"
+| "bv9 (Lam9 x b) = {atom x}"
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExPS3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExPS3.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,38 @@
+theory ExPS3
+imports "../Parser"
+begin
+
+(* example 3 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype exp =
+  VarP "name"
+| AppP "exp" "exp"
+| LamP x::"name" e::"exp" bind x in e
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
+and pat3 =
+  PVar "name"
+| PUnit
+| PPair "pat3" "pat3"
+binder
+  bp :: "pat3 \<Rightarrow> atom set"
+where
+  "bp (PVar x) = {atom x}"
+| "bp (PUnit) = {}"
+| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
+
+thm exp_pat3.fv
+thm exp_pat3.eq_iff
+thm exp_pat3.bn
+thm exp_pat3.perm
+thm exp_pat3.induct
+thm exp_pat3.distinct
+thm exp_pat3.fv
+thm exp_pat3.supp
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExPS6.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExPS6.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,39 @@
+theory ExPS6
+imports "../Parser"
+begin
+
+(* example 6 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+(* The binding structure is too complicated, so equivalence the
+   way we define it is not true *)
+
+ML {* val _ = recursive := false  *}
+nominal_datatype exp6 =
+  EVar name
+| EPair exp6 exp6
+| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
+and pat6 =
+  PVar' name
+| PUnit'
+| PPair' pat6 pat6
+binder
+  bp6 :: "pat6 \<Rightarrow> atom set"
+where
+  "bp6 (PVar' x) = {atom x}"
+| "bp6 (PUnit') = {}"
+| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+
+thm exp6_pat6.fv
+thm exp6_pat6.eq_iff
+thm exp6_pat6.bn
+thm exp6_pat6.perm
+thm exp6_pat6.induct
+thm exp6_pat6.distinct
+thm exp6_pat6.supp
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExPS7.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExPS7.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,33 @@
+theory ExPS7
+imports "../Parser"
+begin
+
+(* example 7 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := true  *}
+nominal_datatype exp7 =
+  EVar name
+| EUnit
+| EPair exp7 exp7
+| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+and lrb =
+  Assign name exp7
+and lrbs =
+  Single lrb
+| More lrb lrbs
+binder
+  b7 :: "lrb \<Rightarrow> atom set" and
+  b7s :: "lrbs \<Rightarrow> atom set"
+where
+  "b7 (Assign x e) = {atom x}"
+| "b7s (Single a) = b7 a"
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
+thm exp7_lrb_lrbs.eq_iff
+thm exp7_lrb_lrbs.supp
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExPS8.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExPS8.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,56 @@
+theory ExPS8
+imports "../Parser"
+begin
+
+(* example 8 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+(* One function is recursive and the other one is not,
+   and as the parser cannot handle this we cannot set
+   the reference.  *)
+ML {* val _ = recursive := false  *}
+
+nominal_datatype exp8 =
+  EVar name
+| EUnit
+| EPair exp8 exp8
+| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
+and fnclause =
+  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
+and fnclauses =
+  S fnclause
+| ORs fnclause fnclauses
+and lrb8 =
+  Clause fnclauses
+and lrbs8 =
+  Single lrb8
+| More lrb8 lrbs8
+and pat8 =
+  PVar name
+| PUnit
+| PPair pat8 pat8
+binder
+  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
+  b_pat :: "pat8 \<Rightarrow> atom set" and
+  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+  b_fnclause :: "fnclause \<Rightarrow> atom set" and
+  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
+where
+  "b_lrbs8 (Single l) = b_lrb8 l"
+| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+| "b_pat (PVar x) = {atom x}"
+| "b_pat (PUnit) = {}"
+| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp8) = {atom x}"
+
+thm exp7_lrb_lrbs.eq_iff
+thm exp7_lrb_lrbs.supp
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExTySch.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExTySch.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,165 @@
+theory ExTySch
+imports "../Parser"
+begin
+
+(* Type Schemes *)
+atom_decl name
+
+ML {* val _ = alpha_type := AlphaRes *}
+nominal_datatype t =
+  Var "name"
+| Fun "t" "t"
+and tyS =
+  All xs::"name fset" ty::"t" bind xs in ty
+
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
+
+lemma size_eqvt_raw:
+  "size (pi \<bullet> t :: t_raw) = size t"
+  "size (pi \<bullet> ts :: tyS_raw) = size ts"
+  apply (induct rule: t_raw_tyS_raw.inducts)
+  apply simp_all
+  done
+
+instantiation t and tyS :: size begin
+
+quotient_definition
+  "size_t :: t \<Rightarrow> nat"
+is
+  "size :: t_raw \<Rightarrow> nat"
+
+quotient_definition
+  "size_tyS :: tyS \<Rightarrow> nat"
+is
+  "size :: tyS_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_t_raw x y \<Longrightarrow> size x = size y"
+  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
+  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
+  apply (simp_all only: t_raw_tyS_raw.size)
+  apply (simp_all only: alphas)
+  apply clarify
+  apply (simp_all only: size_eqvt_raw)
+  done
+
+lemma [quot_respect]:
+  "(alpha_t_raw ===> op =) size size"
+  "(alpha_tyS_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_t ---> id) size = size"
+  "(rep_tyS ---> id) size = size"
+  by (simp_all add: size_t_def size_tyS_def)
+
+instance
+  by default
+
+end
+
+thm t_raw_tyS_raw.size(4)[quot_lifted]
+thm t_raw_tyS_raw.size(5)[quot_lifted]
+thm t_raw_tyS_raw.size(6)[quot_lifted]
+
+
+thm t_tyS.fv
+thm t_tyS.eq_iff
+thm t_tyS.bn
+thm t_tyS.perm
+thm t_tyS.inducts
+thm t_tyS.distinct
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
+
+lemma induct:
+  assumes a1: "\<And>name b. P b (Var name)"
+  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
+  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
+  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
+proof -
+  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
+    apply (rule t_tyS.induct)
+    apply (simp add: a1)
+    apply (simp)
+    apply (rule allI)+
+    apply (rule a2)
+    apply simp
+    apply simp
+    apply (rule allI)
+    apply (rule allI)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
+    apply clarify
+    apply(rule_tac t="p \<bullet> All fset t" and 
+                   s="pa \<bullet> (p \<bullet> All fset t)" in subst)
+    apply (rule supp_perm_eq)
+    apply assumption
+    apply (simp only: t_tyS.perm)
+    apply (rule a3)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2)
+    apply (simp add: fin_fset_to_set)
+    apply (simp add: finite_supp)
+    apply (simp add: eqvts finite_supp)
+    apply (subst atom_eqvt_raw[symmetric])
+    apply (subst fmap_eqvt[symmetric])
+    apply (subst fset_to_set_eqvt[symmetric])
+    apply (simp only: fresh_star_permute_iff)
+    apply (simp add: fresh_star_def)
+    apply clarify
+    apply (simp add: fresh_def)
+    apply (simp add: t_tyS_supp)
+    done
+  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
+  then show ?thesis by simp
+qed
+
+lemma
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas)
+  apply(simp add: fresh_star_def fresh_zero_perm)
+  done
+
+lemma
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: alphas fresh_star_def eqvts)
+  done
+
+lemma
+  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
+done
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+  using a
+  apply(simp add: t_tyS.eq_iff)
+  apply(clarify)
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
+  apply auto
+  done
+
+(* PROBLEM:
+Type schemes with separate datatypes
+
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" bind xs in ty
+
+*** exception Datatype raised
+*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
+*** At command "nominal_datatype".
+*)
+
+
+end
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Test.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,47 @@
+(*<*)
+theory Test
+imports "../Parser"
+begin
+
+(* This file contains only the examples that are not supposed to work yet. *)
+
+
+atom_decl name
+
+(* example 4 from Terms.thy *)
+(* fv_eqvt does not work, we need to repaire defined permute functions
+   defined fv and defined alpha... *)
+(* lists-datastructure does not work yet
+nominal_datatype trm4 =
+  Vr4 "name"
+| Ap4 "trm4" "trm4 list"
+| Lm4 x::"name" t::"trm4"  bind x in t
+
+thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
+*)
+
+(* example 8 from Terms.thy *)
+
+(* Binding in a term under a bn, needs to fail *)
+(*
+nominal_datatype foo8 =
+  Foo0 "name"
+| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
+and bar8 =
+  Bar0 "name"
+| Bar1 "name" s::"name" b::"bar8" bind s in b
+binder
+  bv8
+where
+  "bv8 (Bar0 x) = {}"
+| "bv8 (Bar1 v x b) = {atom v}"
+*)
+
+(* example 9 from Peter Sewell's bestiary *)
+(* run out of steam at the moment *)
+
+end
+(*>*)
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/TestMorePerm.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/TestMorePerm.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,49 @@
+theory TestMorePerm
+imports "../Parser"
+begin
+
+(* Since there are more permutations, we do not know how to prove equivalence
+   (it is probably not true with the way alpha is defined now) so *)
+ML {* val _ = cheat_equivp := true *}
+
+
+atom_decl name
+
+(* example from my PHD *)
+
+atom_decl coname
+
+nominal_datatype phd =
+   Ax "name" "coname"
+|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"phd" "name"                              bind n in t
+|  AndL2 n::"name" t::"phd" "name"                              bind n in t
+|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
+
+thm phd.fv
+thm phd.eq_iff
+thm phd.bn
+thm phd.perm
+thm phd.induct
+thm phd.distinct
+thm phd.fv[simplified phd.supp]
+
+text {* weirdo example from Peter Sewell's bestiary *}
+
+nominal_datatype weird =
+  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+    bind x in p1, bind x in p2, bind y in p2, bind y in p3
+| WV "name"
+| WP "weird" "weird"
+
+thm permute_weird_raw.simps[no_vars]
+thm alpha_weird_raw.intros[no_vars]
+thm fv_weird_raw.simps[no_vars]
+
+
+end
+
+
+
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex1.thy
--- a/Nominal/Ex1.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory Ex1
-imports "Parser"
-begin
-
-text {* example 1, equivalent to example 2 from Terms *}
-
-atom_decl name
-
-ML {* val _ = recursive := false *}
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name" "lam"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-
-thm lam_bp.fv
-thm lam_bp.supp
-thm lam_bp.eq_iff
-thm lam_bp.bn
-thm lam_bp.perm
-thm lam_bp.induct
-thm lam_bp.inducts
-thm lam_bp.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex1rec.thy
--- a/Nominal/Ex1rec.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-theory Ex1rec
-imports "Parser" "../Attic/Prove"
-begin
-
-atom_decl name
-
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaGen *}
-nominal_datatype lam' =
-  VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'"  bind x in t
-| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
-and bp' =
-  BP' "name" "lam'"
-binder
-  bi'::"bp' \<Rightarrow> atom set"
-where
-  "bi' (BP' x t) = {atom x}"
-
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex2.thy
--- a/Nominal/Ex2.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-theory Ex2
-imports "Parser"
-begin
-
-text {* example 2 *}
-
-atom_decl name
-
-ML {* val _ = recursive := false  *}
-nominal_datatype trm' =
-  Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'"          bind x in t
-| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
-and pat' =
-  PN
-| PS "name"
-| PD "name" "name"
-binder
-  f::"pat' \<Rightarrow> atom set"
-where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex3.thy
--- a/Nominal/Ex3.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-theory Ex3
-imports "Parser"
-begin
-
-(* Example 3, identical to example 1 from Terms.thy *)
-
-atom_decl name
-
-ML {* val _ = recursive := false  *}
-nominal_datatype trm0 =
-  Var0 "name"
-| App0 "trm0" "trm0"
-| Lam0 x::"name" t::"trm0"          bind x in t
-| Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
-and pat0 =
-  PN0
-| PS0 "name"
-| PD0 "pat0" "pat0"
-binder
-  f0::"pat0 \<Rightarrow> atom set"
-where
-  "f0 PN0 = {}"
-| "f0 (PS0 x) = {atom x}"
-| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
-
-thm trm0_pat0.fv
-thm trm0_pat0.eq_iff
-thm trm0_pat0.bn
-thm trm0_pat0.perm
-thm trm0_pat0.induct
-thm trm0_pat0.distinct
-thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,677 +0,0 @@
-theory ExCoreHaskell
-imports "Parser"
-begin
-
-(* core haskell *)
-
-ML {* val _ = recursive := false *}
-
-atom_decl var
-atom_decl cvar
-atom_decl tvar
-
-(* there are types, coercion types and regular types list-data-structure *)
-
-ML {* val _ = alpha_type := AlphaLst *}
-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
- apply (rule_tac [!] alpha_intros)
- apply simp_all
- 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(rule TrueI)
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct c rule: inducts(11))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct d rule: inducts(10))
-  apply(rule TrueI)
-  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(rule TrueI)
-  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 (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 (simp add: alpha_perm_bn)
-  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(rule TrueI)
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct c rule: inducts(11))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bv eqvts)
-  apply(induct d rule: inducts(10))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bv eqvts)
-  done
-
-lemma permute_bv_zero2:
-  "permute_bv 0 a = a"
-  apply(induct a rule: inducts(9))
-  apply(rule TrueI)
-  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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-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 (tactic {* ALLGOALS (TRY o rtac @{thm 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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
-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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
-apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (simp add: eqvts)
-done
-
-lemma fin1: "finite (fv_bv_tvs x)"
-apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin2: "finite (fv_bv_cvs x)"
-apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin3: "finite (fv_bv_vs x)"
-apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_fv_bv: "finite (fv_bv x)"
-apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp add: fin1 fin2 fin3)
-done
-
-lemma finb1: "finite (set (bv_tvs x))"
-apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb2: "finite (set (bv_cvs x))"
-apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb3: "finite (set (bv_vs x))"
-apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_bv: "finite (set (bv x))"
-apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp add: finb1 finb2 finb3)
-done
-
-thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct
-
-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 only: 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 only: 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 only: 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 only: 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 only: 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 only: 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
-
-end
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLF.thy
--- a/Nominal/ExLF.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory ExLF
-imports "Parser"
-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
-
-end
-
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLam.thy
--- a/Nominal/ExLam.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-theory ExLam
-imports "Parser"
-begin
-
-atom_decl name
-
-nominal_datatype lm =
-  Vr "name"
-| Ap "lm" "lm"
-| Lm x::"name" l::"lm"  bind x in l
-
-lemmas supp_fn' = lm.fv[simplified lm.supp]
-
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
-proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
-    apply(rule a1)
-    apply(simp only: lm.perm)
-    apply(rule a2)
-    apply(blast)[1]
-    apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
-    defer
-    apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
-    apply(simp add: supp_Pair finite_supp)
-    apply(blast)
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp del: lm.perm)
-    apply(subst lm.perm)
-    apply(subst (2) lm.perm)
-    apply(rule flip_fresh_fresh)
-    apply(simp add: fresh_def)
-    apply(simp only: supp_fn')
-    apply(simp)
-    apply(simp add: fresh_Pair)
-    apply(simp)
-    apply(rule a3)
-    apply(simp add: fresh_Pair)
-    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
-    apply(simp)
-    done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
-qed
-
-
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
-proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
-    apply(rule a1)
-    apply(simp only: lm.perm)
-    apply(rule a2)
-    apply(blast)[1]
-    apply(assumption)
-    thm at_set_avoiding
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
-    defer
-    apply(simp add: lm.perm)
-    apply(rule a3)
-    apply(simp add: eqvts fresh_star_def)
-    apply(drule_tac x="q + p" in meta_spec)
-    apply(simp)
-    sorry
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
-qed
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLeroy.thy
--- a/Nominal/ExLeroy.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-theory ExLeroy
-imports "Parser"
-begin
-
-(* example form Leroy 96 about modules; OTT *)
-
-atom_decl name
-
-ML {* val _ = recursive := false  *}
-nominal_datatype mexp =
-  Acc "path"
-| Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind x in m
-| FApp "mexp" "path"
-| Ascr "mexp" "sexp"
-and body =
-  Empty
-| Seq c::defn d::"body"     bind "cbinders c" in d
-and defn =
-  Type "name" "tyty"
-| Dty "name"
-| DStru "name" "mexp"
-| Val "name" "trmtrm"
-and sexp =
-  Sig sbody
-| SFunc "name" "sexp" "sexp"
-and sbody =
-  SEmpty
-| SSeq C::spec D::sbody    bind "Cbinders C" in D
-and spec =
-  Type1 "name"
-| Type2 "name" "tyty"
-| SStru "name" "sexp"
-| SVal "name" "tyty"
-and tyty =
-  Tyref1 "name"
-| Tyref2 "path" "tyty"
-| Fun "tyty" "tyty"
-and path =
-  Sref1 "name"
-| Sref2 "path" "name"
-and trmtrm =
-  Tref1 "name"
-| Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
-| App' "trmtrm" "trmtrm"
-| Let' "body" "trmtrm"
-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_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-theory ExLet
-imports "Parser" "../Attic/Prove"
-begin
-
-text {* example 3 or example 5 from Terms.thy *}
-
-atom_decl name
-
-ML {* val _ = recursive := false *}
-ML {* val _ = alpha_type := AlphaLst *}
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in t
-(*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
-binder
-  bn
-where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-
-thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
-
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct[no_vars]
-thm trm_lts.inducts[no_vars]
-thm trm_lts.distinct
-(*thm trm_lts.supp*)
-thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-
-
-primrec
-  permute_bn_raw
-where
-  "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
-| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
-
-quotient_definition
-  "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
-is
-  "permute_bn_raw"
-
-lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
-  apply simp
-  apply clarify
-  apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
-  apply simp_all
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
-  done
-
-lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
-
-lemma permute_bn_zero:
-  "permute_bn 0 a = a"
-  apply(induct a rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  done
-
-lemma permute_bn_add:
-  "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
-  oops
-
-lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
-  apply(induct lts rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
-  done
-
-lemma perm_bn:
-  "p \<bullet> bn l = bn(permute_bn p l)"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  done
-
-lemma fv_perm_bn:
-  "fv_bn l = fv_bn (permute_bn p l)"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  done
-
-lemma fv_fv_bn:
-  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  by blast
-
-lemma Lt_subst:
-  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
-  apply (simp only: trm_lts.eq_iff)
-  apply (rule_tac x="q" in exI)
-  apply (simp add: alphas)
-  apply (simp add: permute_bn_alpha_bn)
-  apply (simp add: perm_bn[symmetric])
-  apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_abs)
-  apply (simp add: trm_lts.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 fin_bn:
-  "finite (set (bn l))"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(simp_all add:permute_bn eqvts)
-  done
-
-thm trm_lts.inducts[no_vars]
-
-lemma 
-  fixes t::trm
-  and   l::lts
-  and   c::"'a::fs"
-  assumes a1: "\<And>name c. P1 c (Vr name)"
-  and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
-  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
-  and     a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
-  and     a5: "\<And>c. P2 c Lnil"
-  and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
-  shows "P1 c t" and "P2 c l"
-proof -
-  have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
-       b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
-    apply(induct rule: trm_lts.inducts)
-    apply(simp)
-    apply(rule a1)
-    apply(simp)
-    apply(rule a2)
-    apply(simp)
-    apply(simp)
-    apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
-    apply(erule exE)
-    apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" 
-               and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
-    apply(rule supp_perm_eq)
-    apply(simp)
-    apply(simp)
-    apply(rule a3)
-    apply(simp add: atom_eqvt)
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    apply(rule at_set_avoiding2_atom)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: fresh_def)
-    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
-    apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
-    apply(erule exE)
-    apply(erule conjE)
-    apply(subst Lt_subst)
-    apply assumption
-    apply(rule a4)
-    apply(simp add:perm_bn[symmetric])
-    apply(simp add: eqvts)
-    apply (simp add: fresh_star_def fresh_def)
-    apply(rotate_tac 1)
-    apply(drule_tac x="q + p" in meta_spec)
-    apply(simp)
-    apply(rule at_set_avoiding2)
-    apply(rule fin_bn)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: fresh_star_def fresh_def supp_abs)
-    apply(simp add: eqvts permute_bn)
-    apply(rule a5)
-    apply(simp add: permute_bn)
-    apply(rule a6)
-    apply simp
-    apply simp
-    done
-  then have a: "P1 c (0 \<bullet> t)" by blast
-  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
-  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
-qed
-
-
-
-lemma lets_bla:
-  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  by (simp add: trm_lts.eq_iff)
-
-lemma lets_ok:
-  "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
-  apply (simp add: trm_lts.eq_iff)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas)
-  apply (simp add: fresh_star_def eqvts)
-  done
-
-lemma lets_ok3:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  done
-
-
-lemma lets_not_ok1:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
-  done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
-  done
-
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLetMult.thy
--- a/Nominal/ExLetMult.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-theory ExLetMult
-imports "Parser"
-begin
-
-atom_decl name
-
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
-ML {* val _ = cheat_equivp := true *}
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind x in t
-| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
-binder
-  bn
-where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-thm trm_lts.eq_iff
-thm trm_lts.induct
-thm trm_lts.fv[simplified trm_lts.supp]
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExLetRec.thy
--- a/Nominal/ExLetRec.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-theory ExLetRec
-imports "Parser"
-begin
-
-
-text {* example 3 or example 5 from Terms.thy *}
-
-atom_decl name
-
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
-binder
-  bn
-where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp]
-
-(* why is this not in HOL simpset? *)
-lemma set_sub: "{a, b} - {b} = {a} - {b}"
-by auto
-
-lemma lets_bla:
-  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  by (simp add: trm_lts.eq_iff alphas2 set_sub)
-
-lemma lets_ok:
-  "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
-  apply (simp add: trm_lts.eq_iff)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas2 fresh_star_def eqvts)
-  done
-
-lemma lets_ok3:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  done
-
-
-lemma lets_not_ok1:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
-  done
-
-lemma lets_ok4:
-  "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp add: atom_eqvt fresh_star_def)
-  done
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExNotRsp.thy
--- a/Nominal/ExNotRsp.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-theory ExNotRsp
-imports "Parser"
-begin
-
-atom_decl name
-
-(* example 6 from Terms.thy *)
-
-nominal_datatype trm6 =
-  Vr6 "name"
-| Lm6 x::"name" t::"trm6"         bind x in t
-| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
-binder
-  bv6
-where
-  "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-
-(* example 7 from Terms.thy *)
-nominal_datatype trm7 =
-  Vr7 "name"
-| Lm7 l::"name" r::"trm7"   bind l in r
-| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
-binder
-  bv7
-where
-  "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
-*)
-
-(* example 9 from Terms.thy *)
-nominal_datatype lam9 =
-  Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
-  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
-binder
-  bv9
-where
-  "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExPS3.thy
--- a/Nominal/ExPS3.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory ExPS3
-imports "Parser"
-begin
-
-(* example 3 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-ML {* val _ = recursive := false  *}
-nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
-and pat3 =
-  PVar "name"
-| PUnit
-| PPair "pat3" "pat3"
-binder
-  bp :: "pat3 \<Rightarrow> atom set"
-where
-  "bp (PVar x) = {atom x}"
-| "bp (PUnit) = {}"
-| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv
-thm exp_pat3.supp
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExPS6.thy
--- a/Nominal/ExPS6.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-theory ExPS6
-imports "Parser"
-begin
-
-(* example 6 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* The binding structure is too complicated, so equivalence the
-   way we define it is not true *)
-
-ML {* val _ = recursive := false  *}
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
-binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
-where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-thm exp6_pat6.supp
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExPS7.thy
--- a/Nominal/ExPS7.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-theory ExPS7
-imports "Parser"
-begin
-
-(* example 7 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-ML {* val _ = recursive := true  *}
-nominal_datatype exp7 =
-  EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
-and lrb =
-  Assign name exp7
-and lrbs =
-  Single lrb
-| More lrb lrbs
-binder
-  b7 :: "lrb \<Rightarrow> atom set" and
-  b7s :: "lrbs \<Rightarrow> atom set"
-where
-  "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExPS8.thy
--- a/Nominal/ExPS8.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-theory ExPS8
-imports "Parser"
-begin
-
-(* example 8 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* One function is recursive and the other one is not,
-   and as the parser cannot handle this we cannot set
-   the reference.  *)
-ML {* val _ = recursive := false  *}
-
-nominal_datatype exp8 =
-  EVar name
-| EUnit
-| EPair exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
-and fnclause =
-  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-and lrb8 =
-  Clause fnclauses
-and lrbs8 =
-  Single lrb8
-| More lrb8 lrbs8
-and pat8 =
-  PVar name
-| PUnit
-| PPair pat8 pat8
-binder
-  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
-  b_pat :: "pat8 \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
-where
-  "b_lrbs8 (Single l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
-
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
-theory ExTySch
-imports "Parser"
-begin
-
-(* Type Schemes *)
-atom_decl name
-
-ML {* val _ = alpha_type := AlphaRes *}
-nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
-and tyS =
-  All xs::"name fset" ty::"t" bind xs in ty
-
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
-lemma size_eqvt_raw:
-  "size (pi \<bullet> t :: t_raw) = size t"
-  "size (pi \<bullet> ts :: tyS_raw) = size ts"
-  apply (induct rule: t_raw_tyS_raw.inducts)
-  apply simp_all
-  done
-
-instantiation t and tyS :: size begin
-
-quotient_definition
-  "size_t :: t \<Rightarrow> nat"
-is
-  "size :: t_raw \<Rightarrow> nat"
-
-quotient_definition
-  "size_tyS :: tyS \<Rightarrow> nat"
-is
-  "size :: tyS_raw \<Rightarrow> nat"
-
-lemma size_rsp:
-  "alpha_t_raw x y \<Longrightarrow> size x = size y"
-  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
-  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
-  apply (simp_all only: t_raw_tyS_raw.size)
-  apply (simp_all only: alphas)
-  apply clarify
-  apply (simp_all only: size_eqvt_raw)
-  done
-
-lemma [quot_respect]:
-  "(alpha_t_raw ===> op =) size size"
-  "(alpha_tyS_raw ===> op =) size size"
-  by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
-  "(rep_t ---> id) size = size"
-  "(rep_tyS ---> id) size = size"
-  by (simp_all add: size_t_def size_tyS_def)
-
-instance
-  by default
-
-end
-
-thm t_raw_tyS_raw.size(4)[quot_lifted]
-thm t_raw_tyS_raw.size(5)[quot_lifted]
-thm t_raw_tyS_raw.size(6)[quot_lifted]
-
-
-thm t_tyS.fv
-thm t_tyS.eq_iff
-thm t_tyS.bn
-thm t_tyS.perm
-thm t_tyS.inducts
-thm t_tyS.distinct
-ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-
-lemma induct:
-  assumes a1: "\<And>name b. P b (Var name)"
-  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
-  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
-proof -
-  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
-    apply (rule t_tyS.induct)
-    apply (simp add: a1)
-    apply (simp)
-    apply (rule allI)+
-    apply (rule a2)
-    apply simp
-    apply simp
-    apply (rule allI)
-    apply (rule allI)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
-    apply clarify
-    apply(rule_tac t="p \<bullet> All fset t" and 
-                   s="pa \<bullet> (p \<bullet> All fset t)" in subst)
-    apply (rule supp_perm_eq)
-    apply assumption
-    apply (simp only: t_tyS.perm)
-    apply (rule a3)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2)
-    apply (simp add: fin_fset_to_set)
-    apply (simp add: finite_supp)
-    apply (simp add: eqvts finite_supp)
-    apply (subst atom_eqvt_raw[symmetric])
-    apply (subst fmap_eqvt[symmetric])
-    apply (subst fset_to_set_eqvt[symmetric])
-    apply (simp only: fresh_star_permute_iff)
-    apply (simp add: fresh_star_def)
-    apply clarify
-    apply (simp add: fresh_def)
-    apply (simp add: t_tyS_supp)
-    done
-  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
-  then show ?thesis by simp
-qed
-
-lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas)
-  apply(simp add: fresh_star_def fresh_zero_perm)
-  done
-
-lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def eqvts)
-  done
-
-lemma
-  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
-done
-
-lemma
-  assumes a: "a \<noteq> b"
-  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
-  using a
-  apply(simp add: t_tyS.eq_iff)
-  apply(clarify)
-  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
-  apply auto
-  done
-
-(* PROBLEM:
-Type schemes with separate datatypes
-
-nominal_datatype T =
-  TVar "name"
-| TFun "T" "T"
-nominal_datatype TyS =
-  TAll xs::"name list" ty::"T" bind xs in ty
-
-*** exception Datatype raised
-*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
-*** At command "nominal_datatype".
-*)
-
-
-end
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sat Apr 03 21:53:04 2010 +0200
+++ b/Nominal/ROOT.ML	Sat Apr 03 22:31:11 2010 +0200
@@ -5,19 +5,19 @@
     "Nominal2_Eqvt",
     "Nominal2_Atoms",
     "Nominal2_Supp",
-    "ExLam",
-    "ExLF",
-    "Ex1",
-    "Ex1rec",
-    "Ex2",
-    "Ex3",
-    "ExLet",
-    "ExLetRec",
-    "ExTySch",
-    "ExLeroy",
-    "ExPS3",
-    "ExPS7",
-    "ExCoreHaskell",
-    "Test"
-(*  "ExPS6", *)
+    "Ex/ExLam",
+    "Ex/ExLF",
+    "Ex/Ex1",
+    "Ex/Ex1rec",
+    "Ex/Ex2",
+    "Ex/Ex3",
+    "Ex/ExLet",
+    "Ex/ExLetRec",
+    "Ex/ExTySch",
+    "Ex/ExLeroy",
+    "Ex/ExPS3",
+    "Ex/ExPS7",
+    "Ex/ExCoreHaskell",
+    "Ex/Test"
+(*  "Ex/ExPS6", *)
     ];
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Test.thy
--- a/Nominal/Test.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*<*)
-theory Test
-imports "Parser"
-begin
-
-(* This file contains only the examples that are not supposed to work yet. *)
-
-
-atom_decl name
-
-(* example 4 from Terms.thy *)
-(* fv_eqvt does not work, we need to repaire defined permute functions
-   defined fv and defined alpha... *)
-(* lists-datastructure does not work yet
-nominal_datatype trm4 =
-  Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 x::"name" t::"trm4"  bind x in t
-
-thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
-*)
-
-(* example 8 from Terms.thy *)
-
-(* Binding in a term under a bn, needs to fail *)
-(*
-nominal_datatype foo8 =
-  Foo0 "name"
-| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
-and bar8 =
-  Bar0 "name"
-| Bar1 "name" s::"name" b::"bar8" bind s in b
-binder
-  bv8
-where
-  "bv8 (Bar0 x) = {}"
-| "bv8 (Bar1 v x b) = {atom v}"
-*)
-
-(* example 9 from Peter Sewell's bestiary *)
-(* run out of steam at the moment *)
-
-end
-(*>*)
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/TestMorePerm.thy
--- a/Nominal/TestMorePerm.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-theory TestMorePerm
-imports "Parser"
-begin
-
-(* Since there are more permutations, we do not know how to prove equivalence
-   (it is probably not true with the way alpha is defined now) so *)
-ML {* val _ = cheat_equivp := true *}
-
-
-atom_decl name
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
-   Ax "name" "coname"
-|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"phd" "name"                              bind n in t
-|  AndL2 n::"name" t::"phd" "name"                              bind n in t
-|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
-
-thm phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
-thm phd.fv[simplified phd.supp]
-
-text {* weirdo example from Peter Sewell's bestiary *}
-
-nominal_datatype weird =
-  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
-    bind x in p1, bind x in p2, bind y in p2, bind y in p3
-| WV "name"
-| WP "weird" "weird"
-
-thm permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
-
-end
-
-
-
diff -r 48c2eb84d5ce -r c0eac04ae3b4 README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,18 @@
+This repository contain a new implementation of
+Nominal Isabelle.
+
+Subdirectories:
+
+Attic       ... old version of the quotient package (is now 
+                part of the Isabelle distribution)
+
+Literature  ... some relevant papers bout binders and
+                Core-Haskell
+
+Nominal     ... main files for Nominal Isabelle
+
+Nominal/Ex  ... examples for new implementation
+
+Paper       ... submitted
+
+Pearl       ... paper accepted at ITP 
\ No newline at end of file