src/HOL/UNITY/FP.thy
 author paulson Sat Feb 08 16:05:33 2003 +0100 (2003-02-08) changeset 13812 91713a1915ee parent 13798 4c1a53627500 child 15481 fc075ae929e4 permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
```     1 (*  Title:      HOL/UNITY/FP
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1998  University of Cambridge
```
```     5
```
```     6 From Misra, "A Logic for Concurrent Programming", 1994
```
```     7 *)
```
```     8
```
```     9 header{*Fixed Point of a Program*}
```
```    10
```
```    11 theory FP = UNITY:
```
```    12
```
```    13 constdefs
```
```    14
```
```    15   FP_Orig :: "'a program => 'a set"
```
```    16     "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
```
```    17
```
```    18   FP :: "'a program => 'a set"
```
```    19     "FP F == {s. F : stable {s}}"
```
```    20
```
```    21 lemma stable_FP_Orig_Int: "F : stable (FP_Orig F Int B)"
```
```    22 apply (unfold FP_Orig_def stable_def)
```
```    23 apply (subst Int_Union2)
```
```    24 apply (blast intro: constrains_UN)
```
```    25 done
```
```    26
```
```    27 lemma FP_Orig_weakest:
```
```    28     "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
```
```    29 by (unfold FP_Orig_def stable_def, blast)
```
```    30
```
```    31 lemma stable_FP_Int: "F : stable (FP F Int B)"
```
```    32 apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
```
```    33 prefer 2 apply blast
```
```    34 apply (simp (no_asm_simp) add: Int_insert_right)
```
```    35 apply (unfold FP_def stable_def)
```
```    36 apply (rule constrains_UN)
```
```    37 apply (simp (no_asm))
```
```    38 done
```
```    39
```
```    40 lemma FP_equivalence: "FP F = FP_Orig F"
```
```    41 apply (rule equalityI)
```
```    42  apply (rule stable_FP_Int [THEN FP_Orig_weakest])
```
```    43 apply (unfold FP_Orig_def FP_def, clarify)
```
```    44 apply (drule_tac x = "{x}" in spec)
```
```    45 apply (simp add: Int_insert_right)
```
```    46 done
```
```    47
```
```    48 lemma FP_weakest:
```
```    49     "(!!B. F : stable (A Int B)) ==> A <= FP F"
```
```    50 by (simp add: FP_equivalence FP_Orig_weakest)
```
```    51
```
```    52 lemma Compl_FP:
```
```    53     "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
```
```    54 by (simp add: FP_def stable_def constrains_def, blast)
```
```    55
```
```    56 lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
```
```    57 by (simp add: Diff_eq Compl_FP)
```
```    58
```
```    59 lemma totalize_FP [simp]: "FP (totalize F) = FP F"
```
```    60 by (simp add: FP_def)
```
```    61
```
```    62 end
```