Theory DiningPhilosophers

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : Example on Structural Parameterisation: Dining Philosophers
 *
 * Copyright (c) 2020 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)

section‹ Generalized Dining Philosophers ›

theory     DiningPhilosophers
 imports   "Process_norm"
begin 

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

lemma numeral_4_eq_4:"4 = Suc (Suc (Suc (Suc 0)))" 
  by simp

lemma numeral_5_eq_5:"5 = Suc (Suc (Suc (Suc (Suc 0))))" 
  by simp

subsection‹The dining processes definition›

locale DiningPhilosophers =
  
  fixes N::nat
  assumes N_g1[simp] : "N > 1"  

begin

datatype dining_event  = picks (phil:nat) (fork:nat) 
                       | putsdown (phil:nat) (fork:nat)

definition RPHIL::  "nat ⇒ dining_event process"
 where "RPHIL i = (μ X. (picks i i → (picks i (i-1) → (putsdown i (i-1) → (putsdown i i → X)))))"

definition LPHIL0::  "dining_event process"
  where "LPHIL0 = (μ X. (picks 0 (N-1) → (picks 0 0 → (putsdown 0 0 → (putsdown 0 (N-1) → X)))))"

definition FORK  :: "nat ⇒ dining_event process"
  where "FORK i = (μ X.   (picks i i → (putsdown i i → X)) 
                        □ (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → X)))"


abbreviation "foldPHILs n ≡ fold (λ i P. P ||| RPHIL i) [1..< n] (LPHIL0)"
abbreviation "foldFORKs n ≡ fold (λ i P. P ||| FORK i) [1..< n] (FORK 0)"


abbreviation "PHILs ≡ foldPHILs N"
abbreviation "FORKs ≡ foldFORKs N"


corollary FORKs_def2: "FORKs = fold (λ i P. P ||| FORK i) [0..< N] SKIP"
  using N_g1 by (subst (2) upt_rec, auto) (metis (no_types, lifting) Inter_commute Inter_SKIP) 

corollary "N = 3 ⟹ PHILs = (LPHIL0 ||| RPHIL 1 ||| RPHIL 2)"
  by (subst upt_rec, auto simp add:numeral_2_eq_2)+


definition DINING :: "dining_event process"
  where "DINING = (FORKs || PHILs)"

subsubsection ‹Unfolding rules›

lemma RPHIL_rec: 
  "RPHIL i = (picks i i → (picks i (i-1) → (putsdown i (i-1) → (putsdown i i  → RPHIL i))))"
  by (simp add:RPHIL_def write0_def, subst fix_eq, simp)

lemma LPHIL0_rec: 
  "LPHIL0 = (picks 0 (N-1) → (picks 0 0 → (putsdown 0 0 → (putsdown 0 (N-1) → LPHIL0))))"
  by (simp add:LPHIL0_def write0_def, subst fix_eq, simp)

lemma FORK_rec: "FORK i = (  (picks i i → (putsdown i i → (FORK i)))
                          □ (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → (FORK i))))"
  by (simp add:FORK_def write0_def, subst fix_eq, simp)

subsection ‹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]

text ‹The one-fork process›

type_synonym idfork = nat

type_synonym σfork = nat


definition fork_transitions:: "idfork ⇒ σfork ⇒ dining_event set" (‹Trf›)
  where "Trf i s = (if s = 0        then {picks i i} ∪ {picks ((i+1) mod N) i}
                    else if s = 1   then {putsdown i i} 
                    else if s = 2   then {putsdown ((i+1) mod N) i}
                    else                 {})"
declare Un_insert_right[simp del] Un_insert_left[simp del]

lemma ev_idforkx[simp]: "e ∈ Trf i s ⟹ fork e = i" 
  by (auto simp add:fork_transitions_def split:if_splits)

definition σfork_update:: "idfork ⇒ σfork ⇒ dining_event ⇒ σfork" (‹Upf›)
  where "Upf i s e = ( if e = (picks i i)                   then 1 
                      else if e = (picks ((i+1) mod N) i)  then 2 
                      else                                      0 )"

definition FORKnorm:: "idfork ⇒ σfork ⇒ dining_event process"
  where "FORKnorm i = Pnorm⟦Trf i ,Upf i⟧"

lemma FORKnorm_rec:  "FORKnorm i = (λ s. □ e ∈ (Trf i s) → FORKnorm i (Upf i s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trf i s) (λe. X (Upf i s e)))"] FORKnorm_def by simp

lemma FORK_refines_FORKnorm: "FORKnorm i 0 ⊑FD FORK i"
proof(unfold FORKnorm_def, 
      induct rule:fix_ind_k_skip[where k=2 and f="Λ x.(λs. Mprefix (Trf i s) (λe. x (Upf i s e)))"])
  case lower_bound
  then show ?case by simp
next
  case admissibility
  then show ?case by (simp add: cont_fun monofunI)
next
  case base_k_steps
  then show ?case (is "∀j<2. (iterate j⋅?f⋅⊥) 0 ⊑FD FORK i")
  proof -
    have less_2:"⋀j. (j::nat) < 2 = (j = 0 ∨ j = 1)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑FD FORK i" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑FD FORK i" 
      by (subst FORK_rec) 
         (simp add: write0_def fork_transitions_def Mprefix_Un_distrib)
    ultimately show ?thesis by simp
  qed
