src/HOL/UNITY/FP.thy
 author haftmann Fri Jun 11 17:14:02 2010 +0200 (2010-06-11) changeset 37407 61dd8c145da7 parent 35416 d8d7d1b785af child 37936 1e4c5015a72e permissions -rw-r--r--
declare lex_prod_def [code del]
```     1 (*  Title:      HOL/UNITY/FP
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1998  University of Cambridge
```
```     4
```
```     5 From Misra, "A Logic for Concurrent Programming", 1994
```
```     6 *)
```
```     7
```
```     8 header{*Fixed Point of a Program*}
```
```     9
```
```    10 theory FP imports UNITY begin
```
```    11
```
```    12 definition FP_Orig :: "'a program => 'a set" where
```
```    13     "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
```
```    14
```
```    15 definition FP :: "'a program => 'a set" where
```
```    16     "FP F == {s. F : stable {s}}"
```
```    17
```
```    18 lemma stable_FP_Orig_Int: "F : stable (FP_Orig F Int B)"
```
```    19 apply (simp only: FP_Orig_def stable_def Int_Union2)
```
```    20 apply (blast intro: constrains_UN)
```
```    21 done
```
```    22
```
```    23 lemma FP_Orig_weakest:
```
```    24     "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
```
```    25 by (simp add: FP_Orig_def stable_def, blast)
```
```    26
```
```    27 lemma stable_FP_Int: "F : stable (FP F Int B)"
```
```    28 apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
```
```    29 prefer 2 apply blast
```
```    30 apply (simp (no_asm_simp) add: Int_insert_right)
```
```    31 apply (simp add: FP_def stable_def)
```
```    32 apply (rule constrains_UN)
```
```    33 apply (simp (no_asm))
```
```    34 done
```
```    35
```
```    36 lemma FP_equivalence: "FP F = FP_Orig F"
```
```    37 apply (rule equalityI)
```
```    38  apply (rule stable_FP_Int [THEN FP_Orig_weakest])
```
```    39 apply (simp add: FP_Orig_def FP_def, clarify)
```
```    40 apply (drule_tac x = "{x}" in spec)
```
```    41 apply (simp add: Int_insert_right)
```
```    42 done
```
```    43
```
```    44 lemma FP_weakest:
```
```    45     "(!!B. F : stable (A Int B)) ==> A <= FP F"
```
```    46 by (simp add: FP_equivalence FP_Orig_weakest)
```
```    47
```
```    48 lemma Compl_FP:
```
```    49     "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
```
```    50 by (simp add: FP_def stable_def constrains_def, blast)
```
```    51
```
```    52 lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
```
```    53 by (simp add: Diff_eq Compl_FP)
```
```    54
```
```    55 lemma totalize_FP [simp]: "FP (totalize F) = FP F"
```
```    56 by (simp add: FP_def)
```
```    57
```
```    58 end
```