110 qed"mkex_nil"; |
110 qed"mkex_nil"; |
111 |
111 |
112 goal thy "!!x.[| x:act A; x~:act B |] \ |
112 goal thy "!!x.[| x:act A; x~:act B |] \ |
113 \ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \ |
113 \ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \ |
114 \ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"; |
114 \ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"; |
115 by (simp_tac (simpset() addsimps [mkex_def] |
115 by (simp_tac (simpset() addsimps [mkex_def]) 1); |
116 setloop (split_tac [expand_if]) ) 1); |
|
117 by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1); |
116 by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1); |
118 by Auto_tac; |
117 by Auto_tac; |
119 qed"mkex_cons_1"; |
118 qed"mkex_cons_1"; |
120 |
119 |
121 goal thy "!!x.[| x~:act A; x:act B |] \ |
120 goal thy "!!x.[| x~:act A; x:act B |] \ |
122 \ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \ |
121 \ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \ |
123 \ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"; |
122 \ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"; |
124 by (simp_tac (simpset() addsimps [mkex_def] |
123 by (simp_tac (simpset() addsimps [mkex_def]) 1); |
125 setloop (split_tac [expand_if]) ) 1); |
|
126 by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1); |
124 by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1); |
127 by Auto_tac; |
125 by Auto_tac; |
128 qed"mkex_cons_2"; |
126 qed"mkex_cons_2"; |
129 |
127 |
130 goal thy "!!x.[| x:act A; x:act B |] \ |
128 goal thy "!!x.[| x:act A; x:act B |] \ |
131 \ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \ |
129 \ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \ |
132 \ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"; |
130 \ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"; |
133 by (simp_tac (simpset() addsimps [mkex_def] |
131 by (simp_tac (simpset() addsimps [mkex_def]) 1); |
134 setloop (split_tac [expand_if]) ) 1); |
|
135 by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1); |
132 by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1); |
136 by Auto_tac; |
133 by Auto_tac; |
137 qed"mkex_cons_3"; |
134 qed"mkex_cons_3"; |
138 |
135 |
139 Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3]; |
136 Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3]; |
214 |
211 |
215 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); |
212 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); |
216 |
213 |
217 (* main case *) |
214 (* main case *) |
218 (* splitting into 4 cases according to a:A, a:B *) |
215 (* splitting into 4 cases according to a:A, a:B *) |
219 by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1); |
216 by (Asm_full_simp_tac 1); |
220 by (safe_tac set_cs); |
217 by (safe_tac set_cs); |
221 |
218 |
222 (* Case y:A, y:B *) |
219 (* Case y:A, y:B *) |
223 by (Seq_case_simp_tac "exA" 1); |
220 by (Seq_case_simp_tac "exA" 1); |
224 (* Case exA=UU, Case exA=nil*) |
221 (* Case exA=UU, Case exA=nil*) |
247 |
244 |
248 (* generalizing the proof above to a tactic *) |
245 (* generalizing the proof above to a tactic *) |
249 |
246 |
250 fun mkex_induct_tac sch exA exB = |
247 fun mkex_induct_tac sch exA exB = |
251 EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], |
248 EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], |
252 asm_full_simp_tac (simpset() setloop split_tac [expand_if]), |
249 Asm_full_simp_tac, |
253 SELECT_GOAL (safe_tac set_cs), |
250 SELECT_GOAL (safe_tac set_cs), |
254 Seq_case_simp_tac exA, |
251 Seq_case_simp_tac exA, |
255 Seq_case_simp_tac exB, |
252 Seq_case_simp_tac exB, |
256 Asm_full_simp_tac, |
253 Asm_full_simp_tac, |
257 Seq_case_simp_tac exA, |
254 Seq_case_simp_tac exA, |