next
  case (step x)
  then show ?case (is "(iterate 2⋅?f⋅x) 0 ⊑FD FORK i")
    by (subst FORK_rec) 
       (simp add: write0_def numeral_2_eq_2 fork_transitions_def σfork_update_def Mprefix_Un_distrib) 
qed



lemma FORKnorm_refines_FORK: "FORK i ⊑FD FORKnorm i 0"
proof(unfold FORK_def, 
      induct rule:fix_ind_k_skip[where k=1])
  show "(1::nat) ≤ 1" by simp
next
  show "adm (λa. a ⊑FD FORKnorm i 0)" by (simp add: monofunI)
next
  case base_k_steps
  show ?case by simp
next
  case (step x)
  then show ?case (is "iterate 1⋅?f⋅x ⊑FD FORKnorm i 0")
    apply (subst FORKnorm_rec) 
    apply (simp add: write0_def fork_transitions_def σfork_update_def Mprefix_Un_distrib)
    by (subst (1 2) FORKnorm_rec) 
       (simp add: fork_transitions_def σfork_update_def Mprefix_Un_distrib) 
qed

lemma FORKnorm_is_FORK: "FORK i = FORKnorm i 0"
  using FORK_refines_FORKnorm FORKnorm_refines_FORK FD_antisym by blast 


text ‹The all-forks process in normal form›

type_synonym σforks = "nat list"

definition forks_transitions:: "nat ⇒ σforks ⇒ dining_event set" (‹TrF›)
  where "TrF n fs = (⋃i<n. Trf i (fs!i))"

lemma forks_transitions_take: "TrF n fs = TrF n (take n fs)"
  by (simp add:forks_transitions_def)

definition σforks_update:: "σforks ⇒ dining_event ⇒ σforks" (‹UpF›)
  where "UpF fs e = (let i=(fork e) in fs[i:=(Upf i (fs!i) e)])"

lemma forks_update_take: "take n (UpF fs e) = UpF (take n fs) e"
  unfolding σforks_update_def
  by (metis nat_less_le nat_neq_iff nth_take order_refl take_update_cancel take_update_swap)

definition FORKsnorm:: "nat ⇒ σforks ⇒ dining_event process"
  where "FORKsnorm n = Pnorm⟦TrF n ,UpF⟧"

lemma FORKsnorm_rec:  "FORKsnorm n = (λ fs. □ e ∈ (TrF n fs) → FORKsnorm n (UpF fs e))"
  using fix_eq[of "Λ X. (λfs. Mprefix (TrF n fs) (λe. X (UpF fs e)))"] FORKsnorm_def by simp

lemma FORKsnorm_0: "FORKsnorm 0 fs = STOP"
  by (subst FORKsnorm_rec, simp add:forks_transitions_def Mprefix_STOP)


lemma FORKsnorm_1_dir1: "length fs > 0 ⟹ FORKsnorm 1 fs ⊑FD (FORKnorm 0 (fs!0))" 
proof(unfold FORKsnorm_def,          
      induct arbitrary:fs rule:fix_ind_k[where k=1  
                                         and f="Λ x. (λfs. Mprefix (TrF 1 fs) (λe. x (UpF fs e)))"])
  case admissibility
  then show ?case by (simp add: cont_fun monofunI) 
next
  case base_k_steps
  then show ?case by simp
next
  case (step X)
  hence "(⋃i<Suc 0. Trf i (fs ! i)) = Trf 0 (fs ! 0)" by auto
  with step show ?case
    apply (subst FORKnorm_rec, simp add:σforks_update_def forks_transitions_def) 
    apply (intro mono_Mprefix_FD, safe)
    by (metis ev_idforkx step.prems list_update_nonempty nth_list_update_eq)
qed


lemma FORKsnorm_1_dir2: "length fs > 0 ⟹ (FORKnorm 0 (fs!0)) ⊑FD FORKsnorm 1 fs" 
proof(unfold FORKnorm_def, 
      induct arbitrary:fs rule:fix_ind_k[where k=1 
                                         and f="Λ x. (λs. Mprefix (Trf 0 s) (λe. x (Upf 0 s e)))"])
  case admissibility
  then show ?case by (simp add: cont_fun monofunI) 
next
  case base_k_steps
  then show ?case by simp
next
  case (step X)
  have "(⋃i<Suc 0. Trf i (fs ! i)) = Trf 0 (fs ! 0)" by auto
  with step show ?case
    apply (subst FORKsnorm_rec, simp add: σforks_update_def forks_transitions_def) 
    apply (intro mono_Mprefix_FD, safe) 
    by (metis ev_idforkx step.prems list_update_nonempty nth_list_update_eq)
qed

lemma FORKsnorm_1: "length fs > 0 ⟹ (FORKnorm 0 (fs!0)) = FORKsnorm 1 fs"
  using FORKsnorm_1_dir1 FORKsnorm_1_dir2 FD_antisym by blast


lemma FORKsnorm_unfold: 
"0 < n ⟹ length fs = Suc n ⟹ 
                              FORKsnorm (Suc n) fs = (FORKsnorm n (butlast fs)|||(FORKnorm n (fs!n)))"
