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