src/HOL/UNITY/FP.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 16417 9bc16273c2d4
child 35416 d8d7d1b785af
permissions -rw-r--r--
simplified method setup;
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
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     7
*)
paulson@4776
     8
paulson@13798
     9
header{*Fixed Point of a Program*}
paulson@13798
    10
haftmann@16417
    11
theory FP imports UNITY begin
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@15481
    22
apply (simp only: FP_Orig_def stable_def Int_Union2)
paulson@13796
    23
apply (blast intro: constrains_UN)
paulson@13796
    24
done
paulson@13796
    25
paulson@13796
    26
lemma FP_Orig_weakest:
paulson@13796
    27
    "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
paulson@15481
    28
by (simp add: FP_Orig_def stable_def, blast)
paulson@13796
    29
paulson@13796
    30
lemma stable_FP_Int: "F : stable (FP F Int B)"
paulson@13796
    31
apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
paulson@13796
    32
prefer 2 apply blast
paulson@13796
    33
apply (simp (no_asm_simp) add: Int_insert_right)
paulson@15481
    34
apply (simp add: FP_def stable_def)
paulson@13796
    35
apply (rule constrains_UN)
paulson@13796
    36
apply (simp (no_asm))
paulson@13796
    37
done
paulson@13796
    38
paulson@13796
    39
lemma FP_equivalence: "FP F = FP_Orig F"
paulson@13796
    40
apply (rule equalityI) 
paulson@13796
    41
 apply (rule stable_FP_Int [THEN FP_Orig_weakest])
paulson@15481
    42
apply (simp add: FP_Orig_def FP_def, clarify)
paulson@13796
    43
apply (drule_tac x = "{x}" in spec)
paulson@13796
    44
apply (simp add: Int_insert_right)
paulson@13796
    45
done
paulson@13796
    46
paulson@13796
    47
lemma FP_weakest:
paulson@13796
    48
    "(!!B. F : stable (A Int B)) ==> A <= FP F"
paulson@13796
    49
by (simp add: FP_equivalence FP_Orig_weakest)
paulson@13796
    50
paulson@13796
    51
lemma Compl_FP: 
paulson@13796
    52
    "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
paulson@13796
    53
by (simp add: FP_def stable_def constrains_def, blast)
paulson@13796
    54
paulson@13796
    55
lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
paulson@13796
    56
by (simp add: Diff_eq Compl_FP)
paulson@13796
    57
paulson@13812
    58
lemma totalize_FP [simp]: "FP (totalize F) = FP F"
paulson@13812
    59
by (simp add: FP_def)
paulson@13812
    60
paulson@4776
    61
end