src/HOL/UNITY/Simple/Common.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 16417 9bc16273c2d4
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 (*  Title:      HOL/UNITY/Common
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Common Meeting Time example from Misra (1994)
     7 
     8 The state is identified with the one variable in existence.
     9 
    10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    11 *)
    12 
    13 theory Common = UNITY_Main:
    14 
    15 consts
    16   ftime :: "nat=>nat"
    17   gtime :: "nat=>nat"
    18 
    19 axioms
    20   fmono: "m \<le> n ==> ftime m \<le> ftime n"
    21   gmono: "m \<le> n ==> gtime m \<le> gtime n"
    22 
    23   fasc:  "m \<le> ftime n"
    24   gasc:  "m \<le> gtime n"
    25 
    26 constdefs
    27   common :: "nat set"
    28     "common == {n. ftime n = n & gtime n = n}"
    29 
    30   maxfg :: "nat => nat set"
    31     "maxfg m == {t. t \<le> max (ftime m) (gtime m)}"
    32 
    33 
    34 (*Misra's property CMT4: t exceeds no common meeting time*)
    35 lemma common_stable:
    36      "[| \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]  
    37       ==> F \<in> Stable (atMost n)"
    38 apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing)
    39 apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
    40 apply (erule Constrains_weaken_R)
    41 apply (blast intro: order_eq_refl fmono gmono le_trans)
    42 done
    43 
    44 lemma 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)"
    48 by (simp add: AlwaysI common_stable)
    49 
    50 
    51 (*** Some programs that implement the safety property above ***)
    52 
    53 lemma "SKIP \<in> {m} co (maxfg m)"
    54 by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    55 
    56 (*This one is  t := ftime t || t := gtime t*)
    57 lemma "mk_total_program
    58          (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
    59        \<in> {m} co (maxfg m)"
    60 apply (simp add: mk_total_program_def) 
    61 apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    62 done
    63 
    64 (*This one is  t := max (ftime t) (gtime t)*)
    65 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
    66        \<in> {m} co (maxfg m)"
    67 apply (simp add: mk_total_program_def) 
    68 apply (simp add: constrains_def maxfg_def max_def gasc)
    69 done
    70 
    71 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    72 lemma  "mk_total_program
    73           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
    74        \<in> {m} co (maxfg m)"
    75 apply (simp add: mk_total_program_def) 
    76 apply (simp add: constrains_def maxfg_def max_def gasc)
    77 done
    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 
    86 declare atMost_Int_atLeast [simp]
    87 
    88 lemma leadsTo_common_lemma:
    89      "[| \<forall>m. F \<in> {m} Co (maxfg m);  
    90          \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);  
    91          n \<in> common |]   
    92       ==> F \<in> (atMost n) LeadsTo common"
    93 apply (rule LeadsTo_weaken_R)
    94 apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
    95 apply (simp_all (no_asm_simp))
    96 apply (rule_tac [2] subset_refl)
    97 apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
    98 done
    99 
   100 (*The "\<forall>m \<in> -common" form echoes CMT6.*)
   101 lemma leadsTo_common:
   102      "[| \<forall>m. F \<in> {m} Co (maxfg m);  
   103          \<forall>m \<in> -common. F \<in> {m} LeadsTo (greaterThan m);  
   104          n \<in> common |]   
   105       ==> F \<in> (atMost (LEAST n. n \<in> common)) LeadsTo common"
   106 apply (rule leadsTo_common_lemma)
   107 apply (simp_all (no_asm_simp))
   108 apply (erule_tac [2] LeastI)
   109 apply (blast dest!: not_less_Least)
   110 done
   111 
   112 end