proof(rule FD_antisym)
  show "0 < n ⟹ length fs = Suc n ⟹ 
                              FORKsnorm (Suc n) fs ⊑FD (FORKsnorm n (butlast fs)|||FORKnorm n (fs!n))"
  proof(subst FORKsnorm_def, 
        induct arbitrary:fs 
               rule:fix_ind_k[where k=1 
                              and f="Λ x. (λfs. Mprefix (TrF (Suc n) fs) (λe. x (UpF fs e)))"])
    case admissibility
    then show ?case by (simp add: cont_fun monofunI) 
  next
    case base_k_steps
    then show ?case by simp
  next
    case (step X)
    have indep:"∀s1 s2. TrF n s1 ∩ Trf n s2 = {}" 
      by (auto simp add:forks_transitions_def fork_transitions_def)
    from step show ?case
      apply (auto simp add:indep dnorm_inter FORKsnorm_def FORKnorm_def)
      apply (subst fix_eq, simp add:forks_transitions_def Un_commute lessThan_Suc nth_butlast)
    proof(rule mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      from 1(4) have a:"fork e = n" 
        by (auto simp add:fork_transitions_def split:if_splits)
      show ?case 
        using 1(1)[rule_format, of "(UpF fs e)"] 
        apply (simp add: 1 a butlast_list_update σforks_update_def)
        by (metis 1(4) ev_idforkx lessThan_iff less_not_refl)
    next
      case (2 e m)
      hence a:"e ∉ Trf n (fs ! n)" 
        using ev_idforkx by fastforce
      hence c:"UpF fs e ! n = fs ! n"
        by (metis 2(4) ev_idforkx σforks_update_def nth_list_update_neq)
      have d:"UpF (butlast fs) e = butlast (UpF fs e)"       
        apply(simp add:σforks_update_def)
        by (metis butlast_conv_take σforks_update_def forks_update_take length_list_update)
      from 2 a show ?case 
        using 2(1)[rule_format, of "(UpF fs e)"] c d σforks_update_def by auto
    qed
  qed
next
  have indep:"∀s1 s2. TrF n s1 ∩ Trf n s2 = {}" 
    by (auto simp add: forks_transitions_def fork_transitions_def)
  show "0 < n ⟹ length fs = Suc n ⟹ 
                              (FORKsnorm n (butlast fs)|||FORKnorm n (fs!n)) ⊑FD FORKsnorm (Suc n) fs"
    apply (subst FORKsnorm_def, auto simp add:indep dnorm_inter FORKnorm_def)
  proof(rule fix_ind[where 
        P="λa. 0 < n ⟶ (∀x. length x = Suc n ⟶ a (butlast x, x ! n) ⊑FD FORKsnorm (Suc n) x)", 
        rule_format], simp_all, goal_cases)
    case base:1
    then show ?case by (simp add: cont_fun monofunI) 
  next
    case step:(2 X fs)
    then show ?case
      apply (unfold FORKsnorm_def, subst fix_eq, simp add:forks_transitions_def 
                                                          Un_commute lessThan_Suc nth_butlast)
    proof(rule mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      from 1(6) have a:"fork e = n" 
        by (auto simp add:fork_transitions_def split:if_splits)
      show ?case 
        using 1(1)[rule_format, of "(UpF fs e)"]        
        apply (simp add: 1 a butlast_list_update σforks_update_def) 
        using a ev_idforkx by blast
    next
      case (2 e m)
      have a:"UpF (butlast fs) e = butlast (UpF fs e)"       
        apply(simp add:σforks_update_def) 
        by (metis butlast_conv_take σforks_update_def forks_update_take length_list_update)
      from 2 show ?case 
        using 2(1)[rule_format, of "(UpF fs e)"] a σforks_update_def by auto
    qed
  qed
qed
   
lemma ft: "0 < n ⟹ FORKsnorm n (replicate n 0) = foldFORKs n"
proof (induct n, simp)
  case (Suc n)
  then show ?case 
    apply (auto simp add: FORKsnorm_unfold FORKnorm_is_FORK)
    apply (metis Suc_le_D butlast_snoc replicate_Suc replicate_append_same)
    by (metis FORKsnorm_1 One_nat_def leI length_replicate less_Suc0 nth_replicate replicate_Suc)
qed
  
corollary FORKs_is_FORKsnorm: "FORKsnorm N (replicate N 0) = FORKs"
  using ft N_pos by simp

text ‹The one-philosopher process in normal form:›

type_synonym phil_id = nat
type_synonym phil_state = nat

definition rphil_transitions:: "phil_id ⇒ phil_state ⇒ dining_event set" (‹Trrp›)
  where "Trrp i s = ( if      s = 0  then {picks i i}
                     else if s = 1  then {picks i (i-1)}
                     else if s = 2  then {putsdown i (i-1)} 
                     else if s = 3  then {putsdown i i}
                     else                {})"

definition lphil0_transitions:: "phil_state ⇒ dining_event set" (‹Trlp›)
    where "Trlp s = ( if s = 0       then {picks 0 (N-1)}
                     else if s = 1  then {picks 0 0}
                     else if s = 2  then {putsdown 0 0} 
                     else if s = 3  then {putsdown 0 (N-1)}
                     else                {})"

corollary rphil_phil: "e ∈ Trrp i s ⟹ phil e = i"
      and lphil0_phil: "e ∈ Trlp s ⟹ phil e = 0"
  by (simp_all add:rphil_transitions_def lphil0_transitions_def split:if_splits)

