(*
 * Title:      Z  
 * Author:     Bertram Felgenhauer (2016)
 * Author:     Julian Nagele (2016)
 * Author:     Vincent van Oostrom (2016)
 * Author:     Christian Sternagel (2016)
 * Maintainer: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at>
 * Maintainer: Juilan Nagele <julian.nagele@uibk.ac.at>
 * Maintainer: Christian Sternagel <c.sternagel@gmail.com>
 * License:    BSD
 *)

section ‹Lambda Calculus has the Church-Rosser property›

theory Lambda_Z
imports
  Nominal2.Nominal2
  "HOL-Eisbach.Eisbach"
  Z
begin

atom_decl name

nominal_datatype "term" =
  Var name
| App "term" "term"
| Abs x::name t::"term" binds x in t

subsection ‹Ad-hoc methods for nominal-functions over lambda terms›

ML ‹
  graph_aux_tac ctxt =
 SUBGOAL (fn (subgoal, i) =>
 (case subgoal of
 Const (@{const_name Trueprop}, _) $ (Const (@{const_name eqvt}, _) $ Free (f, _)) =>
 full_simp_tac (
 ctxt addsimps [@{thm eqvt_def}, Proof_Context.get_thm ctxt (f ^ "_def")]) i
 | _ => no_tac))
 ›

