theory Beta

imports 

  "../Nominal2"

begin

atom_decl name

nominal_datatype lam =

  Var "name"

| App "lam" "lam"

| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

section {* capture-avoiding substitution *}

nominal_primrec

  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)

where

  "(Var x)[y ::= s] = (if x = y then s else (Var x))"

| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

  unfolding eqvt_def subst_graph_def

  apply (rule, perm_simp, rule)

  apply(rule TrueI)

  apply(auto simp add: lam.distinct lam.eq_iff)

  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

  apply(blast)+

  apply(simp_all add: fresh_star_def fresh_Pair_elim)

  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

  apply(simp_all add: Abs_fresh_iff)

  apply(simp add: fresh_star_def fresh_Pair)

  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

done

termination (eqvt)

  by lexicographic_order

lemma forget:

  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

  by (nominal_induct t avoiding: x s rule: lam.strong_induct)

     (auto simp add: lam.fresh fresh_at_base)

lemma fresh_fact:

  fixes z::"name"

  assumes a: "atom z \<sharp> s"

      and b: "z = y \<or> atom z \<sharp> t"

  shows "atom z \<sharp> t[y ::= s]"

  using a b

  by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

     (auto simp add: lam.fresh fresh_at_base)

lemma substitution_lemma:  

  assumes a: "x \<noteq> y" "atom x \<sharp> u"

  shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"

using a 

by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)

   (auto simp add: fresh_fact forget)

inductive

  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _")

where

  beta_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<rightarrow> t[x ::= s]"

| beta_Lam:   "t \<rightarrow> s \<Longrightarrow> Lam [x].t \<rightarrow> Lam [x].s"

| beta_App1:  "t \<rightarrow> s \<Longrightarrow> App t u \<rightarrow> App s u"

| beta_App2:  "t \<rightarrow> s \<Longrightarrow> App u t \<rightarrow> App u s"

equivariance beta

nominal_inductive beta

  avoids beta_beta: "x" 

       | beta_Lam: "x"

by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

inductive

  equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _")

where

  equ_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<approx> t[x ::= s]"

| equ_refl:  "t \<approx> t"

| equ_sym:   "t \<approx> s \<Longrightarrow> s \<approx> t"

| equ_trans: "\<lbrakk>t1 \<approx> t2; t2 \<approx> t3\<rbrakk> \<Longrightarrow> t1 \<approx> t3"

| equ_Lam:   "t \<approx> s \<Longrightarrow> Lam [x].t \<approx> Lam [x].s"

| equ_App1:  "t \<approx> s \<Longrightarrow> App t u \<approx> App s u"

| equ_App2:  "t \<approx> s \<Longrightarrow> App u t \<approx> App u s"

equivariance equ

nominal_inductive equ

  avoids equ_beta: "x" 

       | equ_Lam: "x"

by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

inductive

  equ2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx>2 _")

where

  equ2_beta1:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) t2 \<approx>2 s1[x ::= s2]"

| equ2_beta2:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> s1[x ::= s2] \<approx>2 App (Lam [x].t1) t2"

| equ2_Var:   "Var x \<approx>2 Var x"

| equ2_Lam:   "t \<approx>2 s \<Longrightarrow> Lam [x].t \<approx>2 Lam [x].s"

| equ2_App:   "\<lbrakk>t1 \<approx>2 s1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> App t1 t2 \<approx>2 App s1 s2"

equivariance equ2

nominal_inductive equ2

  avoids equ2_beta1: "x"

       | equ2_beta2: "x" 

       | equ2_Lam: "x"

by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

lemma equ2_refl:

  fixes t::"lam"

  shows "t \<approx>2 t"

apply(induct t rule: lam.induct)

apply(auto intro: equ2.intros)

done

lemma equ2_symm:

  fixes t s::"lam"

  assumes "t \<approx>2 s"

  shows "s \<approx>2 t"

using assms

apply(induct)

apply(auto intro: equ2.intros)

done