definition rphil_state_update:: "idfork ⇒ σfork ⇒ dining_event ⇒ σfork" (‹Uprp›)
  where "Uprp i s e = ( if e = (picks i i)               then 1 
                       else if e = (picks i (i-1))      then 2
                       else if e = (putsdown i (i-1))   then 3
                       else                                  0 )"

definition lphil0_state_update:: "σfork ⇒ dining_event ⇒ σfork" (‹Uplp›)
  where "Uplp s e = ( if e = (picks 0 (N-1))         then 1
                     else if e = (picks 0 0)        then 2 
                     else if e = (putsdown 0 0)     then 3
                     else                                0 )"

definition RPHILnorm:: "idfork ⇒ σfork ⇒ dining_event process"
  where "RPHILnorm i = Pnorm⟦Trrp i,Uprp i⟧"

definition LPHIL0norm:: "σfork ⇒ dining_event process"
  where "LPHIL0norm = Pnorm⟦Trlp,Uplp⟧"

lemma RPHILnorm_rec:  "RPHILnorm i = (λ s. □ e ∈ (Trrp i s) → RPHILnorm i (Uprp i s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trrp i s) (λe. X (Uprp i s e)))"] RPHILnorm_def by simp

lemma LPHIL0norm_rec:  "LPHIL0norm = (λ s. □ e ∈ (Trlp s) → LPHIL0norm (Uplp s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trlp s) (λe. X (Uplp s e)))"] LPHIL0norm_def by simp


lemma RPHIL_refines_RPHILnorm: 
  assumes i_pos: "i > 0"
  shows "RPHILnorm i 0 ⊑FD RPHIL i"
proof(unfold RPHILnorm_def, 
      induct rule:fix_ind_k_skip[where k=4 and f="Λ x. (λs. Mprefix (Trrp i s) (λe. x (Uprp i s e)))"])
  case lower_bound
  then show ?case (is "1 ≤ 4") by simp
next
  case admissibility
  then show ?case (is "adm (λa. a 0 ⊑FD RPHIL i)")
    by (simp add: cont_fun monofunI)
next
  case base_k_steps
  then show ?case (is "∀j<4. (iterate j⋅?f⋅⊥) 0 ⊑FD RPHIL i")  
  proof -
    have less_2:"⋀j. (j::nat) < 4 = (j = 0 ∨ j = 1  ∨ j = 2  ∨ j = 3)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑FD RPHIL i" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑FD RPHIL i" 
      by (subst RPHIL_rec) (simp add: write0_def rphil_transitions_def)
    moreover have "(iterate 2⋅?f⋅⊥) 0 ⊑FD RPHIL i" 
      by (subst RPHIL_rec) 
         (simp add: numeral_2_eq_2 write0_def rphil_transitions_def rphil_state_update_def)
    moreover have "(iterate 3⋅?f⋅⊥) 0 ⊑FD RPHIL i" 
      by (subst RPHIL_rec) (simp add: numeral_3_eq_3 write0_def rphil_transitions_def 
                                      rphil_state_update_def minus_suc[OF i_pos])
    ultimately show ?thesis by simp
  qed
next
  case (step x)
  then show ?case (is "(iterate 4⋅?f⋅x) 0 ⊑FD RPHIL i")
    apply (subst RPHIL_rec) 
    apply (simp add: write0_def numeral_4_eq_4 rphil_transitions_def rphil_state_update_def)
    apply (rule mono_Mprefix_FD, auto simp:minus_suc[OF i_pos])+ 
    using minus_suc[OF i_pos] by auto
qed


lemma LPHIL0_refines_LPHIL0norm: "LPHIL0norm 0 ⊑FD LPHIL0"
proof(unfold LPHIL0norm_def,
      induct rule:fix_ind_k_skip[where k=4 and f="Λ x. (λs. Mprefix (Trlp s) (λe. x (Uplp s e)))"])
  show "(1::nat) ≤ 4" by simp
next
  show "adm (λa. a 0 ⊑FD LPHIL0)" by (simp add: cont_fun monofunI)
next
  case base_k_steps
  show ?case (is "∀j<4. (iterate j⋅?f⋅⊥) 0 ⊑FD LPHIL0")
  proof -
    have less_2:"⋀j. (j::nat) < 4 = (j = 0 ∨ j = 1  ∨ j = 2  ∨ j = 3)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑FD LPHIL0" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑FD LPHIL0" 
      by (subst LPHIL0_rec) (simp add: write0_def lphil0_transitions_def)
    moreover have "(iterate 2⋅?f⋅⊥) 0 ⊑FD LPHIL0" 
      by (subst LPHIL0_rec) (simp add: numeral_2_eq_2 write0_def lphil0_transitions_def 
                                       lphil0_state_update_def)
    moreover have "(iterate 3⋅?f⋅⊥) 0 ⊑FD LPHIL0" 
      by (subst LPHIL0_rec) (simp add: numeral_3_eq_3 write0_def lphil0_transitions_def 
                                       lphil0_state_update_def)
    ultimately show ?thesis by simp
  qed
next
  case (step x)
  then show ?case (is "(iterate 4⋅?f⋅x) 0 ⊑FD LPHIL0")
    by (subst LPHIL0_rec) (simp add: write0_def numeral_4_eq_4 lphil0_transitions_def 
                                     lphil0_state_update_def)
