94 \ (F : constrains A B & G : constrains A B)"; |
94 \ (F : constrains A B & G : constrains A B)"; |
95 by (auto_tac |
95 by (auto_tac |
96 (claset(), |
96 (claset(), |
97 simpset() addsimps [constrains_def, Join_def])); |
97 simpset() addsimps [constrains_def, Join_def])); |
98 qed "constrains_Join"; |
98 qed "constrains_Join"; |
|
99 |
|
100 |
|
101 (** |
|
102 Michel says... |
|
103 |
|
104 p inductive-next q' in F |
|
105 p inductive-next q'' in G |
|
106 p noninductive-next q in FoG |
|
107 ------------------------------------------- |
|
108 p noninductive-next q /\ (q' \/ q'') in FoG |
|
109 |
|
110 From which you deduce: |
|
111 |
|
112 inductive-stable A /\ B in F |
|
113 inductive-stable A in G |
|
114 noninductive-stable B in FoG |
|
115 --------------------------------- |
|
116 noninductive-stable A /\ B in FoG |
|
117 **) |
|
118 |
|
119 Goal "[| F : constrains A B'; G : constrains A B''; \ |
|
120 \ F Join G : Constrains A B |] \ |
|
121 \ ==> F Join G : Constrains A (B Int (B' Un B''))"; |
|
122 by (auto_tac |
|
123 (claset() addIs [constrains_Int RS constrains_weaken], |
|
124 simpset() addsimps [Constrains_def, constrains_Join])); |
|
125 qed "constrains_imp_Join_Constrains"; |
|
126 |
|
127 Goalw [Stable_def, stable_def] |
|
128 "[| F : stable (A Int B); G : stable A; \ |
|
129 \ F Join G : Stable B |] \ |
|
130 \ ==> F Join G : Stable (A Int B)"; |
|
131 by (auto_tac |
|
132 (claset() addIs [constrains_Int RS constrains_weaken], |
|
133 simpset() addsimps [Constrains_def, constrains_Join])); |
|
134 qed "stable_imp_Join_Stable"; |
|
135 |
|
136 |
99 |
137 |
100 (**FAILS, I think; see 5.4.1, Substitution Axiom. |
138 (**FAILS, I think; see 5.4.1, Substitution Axiom. |
101 The problem is to relate reachable (F Join G) with |
139 The problem is to relate reachable (F Join G) with |
102 reachable F and reachable G |
140 reachable F and reachable G |
103 |
141 |