theory BetaCR
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)

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])"
| "atom x \<sharp> (y, s) \<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 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)

inductive 
  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
where
  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
| b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"

equivariance beta

(* HERE 1 *)
nominal_inductive beta
  avoids b3: x
  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

(* This also works, but we cannot have them together: *)
(*nominal_inductive beta
  avoids b4: x
  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)*)

(* But I need a combination, possibly with an 'and' syntax:
nominal_inductive beta
  avoids b3: x and b4: x
  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
*)

(* The combination should look like this: *)
lemma beta_strong_induct:
  assumes "x1 \<longrightarrow>b x2"
  and "\<And>t1 t2 s c. \<lbrakk> t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (App t1 s) (App t2 s)"
  and "\<And>s1 s2 t c. \<lbrakk> s1 \<longrightarrow>b s2; \<And>c. P c s1 s2\<rbrakk> \<Longrightarrow> P c (App t s1) (App t s2)"
  and "\<And>t1 t2 x c. \<lbrakk>{atom x} \<sharp>* c;  t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (Lam [x]. t1) (Lam [x]. t2)"
  and "\<And>x s t c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> s\<rbrakk> \<Longrightarrow> P c (App (Lam [x]. t) s) (t [x ::= s])"
  shows "P (c\<Colon>'a\<Colon>fs) x1 x2"
  sorry

inductive
  beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80)
where
  bs1[intro, simp]: "M \<longrightarrow>b* M"
| bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"

lemma beta_star_trans:
  assumes "A \<longrightarrow>b* B"
  and     "B \<longrightarrow>b* C"
  shows   "A \<longrightarrow>b* C"
  using assms(2) assms(1)
  by induct auto

(* HERE 2: Does not work:*)

(* equivariance beta_star *)

(* proved manually below. *)

lemma eqvt_helper: "x1 \<longrightarrow>b* x2 \<Longrightarrow>  (p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2)"
  apply (erule beta_star.induct)
  apply auto
  using eqvt(1) bs2
  by blast

lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))"
  apply rule
  apply (drule permute_boolE)
  apply (erule eqvt_helper)
  apply (intro permute_boolI)
  apply (drule_tac p="-p" in eqvt_helper)
  by simp

definition
  equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _")
where
  "t \<approx> s \<longleftrightarrow> (\<exists>r. t \<longrightarrow>b* r \<and> s \<longrightarrow>b* r)"

lemma equ_refl:
  shows "t \<approx> t"
  unfolding equ_def by auto

lemma equ_sym:
  assumes "t \<approx> s"
  shows "s \<approx> t"
  using assms unfolding equ_def
  by auto

(* can be ported from nominal1 *)
lemma cr:
  assumes "t \<longrightarrow>b* t1" and "t \<longrightarrow>b* t2" shows "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3"
  sorry

lemma equ_trans:
  assumes "A \<approx> B" "B \<approx> C"
  shows "A \<approx> C"
  using assms unfolding equ_def
proof (elim exE conjE)
  fix D E
  assume a: "A \<longrightarrow>b* D" "B \<longrightarrow>b* D" "B \<longrightarrow>b* E" "C \<longrightarrow>b* E"
  then obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using cr by blast
  then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a beta_star_trans by blast
  then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast
qed

lemma App_beta: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> App A C \<longrightarrow>b* App B D"
  apply (erule beta_star.induct)
  apply auto
  apply (erule beta_star.induct)
  apply auto
  done

lemma Lam_beta: "A \<longrightarrow>b* B \<Longrightarrow> Lam [x]. A \<longrightarrow>b* Lam [x]. B"
  by (erule beta_star.induct) auto

lemma Lam_rsp: "A \<approx> B \<Longrightarrow> Lam [x]. A \<approx> Lam [x]. B"
  unfolding equ_def
  apply auto
  apply (rule_tac x="Lam [x]. r" in exI)
  apply (auto simp add: Lam_beta)
  done

lemma [quot_respect]:
  shows "(op = ===> equ) Var Var"
  and   "(equ ===> equ ===> equ) App App"
  and   "(op = ===> equ ===> equ) BetaCR.Lam BetaCR.Lam"
  unfolding fun_rel_def equ_def
  apply auto
  apply (rule_tac x="App r ra" in exI)
  apply (auto simp add: App_beta)
  apply (rule_tac x="Lam [x]. r" in exI)
  apply (auto simp add: Lam_beta)
  done