qed

lemma RPHILnorm_refines_RPHIL:   
  assumes i_pos: "i > 0"
  shows "RPHIL i ⊑FD RPHILnorm i 0"
proof(unfold RPHIL_def, induct rule:fix_ind_k_skip[where k=1])
  case lower_bound
  then show ?case (is "1 ≤ 1")  by simp
next
  case admissibility
  then show ?case by (simp add: monofunI)
next
  case base_k_steps
  then show ?case by simp
next
  case (step x)then show ?case
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def) 
    apply (rule mono_Mprefix_FD, simp)
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_Mprefix_FD, simp add:minus_suc[OF i_pos])
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_Mprefix_FD, simp add:minus_suc[OF i_pos])
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_Mprefix_FD, simp add:minus_suc[OF i_pos])
    using minus_suc[OF i_pos] by auto
qed


lemma LPHIL0norm_refines_LPHIL0: "LPHIL0 ⊑FD LPHIL0norm 0"
proof(unfold LPHIL0_def, 
      induct rule:fix_ind_k_skip[where k=1])
  show "(1::nat) ≤ 1" by simp
next
  show "adm (λa. a ⊑FD LPHIL0norm 0)" by (simp add: monofunI)
next
  case base_k_steps
  show ?case by simp
next
  case (step x)
  then show ?case (is "iterate 1⋅?f⋅x ⊑FD LPHIL0norm 0")
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def) 
    apply (rule mono_Mprefix_FD, simp)
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def) 
    apply (rule mono_Mprefix_FD, simp)
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def) 
    apply (rule mono_Mprefix_FD, simp)
       by (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def) 
qed

lemma RPHILnorm_is_RPHIL: "i > 0 ⟹ RPHIL i = RPHILnorm i 0"
  using RPHIL_refines_RPHILnorm RPHILnorm_refines_RPHIL FD_antisym by blast 

lemma LPHIL0norm_is_LPHIL0: "LPHIL0 = LPHIL0norm 0"
  using LPHIL0_refines_LPHIL0norm LPHIL0norm_refines_LPHIL0 FD_antisym by blast 

subsection ‹The normal form for the global philosopher network›

type_synonym σphils = "nat list"

definition phils_transitions:: "nat ⇒ σphils ⇒ dining_event set" (‹TrP›)
  where "TrP n ps = Trlp (ps!0) ∪ (⋃i∈{1..< n}. Trrp i (ps!i))"

corollary phils_phil: "0 < n ⟹ e ∈ TrP n s ⟹ phil e < n"
  by (auto simp add:phils_transitions_def lphil0_phil rphil_phil)

lemma phils_transitions_take: "0 < n ⟹ TrP n ps = TrP n (take n ps)"
  by (auto simp add:phils_transitions_def) 

definition σphils_update:: "σphils ⇒ dining_event ⇒ σphils" (‹UpP›)
  where "UpP ps e = (let i=(phil e) in if i = 0 then ps[i:=(Uplp (ps!i) e)] 
                                       else          ps[i:=(Uprp i (ps!i) e)])"

lemma phils_update_take: "take n (UpP ps e) = UpP (take n ps) e"
  by (cases e) (simp_all add: σphils_update_def lphil0_state_update_def 
                              rphil_state_update_def take_update_swap)

definition PHILsnorm:: "nat ⇒ σphils ⇒ dining_event process"
  where "PHILsnorm n = Pnorm⟦TrP n,UpP⟧"

lemma PHILsnorm_rec:  "PHILsnorm n = (λ ps. □ e ∈ (TrP n ps) → PHILsnorm n (UpP ps e))"
  using fix_eq[of "Λ X. (λps. Mprefix (TrP n ps) (λe. X (UpP ps e)))"] PHILsnorm_def by simp

lemma PHILsnorm_1_dir1: "length ps > 0 ⟹ PHILsnorm 1 ps ⊑FD (LPHIL0norm (ps!0))" 
proof(unfold PHILsnorm_def,
      induct arbitrary:ps 
             rule:fix_ind_k[where k=1 
                            and f="Λ x. (λps. Mprefix (TrP 1 ps) (λe. x (UpP ps e)))"])
  case admissibility
  then show ?case by (simp add: cont_fun monofunI) 
next
  case base_k_steps
  then show ?case by simp
