author | paulson |
Thu, 03 Sep 1998 16:40:02 +0200 | |
changeset 5426 | 566f47250bd0 |
parent 5313 | 1861a564d7e2 |
child 5584 | aad639e56d4e |
permissions | -rw-r--r-- |
5252 | 1 |
(* Title: HOL/UNITY/Union.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Unions of programs |
|
7 |
||
8 |
From Misra's Chapter 5: Asynchronous Compositions of Programs |
|
9 |
*) |
|
10 |
||
11 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
12 |
Goal "Init (Join prgF prgG) = Init prgF Int Init prgG"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
13 |
by (simp_tac (simpset() addsimps [Join_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
14 |
qed "Init_Join"; |
5252 | 15 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
16 |
Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
17 |
by (simp_tac (simpset() addsimps [Join_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
18 |
qed "Acts_Join"; |
5252 | 19 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
20 |
Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
21 |
by (simp_tac (simpset() addsimps [JOIN_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
22 |
qed "Init_JN"; |
5252 | 23 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
24 |
Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
25 |
by (simp_tac (simpset() addsimps [JOIN_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
26 |
qed "Acts_JN"; |
5252 | 27 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
28 |
Addsimps [Init_Join, Init_JN]; |
5259 | 29 |
|
30 |
(** Theoretical issues **) |
|
31 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
32 |
Goal "Join prgF prgG = Join prgG prgF"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
33 |
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1); |
5259 | 34 |
qed "Join_commute"; |
35 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
36 |
Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
37 |
by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1); |
5259 | 38 |
qed "Join_assoc"; |
39 |
||
40 |
||
41 |
(* |
|
42 |
val field_defs = thms"program.field_defs"; |
|
43 |
val dest_defs = thms"program.dest_defs"; |
|
44 |
val dest_convs = thms"program.dest_convs"; |
|
45 |
||
46 |
val update_defs = thms"program.update_defs"; |
|
47 |
val make_defs = thms"program.make_defs"; |
|
48 |
val update_convs = thms"program.update_convs"; |
|
49 |
val simps = thms"program.simps"; |
|
50 |
*) |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
51 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
52 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
53 |
(**NOT PROVABLE because no "surjective pairing" for records |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
54 |
Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
55 |
by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
56 |
qed "Join_Null"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
57 |
*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
58 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
59 |
(**NOT PROVABLE because no "surjective pairing" for records |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
60 |
Goalw [Join_def] "Join prgF prgF = prgF"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
61 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
62 |
qed "Join_absorb"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
63 |
*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
64 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
65 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
66 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
67 |
(*** Safety: constrains, stable, FP ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
68 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
69 |
Goalw [constrains_def, JOIN_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
70 |
"constrains (Acts (JN i:I. prg i)) A B = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
71 |
\ (ALL i:I. constrains (Acts (prg i)) A B)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
72 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
73 |
qed "constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
74 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
75 |
(**FAILS, I think; see 5.4.1, Substitution Axiom. |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
76 |
Goalw [Constrains_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
77 |
"Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
78 |
by (simp_tac (simpset() addsimps [constrains_JN]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
79 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
80 |
qed "Constrains_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
81 |
**) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
82 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
83 |
Goalw [constrains_def, Join_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
84 |
"constrains (Acts (Join prgF prgG)) A B = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
85 |
\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
86 |
by (simp_tac (simpset() addsimps [ball_Un]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
87 |
qed "constrains_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
88 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
89 |
Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
90 |
\ ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
91 |
by (simp_tac (simpset() addsimps [constrains_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
92 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
93 |
qed "constrains_Join_weaken"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
94 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
95 |
Goalw [stable_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
96 |
"stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
97 |
by (simp_tac (simpset() addsimps [constrains_JN]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
98 |
qed "stable_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
99 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
100 |
Goal "stable (Acts (Join prgF prgG)) A = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
101 |
\ (stable (Acts prgF) A & stable (Acts prgG) A)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
102 |
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
103 |
qed "stable_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
104 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
105 |
Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
106 |
by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
107 |
qed "FP_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
108 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
109 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
110 |
(*** Progress: transient, ensures ***) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
111 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
112 |
Goalw [transient_def, JOIN_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
113 |
"transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
114 |
by (Simp_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
115 |
qed "transient_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
116 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
117 |
Goalw [transient_def, Join_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
118 |
"transient (Acts (Join prgF prgG)) A = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
119 |
\ (transient (Acts prgF) A | transient (Acts prgG) A)"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
120 |
by (simp_tac (simpset() addsimps [bex_Un]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
121 |
qed "transient_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
122 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
123 |
Goalw [ensures_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
124 |
"ensures (Acts (JN i:I. prg i)) A B = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
125 |
\ ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
126 |
\ (EX i:I. ensures (Acts (prg i)) A B))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
127 |
by (auto_tac (claset(), |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
128 |
simpset() addsimps [constrains_JN, transient_JN])); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
129 |
qed "ensures_JN"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
130 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
131 |
Goalw [ensures_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
132 |
"ensures (Acts (Join prgF prgG)) A B = \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
133 |
\ (constrains (Acts prgF) (A-B) (A Un B) & \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
134 |
\ constrains (Acts prgG) (A-B) (A Un B) & \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
135 |
\ (ensures (Acts prgF) A B | ensures (Acts prgG) A B))"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
136 |
by (auto_tac (claset(), |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
137 |
simpset() addsimps [constrains_Join, transient_Join])); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
138 |
qed "ensures_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
139 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
140 |
Goalw [stable_def, constrains_def, Join_def] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
141 |
"[| stable (Acts prgF) A; constrains (Acts prgG) A A'; id: Acts prgG |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
142 |
\ ==> constrains (Acts (Join prgF prgG)) A A'"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
143 |
by (asm_simp_tac (simpset() addsimps [ball_Un]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
144 |
by (Blast_tac 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
145 |
qed "stable_constrains_Join"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
146 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
147 |
(*Premises cannot use Invariant because Stable prgF A is weaker than |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
148 |
stable (Acts prgG) A *) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
149 |
Goal "[| stable (Acts prgF) A; Init prgG <= A; stable (Acts prgG) A |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
150 |
\ ==> Invariant (Join prgF prgG) A"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
151 |
by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable, |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
152 |
stable_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
153 |
by (force_tac(claset() addIs [stable_reachable, stable_Int], |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
154 |
simpset() addsimps [Acts_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
155 |
qed "stable_Join_Invariant"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
156 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
157 |
Goal "[| stable (Acts prgF) A; ensures (Acts prgG) A B |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
158 |
\ ==> ensures (Acts (Join prgF prgG)) A B"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
159 |
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
160 |
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
161 |
by (etac constrains_weaken 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
162 |
by Auto_tac; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
163 |
qed "ensures_stable_Join1"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
164 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
165 |
(*As above, but exchanging the roles of F and G*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
166 |
Goal "[| ensures (Acts prgF) A B; stable (Acts prgG) A |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
167 |
\ ==> ensures (Acts (Join prgF prgG)) A B"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
168 |
by (stac Join_commute 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
169 |
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
170 |
qed "ensures_stable_Join2"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
171 |