src/HOL/UNITY/FP.thy
 author haftmann Fri Jun 17 16:12:49 2005 +0200 (2005-06-17) changeset 16417 9bc16273c2d4 parent 15481 fc075ae929e4 child 35416 d8d7d1b785af permissions -rw-r--r--
migrated theory headers to new format
```     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 imports UNITY begin
```
```    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 (simp only: FP_Orig_def stable_def Int_Union2)
```
```    23 apply (blast intro: constrains_UN)
```
```    24 done
```
```    25
```
```    26 lemma FP_Orig_weakest:
```
```    27     "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
```
```    28 by (simp add: FP_Orig_def stable_def, blast)
```
```    29
```
```    30 lemma stable_FP_Int: "F : stable (FP F Int B)"
```
```    31 apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
```
```    32 prefer 2 apply blast
```
```    33 apply (simp (no_asm_simp) add: Int_insert_right)
```
```    34 apply (simp add: FP_def stable_def)
```
```    35 apply (rule constrains_UN)
```
```    36 apply (simp (no_asm))
```
```    37 done
```
```    38
```
```    39 lemma FP_equivalence: "FP F = FP_Orig F"
```
```    40 apply (rule equalityI)
```
```    41  apply (rule stable_FP_Int [THEN FP_Orig_weakest])
```
```    42 apply (simp add: FP_Orig_def FP_def, clarify)
```
```    43 apply (drule_tac x = "{x}" in spec)
```
```    44 apply (simp add: Int_insert_right)
```
```    45 done
```
```    46
```
```    47 lemma FP_weakest:
```
```    48     "(!!B. F : stable (A Int B)) ==> A <= FP F"
```
```    49 by (simp add: FP_equivalence FP_Orig_weakest)
```
```    50
```
```    51 lemma Compl_FP:
```
```    52     "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
```
```    53 by (simp add: FP_def stable_def constrains_def, blast)
```
```    54
```
```    55 lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
```
```    56 by (simp add: Diff_eq Compl_FP)
```
```    57
```
```    58 lemma totalize_FP [simp]: "FP (totalize F) = FP F"
```
```    59 by (simp add: FP_def)
```
```    60
```
```    61 end
```