next
  case (step X)
  then show ?case
    apply (subst LPHIL0norm_rec, simp add:σphils_update_def phils_transitions_def) 
    proof (intro mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      with 1(2) show ?case 
        using 1(1)[rule_format, of "ps[0 := Uplp (ps ! 0) e]"] 
        by (simp add:lphil0_transitions_def split:if_splits)
    qed
qed

lemma PHILsnorm_1_dir2: "length ps > 0 ⟹ (LPHIL0norm (ps!0)) ⊑FD PHILsnorm 1 ps" 
proof(unfold LPHIL0norm_def, 
      induct arbitrary:ps rule:fix_ind_k[where k=1 
                                         and f="Λ x. (λs. Mprefix (Trlp s) (λe. x (Uplp s e)))"])
  case admissibility
  then show ?case by (simp add: cont_fun monofunI) 
next
  case base_k_steps
  then show ?case by simp
next
  case (step X)
  then show ?case
    apply (subst PHILsnorm_rec, simp add:σphils_update_def phils_transitions_def) 
    proof (intro mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      with 1(2) show ?case 
        using 1(1)[rule_format, of "ps[0 := Uplp (ps ! 0) e]"] 
        by (simp add:lphil0_transitions_def split:if_splits)
    qed
qed

lemma PHILsnorm_1: "length ps > 0 ⟹ PHILsnorm 1 ps = (LPHIL0norm (ps!0))"
  using PHILsnorm_1_dir1 PHILsnorm_1_dir2 FD_antisym by blast

lemma PHILsnorm_unfold: 
  assumes n_pos:"0 < n" 
  shows "length ps = Suc n ⟹ 
                            PHILsnorm (Suc n) ps = (PHILsnorm n (butlast ps)|||(RPHILnorm n (ps!n)))"
proof(rule FD_antisym)
  show "length ps = Suc n ⟹ PHILsnorm (Suc n) ps ⊑FD (PHILsnorm n (butlast ps)|||RPHILnorm n (ps!n))"
  proof(subst PHILsnorm_def, 
        induct arbitrary:ps 
               rule:fix_ind_k[where k=1 
                              and f="Λ x. (λps. Mprefix (TrP (Suc n) ps) (λe. x (UpP ps e)))"])
    case admissibility
    then show ?case by (simp add: cont_fun monofunI) 
  next
    case base_k_steps
    then show ?case by simp
  next
    case (step X)
    have indep:"∀s1 s2. TrP n s1 ∩ Trrp n s2 = {}" 
      using phils_phil rphil_phil n_pos by blast
    from step have tra:"(TrP (Suc n) ps) =(TrP n (butlast ps) ∪ Trrp n (ps ! n))" 
      by (auto simp add:n_pos phils_transitions_def nth_butlast Suc_leI 
                        atLeastLessThanSuc Un_commute Un_assoc)
    from step show ?case
      apply (auto simp add:indep dnorm_inter PHILsnorm_def RPHILnorm_def)
      apply (subst fix_eq, auto simp add:tra) 
    proof(rule mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      hence c:"UpP ps e ! n = ps ! n"
        using 1(3) phils_phil σphils_update_def step n_pos 
        by (cases "phil e", auto) (metis exists_least_iff nth_list_update_neq)
      have d:"UpP (butlast ps) e = butlast (UpP ps e)"       
        by (cases "phil e", auto simp add:σphils_update_def butlast_list_update 
                                          lphil0_state_update_def rphil_state_update_def)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(2) length_list_update σphils_update_def)
      from 1 show ?case 
        using 1(1)[rule_format, of "(UpP ps e)"] c d e by auto
    next
      case (2 e)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(2) length_list_update σphils_update_def)
      from 2 show ?case 
        using 2(1)[rule_format, of "(UpP ps e)", OF e] n_pos 
        apply(auto simp add: butlast_list_update rphil_phil σphils_update_def)
        by (meson disjoint_iff_not_equal indep)
    qed
  qed
next
  have indep:"∀s1 s2. TrP n s1 ∩ Trrp n s2 = {}" 
    using phils_phil rphil_phil using n_pos by blast

  show "length ps = Suc n ⟹ (PHILsnorm n (butlast ps)|||RPHILnorm n (ps!n)) ⊑FD PHILsnorm (Suc n) ps"
    apply (subst PHILsnorm_def, auto simp add:indep dnorm_inter RPHILnorm_def)
  proof(rule fix_ind[where 
        P="λa. ∀x. length x = Suc n ⟶ a (butlast x, x ! n) ⊑FD PHILsnorm (Suc n) x", rule_format], 
        simp_all, goal_cases base step)
    case base
    then show ?case by (simp add: cont_fun monofunI) 
  next
    case (step X ps)
    hence tra:"(TrP (Suc n) ps) =(TrP n (butlast ps) ∪ Trrp n (ps ! n))" 
      by (auto simp add:n_pos phils_transitions_def nth_butlast 
                        Suc_leI atLeastLessThanSuc Un_commute Un_assoc)
    from step show ?case
      apply (auto simp add:indep dnorm_inter PHILsnorm_def RPHILnorm_def)
      apply (subst fix_eq, auto simp add:tra)     
    proof(rule mono_Mprefix_FD, safe, goal_cases)
      case (1 e)
      hence c:"UpP ps e ! n = ps ! n"
        using 1(3) phils_phil σphils_update_def step n_pos 
        by (cases "phil e", auto) (metis exists_least_iff nth_list_update_neq)
      have d:"UpP (butlast ps) e = butlast (UpP ps e)"       
        by (cases "phil e", auto simp add:σphils_update_def butlast_list_update 
                                          lphil0_state_update_def rphil_state_update_def)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(3) length_list_update σphils_update_def)
      from 1 show ?case 
        using 1(2)[rule_format, of "(UpP ps e)", OF e] c d by auto       
    next
      case (2 e)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) 2(3) length_list_update σphils_update_def)
      from 2 show ?case 
        using 2(2)[rule_format, of "(UpP ps e)", OF e] n_pos 
        apply(auto simp add: butlast_list_update rphil_phil σphils_update_def)
        by (meson disjoint_iff_not_equal indep)
    qed
  qed
qed
   
