author | paulson |
Tue, 01 Feb 2005 18:01:57 +0100 | |
changeset 15481 | fc075ae929e4 |
parent 14092 | 68da54626309 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: ZF/UNITY/FP.thy |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
7 |
||
8 |
Theory ported from HOL. |
|
9 |
*) |
|
10 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
11 |
header{*Fixed Point of a Program*} |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
12 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
13 |
theory FP = UNITY: |
11479 | 14 |
|
15 |
constdefs |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
16 |
FP_Orig :: "i=>i" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
17 |
"FP_Orig(F) == Union({A \<in> Pow(state). \<forall>B. F \<in> stable(A Int B)})" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
18 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
19 |
FP :: "i=>i" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
20 |
"FP(F) == {s\<in>state. F \<in> stable({s})}" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
21 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
22 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
23 |
lemma FP_Orig_type: "FP_Orig(F) \<subseteq> state" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
24 |
by (unfold FP_Orig_def, blast) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
25 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
26 |
lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
27 |
apply (unfold st_set_def) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
28 |
apply (rule FP_Orig_type) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
29 |
done |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
30 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
31 |
lemma FP_type: "FP(F) \<subseteq> state" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
32 |
by (unfold FP_def, blast) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
33 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
34 |
lemma st_set_FP [iff]: "st_set(FP(F))" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
35 |
apply (unfold st_set_def) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
36 |
apply (rule FP_type) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
37 |
done |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
38 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
39 |
lemma stable_FP_Orig_Int: "F \<in> program ==> F \<in> stable(FP_Orig(F) Int B)" |
15481 | 40 |
apply (simp only: FP_Orig_def stable_def Int_Union2) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
41 |
apply (blast intro: constrains_UN) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
42 |
done |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
43 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
44 |
lemma FP_Orig_weakest2: |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
45 |
"[| \<forall>B. F \<in> stable (A Int B); st_set(A) |] ==> A \<subseteq> FP_Orig(F)" |
15481 | 46 |
by (unfold FP_Orig_def stable_def st_set_def, blast) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
47 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
48 |
lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard] |
11479 | 49 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
50 |
lemma stable_FP_Int: "F \<in> program ==> F \<in> stable (FP(F) Int B)" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
51 |
apply (subgoal_tac "FP (F) Int B = (\<Union>x\<in>B. FP (F) Int {x}) ") |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
52 |
prefer 2 apply blast |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
53 |
apply (simp (no_asm_simp) add: Int_cons_right) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
54 |
apply (unfold FP_def stable_def) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
55 |
apply (rule constrains_UN) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
56 |
apply (auto simp add: cons_absorb) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
57 |
done |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
58 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
59 |
lemma FP_subset_FP_Orig: "F \<in> program ==> FP(F) \<subseteq> FP_Orig(F)" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
60 |
by (rule stable_FP_Int [THEN FP_Orig_weakest], auto) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
61 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
62 |
lemma FP_Orig_subset_FP: "F \<in> program ==> FP_Orig(F) \<subseteq> FP(F)" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
63 |
apply (unfold FP_Orig_def FP_def, clarify) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
64 |
apply (drule_tac x = "{x}" in spec) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
65 |
apply (simp add: Int_cons_right) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
66 |
apply (frule stableD2) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
67 |
apply (auto simp add: cons_absorb st_set_def) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
68 |
done |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
69 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
70 |
lemma FP_equivalence: "F \<in> program ==> FP(F) = FP_Orig(F)" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
71 |
by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
72 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
73 |
lemma FP_weakest [rule_format]: |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
74 |
"[| \<forall>B. F \<in> stable(A Int B); F \<in> program; st_set(A) |] ==> A \<subseteq> FP(F)" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
75 |
by (simp add: FP_equivalence FP_Orig_weakest) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
76 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
77 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
78 |
lemma Diff_FP: |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
79 |
"[| F \<in> program; st_set(A) |] |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
80 |
==> A-FP(F) = (\<Union>act \<in> Acts(F). A - {s \<in> state. act``{s} \<subseteq> {s}})" |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
81 |
by (unfold FP_def stable_def constrains_def st_set_def, blast) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
82 |
|
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
83 |
ML |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
84 |
{* |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
85 |
val FP_Orig_type = thm "FP_Orig_type"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
86 |
val st_set_FP_Orig = thm "st_set_FP_Orig"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
87 |
val FP_type = thm "FP_type"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
88 |
val st_set_FP = thm "st_set_FP"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
89 |
val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
90 |
val FP_Orig_weakest2 = thm "FP_Orig_weakest2"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
91 |
val stable_FP_Int = thm "stable_FP_Int"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
92 |
val FP_subset_FP_Orig = thm "FP_subset_FP_Orig"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
93 |
val FP_Orig_subset_FP = thm "FP_Orig_subset_FP"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
94 |
val FP_equivalence = thm "FP_equivalence"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
95 |
val FP_weakest = thm "FP_weakest"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
96 |
val Diff_FP = thm "Diff_FP"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
12195
diff
changeset
|
97 |
*} |
11479 | 98 |
|
99 |
end |