1 (* Title: HOL/UNITY/FP |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Fixed Point of a Program |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 *) |
|
10 |
|
11 Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)"; |
|
12 by (stac Int_Union2 1); |
|
13 by (blast_tac (claset() addIs [constrains_UN]) 1); |
|
14 qed "stable_FP_Orig_Int"; |
|
15 |
|
16 |
|
17 val prems = goalw thy [FP_Orig_def, stable_def] |
|
18 "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"; |
|
19 by (blast_tac (claset() addIs prems) 1); |
|
20 qed "FP_Orig_weakest"; |
|
21 |
|
22 |
|
23 Goal "F : stable (FP F Int B)"; |
|
24 by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1); |
|
25 by (Blast_tac 2); |
|
26 by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1); |
|
27 by (rewrite_goals_tac [FP_def, stable_def]); |
|
28 by (rtac constrains_UN 1); |
|
29 by (Simp_tac 1); |
|
30 qed "stable_FP_Int"; |
|
31 |
|
32 Goal "FP F <= FP_Orig F"; |
|
33 by (rtac (stable_FP_Int RS FP_Orig_weakest) 1); |
|
34 val lemma1 = result(); |
|
35 |
|
36 Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F"; |
|
37 by (Clarify_tac 1); |
|
38 by (dres_inst_tac [("x", "{x}")] spec 1); |
|
39 by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1); |
|
40 val lemma2 = result(); |
|
41 |
|
42 Goal "FP F = FP_Orig F"; |
|
43 by (rtac ([lemma1,lemma2] MRS equalityI) 1); |
|
44 qed "FP_equivalence"; |
|
45 |
|
46 val [prem] = goal thy |
|
47 "(!!B. F : stable (A Int B)) ==> A <= FP F"; |
|
48 by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1); |
|
49 qed "FP_weakest"; |
|
50 |
|
51 Goalw [FP_def, stable_def, constrains_def] |
|
52 "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"; |
|
53 by (Blast_tac 1); |
|
54 qed "Compl_FP"; |
|
55 |
|
56 Goal "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"; |
|
57 by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1); |
|
58 qed "Diff_FP"; |
|
59 |
|