lemma beta_subst1_pre: "B \<longrightarrow>b C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"
  by (nominal_induct A avoiding: x B C rule: lam.strong_induct)
     (auto simp add: App_beta Lam_beta)

lemma beta_subst1: "B \<longrightarrow>b* C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"
  apply (erule beta_star.induct)
  apply auto
  apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]")
  apply (rotate_tac 1)
  apply (erule beta_star_trans)
  apply assumption
  apply (simp add: beta_subst1_pre)
  done

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

lemma beta_subst2_pre:
  assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]"
  using assms
(* HERE 3: nominal_induct doesn't work - leaves the assumption *)
(*  apply (nominal_induct avoiding: x C rule: beta_strong_induct)*)
  apply -
  apply (erule beta_strong_induct[of A B "\<lambda>c A B. A [(fst c) ::= (snd c)] \<longrightarrow>b* B [(fst c) ::= (snd c)]" "(x, C)", simplified])
  apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3]
  apply (subst substitution_lemma)
  apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2]
  apply (auto simp add: fresh_star_def fresh_Pair)
  apply (rule beta_star.intros)
  defer
  apply (subst beta.intros)
  apply (auto simp add: fresh_fact)
  done

lemma beta_subst2: "A \<longrightarrow>b* B \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= C]"
  apply (erule beta_star.induct)
  apply auto
  apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]")
  apply (rotate_tac 1)
  apply (erule beta_star_trans)
  apply assumption
  apply (simp add: beta_subst2_pre)
  done

lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]"
  using beta_subst1 beta_subst2 beta_star_trans by metis

lemma subst_rsp_pre:
  "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]"
  unfolding equ_def
  apply auto
  apply (rule_tac x="r [xa ::= ra]" in exI)
  apply (simp add: beta_subst)
  done

lemma [quot_respect]:
  shows "(equ ===> op = ===> equ ===> equ) subst subst"
unfolding fun_rel_def by (auto simp add: subst_rsp_pre)

lemma [quot_respect]:
  shows "(op = ===> equ ===> equ) permute permute"
  unfolding fun_rel_def equ_def
  apply (auto intro: eqvts)
  apply (rule_tac x="x \<bullet> r" in exI)
  using eqvts(1) permute_boolI by metis

quotient_type qlam = lam / equ
  by (auto intro!: equivpI reflpI sympI transpI simp add: equ_refl equ_sym)
     (erule equ_trans, assumption)

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 BetaCR.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, eqvt]:
  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)"
  by(descending, simp add: equ_refl)+

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  

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

lemma Supp_rsp:
  "a \<approx> b \<Longrightarrow> Supp a = Supp b"
  unfolding Supp_def
  apply(rule_tac f="Inter" in arg_cong)
  apply(auto)
  apply (metis equ_trans)
  by (metis equivp_def qlam_equivp)

lemma [quot_respect]:
  shows "(equ ===> op=) Supp Supp"
  unfolding fun_rel_def by (auto simp add: Supp_rsp)

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_subst:
  shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
  by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)

lemma supp_beta: "x \<longrightarrow>b r \<Longrightarrow> supp r \<subseteq> supp x"
  apply (induct rule: beta.induct)
  apply (simp_all add: lam.supp)
  apply blast+
  using supp_subst by blast

lemma supp_beta_star: "x \<longrightarrow>b* r \<Longrightarrow> supp r \<subseteq> supp x"
  apply (erule beta_star.induct)
  apply auto
  using supp_beta by blast

lemma supp_equ: "x \<approx> y \<Longrightarrow> \<exists>z. z \<approx> x \<and> supp z \<subseteq> supp x \<inter> supp y"
  unfolding equ_def
  apply (simp (no_asm) only: equ_def[symmetric])
  apply (elim exE)
  apply (rule_tac x=r in exI)
  apply rule
  apply (metis bs1 equ_def)
  using supp_beta_star by blast

lemma supp_psubset: "Supp x \<subset> supp x \<Longrightarrow> \<exists>t. t \<approx> x \<and> supp t \<subset> supp x"
proof -
  assume "Supp x \<subset> supp x"
  then obtain a where "a \<in> supp x" "a \<notin> Supp x" by blast
  then obtain y where nin: "y \<approx> x" "a \<notin> supp y" unfolding Supp_def by blast
  then obtain t where eq: "t \<approx> x" "supp t \<subseteq> supp x \<inter> supp y"
    using supp_equ equ_sym by blast
  then have "supp t \<subset> supp x" using nin
    by (metis `(a\<Colon>atom) \<in> supp (x\<Colon>lam)` le_infE psubset_eq set_rev_mp)
  then show "\<exists>t. t \<approx> x \<and> supp t \<subset> supp x" using eq by blast