method_setup eqvt_graph_aux =
  ‹Scan.succeed (fn ctxt : Proof.context => SIMPLE_METHOD' (graph_aux_tac ctxt))›
  "show equivariance of auxilliary graph construction for nominal functions"

method without_alpha_lst methods m =
  (match termI in H [simproc del: alpha_lst]: _ → ‹m›)

method Abs_lst =
  (match premises in
    "atom ?x ♯ c" and P [thin]: "[[atom _]]lst. _ = [[atom _]]lst. _" for c :: "'a::fs" →
      ‹rule Abs_lst1_fcb2' [where c = c, OF P]›
  ∣ P [thin]: "[[atom _]]lst. _ = [[atom _]]lst. _" → ‹rule Abs_lst1_fcb2' [where c = "()", OF P]›)

method pat_comp_aux =
  (match premises in
    "x = (_ :: term) ==> _" for x → ‹rule term.strong_exhaust [where y = x and c = x]›
  ∣ "x = (Var _, _) ==> _" for x :: "_ :: fs" →
    ‹rule term.strong_exhaust [where y = "fst x" and c = x]›
  ∣ "x = (_, Var _) ==> _" for x :: "_ :: fs" →
    ‹rule term.strong_exhaust [where y = "snd x" and c = x]›
  ∣ "x = (_, _, Var _) ==> _" for x :: "_ :: fs" →
    ‹rule term.strong_exhaust [where y = "snd (snd x)" and c = x]›)

method pat_comp = (pat_comp_aux; force simp: fresh_star_def fresh_Pair_elim)

method freshness uses fresh =
  (match conclusion in
    "_ ♯ _" → ‹simp add: fresh_Unit fresh_Pair fresh›
  ∣ "_ ♯* _" → ‹simp add: fresh_star_def fresh_Unit fresh_Pair fresh›)

method solve_eqvt_at =
  (simp add: eqvt_at_def; simp add: perm_supp_eq fresh_star_Pair)+

method nf uses fresh = without_alpha_lst ‹
 eqvt_graph_aux, rule TrueI, pat_comp, auto, Abs_lst,
 auto simp: Abs_fresh_iff pure_fresh perm_supp_eq,
 (freshness fresh: fresh)+,
 solve_eqvt_at?›


subsection ‹Substitutions›

nominal_function subst
where
  "subst x s (Var y) = (if x = y then s else Var y)"
| "subst x s (App t u) = App (subst x s t) (subst x s u)"
| "atom y ♯ (x, s) ==> subst x s (Abs y t) = Abs y (subst x s t)"
by nf
nominal_termination (eqvt) by lexicographic_order

lemma fresh_subst:
  "atom z ♯ s ==> z = y ∨ atom z ♯ t ==> atom z ♯ subst y s t"
by (nominal_induct t avoiding: z y s rule: term.strong_induct) auto

lemma fresh_subst_id [simp]:
  "atom x ♯ t ==> subst x s t = t"
by (nominal_induct t avoiding: x s rule: term.strong_induct) (auto simp: fresh_at_base)

text ‹The substitution lemma.›
lemma subst_subst:
  assumes "x ≠ y" and "atom x ♯ u"
  shows "subst y u (subst x s t) = subst x (subst y u s) (subst y u t)"
using assms by (nominal_induct t avoiding: x y u s rule: term.strong_induct) (auto simp: fresh_subst)

inductive_set Beta (‹{→_\β}›)
where
  root: "atom x ♯ t ==> (App (Abs x s) t, subst x t s) ∈ {→_\<beta>}"
| Appl: "(s, t) ∈ {→_\<beta>} ==> (App s u, App t u) ∈ {→_\<beta>}"
| Appr: "(s, t) ∈ {→_\<beta>} ==> (App u s, App u t) ∈ {→_\<beta>}"
| Abs: "(s, t) ∈ {→_\<beta>} ==> (Abs x s, Abs x t) ∈ {→_\<beta>}"

abbreviation beta (‹(_/ →_\β _)› [56, 56] 55)
where
  "s →_\<beta> t ≡ (s, t) ∈ {→_\<beta>}"

equivariance Betap
lemmas Beta_eqvt = Betap.eqvt [to_set]

nominal_inductive Betap
  avoids Abs: x
       | root: x
by (simp_all add: fresh_star_def fresh_subst)

lemmas Beta_strong_induct = Betap.strong_induct [to_set]

abbreviation betas (infix ‹→_\β^*› 50)
where
  "s →_\<beta>^* t ≡ (s, t) ∈ {→_\<beta>}^*"

nominal_function app_beta :: "term → term → term"
where
  "atom x ♯ u ==> app_beta (Abs x s') u = subst x u s'"
| "app_beta (Var x) u = App (Var x) u"
| "app_beta (App s t) u = App (App s t) u"
by (nf fresh: fresh_subst)
nominal_termination (eqvt) by lexicographic_order

nominal_function bullet :: "term → term" (‹_^\∙› [1000] 1000)
where
  "(Var x)^\<bullet> = Var x"
| "(Abs x t)^\<bullet> = Abs x t^\<bullet>"
| "(App s t)^\<bullet> = app_beta s^\<bullet> t^\<bullet>"
by nf
nominal_termination (eqvt) by lexicographic_order

lemma app_beta_exhaust [case_names Redex no_Redex]:
  fixes c :: "'a :: fs"
  assumes "∧x s'. atom x ♯ c ==> s = Abs x s' ==> thesis"
    and "(∧t. app_beta s t = App s t) ==> thesis"
  shows "thesis"
by (cases s rule: term.strong_exhaust [of _ _ c]) (auto simp: fresh_star_def fresh_Pair intro: assms)

lemma App_Betas:
  assumes "s →_\<beta>^* t" and "u →_\<beta>^* v"
  shows "App s u →_\<beta>^* App t v"
using assms(1)
proof (induct)
  case base
  show ?case using assms(2) by (induct) (auto intro: Beta.intros rtrancl_into_rtrancl)
qed (auto intro: Beta.intros rtrancl_into_rtrancl)

lemma Abs_Betas:
  assumes "s →_\<beta>^* t"
  shows "Abs x s →_\<beta>^* Abs x t"
using assms by (induct) (auto intro: Beta.intros rtrancl_into_rtrancl)

lemma self:
  "t →_\<beta>^* t^\<bullet>"
proof (nominal_induct t rule: term.strong_induct)
  case (App t u)
  then show ?case
    by (cases "t^\<bullet>" rule: app_beta_exhaust[of "u^\<bullet>"])
       (auto intro: App_Betas Beta.intros rtrancl_into_rtrancl)
qed (auto intro: Abs_Betas)

lemma fresh_atom_bullet:
  "atom (x::name) ♯ t ==> atom x ♯ t^\<bullet>"
proof (nominal_induct t avoiding: x rule: term.strong_induct)
  case (App t u)
  then show ?case by (cases "t^\<bullet>" rule: app_beta_exhaust[of "u^\<bullet>"]) (auto intro: fresh_subst)
qed auto

lemma subst_Beta:
  assumes "t →_\<beta> t'"
  shows "subst x s t →_\<beta> subst x s t'"
using assms
proof (nominal_induct avoiding: x s rule: Beta_strong_induct)
  case (root y t u)
  then show ?case by (auto simp: subst_subst fresh_subst intro: Beta.root)
qed (auto intro: Beta.intros)

lemma Beta_in_subst:
  assumes "s →_\<beta> s'"
  shows "subst x s t →_\<beta>^* subst x s' t"
using assms
by (nominal_induct t avoiding: x s s' rule: term.strong_induct)
   (auto intro: App_Betas Abs_Betas)

lemma subst_Betas:
  assumes "s →_\<beta>^* s'" and "t →_\<beta>^* t'"
  shows "subst x s t →_\<beta>^* subst x s' t'"
using assms(1)
proof (induct)
  case base
  from assms(2) show ?case by (induct) (auto simp: subst_Beta intro: rtrancl_into_rtrancl)
next
  case (step u v)
  from Beta_in_subst [OF this(2), of x t'] and this(3) show ?case by auto
qed

lemma Beta_fresh:
  fixes x :: name
  assumes "s →_\<beta> t" and "atom x ♯ s"
  shows "atom x ♯ t"
using assms by (nominal_induct rule: Beta_strong_induct) (auto simp: fresh_subst)

lemma Abs_BetaD:
  assumes "Abs x s →_\<beta> t"
  shows "∃u. t = Abs x u ∧ s →_\<beta> u"
using assms
proof (nominal_induct "Abs x s" t avoiding: s rule: Beta_strong_induct)
  case (Abs u v y)
  then show ?case
    by (auto simp: Abs1_eq_iff Beta_fresh fresh_permute_left intro!: exI [of _ "(y ↔ x) ∙ v"])
       (metis Abs1_eq_iff(3) Beta_eqvt flip_commute)
qed

lemma Abs_BetaE:
  assumes "Abs x s →_\<beta> t"
  obtains u where "t = Abs x u" and "s →_\<beta> u"
using assms by (blast dest: Abs_BetaD)

lemma Abs_BetasE:
  assumes "Abs x s →_\<beta>^* t"
  obtains u where "t = Abs x u" and "s →_\<beta>^* u"
using assms by (induct "Abs x s" t) (auto elim: Abs_BetaE intro: rtrancl_into_rtrancl)

lemma bullet_App:
  "(App s^\<bullet> t^\<bullet>, (App s t)^\<bullet>) ∈ {→_\<beta>}⁼"
by (cases "s^\<bullet>" rule: term.strong_exhaust[of _ _ "t^\<bullet>"])
   (auto simp: fresh_star_def intro: Beta.root)

lemma rhs:
  "subst x s^\<bullet> t^\<bullet> →_\<beta>^* (subst x s t)^\<bullet>"
proof (nominal_induct t avoiding: x s rule: term.strong_induct)
  case (App t₁ t₂)
  show ?case
  proof (cases "t₁^\<bullet>" rule: app_beta_exhaust[of "(x, t₂, s)"])
    case (Redex y u)
    then have "Abs y (subst x s^\<bullet> u) →_\<beta>^* (subst x s t₁)^\<bullet>"
      using App(1) [of x s] by (simp add: fresh_star_def fresh_atom_bullet)
    with Abs_BetasE obtain v where "(subst x s t₁)^\<bullet> = Abs y v" and " subst x s^\<bullet> u →_\<beta>^* v" by blast
    then show ?thesis using subst_subst and subst_Betas and App(2) and Redex
      by (simp add: fresh_atom_bullet fresh_subst)
  next
    case (no_Redex)
    then have "subst x s^\<bullet> ((App t₁ t₂)^\<bullet>) →_\<beta>^* App ((subst x s t₁)^\<bullet>) ((subst x s t₂)^\<bullet>)"
      using App by (auto intro: App_Betas)
    then show ?thesis using bullet_App by (force intro: rtrancl_into_rtrancl)
  qed
qed (force dest: fresh_atom_bullet intro: Abs_Betas)+

lemma Betas_fresh:
  fixes x :: name
  assumes "s →_\<beta>^* t" and "atom x ♯ s"
  shows "atom x ♯ t"
using assms by (induct) (auto dest: Beta_fresh)

lemma Var_BetaD:
  assumes "Var x →_\<beta> t"
  shows False
using assms by (induct "Var x" t)

lemma Var_BetasD:
  assumes "Var x →_\<beta>^* t"
  shows "t = Var x"
using assms by (induct) (auto dest: Var_BetaD)

lemma app_beta_Betas:
  assumes "s →_\<beta>^* s'" and "t →_\<beta>^* t'"
  shows "app_beta s t →_\<beta>^* app_beta s' t'"
using assms
proof (cases s rule: term.strong_exhaust [of _ _ t])
  case (App s₁ s₂)
  with assms show ?thesis
    by (cases s' rule: app_beta_exhaust [of t']) (auto intro: root rtrancl_into_rtrancl App_Betas)
qed (auto simp: fresh_star_def Betas_fresh subst_Betas elim: Abs_BetasE intro: App_Betas dest!: Var_BetasD)

lemma lambda_Z:
  assumes "s →_\<beta> t"
  shows "t →_\<beta>^* s^\<bullet> ∧ s^\<bullet> →_\<beta>^* t^\<bullet>"
using assms
proof (nominal_induct rule: Beta_strong_induct)
  case (Appl s t u)
  then have "App t u →_\<beta>^* App s^\<bullet> u^\<bullet>" using self by (auto intro: App_Betas)
  also have "App s^\<bullet> u^\<bullet> →_\<beta>^* (App s u)^\<bullet>" using bullet_App by force
  finally show ?case using Appl by (auto intro: App_Betas app_beta_Betas)
next
  case (Appr s t u)
  then have "App u t →_\<beta>^* App u^\<bullet> s^\<bullet>" using self by (auto intro: App_Betas)
  also have "App u^\<bullet> s^\<bullet> →_\<beta>^* (App u s)^\<bullet>" using bullet_App by force
  finally show ?case using Appr by (auto intro: App_Betas app_beta_Betas)
qed (auto intro: Abs_Betas subst_Betas rhs simp: self fresh_atom_bullet)

interpretation lambda_z: z_property bullet Beta
by (standard) (fact lambda_Z)

end