lemma pt: "0 < n ⟹ PHILsnorm n (replicate n 0) = foldPHILs n"
proof (induct n, simp)
  case (Suc n)
  then show ?case 
    apply (auto simp add: PHILsnorm_unfold LPHIL0norm_is_LPHIL0)
     apply (metis Suc_le_eq butlast.simps(2) butlast_snoc RPHILnorm_is_RPHIL
                    nat_neq_iff replicate_append_same replicate_empty)
    by (metis One_nat_def leI length_replicate less_Suc0 PHILsnorm_1 nth_Cons_0 replicate_Suc)
qed
  
corollary PHILs_is_PHILsnorm: "PHILsnorm N (replicate N 0) = PHILs"
  using pt N_pos by simp

subsection ‹The complete process system under normal form›

definition dining_transitions:: "nat ⇒ σphils × σforks ⇒ dining_event set" (‹TrD›)
  where "TrD n = (λ(ps,fs). (TrP n ps) ∩ (TrF n fs))"

definition dining_state_update:: 
  "σphils × σforks ⇒ dining_event ⇒ σphils × σforks" (‹UpD›)
  where "UpD = (λ(ps,fs) e. (UpP ps e, UpF fs e))"

definition DININGnorm:: "nat ⇒ σphils × σforks ⇒ dining_event process"
  where "DININGnorm n = Pnorm⟦TrD n, UpD⟧"

lemma ltsDining_rec:  "DININGnorm n = (λ s. □ e ∈ (TrD n s) → DININGnorm n (UpD s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (TrD n s) (λe. X (UpD s e)))"] DININGnorm_def by simp

lemma DINING_is_DININGnorm: "DINING = DININGnorm N (replicate N 0, replicate N 0)"
proof -
  have "DININGnorm N (replicate N 0, replicate N 0) = 
                                        (PHILsnorm N (replicate N 0) || FORKsnorm N (replicate N 0))"
    unfolding DININGnorm_def PHILsnorm_def FORKsnorm_def dining_transitions_def 
              dining_state_update_def dnorm_par by simp
  thus ?thesis
    using PHILs_is_PHILsnorm FORKs_is_FORKsnorm DINING_def
    by (simp add: Par_commute)
qed

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

corollary lphil_states:"Uplp r e = 0 ∨ Uplp r e = 1 ∨ Uplp r e = 2 ∨ Uplp r e = 3" 
      and rphil_states:"Uprp i r e = 0 ∨ Uprp i r e = 1 ∨ Uprp i r e = 2 ∨ Uprp i r e = 3" 
  unfolding lphil0_state_update_def rphil_state_update_def by auto

lemma dining_events: 
"e ∈ TrD N s ⟹ 
        (∃i∈{1..<N}. e = picks i i ∨ e = picks i (i-1)  ∨ e = putsdown i i ∨ e = putsdown i (i-1)) 
     ∨ (e = picks 0 0 ∨ e = picks 0 (N-1) ∨ e = putsdown 0 0 ∨ e = putsdown 0 (N-1))" 
  by (auto simp add:dining_transitions_def phils_transitions_def rphil_transitions_def 
                    lphil0_transitions_def split:prod.splits if_splits) 

definition "inv_dining ps fs ≡      
            (∀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)
          ∧ (∀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)
          ∧ length fs = N ∧ length ps = N" 

lemma inv_DINING: "s ∈ ℜ (TrD N) UpD (replicate N 0, replicate N 0) ⟹ inv_dining (fst s) (snd s)"
proof(induct rule:ℜ.induct)
  case rbase
  show ?case 
    by (simp add: inv_dining_def)
next
  case (rstep s e)
  from rstep(2,3) show ?case
    apply(auto simp add:dining_transitions_def phils_transitions_def forks_transitions_def
                       lphil0_transitions_def rphil_transitions_def fork_transitions_def
                       lphil0_state_update_def rphil_state_update_def σfork_update_def 
                       dining_state_update_def σphils_update_def σforks_update_def 
                   split:if_splits prod.split) 
    unfolding inv_dining_def
  proof(goal_cases)  
    case (1 ps fs)
    then show ?case 
      by (simp add:nth_list_update) force
  next
    case (2 ps fs)
    then show ?case 
      by (auto simp add:nth_list_update) 
  next
    case (3 ps fs)
    then show ?case 
      using N_pos_simps(3) by force
  next
    case (4 ps fs)
    then show ?case     
      by (simp add:nth_list_update) force
  next
    case (5 ps fs)
    then show ?case     
      using N_g1 by linarith
  next
    case (6 ps fs)
    then show ?case     
      by (auto simp add:nth_list_update)
  next
    case (7 ps fs i)
    then show ?case     
      apply (simp add:nth_list_update, intro impI conjI, simp_all)  
      by  auto[1] (metis N_pos Suc_pred less_antisym, metis zero_neq_numeral)
  next
    case (8 ps fs i)
    then show ?case     
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all)
      by (metis "8"(1) zero_neq_one)+
  next
    case (9 ps fs i)
    then show ?case     
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all)
      by (metis N_pos Suc_pred less_antisym) (metis n_not_Suc_n numeral_2_eq_2)
  next
    case (10 ps fs i)
    then show ?case     
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all) 
      by (metis "10"(1) "10"(5) One_nat_def n_not_Suc_n numeral_2_eq_2)+
  qed
