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