lemma equ2_trans:

  fixes t1 t2 t3::"lam"

  assumes "t1 \<approx>2 t2" "t2 \<approx>2 t3"

  shows "t1 \<approx>2 t3"

using assms

apply(nominal_induct t1 t2 avoiding: t3 rule: equ2.strong_induct)

defer

defer

apply(erule equ2.cases)

apply(auto)

apply(rule equ2_beta2)

apply(simp)

apply(simp)

apply(simp)

apply(rule equ2_refl)

defer

apply(rotate_tac 4)

apply(erule equ2.cases)

apply(auto)

oops

lemma "a \<noteq> x \<Longrightarrow> x \<noteq> y \<Longrightarrow> y \<noteq> a \<Longrightarrow> y \<noteq> b \<Longrightarrow> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx> App (Var b) (Var a))"

  apply (rule equ_trans)

  apply (rule equ_App1)

  apply (rule equ_beta)

  apply (simp add: lam.fresh fresh_at_base)

  apply (subst subst.simps)

  apply (simp add: lam.fresh fresh_at_base)+

  apply (rule equ_trans)

  apply (rule equ_beta)

  apply (simp add: lam.fresh fresh_at_base)

  apply (simp add: equ_refl)

  done

lemma "\<not> (Var b \<approx>2 Var a) \<Longrightarrow> \<not> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx>2 App (Var b) (Var a))"

  apply rule

  apply (erule equ2.cases)

  apply auto

  done

lemma [quot_respect]:

  shows "(op = ===> equ) Var Var"

  and   "(equ ===> equ ===> equ) App App"

  and   "(op = ===> equ ===> equ) Beta.Lam Beta.Lam"

unfolding fun_rel_def

by (auto intro: equ.intros)

lemma equ_subst1:

  assumes "t \<approx> s"

  shows "t[x ::= u] \<approx> s[x ::= u]"

using assms

apply(nominal_induct avoiding: x u rule: equ.strong_induct)

apply(simp)

apply(rule equ_trans)

apply(rule equ_beta)

apply(simp add: fresh_fact)

apply(subst (2) substitution_lemma)

apply(simp add: fresh_at_base)

apply(simp)

apply(rule equ_refl)

apply(rule equ_refl)

apply(auto intro: equ_sym)[1]

apply(blast intro: equ_trans)

apply(simp add: equ_Lam)

apply(simp add: equ_App1)

apply(simp add: equ_App2)

done

lemma equ_subst2:

  assumes "t \<approx> s"

  shows "u[x ::= t] \<approx> u[x ::= s]"

using assms

apply(nominal_induct u avoiding: x t s rule: lam.strong_induct)

apply(simp add: equ_refl)

apply(simp)

apply(smt equ_App1 equ_App2 equ_trans)

apply(simp)

apply(metis equ_Lam)

done

lemma [quot_respect]:

  shows "(equ ===> op = ===> equ ===> equ) subst subst"

unfolding fun_rel_def

by (metis equ_subst1 equ_subst2 equ_trans)

lemma [quot_respect]:

  shows "(op = ===> equ ===> equ) permute permute"

unfolding fun_rel_def

by (auto intro: eqvts)

quotient_type qlam = lam / equ

apply(rule equivpI)

apply(rule reflpI)

apply(simp add: equ_refl)

apply(rule sympI)

apply(simp add: equ_sym)

apply(rule transpI)

apply(auto intro: equ_trans)

done

quotient_definition "QVar::name \<Rightarrow> qlam" is Var

quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App

quotient_definition QLam ("QLam [_]._") 

  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam

lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]

lemmas qlam_induct = lam.induct[quot_lifted]

instantiation qlam :: pt

begin

quotient_definition "permute_qlam::perm \<Rightarrow> qlam \<Rightarrow> qlam" 

  is "permute::perm \<Rightarrow> lam \<Rightarrow> lam"

instance

apply default

apply(descending)

apply(simp)

apply(rule equ_refl)

apply(descending)

apply(simp)

apply(rule equ_refl)

done

end

