--- a/Nominal/Ex/CoreHaskell.thy Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Ex/CoreHaskell.thy Tue Dec 28 00:20:50 2010 +0000
@@ -102,218 +102,8 @@
thm core_haskell.size_eqvt
thm core_haskell.supp
-(*
-lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
- unfolding fresh_star_def Ball_def
- by auto (simp_all add: fresh_minus_perm)
-
-primrec permute_bv_vs_raw
-where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
-| "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
-primrec permute_bv_cvs_raw
-where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
-| "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
-primrec permute_bv_tvs_raw
-where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
-| "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
-primrec permute_bv_raw
-where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
- Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
-
-quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
-is "permute_bv_vs_raw"
-quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
-is "permute_bv_cvs_raw"
-quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
-is "permute_bv_tvs_raw"
-quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
-is "permute_bv_raw"
-
-lemma rsp_pre:
- "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
- "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
- "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
- apply (erule_tac [!] alpha_inducts)
- apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
- done
-
-lemma [quot_respect]:
- "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
- "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
- "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
- "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
- apply (simp_all add: rsp_pre)
- apply clarify
- apply (erule_tac alpha_inducts)
- apply (simp_all)
- apply (rule alpha_intros)
- apply (simp_all add: rsp_pre)
- done
-
-thm permute_bv_raw.simps[no_vars]
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma permute_bv_pre:
- "permute_bv p (Kpat c l1 l2 l3) =
- Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
- by (lifting permute_bv_raw.simps)
-
-lemmas permute_bv[simp] =
- permute_bv_pre
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma perm_bv1:
- "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
- "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
- "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
- apply(induct b rule: inducts(12))
- apply(simp_all add:permute_bv eqvts)
- apply(induct c rule: inducts(11))
- apply(simp_all add:permute_bv eqvts)
- apply(induct d rule: inducts(10))
- apply(simp_all add:permute_bv eqvts)
- done
-
-lemma perm_bv2:
- "p \<bullet> bv l = bv (permute_bv p l)"
- apply(induct l rule: inducts(9))
- apply(simp_all add:permute_bv)
- apply(simp add: perm_bv1[symmetric])
- apply(simp add: eqvts)
- done
-
-lemma alpha_perm_bn1:
- "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
- "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
- "alpha_bv_vs vars (permute_bv_vs q vars)"
- apply(induct tvars rule: inducts(11))
- apply(simp_all add:permute_bv eqvts eq_iff)
- apply(induct cvars rule: inducts(12))
- apply(simp_all add:permute_bv eqvts eq_iff)
- apply(induct vars rule: inducts(10))
- apply(simp_all add:permute_bv eqvts eq_iff)
- done
-
-lemma alpha_perm_bn:
- "alpha_bv pt (permute_bv q pt)"
- apply(induct pt rule: inducts(9))
- apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
- done
-
-lemma ACons_subst:
- "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
- apply (simp only: eq_iff)
- apply (simp add: alpha_perm_bn)
- apply (rule_tac x="q" in exI)
- apply (simp add: alphas)
- apply (simp add: perm_bv2[symmetric])
- apply (simp add: supp_abs)
- apply (simp add: fv_supp)
- apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
- apply (rule supp_perm_eq[symmetric])
- apply (subst supp_finite_atom_set)
- apply (rule finite_Diff)
- apply (simp add: finite_supp)
- apply (assumption)
- done
-
-lemma permute_bv_zero1:
- "permute_bv_cvs 0 b = b"
- "permute_bv_tvs 0 c = c"
- "permute_bv_vs 0 d = d"
- apply(induct b rule: inducts(12))
- apply(simp_all add:permute_bv eqvts)
- apply(induct c rule: inducts(11))
- apply(simp_all add:permute_bv eqvts)
- apply(induct d rule: inducts(10))
- apply(simp_all add:permute_bv eqvts)
- done
-
-lemma permute_bv_zero2:
- "permute_bv 0 a = a"
- apply(induct a rule: inducts(9))
- apply(simp_all add:permute_bv eqvts permute_bv_zero1)
- done
-
-lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
- apply (induct x rule: inducts(11))
- apply (simp_all add: eq_iff fresh_star_union)
- done
-
-lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
-apply (induct x rule: inducts(12))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
-apply (induct x rule: inducts(10))
-apply (rule TrueI)+
-apply (simp_all add: fresh_star_union eq_iff)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fin1: "finite (fv_bv_tvs x)"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin2: "finite (fv_bv_cvs x)"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin3: "finite (fv_bv_vs x)"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_fv_bv: "finite (fv_bv x)"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-defer
-apply (rule TrueI)+
-apply (simp add: fin1 fin2 fin3)
-apply (rule finite_supp)
-done
-
-lemma finb1: "finite (set (bv_tvs x))"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb2: "finite (set (bv_cvs x))"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb3: "finite (set (bv_vs x))"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_bv: "finite (set (bv x))"
-apply (induct x rule: inducts(9))
-apply (simp_all add: finb1 finb2 finb3)
-done
-
lemma strong_induction_principle:
+ fixes c::"'a::fs"
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)"
@@ -372,295 +162,19 @@
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) pt \<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> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
- apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
- apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
- apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
-
---"GOAL1"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
- supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
- and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
- and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a08)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
---"GOAL2"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
- supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
- and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
- and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a15)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
- and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a29)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
---"GOAL4 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
- and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a30)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL5 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
- and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a32)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL6 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
- and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
- and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- 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> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
- ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
-qed
-*)
-
-section {* test about equivariance for alpha *}
-
-(* this should not be an equivariance rule *)
-(* for the moment, we force it to be *)
-
-(*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
-
-thm eqvts
-thm eqvts_raw
-
+ shows "P1 c tkind"
+ "P2 c ckind"
+ "P3 c ty"
+ "P4 c ty_lst"
+ "P5 c co"
+ "P6 c co_lst"
+ "P7 c trm"
+ "P8 c assoc_lst"
+ "P9 c pt"
+ "P10 c vars"
+ "P11 c tvars"
+ "P12 c cvars"
+oops
end