qed

lemma Supp_exists: "\<exists>t. supp t = Supp t \<and> t \<approx> x"
proof -
  have "\<And>fs x. supp x = fs \<Longrightarrow> \<exists>t. supp t = Supp t \<and> t \<approx> x"
  proof -
    fix fs
    show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
    proof (cases "finite fs")
      case True
      assume fs: "finite fs"
      then show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
      proof (induct fs rule: finite_psubset_induct, clarify)
        fix A :: "atom set" fix x :: lam
        assume IH: "\<And>B xa. \<lbrakk>B \<subset> supp x; supp xa = B\<rbrakk> \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> xa"
        show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
        proof (cases "supp x = Supp x")
          assume "supp x = Supp x"
          then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
            by (rule_tac x="x" in exI) (simp add: equ_refl)
        next
          assume "supp x \<noteq> Supp x"
          then have "Supp x \<subset> supp x" using Supp_supp by blast
          then obtain y where a1: "supp y \<subset> supp x" "y \<approx> x"
            using supp_psubset by blast
          then obtain t where "supp t = Supp t \<and> t \<approx> y"
            using IH[of "supp y" y] by blast
          then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" using a1 equ_trans
            by blast
        qed
      qed
    next
      case False
      fix x :: lam
      assume "supp x = fs" "infinite fs"
      then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
        by (auto simp add: finite_supp)
    qed simp
  qed
  then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by blast
qed

lemma subst3: "x \<noteq> y \<and> atom x \<notin> Supp s \<Longrightarrow> Lam [x]. t [y ::= s] \<approx> Lam [x]. (t [y ::= s])"
proof -
  assume as: "x \<noteq> y \<and> atom x \<notin> Supp s"
  obtain s' where s: "supp s' = Supp s'" "s' \<approx> s" using Supp_exists[of s] by blast
  then have lhs: "Lam [x]. t [y ::= s] \<approx> Lam [x]. t [y ::= s']" using subst_rsp_pre equ_refl equ_sym by blast
  have supp: "Supp s' = Supp s" using Supp_rsp s(2) by blast
  have lhs_rhs: "Lam [x]. t [y ::= s'] = Lam [x]. (t [y ::= s'])"
    by (simp add: fresh_def supp_Pair s supp as supp_at_base)
  have "t [y ::= s'] \<approx> t [y ::= s]"
    using subst_rsp_pre[OF equ_refl s(2)] .
  with Lam_rsp have rhs: "Lam [x]. (t [y ::= s']) \<approx> Lam [x]. (t [y ::= s])" .
  show ?thesis 
    using lhs[unfolded lhs_rhs] rhs equ_trans by blast
qed

thm subst3[quot_lifted]

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

lemma [eqvt]: "(p \<bullet> (a \<approx> b)) = ((p \<bullet> a) \<approx> (p \<bullet> b))"
  unfolding equ_def
  by perm_simp rule

lemma [eqvt]: "p \<bullet> (Supp x) = Supp (p \<bullet> x)"
  unfolding Supp_def
  by perm_simp rule

lemmas s = Supp_Lam[quot_lifted]

lemma var_beta_pre: "s \<longrightarrow>b* r \<Longrightarrow> s = Var name \<Longrightarrow> r = Var name"
  apply (induct rule: beta_star.induct)
  apply simp
  apply (subgoal_tac "M2 = Var name")
  apply (thin_tac "M1 \<longrightarrow>b* M2")
  apply (thin_tac "M1 = Var name")
  apply (thin_tac "M1 = Var name \<Longrightarrow> M2 = Var name")
  defer
  apply simp
  apply (erule_tac beta.cases)
  apply simp_all
  done

lemma var_beta: "Var name \<longrightarrow>b* r \<longleftrightarrow> r = Var name"
  by (auto simp add: var_beta_pre)

lemma qlam_eq_iff:
  "(QVar n = QVar m) = (n = m)"
  apply descending unfolding equ_def var_beta by auto

lemma "supp (QVar n) = {atom n}"
  unfolding supp_def
  apply simp
  unfolding qlam_eq_iff
  apply (fold supp_def)
  apply (simp add: supp_at_base)
  done

end