Theory Lambda_Z

(*
 * 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 ‹
fun 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 |> Simplifier.add_simps [@{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) ∈ {→⇩β}"
| Appl: "(s, t) ∈ {→⇩β} ⟹ (App s u, App t u) ∈ {→⇩β}"
| Appr: "(s, t) ∈ {→⇩β} ⟹ (App u s, App u t) ∈ {→⇩β}"
| Abs: "(s, t) ∈ {→⇩β} ⟹ (Abs x s, Abs x t) ∈ {→⇩β}"

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

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 →⇩β⇧* t ≡ (s, t) ∈ {→⇩β}⇧*"

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)⇧∙ = Var x"
| "(Abs x t)⇧∙ = Abs x t⇧∙"
| "(App s t)⇧∙ = app_beta s⇧∙ t⇧∙"
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 →⇩β⇧* t" and "u →⇩β⇧* v"
  shows "App s u →⇩β⇧* 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 →⇩β⇧* t"
  shows "Abs x s →⇩β⇧* Abs x t"
using assms by (induct) (auto intro: Beta.intros rtrancl_into_rtrancl)

lemma self:
  "t →⇩β⇧* t⇧∙"
proof (nominal_induct t rule: term.strong_induct)
  case (App t u)
  then show ?case
    by (cases "t⇧∙" rule: app_beta_exhaust[of "u⇧∙"])
       (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⇧∙"
proof (nominal_induct t avoiding: x rule: term.strong_induct)
  case (App t u)
  then show ?case by (cases "t⇧∙" rule: app_beta_exhaust[of "u⇧∙"]) (auto intro: fresh_subst)
qed auto

lemma subst_Beta:
  assumes "t →⇩β t'"
  shows "subst x s t →⇩β 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 →⇩β s'"
  shows "subst x s t →⇩β⇧* 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 →⇩β⇧* s'" and "t →⇩β⇧* t'"
  shows "subst x s t →⇩β⇧* 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 →⇩β 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 →⇩β t"
  shows "∃u. t = Abs x u ∧ s →⇩β 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 →⇩β t"
  obtains u where "t = Abs x u" and "s →⇩β u"
using assms by (blast dest: Abs_BetaD)

lemma Abs_BetasE:
  assumes "Abs x s →⇩β⇧* t"
  obtains u where "t = Abs x u" and "s →⇩β⇧* u"
using assms by (induct "Abs x s" t) (auto elim: Abs_BetaE intro: rtrancl_into_rtrancl)

lemma bullet_App:
  "(App s⇧∙ t⇧∙, (App s t)⇧∙) ∈ {→⇩β}⇧="
by (cases "s⇧∙" rule: term.strong_exhaust[of _ _ "t⇧∙"])
   (auto simp: fresh_star_def intro: Beta.root)

lemma rhs:
  "subst x s⇧∙ t⇧∙ →⇩β⇧* (subst x s t)⇧∙"
proof (nominal_induct t avoiding: x s rule: term.strong_induct)
  case (App t⇩1 t⇩2)
  show ?case
  proof (cases "t⇩1⇧∙" rule: app_beta_exhaust[of "(x, t⇩2, s)"])
    case (Redex y u)
    then have "Abs y (subst x s⇧∙ u) →⇩β⇧* (subst x s t⇩1)⇧∙"
      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⇩1)⇧∙ = Abs y v" and " subst x s⇧∙ u →⇩β⇧* 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⇧∙ ((App t⇩1 t⇩2)⇧∙) →⇩β⇧* App ((subst x s t⇩1)⇧∙) ((subst x s t⇩2)⇧∙)"
      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 →⇩β⇧* t" and "atom x ♯ s"
  shows "atom x ♯ t"
using assms by (induct) (auto dest: Beta_fresh)

lemma Var_BetaD:
  assumes "Var x →⇩β t"
  shows False
using assms by (induct "Var x" t)

lemma Var_BetasD:
  assumes "Var x →⇩β⇧* t"
  shows "t = Var x"
using assms by (induct) (auto dest: Var_BetaD)

lemma app_beta_Betas:
  assumes "s →⇩β⇧* s'" and "t →⇩β⇧* t'"
  shows "app_beta s t →⇩β⇧* app_beta s' t'"
using assms
proof (cases s rule: term.strong_exhaust [of _ _ t])
  case (App s⇩1 s⇩2)
  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 →⇩β t"
  shows "t →⇩β⇧* s⇧∙ ∧ s⇧∙ →⇩β⇧* t⇧∙"
using assms
proof (nominal_induct rule: Beta_strong_induct)
  case (Appl s t u)
  then have "App t u →⇩β⇧* App s⇧∙ u⇧∙" using self by (auto intro: App_Betas)
  also have "App s⇧∙ u⇧∙ →⇩β⇧* (App s u)⇧∙" 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 →⇩β⇧* App u⇧∙ s⇧∙" using self by (auto intro: App_Betas)
  also have "App u⇧∙ s⇧∙ →⇩β⇧* (App u s)⇧∙" 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