qed

lemma inv_implies_DF:"inv_dining ps fs ⟹ TrD N (ps, fs) ≠ {}"
  unfolding inv_dining_def
  apply(simp add:dining_transitions_def phils_transitions_def forks_transitions_def
                 lphil0_transitions_def
             split: if_splits prod.splits)
proof(elim conjE, intro conjI impI, goal_cases)
  case 1
  hence "putsdown 0 (N - Suc 0) ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def) 
  then show ?case 
    by blast 
next
  case 2
  hence "putsdown 0 0 ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def) 
  then show ?case
    by (simp add:fork_transitions_def) force
next
  case 3
  hence a:"fs!0 = 0 ⟹ picks 0 0 ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def) 
  from 3 have b1:"ps!1 = 2 ⟹ putsdown 1 0 ∈ (⋃x∈{Suc 0..<N}. Trrp x (ps ! x))"
    using N_g1 by (auto simp add:rphil_transitions_def) 
  from 3 have b2:"fs!0 = 2 ⟹ putsdown 1 0 ∈ Trf 0 (fs ! 0)"
    using N_g1 by (auto simp add:fork_transitions_def) fastforce
  from 3 have c:"fs!0 ≠ 0 ⟹ ps!1 = 2"
    by (metis N_pos N_pos_simps(3) One_nat_def diff_is_0_eq neq0_conv)
  from 3 have d:"fs!0 ≠ 0 ⟹ fs!0 = 2" 
    using N_pos by meson
  then show ?case
    apply(cases "fs!0 = 0")
    using a apply (simp add: fork_transitions_def Un_insert_left)
    using b1[OF c] b2[OF d] N_pos by blast 
next
  case 4
  then show ?case
    using 4(5)[rule_format, of 0, OF N_pos] apply(elim disjE)
  proof(goal_cases)
    case 41:1 (* fs!0 = 0 *)
    then show ?case
    using 4(5)[rule_format, of 1, OF N_g1] apply(elim disjE) 
    proof(goal_cases)
      case 411:1 (* fs!1 = 0 *)
      from 411 have a0: "ps!1 = 0"
        by (metis N_g1 One_nat_def neq0_conv) 
      from 411 have a1: "picks 1 1 ∈ (⋃i<N. Trf i (fs ! i))"
        apply (auto simp add:fork_transitions_def)
        by (metis (mono_tags, lifting) N_g1 Int_Collect One_nat_def lessThan_iff)
      from 411 have a2: "ps!1 = 0 ⟹ picks 1 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
        apply (auto simp add:rphil_transitions_def) 
        using N_g1 by linarith 
      from 411 show ?case
        using a0 a1 a2 by blast
    next
      case 412:2 (* fs!1 = 1 *)
      hence "ps!1 = 1 ∨ ps!1 = 3" 
        by (metis N_g1 One_nat_def less_numeral_extra(3) zero_less_diff)
      with 412 show ?case 
      proof(elim disjE, goal_cases)
        case 4121:1 (* ps!1 = 1 *)
        from 4121 have b1: "picks 1 0 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def) 
          by (metis (full_types) Int_Collect N_g1 N_pos One_nat_def lessThan_iff mod_less)
        from 4121 have b2: "picks 1 0 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def)         
          using N_g1 by linarith 
        from 4121 show ?case
          using b1 b2 by blast
      next
        case 4122:2 (* ps!1 = 3 *)
        from 4122 have b3: "putsdown 1 1 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def)  
          using N_g1 by linarith        
        from 4122 have b4: "putsdown 1 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def)           
          using N_g1 by linarith        
        then show ?case 
          using b3 b4 by blast
      qed      
    next
      case 413:3 (* fs!1 = 2 *)
      then show ?case
      proof(cases "N = 2")
        case True
        with 413 show ?thesis by simp
      next
        case False
        from False 413 have c0: "ps!2 = 2"
          by (metis N_g1 Suc_1 Suc_diff_1 nat_neq_iff not_gr0 zero_less_diff)
        from False 413 have c1: "putsdown 2 1 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def) 
          using N_g1 apply linarith
          using N_g1 by auto
        from False 413 have c2: "ps!2 = 2 ⟹ putsdown 2 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def) 
          using N_g1 by linarith 
        from 413 False show ?thesis 
          using c0 c1 c2 by blast
      qed
    qed
  next
    case 42:2 (* fs!0 = 1 *)
    then show ?case by blast
  next
    case 43:3 (* fs!0 = 2*)
    from 43 have d0: "ps!1 = 2"  
      by (metis One_nat_def gr0I)   
    from 43 have d1: "putsdown 1 0 ∈ (⋃i<N. Trf i (fs ! i))"
      by (auto simp add:fork_transitions_def)
    from 43 have d2: "ps!1 = 2 ⟹ putsdown 1 0 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
      apply (auto simp add:rphil_transitions_def) 
      using N_g1 by linarith 
    from 43 show ?case 
      using d0 d1 d2 by blast
  qed
next
  case 5
  then show ?case
    using 5(6)[rule_format, of 0] by simp
qed
  
corollary DF_DINING: "deadlock_free_v2 DINING"
  unfolding DINING_is_DININGnorm DININGnorm_def 
  using inv_DINING inv_implies_DF by (subst deadlock_free_dnorm) auto

end

end