author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 15481 | fc075ae929e4 |
child 35413 | d8d7d1b785af |
permissions | -rw-r--r-- |
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 |