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