theory Let

imports "../Nominal2" 

begin

atom_decl name

nominal_datatype trm =

  Var "name"

| App "trm" "trm"

| Lam x::"name" t::"trm"  bind  x in t

| Let as::"assn" t::"trm"   bind "bn as" in t

and assn =

  ANil

| ACons "name" "trm" "assn"

binder

  bn

where

  "bn ANil = []"

| "bn (ACons x t as) = (atom x) # (bn as)"

thm at_set_avoiding2

thm trm_assn.fv_defs

thm trm_assn.eq_iff 

thm trm_assn.bn_defs

thm trm_assn.perm_simps

thm trm_assn.induct

thm trm_assn.inducts

thm trm_assn.distinct

thm trm_assn.supp

thm trm_assn.fresh

thm trm_assn.exhaust[where y="t", no_vars]

quotient_definition

  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"

is

  "permute_bn_raw"

lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"

  apply (simp add: fun_rel_def)

  apply clarify

  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)

  apply (rule TrueI)+

  apply simp_all

  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)

  apply simp_all

  done

lemmas permute_bn = permute_bn_raw.simps[quot_lifted]

lemma uu:

  shows "alpha_bn as (permute_bn p as)"

apply(induct as rule: trm_assn.inducts(2))

apply(auto)[4]

apply(simp add: permute_bn)

apply(simp add: trm_assn.eq_iff)

apply(simp add: permute_bn)

apply(simp add: trm_assn.eq_iff)

done

lemma tt:

  shows "(p \<bullet> bn as) = bn (permute_bn p as)"

apply(induct as rule: trm_assn.inducts(2))

apply(auto)[4]

apply(simp add: permute_bn trm_assn.bn_defs)

apply(simp add: permute_bn trm_assn.bn_defs)

apply(simp add: atom_eqvt)

done

lemma strong_exhaust1:

  fixes c::"'a::fs"

  assumes "\<And>name. y = Var name \<Longrightarrow> P" 

  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"

  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 

  and     "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"

  shows "P"

apply(rule_tac y="y" in trm_assn.exhaust(1))

apply(rule assms(1))

apply(assumption)

apply(rule assms(2))

apply(assumption)

apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

apply(rule assms(3))

apply(perm_simp)

apply(assumption)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: trm_assn.fresh fresh_star_def)

apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

apply(simp add: set_eqvt)

apply(subst (asm) tt)

apply(rule_tac assms(4))

apply(simp)

apply(simp add: trm_assn.eq_iff)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(simp add: tt uu)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: Abs_fresh_star)

done

lemma strong_exhaust2:

  assumes "as = ANil \<Longrightarrow> P" 

  and     "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 

  shows "P"

apply(rule_tac y="as" in trm_assn.exhaust(2))

apply(rule assms(1))

apply(assumption)

apply(rule assms(2))

apply(assumption)+

done

lemma 

  fixes t::trm

  and   as::assn

  and   c::"'a::fs"

  assumes a1: "\<And>x c. P1 c (Var x)"

  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"

  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"

  and     a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"

  and     a5: "\<And>c. P2 c ANil"

  and     a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"

  shows "P1 c t" "P2 c as"

using assms

apply(induction_schema)

apply(rule_tac y="t" in strong_exhaust1)

apply(blast)

apply(blast)

apply(blast)

apply(blast)

apply(rule_tac as="as" in strong_exhaust2)

apply(blast)

apply(blast)

apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")

apply(simp_all add: trm_assn.size)

done

text {* *}

(*

proof -

  have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" 

   and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"

    apply(induct rule: trm_assn.inducts)

    apply(simp)

    apply(rule a1)

    apply(simp)

    apply(rule a2)

    apply(assumption)

    apply(assumption)

    -- "lam case"

    apply(simp)

    apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")

    apply(erule exE)

    apply(erule conjE)

    apply(drule supp_perm_eq[symmetric])

    apply(simp)

    apply(thin_tac "?X = ?Y")

    apply(rule a3)

    apply(simp add: atom_eqvt permute_set_eq)

    apply(simp only: permute_plus[symmetric])

    apply(rule at_set_avoiding2)

    apply(simp add: finite_supp)

    apply(simp add: finite_supp)

    apply(simp add: finite_supp)

    apply(simp add: freshs fresh_star_def)

    --"let case"

    apply(simp)

    thm trm_assn.eq_iff

    thm eq_iffs

    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")

    apply(erule exE)

    apply(erule conjE)

    prefer 2

    apply(rule at_set_avoiding2)

    apply(rule fin_bn)

    apply(simp add: finite_supp)

    apply(simp add: finite_supp)

    apply(simp add: abs_fresh)

    apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)

    prefer 2

    apply(rule a4)

    prefer 4

    apply(simp add: eq_iffs)

    apply(rule conjI)

    prefer 2

    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)

    apply(subst permute_plus[symmetric])

    apply(blast)

    prefer 2

    apply(simp add: eq_iffs)

    thm eq_iffs

    apply(subst permute_plus[symmetric])

    apply(blast)

    apply(simp add: supps)

    apply(simp add: fresh_star_def freshs)

    apply(drule supp_perm_eq[symmetric])

    apply(simp)

    apply(simp add: eq_iffs)

    apply(simp)

    apply(thin_tac "?X = ?Y")

    apply(rule a4) 

    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)

    apply(subst permute_plus[symmetric])

    apply(blast)

    apply(subst permute_plus[symmetric])

    apply(blast)

    apply(simp add: supps)

    thm at_set_avoiding2

    --"HERE"

    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 freshs)

    apply(rule ballI)

    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

*)

text {* *}

(*

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 (rule TrueI)+

  apply simp_all

  apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)

  apply simp_all

  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)

  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 Lt_subst:

  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"

  apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)

  apply (rule_tac x="q" in exI)

  apply (simp add: alphas)

  apply (simp add: perm_bn[symmetric])

  apply(rule conjI)

  apply(drule supp_perm_eq)

  apply(simp add: abs_eq_iff)

  apply(simp add: alphas_abs alphas)

  apply(drule conjunct1)

  apply (simp add: trm_lts.supp)

  apply(simp add: supp_abs)

  apply (simp add: trm_lts.supp)

  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)

    thm Lt_subst

    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 eqvts supp_at_base fresh_star_def)

  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