src/HOL/UNITY/Simple/Common.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 18556 dc39832e9280 child 21026 3b2821e0d541 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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 imports "../UNITY_Main" begin
```
```    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
```