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