Theory Compactification_DiningPhilosophers

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Application : May Philosophers dine ? ›

(*<*)
theory Compactification_DiningPhilosophers
  imports Compactification_Synchronization_Product "HOL-CSPM.DiningPhilosophers"
begin

unbundle option_type_syntax
  (*>*)



section ‹Preliminaries›

subsection ‹Preliminary lemmas for proof automation›

lemma Suc_mod: ‹n > 1 ⟹ i ≠ Suc i mod n›
  by (metis One_nat_def mod_Suc mod_if mod_mod_trivial n_not_Suc_n)

lemmas suc_mods = Suc_mod Suc_mod[symmetric]

lemma l_suc: ‹n > 1 ⟹ ¬ n ≤ Suc 0›
  by simp 

lemma minus_suc: ‹n > 0 ⟹ n - Suc 0 ≠ n›
  by linarith

declare Un_insert_right[simp del] Un_insert_left[simp del] 

(*declare Mprefix_Un_distrib[simp]  is there an issue declaring this lemma simp ? *)


section ‹The dining processes definition›

context DiningPhilosophers begin

lemma RPHIL_restriction_fix_def:
  ‹RPHIL i = (υ X. picks i i → picks i ((i - 1) mod N) →
                   putsdown i ((i - 1) mod N) → putsdown i i → X)›
  by (simp add: RPHIL_def restriction_fix_is_fix)

lemma LPHIL0_restriction_fix_def:
  ‹LPHIL0 = (υ X. picks 0 (N - 1) → picks 0 0 →
                  putsdown 0 0 → putsdown 0 (N - 1) → X)›
  by (simp add: LPHIL0_def restriction_fix_is_fix)

lemma FORK_restriction_fix_def:
  ‹FORK i = (υ X. (picks i i → putsdown i i → X) □
                  (picks ((i + 1) mod N) i → putsdown ((i + 1) mod N) i → X))›
  by (simp add: FORK_def restriction_fix_is_fix)



subsection ‹Unfolding rules›

lemmas  RPHIL_rec = cont_process_rec[OF  RPHIL_def[THEN meta_eq_to_obj_eq], simplified]
  and LPHIL0_rec = cont_process_rec[OF LPHIL0_def[THEN meta_eq_to_obj_eq], simplified]
  and   FORK_rec = cont_process_rec[OF   FORK_def[THEN meta_eq_to_obj_eq], simplified]



section ‹Translation into normal form›

lemma N_pos[simp]: ‹N > 0›
  using N_g1 neq0_conv by blast

lemmas N_pos_simps[simp] = suc_mods[OF N_g1] l_suc[OF N_g1] minus_suc[OF N_pos]



subsection ‹\<^const>‹FORK›, \<^const>‹LPHIL0› and \<^const>‹RPHIL› are normalizable›

text ‹Definition of one ∗‹fork› and one ∗‹philosopher› automata›

type_synonym id⇩f⇩o⇩r⇩k = nat
type_synonym σ⇩f⇩o⇩r⇩k  = nat
type_synonym id⇩p⇩h⇩i⇩l = nat
type_synonym σ⇩p⇩h⇩i⇩l  = nat



definition   fork_A :: ‹id⇩f⇩o⇩r⇩k ⇒ (σ⇩f⇩o⇩r⇩k, dining_event, unit) A⇩d› (‹A⇩f›)
  where ‹A⇩f i ≡ recursive_constructor_A⇩d
                [((0, picks i i),    ⌊1⌋), ((0, picks ((i + 1) mod N) i),    ⌊2⌋),
                 ((1, putsdown i i), ⌊0⌋), ((2, putsdown ((i + 1) mod N) i), ⌊0⌋)] (λσ. ◇)›


definition  rphil_A :: ‹id⇩p⇩h⇩i⇩l ⇒ (σ⇩p⇩h⇩i⇩l, dining_event, unit) A⇩d› (‹A⇩r⇩p›)
  where ‹A⇩r⇩p i ≡ recursive_constructor_A⇩d
                 [((0, picks i i),                ⌊1⌋), ((1, picks i ((i-1) mod N)), ⌊2⌋),
                  ((2, putsdown i ((i-1) mod N)), ⌊3⌋), ((3, putsdown i i),          ⌊0⌋)] (λσ. ◇)›


definition lphil0_A :: ‹(σ⇩p⇩h⇩i⇩l, dining_event, unit) A⇩d› (‹A⇩l⇩p›)
  where ‹A⇩l⇩p ≡ recursive_constructor_A⇩d
               [((0, picks 0 (N - 1)), ⌊1⌋), ((1, picks 0 0),          ⌊2⌋),
                ((2, putsdown 0 0),    ⌊3⌋), ((3, putsdown 0 (N - 1)), ⌊0⌋)] (λσ. ◇)›



text ‹Definition and first properties of associated normal processes›

