author | nipkow |
Fri, 27 Mar 2020 12:28:05 +0100 | |
changeset 71593 | 71579bd59cd4 |
parent 69661 | a03a63b81f44 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/FP.thy |
4776 | 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 |
||
63146 | 8 |
section\<open>Fixed Point of a Program\<close> |
13798 | 9 |
|
16417 | 10 |
theory FP imports UNITY begin |
4776 | 11 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
12 |
definition FP_Orig :: "'a program => 'a set" where |
67613 | 13 |
"FP_Orig F == \<Union>{A. \<forall>B. F \<in> stable (A \<inter> B)}" |
4776 | 14 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
15 |
definition FP :: "'a program => 'a set" where |
67613 | 16 |
"FP F == {s. F \<in> stable {s}}" |
4776 | 17 |
|
67613 | 18 |
lemma stable_FP_Orig_Int: "F \<in> stable (FP_Orig F Int B)" |
15481 | 19 |
apply (simp only: FP_Orig_def stable_def Int_Union2) |
13796 | 20 |
apply (blast intro: constrains_UN) |
21 |
done |
|
22 |
||
23 |
lemma FP_Orig_weakest: |
|
67613 | 24 |
"(\<And>B. F \<in> stable (A \<inter> B)) \<Longrightarrow> A <= FP_Orig F" |
15481 | 25 |
by (simp add: FP_Orig_def stable_def, blast) |
13796 | 26 |
|
67613 | 27 |
lemma stable_FP_Int: "F \<in> stable (FP F \<inter> B)" |
69661 | 28 |
proof - |
29 |
have "F \<in> stable (\<Union>x\<in>B. FP F \<inter> {x})" |
|
30 |
apply (simp only: Int_insert_right FP_def stable_def) |
|
31 |
apply (rule constrains_UN) |
|
32 |
apply simp |
|
33 |
done |
|
34 |
also have "(\<Union>x\<in>B. FP F \<inter> {x}) = FP F \<inter> B" |
|
35 |
by simp |
|
36 |
finally show ?thesis . |
|
37 |
qed |
|
13796 | 38 |
|
39 |
lemma FP_equivalence: "FP F = FP_Orig F" |
|
40 |
apply (rule equalityI) |
|
41 |
apply (rule stable_FP_Int [THEN FP_Orig_weakest]) |
|
15481 | 42 |
apply (simp add: FP_Orig_def FP_def, clarify) |
13796 | 43 |
apply (drule_tac x = "{x}" in spec) |
44 |
apply (simp add: Int_insert_right) |
|
45 |
done |
|
46 |
||
47 |
lemma FP_weakest: |
|
67613 | 48 |
"(\<And>B. F \<in> stable (A Int B)) \<Longrightarrow> A <= FP F" |
13796 | 49 |
by (simp add: FP_equivalence FP_Orig_weakest) |
50 |
||
51 |
lemma Compl_FP: |
|
52 |
"-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})" |
|
53 |
by (simp add: FP_def stable_def constrains_def, blast) |
|
54 |
||
55 |
lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})" |
|
56 |
by (simp add: Diff_eq Compl_FP) |
|
57 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
58 |
lemma totalize_FP [simp]: "FP (totalize F) = FP F" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
59 |
by (simp add: FP_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
60 |
|
4776 | 61 |
end |