17 qed "Init_PLam"; |
17 qed "Init_PLam"; |
18 Addsimps [Init_PLam]; |
18 Addsimps [Init_PLam]; |
19 |
19 |
20 Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
20 Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
21 by (auto_tac (claset(), |
21 by (auto_tac (claset(), |
22 simpset() addsimps [PLam_def, Acts_JN])); |
22 simpset() addsimps [PLam_def])); |
23 qed "Acts_PLam"; |
23 qed "Acts_PLam"; |
24 |
24 |
25 Goal "PLam {} F = SKIP"; |
25 Goal "PLam {} F = SKIP"; |
26 by (simp_tac (simpset() addsimps [PLam_def]) 1); |
26 by (simp_tac (simpset() addsimps [PLam_def]) 1); |
27 qed "PLam_empty"; |
27 qed "PLam_empty"; |
138 by (etac reachable.induct 1); |
138 by (etac reachable.induct 1); |
139 (*Init, Init case*) |
139 (*Init, Init case*) |
140 by (force_tac (claset() addIs reachable.intrs, simpset()) 1); |
140 by (force_tac (claset() addIs reachable.intrs, simpset()) 1); |
141 (*Init of F, action of PLam F case*) |
141 (*Init of F, action of PLam F case*) |
142 by (rtac reachable.Acts 1); |
142 by (rtac reachable.Acts 1); |
143 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
143 by (Force_tac 1); |
144 by (assume_tac 1); |
144 by (assume_tac 1); |
145 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
145 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
146 (*induction over the 2nd "reachable" assumption*) |
146 (*induction over the 2nd "reachable" assumption*) |
147 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
147 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
148 (*Init of PLam F, action of F case*) |
148 (*Init of PLam F, action of F case*) |
149 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
149 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
150 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
150 by (Force_tac 1); |
151 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
151 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
152 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
152 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
153 (*last case: an action of PLam I F*) |
153 (*last case: an action of PLam I F*) |
154 by (rtac reachable.Acts 1); |
154 by (rtac reachable.Acts 1); |
155 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
155 by (Force_tac 1); |
156 by (assume_tac 1); |
156 by (assume_tac 1); |
157 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
157 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
158 qed_spec_mp "reachable_lift_Join_PLam"; |
158 qed_spec_mp "reachable_lift_Join_PLam"; |
159 |
159 |
160 |
160 |
183 by (auto_tac |
183 by (auto_tac |
184 (claset(), |
184 (claset(), |
185 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
185 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
186 reachable_PLam_eq])); |
186 reachable_PLam_eq])); |
187 by (auto_tac (claset(), |
187 by (auto_tac (claset(), |
188 simpset() addsimps [constrains_def, PLam_def, Acts_JN])); |
188 simpset() addsimps [constrains_def, PLam_def])); |
189 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
189 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
190 qed "Constrains_imp_PLam_Constrains"; |
190 qed "Constrains_imp_PLam_Constrains"; |
191 |
191 |
192 Goal "[| ALL j:I. f0 j : A j; i: I |] \ |
192 Goal "[| ALL j:I. f0 j : A j; i: I |] \ |
193 \ ==> drop_set i (INT j:I. lift_set j (A j)) = A i"; |
193 \ ==> drop_set i (INT j:I. lift_set j (A j)) = A i"; |