--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
--- /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
+
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
+
+
+
--- /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
--- /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
+(*>*)
+
+
--- /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
+
+
+
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
--- 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
-
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
-
-
-
--- 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
--- 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", *)
];
--- 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
-(*>*)
-
-
--- 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
-
-
-
--- /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