definition fork_P_d :: ‹id⇩f⇩o⇩r⇩k ⇒ σ⇩f⇩o⇩r⇩k ⇒ dining_event process›  where ‹fork_P_d  i ≡ P⟪A⇩f i⟫⇩d›
definition rphil_P_d :: ‹id⇩p⇩h⇩i⇩l ⇒ σ⇩p⇩h⇩i⇩l ⇒ dining_event process› where ‹rphil_P_d i ≡ P⟪A⇩r⇩p i⟫⇩d›
definition lphil0_P_d :: ‹σ⇩p⇩h⇩i⇩l ⇒ dining_event process›         where ‹lphil0_P_d  ≡ P⟪A⇩l⇩p⟫⇩d›


lemmas   fork_P_d_rec = P_d_rec[of ‹A⇩f _›,  folded fork_P_d_def]
  and  rphil_P_d_rec = P_d_rec[of ‹A⇩r⇩p _›, folded rphil_P_d_def]
  and lphil0_P_d_rec = P_d_rec[of ‹A⇩l⇩p›,   folded lphil0_P_d_def]




schematic_goal   fork_ε: ‹ε (A⇩f i) σ = ?S›
  and  rphil_ε: ‹ε (A⇩r⇩p i) σ = ?T›
  and lphil0_ε: ‹ε A⇩l⇩p σ = ?U› 
  unfolding fork_A_def rphil_A_def lphil0_A_def by (all ε_det_calc)

schematic_goal   fork_τ: ‹τ (A⇩f i) σ = ?S›
  and  rphil_τ: ‹τ (A⇩r⇩p i) σ = ?T›
  and lphil0_τ: ‹τ A⇩l⇩p σ = ?U›
  unfolding fork_A_def rphil_A_def lphil0_A_def by (all τ_det_calc)


corollary   ev_id⇩f⇩o⇩r⇩kx: ‹e ∈ ε (A⇩f i) σ ⟹ fork e = i› 
  and  rphil_phil: ‹e ∈ ε (A⇩r⇩p i) σ ⟹ phil e = i›
  and lphil0_phil: ‹e ∈ ε A⇩l⇩p σ     ⟹ phil e = 0›
  by (auto simp add: fork_ε rphil_ε lphil0_ε split: if_split_asm)

