1(*  Title:      HOL/UNITY/Simple/Common.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Common Meeting Time example from Misra (1994)
6
7The state is identified with the one variable in existence.
8
9From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
10*)
11
12theory Common
13imports "../UNITY_Main"
14begin
15
16consts
17  ftime :: "nat=>nat"
18  gtime :: "nat=>nat"
19
20axiomatization where
21  fmono: "m \<le> n ==> ftime m \<le> ftime n" and
22  gmono: "m \<le> n ==> gtime m \<le> gtime n" and
23
24  fasc:  "m \<le> ftime n" and
25  gasc:  "m \<le> gtime n"
26
27definition common :: "nat set" where
28    "common == {n. ftime n = n & gtime n = n}"
29
30definition maxfg :: "nat => nat set" where
31    "maxfg m == {t. t \<le> max (ftime m) (gtime m)}"
32
33
34(*Misra's property CMT4: t exceeds no common meeting time*)
35lemma common_stable:
36     "[| \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]  
37      ==> F \<in> Stable (atMost n)"
38apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing)
39apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
40apply (erule Constrains_weaken_R)
41apply (blast intro: order_eq_refl le_trans dest: fmono gmono)
42done
43
44lemma common_safety:
45     "[| Init F \<subseteq> atMost n;   
46         \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]  
47      ==> F \<in> Always (atMost n)"
48by (simp add: AlwaysI common_stable)
49
50
51(*** Some programs that implement the safety property above ***)
52
53lemma "SKIP \<in> {m} co (maxfg m)"
54by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
55
56(*This one is  t := ftime t || t := gtime t*)
57lemma "mk_total_program
58         (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
59       \<in> {m} co (maxfg m)"
60apply (simp add: mk_total_program_def) 
61apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
62done
63
64(*This one is  t := max (ftime t) (gtime t)*)
65lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
66       \<in> {m} co (maxfg m)"
67apply (simp add: mk_total_program_def) 
68apply (simp add: constrains_def maxfg_def gasc max.absorb2)
69done
70
71(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
72lemma  "mk_total_program
73          (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
74       \<in> {m} co (maxfg m)"
75apply (simp add: mk_total_program_def) 
76apply (simp add: constrains_def maxfg_def gasc max.absorb2)
77done
78
79
80(*It remans to prove that they satisfy CMT3': t does not decrease,
81  and that CMT3' implies that t stops changing once common(t) holds.*)
82
83
84(*** Progress under weak fairness ***)
85
86lemma leadsTo_common_lemma:
87  assumes "\<forall>m. F \<in> {m} Co (maxfg m)"
88    and "\<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m)"
89    and "n \<in> common"
90  shows "F \<in> (atMost n) LeadsTo common"
91proof (rule LeadsTo_weaken_R)
92  show "F \<in> {..n} LeadsTo {..n} \<inter> id -` {n..} \<union> common"
93  proof (induct rule: GreaterThan_bounded_induct [of n _ _ id])
94    case 1
95    from assms have "\<forall>m\<in>{..<n}. F \<in> {..n} \<inter> {m} LeadsTo {..n} \<inter> {m<..} \<union> common"
96      by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
97    then show ?case by simp
98  qed
99next
100  from \<open>n \<in> common\<close>
101  show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
102    by (simp add: atMost_Int_atLeast)
103qed
104
105(*The "\<forall>m \<in> -common" form echoes CMT6.*)
106lemma leadsTo_common:
107     "[| \<forall>m. F \<in> {m} Co (maxfg m);  
108         \<forall>m \<in> -common. F \<in> {m} LeadsTo (greaterThan m);  
109         n \<in> common |]   
110      ==> F \<in> (atMost (LEAST n. n \<in> common)) LeadsTo common"
111apply (rule leadsTo_common_lemma)
112apply (simp_all (no_asm_simp))
113apply (erule_tac [2] LeastI)
114apply (blast dest!: not_less_Least)
115done
116
117end
118