SSL ParRed.thy

(*  Title:      HOL/Proofs/Lambda/ParRed.thy
  Author: Tobias Nipkow
  Copyright 1995 TU Muenchen
 
 Properties of => and "cd", in particular the diamond property of => and
 confluence of beta.
*)

section ‹Parallel reduction and a complete developments›

theory ParRed imports Lambda Commutation begin


subsection ‹Parallel reduction›

inductive par_beta :: "[dB, dB] => bool"  (infixl ‹=>› 50)
  where
    var [simp, intro!]: "Var n => Var n"
  | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
  | app [simp, intro!]: "[| s => s'; t => t' |] ==> s 🍋 t => s' 🍋 t'"
  | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) 🍋 t => s'[t'/0]"

inductive_cases par_beta_cases [elim!]:
  "Var n => t"
  "Abs s => Abs t"
  "(Abs s) 🍋 t => u"
  "s 🍋 t => u"
  "Abs s => t"


subsection ‹Inclusions›

text ‹‹beta ⊆ par_beta ⊆ beta🪙*› \medskip›

lemma par_beta_varL [simp]:
    "(Var n => t) = (t = Var n)"
  by blast

lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
  by (induct t) simp_all

lemma beta_subset_par_beta: "beta <= par_beta"
  apply (rule predicate2I)
  apply (erule beta.induct)
     apply (blast intro!: par_beta_refl)+
  done

lemma par_beta_subset_beta: "par_beta ≤ beta🪙*🪙*"
  apply (rule predicate2I)
  apply (erule par_beta.induct)
     apply blast
    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
      🍋 ‹@{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor›
  done


subsection ‹Misc properties of ‹par_beta›\
lemma par_beta_lift [simp]:
    "t => t' ==> lift t n => lift t' n"
  by (induct t arbitrary: t' n) fastforce+

lemma par_beta_subst:
    "s => s' ==> t => t' ==> t[s/n] => t'[s'/n]"
  apply (induct t arbitrary: s s' t' n)
    apply (simp add: subst_Var)
   apply (erule par_beta_cases)
    apply simp
   apply (simp add: subst_subst [symmetric])
   apply (fastforce intro!: par_beta_lift)
  apply fastforce
  done


subsection ‹Confluence (directly)›

lemma diamond_par_beta: "diamond par_beta"
  apply (unfold diamond_def commute_def square_def)
  apply (rule impI [THEN allI [THEN allI]])
  apply (erule par_beta.induct)
     apply (blast intro!: par_beta_subst)+
  done


subsection ‹Complete developments›

fun
  cd :: "dB => dB"
where
  "cd (Var n) = Var n"
| "cd (Var n 🍋 t) = Var n 🍋 cd t"
| "cd ((s1 🍋 s2) 🍋 t) = cd (s1 🍋 s2) 🍋 cd t"
| "cd (Abs u 🍋 t) = (cd u)[cd t/0]"
| "cd (Abs s) = Abs (cd s)"

lemma par_beta_cd: "s => t ==> t => cd s"
  apply (induct s arbitrary: t rule: cd.induct)
      apply auto
  apply (fast intro!: par_beta_subst)
  done


subsection ‹Confluence (via complete developments)›

lemma diamond_par_beta2: "diamond par_beta"
  unfolding diamond_def commute_def square_def
  by (blast intro: par_beta_cd)

theorem beta_confluent: "confluent beta"
  by (rule diamond_par_beta2 diamond_to_confluence
    par_beta_subset_beta beta_subset_par_beta)+

end