# Theory Common

theory Common
imports UNITY_Main
```(*  Title:      HOL/UNITY/Simple/Common.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Common Meeting Time example from Misra (1994)

The state is identified with the one variable in existence.

From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)

theory Common
imports "../UNITY_Main"
begin

consts
ftime :: "nat=>nat"
gtime :: "nat=>nat"

axiomatization where
fmono: "m ≤ n ==> ftime m ≤ ftime n" and
gmono: "m ≤ n ==> gtime m ≤ gtime n" and

fasc:  "m ≤ ftime n" and
gasc:  "m ≤ gtime n"

definition common :: "nat set" where
"common == {n. ftime n = n & gtime n = n}"

definition maxfg :: "nat => nat set" where
"maxfg m == {t. t ≤ max (ftime m) (gtime m)}"

(*Misra's property CMT4: t exceeds no common meeting time*)
lemma common_stable:
"[| ∀m. F ∈ {m} Co (maxfg m); n ∈ common |]
==> F ∈ Stable (atMost n)"
apply (drule_tac M = "{t. t ≤ n}" in Elimination_sing)
apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
apply (erule Constrains_weaken_R)
apply (blast intro: order_eq_refl le_trans dest: fmono gmono)
done

lemma common_safety:
"[| Init F ⊆ atMost n;
∀m. F ∈ {m} Co (maxfg m); n ∈ common |]
==> F ∈ Always (atMost n)"

(*** Some programs that implement the safety property above ***)

lemma "SKIP ∈ {m} co (maxfg m)"
by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)

(*This one is  t := ftime t || t := gtime t*)
lemma "mk_total_program
(UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
∈ {m} co (maxfg m)"
apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
done

(*This one is  t := max (ftime t) (gtime t)*)
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
∈ {m} co (maxfg m)"
apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done

(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
lemma  "mk_total_program
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
∈ {m} co (maxfg m)"
apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done

(*It remans to prove that they satisfy CMT3': t does not decrease,
and that CMT3' implies that t stops changing once common(t) holds.*)

(*** Progress under weak fairness ***)

assumes "∀m. F ∈ {m} Co (maxfg m)"
and "∀m ∈ lessThan n. F ∈ {m} LeadsTo (greaterThan m)"
and "n ∈ common"
shows "F ∈ (atMost n) LeadsTo common"
show "F ∈ {..n} LeadsTo {..n} ∩ id -` {n..} ∪ common"
proof (induct rule: GreaterThan_bounded_induct [of n _ _ id])
case 1
from assms have "∀m∈{..<n}. F ∈ {..n} ∩ {m} LeadsTo {..n} ∩ {m<..} ∪ common"
by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
then show ?case by simp
qed
next
from ‹n ∈ common›
show "{..n} ∩ id -` {n..} ∪ common ⊆ common"
qed

(*The "∀m ∈ -common" form echoes CMT6.*)