corollary ev_id⇩p⇩h⇩i⇩lx: ‹i < n ⟹ σ ∈ ε ((A⇩l⇩p # map A⇩r⇩p [1..< n]) ! i) s ⟹ phil σ = i›
  by (cases ‹i = 0›) (simp_all add: lphil0_phil rphil_phil) 


lemma indep_forks: ‹i ≠ j ⟹ ε (A⇩f i) σ ∩ ε (A⇩f j) σ' = {}›
  and indep_phils: ‹i ≠ 0 ⟹ ε A⇩l⇩p σ ∩ ε (A⇩r⇩p i) σ' = {}›
  ‹i ≠ j ⟹ ε (A⇩r⇩p i) σ ∩ ε (A⇩r⇩p j) σ' = {}›
  using ev_id⇩f⇩o⇩r⇩kx lphil0_phil rphil_phil by (blast, simp, fastforce, blast)



text ‹Equalities between \<^const>‹FORK›, \<^const>‹RPHIL›, \<^const>‹LPHIL0›
      and respectively \<^const>‹fork_P_d›, \<^const>‹rphil_P_d›, \<^const>‹lphil0_P_d››

lemma FORK_is_fork_P_d: ‹FORK i = fork_P_d i 0›
proof (unfold fork_P_d_def)
  have ‹(0 :: nat) < 2› by simp
  thus ‹FORK i = P⟪A⇩f i⟫⇩d 0›
  proof (induct rule: P_d_induct_iterated)
    show ‹FORK i = X 0 ⟹ FORK i = (P_d_step (ε (A⇩f i)) (τ (A⇩f i)) ^^ 2) X 0› for X
      by (subst FORK_rec)
        (auto simp add: Mprefix_Det_Mprefix write0_def numeral_eq_Suc
          fork_ε fork_τ Un_commute intro!: mono_Mprefix_eq)
  qed simp_all
qed


lemma RPHIL_is_rphil_P_d: ‹RPHIL i = rphil_P_d i 0›
proof (unfold rphil_P_d_def)
  have ‹(0 :: nat) < 4› by simp
  thus ‹RPHIL i = P⟪A⇩r⇩p i⟫⇩d 0›
  proof (induct rule: P_d_induct_iterated)
    show ‹RPHIL i = X 0 ⟹ RPHIL i = (P_d_step (ε (A⇩r⇩p i)) (τ (A⇩r⇩p i)) ^^ 4) X 0› for X
      by (subst RPHIL_rec)
        (auto simp add: write0_def numeral_eq_Suc rphil_ε rphil_τ intro!: mono_Mprefix_eq)
  qed simp_all
qed


lemma LPHIL0_is_lphil0_P_d: ‹LPHIL0 = lphil0_P_d 0›
proof (unfold lphil0_P_d_def)
  have ‹(0 :: nat) < 4› by simp
  thus ‹LPHIL0 = P⟪A⇩l⇩p⟫⇩d 0›
  proof (induct rule: P_d_induct_iterated)
    show ‹LPHIL0 = X 0 ⟹ LPHIL0 = (P_d_step (ε A⇩l⇩p) (τ A⇩l⇩p) ^^ 4) X 0› for X
      by (subst LPHIL0_rec)
        (auto simp add: write0_def numeral_eq_Suc lphil0_ε lphil0_τ intro!: mono_Mprefix_eq)
  qed simp_all
qed



subsection ‹\<^const>‹FORKS› is normalizable›

text ‹Definition of the all-forks automaton›

type_synonym σ⇩f⇩o⇩r⇩k⇩s = ‹nat list›


definition forks_A :: ‹(σ⇩f⇩o⇩r⇩k⇩s, dining_event, unit) A⇩d› (‹A⇩F›) where ‹A⇩F ≡ ⟪⇩d⨂⟦{}⟧ map A⇩f [0..<N]⟫›



text ‹Definition and first properties of the associated normal process›

definition forks_P_d:: ‹σ⇩f⇩o⇩r⇩k⇩s ⇒ dining_event process› where ‹forks_P_d ≡ P⟪A⇩F⟫⇩d›


lemma forks_ε: ‹length fs = N ⟹ ε A⇩F fs = (⋃i<N. ε (A⇩f i) (fs ! i))›
  unfolding forks_A_def using N_pos by (subst ε_iterated_combine⇩d_Sync_general_form) force+ 



text ‹Equality between \<^const>‹FORKS› and \<^const>‹forks_P_d››

lemma NFORKS_is_forks_P_d: ‹FORKS = forks_P_d (replicate N 0)›
  unfolding forks_P_d_def forks_A_def FORKS_def
  apply (subst P_d_compactification_Sync_upt_version)
  by (simp_all add: FORK_is_fork_P_d[unfolded fork_P_d_def] indep_forks indep_enabl_def)



subsection ‹\<^const>‹PHILS› is normalizable›

text ‹Definition of the all-philosophers automaton›

type_synonym σ⇩p⇩h⇩i⇩l⇩s = ‹nat list›


definition phils_A :: ‹(σ⇩p⇩h⇩i⇩l⇩s, dining_event, unit) A⇩d› (‹A⇩P›) where ‹A⇩P ≡ ⟪⇩d⨂⟦{}⟧ A⇩l⇩p # map A⇩r⇩p [1..< N]⟫›

lemma phils_A_def_bis: ‹A⇩P = ⟪⇩d⨂⟦{}⟧ map (λi. if i = 0 then A⇩l⇩p else A⇩r⇩p i) [0..<N]⟫›
  unfolding phils_A_def apply (subst (2) upt_rec, simp)
  apply (subgoal_tac ‹map (λi. if i = 0 then A⇩l⇩p else A⇩r⇩p i) [Suc 0..<N] = map A⇩r⇩p [Suc 0..<N]›)
  by (presburger, subst list_eq_iff_nth_eq, simp)



text ‹Definition and first properties of the associated normal process›

definition phils_P_d:: ‹σ⇩p⇩h⇩i⇩l⇩s ⇒ dining_event process› where ‹phils_P_d ≡ P⟪A⇩P⟫⇩d›


lemma phils_ε: ‹length ps = N ⟹ ε A⇩P ps = ε A⇩l⇩p (ps ! 0) ∪ (⋃i∈{1..<N}. ε (A⇩r⇩p i) (ps ! i))›
  unfolding phils_A_def_bis using N_pos
  by (subst ε_iterated_combine⇩d_Sync_general_form, (auto split: if_splits)+)



text ‹Equality between \<^const>‹PHILS› and \<^const>‹phils_P_d››

lemma NPHILS_is_phils_P_d: ‹PHILS = phils_P_d (replicate N 0)›
  unfolding phils_P_d_def phils_A_def_bis PHILS_def
  apply (subst P_d_compactification_Sync_upt_version[symmetric])
    apply (simp_all add: indep_enabl_def indep_phils(1,2) inf_sup_aci(1))
  apply (subgoal_tac ‹{0..<N} = insert 0 {1..<N}›)
   apply (simp add: LPHIL0_is_lphil0_P_d lphil0_P_d_def)
  by (rule arg_cong[OF image_mset_cong]) (auto simp add: RPHIL_is_rphil_P_d rphil_P_d_def)



subsection ‹The complete process \<^const>‹DINING› is normalizable›

text ‹Definition of the dining automaton›

definition dining_A :: ‹(σ⇩p⇩h⇩i⇩l⇩s × σ⇩f⇩o⇩r⇩k⇩s, dining_event, unit) A⇩d› (‹A⇩D›) where ‹A⇩D ≡ ⟪A⇩P ⇩d⊗⟦UNIV⟧⇩P⇩a⇩i⇩r A⇩F⟫›



text ‹Definition and first properties of the associated normal process›

definition dining_P_d:: ‹σ⇩p⇩h⇩i⇩l⇩s × σ⇩f⇩o⇩r⇩k⇩s ⇒ dining_event process› where ‹dining_P_d ≡ P⟪A⇩D⟫⇩d›

lemma dining_ε:
  ‹length ps = N ⟹ length fs = N ⟹
   ε A⇩D (ps, fs) = (ε A⇩l⇩p (ps ! 0) ∪ (⋃i∈{1..<N}. ε (A⇩r⇩p i) (ps ! i))) ∩ (⋃i<N. ε (A⇩f i) (fs ! i))›
  by (simp add: dining_A_def ε_combine⇩P⇩a⇩i⇩r_Sync combine_Sync_ε_def forks_ε phils_ε)


text ‹Equality between \<^const>‹DINING› and \<^const>‹dining_P_d››

lemma DINING_is_dining_P_d: ‹DINING = dining_P_d (replicate N 0, replicate N 0)›
  unfolding dining_P_d_def dining_A_def
  apply (subst P_d_combine⇩P⇩a⇩i⇩r_Sync[symmetric])
   apply (simp add: indep_enabl_def)
  by (simp add: DINING_def NFORKS_is_forks_P_d NPHILS_is_phils_P_d Sync_commute forks_P_d_def phils_P_d_def)



section ‹And finally: Philosophers may dine ! Always !›

method ε_sets_simp uses opt = (simp_all split: if_split_asm)?,
  simp_all add: fork_ε lphil0_ε rphil_ε opt split: if_splits
method A_defs_simp uses opt = (simp_all split: if_split_asm)?,
  simp_all add: fork_A_def lphil0_A_def rphil_A_def opt split: if_splits



subsection ‹Construction of an invariant for the dining automaton›

definition ‹inv_dining ps fs ≡
            length fs = N ∧ length ps = N
          ∧ (∀i < N. fs ! i = 0 ∨ fs ! i = 1 ∨ fs ! i = 2) 
          ∧ (∀i < N. ps ! i = 0 ∨ ps ! i = 1 ∨ ps ! i = 2 ∨ ps ! i = 3)
          ∧ (∀i. Suc i < N ⟶ ((fs ! Suc i = 1) ⟷ ps ! Suc i ≠ 0)) ∧ (fs ! (N - 1) = 2 ⟷ ps ! 0 ≠ 0)
          ∧ (∀i < N - 1.           fs ! i = 2    ⟷ ps ! Suc i = 2)  ∧    (fs ! 0  = 1   ⟷ ps ! 0 = 2)› 


lemma show_inv_dining: 
  ‹length fs = N ∧ length ps = N ⟹
   (∀i < N. fs ! i = 0 ∨ fs ! i = 1 ∨ fs ! i = 2) ⟹
   (∀i < N. ps ! i = 0 ∨ ps ! i = 1 ∨ ps ! i = 2 ∨ ps ! i = 3) ⟹
   (∀i. Suc i < N ⟶ (fs ! Suc i = 1 ⟷ ps ! Suc i ≠ 0)) ⟹ (fs ! (N - 1) = 2 ⟷ ps ! 0 ≠ 0) ⟹
   (∀i < N - 1. fs ! i = 2 ⟷ ps ! Suc i = 2) ⟹ (fs ! 0  = 1 ⟷ ps ! 0 = 2) ⟹ 
   inv_dining ps fs›
  by (simp add: inv_dining_def)



lemma inv_DINING: ‹s ∈ ℛ⇩d A⇩D (replicate N 0, replicate N 0) ⟹ inv_dining (fst s) (snd s)›
proof(induct rule: ℛ⇩d.induct)
  case init show ?case by (simp add: inv_dining_def)
next
  case (step t u e)
  obtain t_ps t_fs u_ps u_fs where t_pair: ‹t = (t_ps, t_fs)› and u_pair: ‹u = (u_ps, u_fs)› by fastforce
  hence inv_hyp: ‹length t_fs = N› ‹length t_ps = N› 
    ‹i < N ⟹ t_fs ! i = 0 ∨ t_fs ! i = 1 ∨ t_fs ! i = 2›
    ‹i < N ⟹ t_ps ! i = 0 ∨ t_ps ! i = 1 ∨ t_ps ! i = 2 ∨ t_ps ! i = 3›
    ‹Suc i < N ⟹ (t_fs ! Suc i = 1) = (t_ps ! Suc i ≠ 0)›
    ‹(t_fs ! (N - 1) = 2) = (t_ps ! 0 ≠ 0)›
    ‹i < N - 1 ⟹ (t_fs ! i = 2) = (t_ps ! Suc i = 2)›
    ‹(t_fs ! 0 = 1) = (t_ps ! 0 = 2)› for i
    using step.hyps(2)[simplified inv_dining_def] by simp_all

  have u_in_ℛ⇩d_prem: ‹(u_ps, u_fs) ∈ ℛ⇩d A⇩P (replicate N 0) × ℛ⇩d A⇩F (replicate N 0)›
    using ℛ⇩d.step[OF step.hyps(1, 3), simplified dining_A_def]
    by (simp add: u_pair[symmetric], rule set_mp[OF ℛ⇩d_combine⇩d⇩P⇩a⇩i⇩r_Sync_subset])
  note u_in_ℛ⇩d = u_in_ℛ⇩d_prem[simplified mem_Times_iff, THEN conjunct1, simplified]
    u_in_ℛ⇩d_prem[simplified mem_Times_iff, THEN conjunct2, simplified]

  have same_length_u: ‹length u_ps = N› ‹length u_fs = N› 
    using same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[rotated, OF u_in_ℛ⇩d(1)[unfolded phils_A_def]]
      same_length_ℛ⇩d_iterated_combine⇩d_Sync_description[rotated, OF u_in_ℛ⇩d(2)[unfolded forks_A_def]]
    by simp+

  have u_is: ‹⌊u_ps⌋ = τ A⇩P t_ps e› ‹⌊u_fs⌋ = τ A⇩F t_fs e›
    using step(3)[simplified dining_A_def, simplified combine_Sync_defs]
    by (simp_all add: t_pair u_pair option.case_eq_if map_option_case split: if_splits)

  have e_in: ‹e ∈ ε A⇩l⇩p (t_ps ! 0) ∪ (⋃i∈{1..<N}. ε (A⇩r⇩p i) (t_ps ! i))›
    ‹e ∈ (⋃i<N. ε (A⇩f i) (t_fs ! i))›
    by (subst phils_ε[symmetric], fact inv_hyp(2), simp add: ε_simps, metis u_is(1))
      (subst forks_ε[symmetric], fact inv_hyp(1), simp add: ε_simps, metis u_is(2))

  have u_nth:
    ‹i < N ⟹ u_ps ! i = 
    (if i = 0 then (if e ∈ ε A⇩l⇩p (t_ps ! 0) then ⌈τ A⇩l⇩p (t_ps ! 0) e⌉ else t_ps ! 0)
     else if e ∈ ε (A⇩r⇩p i) (t_ps ! i) then ⌈τ (A⇩r⇩p i) (t_ps ! i) e⌉ else t_ps ! i)› 
    ‹i < N ⟹ u_fs ! i =
     (if e ∈ ε (A⇩f i) (t_fs ! i) then ⌈τ (A⇩f i) (t_fs ! i) e⌉ else t_fs ! i)› for i
    by (insert u_is(1), unfold phils_A_def, subst (asm) τ_iterated_combine⇩d_Sync_general_form,
        simp_all add: inv_hyp(2) split: if_splits)
      (insert u_is(2), unfold forks_A_def, subst (asm) τ_iterated_combine⇩d_Sync_general_form,
        simp_all add: inv_hyp(1) split: if_splits)
  have ‹e ∈ ε A⇩P t_ps› ‹e ∈ ε A⇩F t_fs› using u_is ε_simps by fastforce+
  hence e_equiv: ‹e ∈ ε A⇩l⇩p (t_ps ! 0) ⟷ phil e = 0›
    ‹Suc i < N ⟹ e ∈ ε (A⇩r⇩p (Suc i)) (t_ps ! Suc i) ⟷ phil e = Suc i›
    ‹i < N ⟹ e ∈ ε (A⇩f i) (t_fs ! i) ⟷ fork e = i› for i
      apply (simp_all add: phils_ε[OF inv_hyp(2)] forks_ε[OF inv_hyp(1)])
    using rphil_phil lphil0_phil ev_id⇩f⇩o⇩r⇩kx by auto (metis Suc_le_eq less_irrefl_nat, blast, metis) 

  show ?case
  proof (simp add: u_pair, rule show_inv_dining[rule_format], simp add: same_length_u, goal_cases)
    case (1 i) thus ?case using u_nth(2)[of i] inv_hyp(3) by ε_sets_simp A_defs_simp
  next
    case (2 i) thus ?case using u_nth(1)[of i] inv_hyp(4) by ε_sets_simp A_defs_simp
  next
    case (3 i)
    with u_nth(1)[of ‹Suc i›] u_nth(2)[of ‹Suc i›] show ?case
      using inv_hyp(5)[of i] apply ε_sets_simp apply A_defs_simp
      using e_equiv(3) fork_ε e_equiv(2) rphil_ε by fastforce+
  next
    case 4
    with u_nth(1)[of 0] u_nth(2) show ?case using inv_hyp(6) N_g1 apply ε_sets_simp apply A_defs_simp
         apply (metis N_pos One_nat_def Suc_pred fork_ε dining_event.sel(3) 
          dining_event.simps(3) inv_hyp(3) lessI singletonD e_equiv(3))
      using lphil0_ε e_equiv(1) by force+
  next
    case (5 i)
    hence ‹Suc i < N› by linarith
    with u_nth(1)[of ‹Suc i›] u_nth(2)[of i] "5" show ?case 
      using inv_hyp(7)[of i] apply ε_sets_simp apply A_defs_simp
          apply (metis Suc_lessD fork_ε dining_event.sel(3) dining_event.simps(3) singletonD e_equiv(3))
         apply (metis One_nat_def Suc_lessD bot_nat_0.not_eq_extremum inv_hyp(3))
      using rphil_ε e_equiv(2) by force+
  next
    case 6
    with u_nth(1)[of 0] u_nth(2)[of 0] show ?case
      using N_g1 inv_hyp(8) apply (simp split: if_split_asm) apply ε_sets_simp apply A_defs_simp
      using lphil0_ε e_equiv(1) fork_ε e_equiv(3) by force+
  qed
qed


subsection ‹The invariant \<^const>‹inv_dining› implies that \<^const>‹DINING› is \<^const>‹deadlock_free››

method nonempty_Int_by_common_element for x = rule_tac ex_in_conv[THEN iffD1, OF exI, OF IntI, of x]

lemma inv_implies_DF: ‹ε A⇩D (ps, fs) ≠ {}› if hyp_inv: ‹inv_dining ps fs›
  apply (subst dining_ε)
    apply (insert hyp_inv, unfold inv_dining_def, simp_all add: lphil0_ε)
proof(elim conjE, intro conjI impI, goal_cases)
  case 1
  with 1(3)[rule_format, of 0, OF N_pos] show ?case
  proof(elim disjE, goal_cases)
    case 11:1 (* fs ! 0 = 0 *)
    thus ?case
      using 1(3)[rule_format, of 1, OF N_g1] apply(elim disjE) 
        (* fs ! 1 = 0 *)
        apply (subgoal_tac ‹ps ! 1 = 0›, nonempty_Int_by_common_element ‹picks 1 1›)
      using N_g1 apply ε_sets_simp[3]
          apply (metis atLeastLessThan_iff le_refl less_irrefl_nat, blast, 
          metis less_zeroE linorder_neqE_nat)
        (* fs ! 1 = 1 *)
       apply (cases ‹ps ! 1 = 1›, nonempty_Int_by_common_element ‹picks 1 0›) (* ps ! 1 = 1 *)
      using N_g1 apply ε_sets_simp[2]
         apply (metis One_nat_def atLeastLessThan_iff diff_self_eq_0 le_refl less_numeral_extra(1) mod_mod_trivial mod_self,
          metis N_pos lessThan_iff mod_less) 
       apply (nonempty_Int_by_common_element ‹putsdown 1 1›) (* ps ! 1 = 3 *)
      using N_g1 apply ε_sets_simp[2]
        apply (metis atLeastLessThan_iff le_refl less_numeral_extra(3) zero_less_diff,
          metis gr0_conv_Suc lessThan_iff)
        (* fs ! 1 = 2 *)
      apply (cases ‹N = 2›, simp)
      apply (subgoal_tac ‹ps ! 2 = 2›, nonempty_Int_by_common_element ‹putsdown 2 1›)
      using N_g1 apply ε_sets_simp
      by (metis One_nat_def Suc_lessI atLeastLessThan_iff diff_Suc_1 le_SucI le_numeral_extra(4)
          mod_less n_not_Suc_n numeral_2_eq_2 zero_less_Suc,
          metis One_nat_def Suc_1 Suc_lessI gr0_conv_Suc lessThan_iff
          less_diff_conv mod_less plus_1_eq_Suc,
          metis One_nat_def Suc_1)
  next
    case 12:2 (* fs ! 0 = 1 *)
    thus ?case by linarith
  next
    case 13:3 (* fs ! 0 = 2 *)
    thus ?case 
      apply (subgoal_tac ‹ps ! 1 = 2›, nonempty_Int_by_common_element ‹putsdown 1 0›)
      using N_g1 apply ε_sets_simp
       apply (metis atLeastLessThan_iff diff_self_eq_0 dvd_1_left le_Suc_eq less_2_cases_iff mod_0 odd_one)
      by (metis "13"(10) N_pos lessThan_iff mod_less n_not_Suc_n numeral_2_eq_2 zero_less_Suc)
  qed
next
  case 2
  from "2"(3, 7, 8, 10) N_g1 have f1: ‹fs ! 0 ≠ 0 ⟹ ps ! 1 = 2 ∧ fs ! 0 = 2› by auto
  from 2 show ?case
    apply (cases ‹fs ! 0 = 0›)
     apply (nonempty_Int_by_common_element ‹picks 0 0›)
    using N_g1 apply ε_sets_simp[2]
    using N_pos apply blast
    apply (nonempty_Int_by_common_element ‹putsdown 1 0›)
     apply ε_sets_simp
     apply (metis N_g1 One_nat_def atLeastLessThan_iff bot_nat_0.not_eq_extremum
        cancel_comm_monoid_add_class.diff_cancel dual_order.refl local.f1 mod_0)
    by (metis N_g1 N_pos One_nat_def lessThan_iff less_irrefl_nat mod_less)
next
  case 3 thus ?case by (nonempty_Int_by_common_element ‹putsdown 0 0›)
      (ε_sets_simp, metis N_pos lessThan_iff zero_less_Suc)
next
  case 4 thus ?case by (nonempty_Int_by_common_element ‹putsdown 0 (N - 1)›)
      (ε_sets_simp, metis N_pos One_nat_def Suc_1 Suc_diff_1 diff_less
        gr0_conv_Suc lessThan_iff mod_self n_not_Suc_n)
next
  case 5 thus ?case using 5(4)[rule_format, of 0] by simp
qed 



subsection ‹Conclusion›

corollary deadlock_free_DINING: ‹deadlock_free DINING›
  unfolding DINING_is_dining_P_d dining_P_d_def
  apply (subst deadlock_free_P_d_iff)
  using inv_DINING inv_implies_DF by force






section ‹Alternative version with only right-handed philosophers
         (in order to show that it's not \<^const>‹deadlock_free›)›

subsection ‹Setup›

definition ‹RPHILS ≡ ❙|❙|❙| P ∈# mset (map RPHIL [0..< N]). P›

corollary ‹N = 3 ⟹ RPHILS = (RPHIL 0 ||| RPHIL 1 ||| RPHIL 2)›
  unfolding RPHILS_def by (simp add: eval_nat_numeral upt_rec Sync_assoc)

definition RDINING :: ‹dining_event process›
  where ‹RDINING = (FORKS || RPHILS)›


subsection ‹Normalization›

definition rphils_A :: ‹(σ⇩p⇩h⇩i⇩l⇩s, dining_event, unit) A⇩d› (‹A⇩R⇩P›) where ‹A⇩R⇩P ≡ ⟪⇩d⨂⟦{}⟧ map A⇩r⇩p [0..< N]⟫›

definition rphils_P_d:: ‹σ⇩p⇩h⇩i⇩l⇩s ⇒ dining_event process› where ‹rphils_P_d ≡ P⟪A⇩R⇩P⟫⇩d›

definition rdining_A :: ‹(σ⇩p⇩h⇩i⇩l⇩s × σ⇩f⇩o⇩r⇩k⇩s, dining_event, unit) A⇩d› (‹A⇩R⇩D›) where ‹A⇩R⇩D ≡ ⟪A⇩R⇩P ⇩d⊗⟦UNIV⟧⇩P⇩a⇩i⇩r A⇩F⟫›

definition rdining_P_d:: ‹σ⇩p⇩h⇩i⇩l⇩s × σ⇩f⇩o⇩r⇩k⇩s ⇒ dining_event process› where ‹rdining_P_d ≡ P⟪A⇩R⇩D⟫⇩d›


subsection ‹Correspondance between our normalized processes and the previous definitions›

lemma rphils_ε: ‹length ps = N ⟹ ε A⇩R⇩P ps = (⋃i∈{0..<N}. ε (A⇩r⇩p i) (ps ! i))›
  unfolding rphils_A_def using N_pos
  by (subst ε_iterated_combine⇩d_Sync_general_form, (auto split: if_splits)+)

lemma NRPHILS_is_rphils_P_d: ‹RPHILS = rphils_P_d (replicate N 0)›
  unfolding rphils_P_d_def rphils_A_def RPHILS_def
  apply (subst P_d_compactification_Sync_upt_version)
  by (simp_all add: RPHIL_is_rphil_P_d[unfolded rphil_P_d_def] indep_phils indep_enabl_def)


lemma rdining_ε:
  ‹length ps = N ⟹ length fs = N ⟹
   ε A⇩R⇩D (ps, fs) = (⋃i∈{0..<N}. ε (A⇩r⇩p i) (ps ! i)) ∩ (⋃i<N. ε (A⇩f i) (fs ! i))›
  by (simp add: rdining_A_def ε_combine⇩P⇩a⇩i⇩r_Sync combine_Sync_ε_def forks_ε rphils_ε)

lemma RDINING_is_rdining_P_d: ‹RDINING = rdining_P_d (replicate N 0, replicate N 0)›
  apply (unfold rdining_P_d_def rdining_A_def)
  apply (subst P_d_combine⇩P⇩a⇩i⇩r_Sync[symmetric])
   apply (simp add: indep_enabl_def)
  by (simp add: NFORKS_is_forks_P_d NRPHILS_is_rphils_P_d RDINING_def Sync_commute forks_P_d_def
      rphils_P_d_def)


subsection ‹Proof that we have a deadlock in the state \<^term>‹(replicate N 1, replicate N 1)››

lemma empty_enabl_replicate1: ‹ε A⇩R⇩D (replicate N 1, replicate N 1) = {}›
  by (subst rdining_ε, auto simp add: rphil_ε fork_ε)

corollary non_dealock_free_rdining: ‹¬ deadlock_free (rdining_P_d (replicate N 1, replicate N 1))›
  unfolding rdining_P_d_def
  by (subst P_d_rec, subst empty_enabl_replicate1, simp add: non_deadlock_free_STOP)


subsection ‹Proof that this state is reachable from our initial state, i.e.
            \<^term>‹(replicate N 1, replicate N 1) ∈ ℛ⇩d A⇩R⇩D (replicate N 0, replicate N 0)››

lemma rdining_τ: ‹length ps = N ⟹ length fs = N ⟹ e ∈ ε A⇩R⇩D (ps, fs) ⟹
                  τ A⇩R⇩D (ps, fs) e = ⌊(⌈τ A⇩R⇩P ps e⌉,  ⌈τ A⇩F fs e⌉)⌋›
  by (auto simp add: rdining_A_def combine⇩P⇩a⇩i⇩r_Sync_defs ε_simps split: if_split_asm)

lemma replicate1_reachable_from_replicate0_prelim:
  ‹n ≤ N ⟹ (replicate n 1 @ replicate (N - n) 0, replicate n 1 @ replicate (N - n) 0) ∈ ℛ⇩d A⇩R⇩D (replicate N 0, replicate N 0)›
proof (induct n, simp add: ℛ⇩d.init)
  case (Suc n)
  have ‹n ≤ N› by (simp add: Suc.prems Suc_leD)
  define σs σt where a1: ‹σs ≡ replicate    n    (1::nat) @ replicate (N -   n)   0›
    and a2: ‹σt ≡ replicate (Suc n) (1::nat) @ replicate (N - Suc n) 0›
  have ‹length σs = N› ‹length σt = N› ‹length σs = length σt›
    by (simp_all add: ‹n ≤ N› a1 a2 Suc.prems)
  have f1: ‹(σs, σs) ∈ ℛ⇩d A⇩R⇩D (replicate N 0, replicate N 0)›
    using Suc.hyps(1) a1 Suc.prems Suc_leD by presburger
  have f2: ‹picks n n ∈ ε A⇩R⇩P σs› ‹picks n n ∈ ε A⇩F σs› ‹picks n n ∈ ε A⇩R⇩D (σs, σs)›
    by (subst rphils_ε forks_ε, insert Suc.prems Suc_le_eq Suc_leD a1,
        auto simp add: rdining_ε rphil_ε fork_ε nth_append)+

  have ‹a ∈ ε (A⇩r⇩p i) (σs ! i) ⟹ i < N ⟹ a ∈ ε (A⇩r⇩p j) (σs ! j) ⟹ j < N ⟹ j = i› for i j a
    by (metis rphil_phil)
  hence * : ‹a ∈ ε (A⇩r⇩p i) (σs ! i) ⟹ i < N ⟹
             (THE j. j < N ∧ a ∈ ε (map A⇩r⇩p [0..<N] ! j) (σs ! j)) = i› for i a by auto

  have ‹a ∈ ε (A⇩f i) (σs ! i) ⟹ i < N ⟹ a ∈ ε (A⇩f j) (σs ! j) ⟹ j < N ⟹ j = i› for i j a
    by (metis ev_id⇩f⇩o⇩r⇩kx)
  hence ** : ‹a ∈ ε (A⇩f i) (σs ! i) ⟹ i < N ⟹
              (THE j. j < N ∧ a ∈ ε (map A⇩f [0..<N] ! j) (σs ! j)) = i› for i a by auto

  have f3: ‹σt = ⌈τ A⇩R⇩P σs (picks n n)⌉›
    apply (unfold rphils_A_def, subst τ_iterated_combine⇩d_Sync_general_form_when_indep)
    subgoal by (simp add: ‹length σs = N›)
    subgoal by (simp add: indep_enablI indep_phils(2))
    using N_pos apply (auto simp del: N_pos)
    subgoal by (metis N_g1 N_pos lessThan_iff rphil_phil zero_neq_one)
    subgoal
      apply (subst "*", simp_all)
      apply (auto simp add: ‹length σs = length σt› intro!: nth_equalityI)
      apply (auto simp add: a1 a2 nth_Cons nth_append nth_list_update dest: rphil_phil split: if_split_asm nat.split)
      by (simp_all add: rphil_A_def)
    using rphils_ε ‹length σs = N› atLeast0LessThan f2(1) by force

  have f4: ‹σt = ⌈τ A⇩F σs (picks n n)⌉›
    apply (unfold forks_A_def, subst τ_iterated_combine⇩d_Sync_general_form_when_indep)
    subgoal by (simp add: ‹length σs = N›)
    subgoal by (simp add: indep_enabl_def indep_forks)
    using N_pos apply (auto simp del: N_pos)
    subgoal by (metis N_g1 N_pos ev_id⇩f⇩o⇩r⇩kx lessThan_iff zero_neq_one)
    subgoal
      apply (subst "**", simp_all)
      apply (auto simp add: ‹length σs = length σt› intro!: nth_equalityI)
      apply (auto simp add: a1 a2 nth_Cons nth_append nth_list_update dest: ev_id⇩f⇩o⇩r⇩kx split: if_split_asm nat.split)
      using N_pos_simps(1) Suc_lessI by (auto simp add: fork_A_def intro: Suc_lessI)
    using forks_ε ‹length σs = N› atLeast0LessThan f2(2) by force
  show ‹(σt, σt) ∈ ℛ⇩d A⇩R⇩D (replicate N 0, replicate N 0)›
    apply (rule ℛ⇩d.step[OF f1], subst rdining_τ)
    using Suc.prems a1 apply fastforce
     apply (rule f2)
    using f3 f4 by blast
qed


corollary replicate1_reachable_from_replicate0: ‹(replicate N 1, replicate N 1) ∈ ℛ⇩d A⇩R⇩D (replicate N 0, replicate N 0)›
  by (simp add: replicate1_reachable_from_replicate0_prelim[of N, simplified])


theorem not_deadlock_free_RDINING: ‹¬ deadlock_free RDINING›
  apply (subst RDINING_is_rdining_P_d[unfolded rdining_P_d_def])
  apply (subst deadlock_free_P_d_iff)
  using empty_enabl_replicate1 replicate1_reachable_from_replicate0 by blast



end


(*<*)
end
  (*>*)