equal
deleted
inserted
replaced
71 "(filter_oseq (%a. a:actions(asig_of(C1))) \ |
71 "(filter_oseq (%a. a:actions(asig_of(C1))) \ |
72 \ (fst ex), \ |
72 \ (fst ex), \ |
73 \ %i. fst (snd ex i))")] bexI 1); |
73 \ %i. fst (snd ex i))")] bexI 1); |
74 (* fst(s) is in projected execution *) |
74 (* fst(s) is in projected execution *) |
75 by (Simp_tac 1); |
75 by (Simp_tac 1); |
76 by (Fast_tac 1); |
76 by (fast_tac (claset() delWrapper "split_all_tac") 1); |
77 (* projected execution is indeed an execution *) |
77 (* projected execution is indeed an execution *) |
78 by (asm_full_simp_tac |
78 by (asm_full_simp_tac |
79 (simpset() addsimps [executions_def,is_execution_fragment_def, |
79 (simpset() addsimps [executions_def,is_execution_fragment_def, |
80 par_def,starts_of_def,trans_of_def,filter_oseq_def] |
80 par_def,starts_of_def,trans_of_def,filter_oseq_def] |
81 addsplits [expand_if,split_option_case]) 1); |
81 addsplits [expand_if,split_option_case]) 1); |
91 "(filter_oseq (%a. a:actions(asig_of(C2)))\ |
91 "(filter_oseq (%a. a:actions(asig_of(C2)))\ |
92 \ (fst ex), \ |
92 \ (fst ex), \ |
93 \ %i. snd (snd ex i))")] bexI 1); |
93 \ %i. snd (snd ex i))")] bexI 1); |
94 (* fst(s) is in projected execution *) |
94 (* fst(s) is in projected execution *) |
95 by (Simp_tac 1); |
95 by (Simp_tac 1); |
96 by (Fast_tac 1); |
96 by (fast_tac (claset() delWrapper "split_all_tac") 1); |
97 (* projected execution is indeed an execution *) |
97 (* projected execution is indeed an execution *) |
98 by (asm_full_simp_tac |
98 by (asm_full_simp_tac |
99 (simpset() addsimps [executions_def,is_execution_fragment_def, |
99 (simpset() addsimps [executions_def,is_execution_fragment_def, |
100 par_def,starts_of_def,trans_of_def,filter_oseq_def] |
100 par_def,starts_of_def,trans_of_def,filter_oseq_def] |
101 addsplits [expand_if,split_option_case]) 1); |
101 addsplits [expand_if,split_option_case]) 1); |