src/HOL/UNITY/FP.thy
author wenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773 d09c66a0ea10
parent 58889 5b7a9633cfa8
child 61952 546958347e05
permissions -rw-r--r--
more symbols by default, without xsymbols mode;
     1 (*  Title:      HOL/UNITY/FP.thy
     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 section{*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