lemma qlam_perm[simp]:

  shows "p \<bullet> (QVar x) = QVar (p \<bullet> x)"

  and "p \<bullet> (QApp t s) = QApp (p \<bullet> t) (p \<bullet> s)"

  and "p \<bullet> (QLam [x].t) = QLam [p \<bullet> x].(p \<bullet> t)"

apply(descending)

apply(simp add: equ_refl)

apply(descending)

apply(simp add: equ_refl)

apply(descending)

apply(simp add: equ_refl)

done

lemma qlam_supports:

  shows "{atom x} supports (QVar x)"

  and   "supp (t, s) supports (QApp t s)"

  and   "supp (x, t) supports (QLam [x].t)"

unfolding supports_def fresh_def[symmetric]

by (auto simp add: swap_fresh_fresh)

lemma qlam_fs:

  fixes t::"qlam"

  shows "finite (supp t)"

apply(induct t rule: qlam_induct)

apply(rule supports_finite)

apply(rule qlam_supports)

apply(simp)

apply(rule supports_finite)

apply(rule qlam_supports)

apply(simp add: supp_Pair)

apply(rule supports_finite)

apply(rule qlam_supports)

apply(simp add: supp_Pair finite_supp)

done

instantiation qlam :: fs

begin

instance

apply(default)

apply(rule qlam_fs)

done

end

quotient_definition subst_qlam ("_[_ ::q= _]")

  where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  

lemma

  "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))"

apply(descending)

apply(simp)

apply(auto intro: equ_refl)

done

lemma

  "(QApp t1 t2)[y ::q= s] = QApp (t1[y ::q= s]) (t2[y ::q= s])"

apply(descending)

apply(simp)

apply(rule equ_refl)

done

definition

  "Supp t = \<Inter>{supp s | s. s \<approx> t}"

lemma [quot_respect]:

  shows "(equ ===> op=) Supp Supp"

unfolding fun_rel_def

unfolding Supp_def

apply(rule allI)+

apply(rule impI)

apply(rule_tac f="Inter" in arg_cong)

apply(auto)

apply (metis equ_trans)

by (metis equivp_def qlam_equivp)

quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 

  is "Supp::lam \<Rightarrow> atom set"

lemma Supp_supp:

  "Supp t \<subseteq> supp t"

unfolding Supp_def

apply(auto)

apply(drule_tac x="supp t" in spec)

apply(auto simp add: equ_refl)

done

lemma Supp_Lam:

  "atom a \<notin> Supp (Lam [a].t)"

proof -

  have "atom a \<notin> supp (Lam [a].t)" by (simp add: lam.supp)

  then show ?thesis using Supp_supp

    by blast

qed

lemmas s = Supp_Lam[quot_lifted]

definition

  ssupp :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ ssupp _")

where

  "A ssupp x \<equiv> \<forall>p. (\<forall>a \<in> A. (p \<bullet> a) = a) \<longleftrightarrow> (p \<bullet> x) = x"

lemma ssupp_supports:

  "A ssupp x \<Longrightarrow> A supports x"

unfolding ssupp_def supports_def

apply(rule allI)+

apply(drule_tac x="(a \<rightleftharpoons> b)" in spec)

apply(auto)

by (metis swap_atom_simps(3))

lemma ssupp_supp:

  assumes a: "finite A"

  and     b: "A ssupp x"

  shows "supp x = A"

