|
1 (* Title: HOL/UNITY/FP.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Fixed Point of a Program |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
|
10 Theory ported form HOL. |
|
11 *) |
|
12 |
|
13 |
|
14 Goalw [FP_Orig_def] |
|
15 "FP_Orig(F):condition"; |
|
16 by (Blast_tac 1); |
|
17 qed "FP_Orig_type"; |
|
18 AddIffs [FP_Orig_type]; |
|
19 AddTCs [FP_Orig_type]; |
|
20 |
|
21 Goalw [FP_Orig_def, condition_def] |
|
22 "x:FP_Orig(F) ==> x:state"; |
|
23 by Auto_tac; |
|
24 qed "FP_OrigD"; |
|
25 |
|
26 Goalw [FP_def, condition_def] |
|
27 "FP(F):condition"; |
|
28 by (Blast_tac 1); |
|
29 qed "FP_type"; |
|
30 AddIffs [FP_type]; |
|
31 AddTCs [FP_type]; |
|
32 |
|
33 Goalw [FP_def, condition_def] |
|
34 "x:FP(F) ==> x:state"; |
|
35 by Auto_tac; |
|
36 qed "FP_D"; |
|
37 |
|
38 Goal "Union(B) Int A = (UN C:B. C Int A)"; |
|
39 by (Blast_tac 1); |
|
40 qed "Int_Union2"; |
|
41 |
|
42 Goalw [FP_Orig_def, stable_def] |
|
43 "[| F:program; B:condition |] \ |
|
44 \ ==> F:stable(FP_Orig(F) Int B)"; |
|
45 by (stac Int_Union2 1); |
|
46 by (blast_tac (claset() addIs [constrains_UN]) 1); |
|
47 qed "stable_FP_Orig_Int"; |
|
48 |
|
49 Goalw [FP_Orig_def, stable_def] |
|
50 "[| ALL B:condition. F : stable (A Int B); A:condition |] \ |
|
51 \ ==> A <= FP_Orig(F)"; |
|
52 by (Blast_tac 1); |
|
53 bind_thm("FP_Orig_weakest", ballI RS result()); |
|
54 |
|
55 Goal "A Int cons(a, B) = \ |
|
56 \ (if a : A then cons(a, cons(a, (A Int B))) else A Int B)"; |
|
57 by Auto_tac; |
|
58 qed "Int_cons_right"; |
|
59 |
|
60 |
|
61 Goal "[| F:program; B:condition |] ==> F : stable (FP(F) Int B)"; |
|
62 by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1); |
|
63 by (Blast_tac 2); |
|
64 by (asm_simp_tac (simpset() addsimps [Int_cons_right]) 1); |
|
65 by (rewrite_goals_tac [FP_def, stable_def]); |
|
66 by (rtac constrains_UN 1); |
|
67 by (auto_tac (claset(), simpset() addsimps [cons_absorb])); |
|
68 qed "stable_FP_Int"; |
|
69 |
|
70 |
|
71 Goal "F:program ==> FP(F) <= FP_Orig(F)"; |
|
72 by (rtac (stable_FP_Int RS FP_Orig_weakest) 1); |
|
73 by Auto_tac; |
|
74 val lemma1 = result(); |
|
75 |
|
76 |
|
77 Goalw [FP_Orig_def, FP_def] |
|
78 "F:program ==> FP_Orig(F) <= FP(F)"; |
|
79 by (Clarify_tac 1); |
|
80 by (dres_inst_tac [("x", "{x}")] bspec 1); |
|
81 by (force_tac (claset(), simpset() addsimps [condition_def]) 1); |
|
82 by (asm_full_simp_tac (simpset() addsimps [Int_cons_right]) 1); |
|
83 by (auto_tac (claset(), simpset() addsimps [cons_absorb])); |
|
84 by (force_tac (claset(), simpset() addsimps [condition_def]) 1); |
|
85 val lemma2 = result(); |
|
86 |
|
87 |
|
88 Goal "F:program ==> FP(F) = FP_Orig(F)"; |
|
89 by (rtac ([lemma1,lemma2] MRS equalityI) 1); |
|
90 by (ALLGOALS(assume_tac)); |
|
91 qed "FP_equivalence"; |
|
92 |
|
93 |
|
94 Goal "[| ALL B:condition. F : stable(A Int B); A:condition; F:program |] \ |
|
95 \ ==> A <= FP(F)"; |
|
96 by (asm_simp_tac (simpset() addsimps [FP_equivalence, FP_Orig_weakest]) 1); |
|
97 bind_thm("FP_weakest", result() RS ballI); |
|
98 |
|
99 Goalw [FP_def, stable_def, constrains_def, condition_def] |
|
100 "[| F:program; A:condition |] ==> \ |
|
101 \ A - FP(F) = (UN act: Acts(F). A -{s:state. act``{s} <= {s}})"; |
|
102 by (Blast_tac 1); |
|
103 qed "Diff_FP"; |
|
104 |