proof -

  { assume 0: "A - supp x \<noteq> {}"

    then obtain a where 1: "a \<in> A - supp x" by auto

    obtain a' where *: "a' \<in>  UNIV - A" and **: "sort_of a' = sort_of a"

      by (rule obtain_atom[OF a]) (auto)  

    have "(a \<rightleftharpoons> a') \<bullet> a = a'" using 1 ** * by (auto)

    then have w0: "(a \<rightleftharpoons> a') \<bullet> x \<noteq> x"

      using b unfolding ssupp_def 

      apply -

      apply(drule_tac x="(a \<rightleftharpoons> a')" in spec)

      apply(auto)

      using 1 *

      apply(auto)

      done

    have w1: "a \<sharp> x" unfolding fresh_def using 1 by auto 

    have w2: "a' \<sharp> x" using *

      apply(rule_tac supports_fresh)

      apply(rule ssupp_supports)

      apply(rule b)

      apply(rule a)

      apply(auto)

      done

    have "False" using w0 w1 w2 by (simp add: swap_fresh_fresh)

    then have "supp x = A" by simp }

  moreover

  { assume "A - supp x = {}"

    moreover

    have "supp x \<subseteq> A"

      apply(rule supp_is_subset)

      apply(rule ssupp_supports)

      apply(rule b)

      apply(rule a)

      done

    ultimately have "supp x = A"

      by blast

  }

  ultimately show "supp x = A" by blast

qed

lemma

  "(supp x) ssupp x"

unfolding ssupp_def

apply(auto)

apply(rule supp_perm_eq)

apply(simp add: fresh_star_def)

apply(auto)

apply(simp add: fresh_perm)

apply(simp add: fresh_perm[symmetric])

(*Tzevelekos 2008, section 2.1.2 property 2.5*)

oops

(* The above is not true. Take p=(a\<leftrightarrow>b) and x={a,b}, then the goal is provably false *)

lemma

  "b \<noteq> a \<Longrightarrow> \<not>(supp {a :: name,b}) ssupp {a,b}"

unfolding ssupp_def

apply (auto)

apply (intro exI[of _ "(a\<leftrightarrow>b) :: perm"])

apply (subgoal_tac "(a \<leftrightarrow> b) \<bullet> {a, b} = {a, b}")

apply simp

apply (subgoal_tac "supp {a, b} = {atom a, atom b}")

apply (simp add: flip_def)

apply (simp add: supp_of_finite_insert supp_at_base supp_set_empty)

apply blast

by (smt empty_eqvt flip_at_simps(1) flip_at_simps(2) insert_commute insert_eqvt)

function

  qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam"  ("_ [_ ::qq= _]" [90, 90, 90] 90)

where

  "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))"

| "(QApp t1 t2)[y ::qq= s] = QApp (t1[y ::qq= s]) (t2[y ::qq= s])"

| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y ::qq= s] = QLam [x].(t[y ::qq= s])"

apply(simp_all add:)

oops

lemma

  assumes a: "Lam [x].t \<approx> s"

  shows "\<exists>x' t'. s = Lam [x']. t' \<and> t \<approx> t'"

using a

apply(induct s rule:lam.induct)

apply(erule equ.cases)

apply(auto)

apply(erule equ.cases)

apply(auto)

lemma

  "atom x \<sharp> y \<Longrightarrow> atom x \<notin> supp_qlam s \<Longrightarrow> (QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])"

apply(descending)

oops

lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)"

 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])

 apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified])

 by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left)

lemma supports_abs_qlam:

  "(supp t) supports (abs_qlam t)"

unfolding supports_def

unfolding fresh_def[symmetric]

apply(auto)

apply(perm_simp)

apply(simp add: swap_fresh_fresh)

done

lemma rep_qlam_inverse:

  "abs_qlam (rep_qlam t) = t"

by (metis Quotient_abs_rep Quotient_qlam)

lemma supports_rep_qlam:

  "supp (rep_qlam t) supports t"

apply(subst (2) rep_qlam_inverse[symmetric])

apply(rule supports_abs_qlam)

done

 lemma supports_qvar:

  "{atom x} supports (QVar x)"

apply(subgoal_tac "supp (Var x) supports (abs_qlam (Var x))")

apply(simp add: lam.supp supp_at_base)

defer

apply(rule supports_abs_qlam)

apply(simp add: QVar_def)

done

section {* Supp *}

lemma s:

  assumes "s \<approx> t"

  shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)"

using assms

by (metis Quotient_qlam Quotient_rel_abs)

lemma ss:

  "Supp t supports (abs_qlam t)"

apply(simp only: supports_def)

apply(rule allI)+

apply(rule impI)

apply(rule swap_fresh_fresh)