src/HOLCF/IOA/meta_theory/Traces.ML
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4536 74f7c556fd90
equal deleted inserted replaced
4476:fbdc87f8ac7e 4477:b3e5857d8d99
   177 \ Forall (%a. a:act A) (filter_act`(snd x))";
   177 \ Forall (%a. a:act A) (filter_act`(snd x))";
   178 
   178 
   179 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   179 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   180 by (pair_tac "x" 1);
   180 by (pair_tac "x" 1);
   181 by (rtac (execfrag_in_sig RS spec RS mp) 1);
   181 by (rtac (execfrag_in_sig RS spec RS mp) 1);
   182 by (Auto_tac());
   182 by Auto_tac;
   183 qed"exec_in_sig";
   183 qed"exec_in_sig";
   184 
   184 
   185 goalw thy [schedules_def,has_schedule_def]
   185 goalw thy [schedules_def,has_schedule_def]
   186   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
   186   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
   187 \   Forall (%a. a:act A) x";
   187 \   Forall (%a. a:act A) x";
   211 goal thy "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)";
   211 goal thy "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)";
   212 by (pair_induct_tac "y" [is_exec_frag_def] 1);
   212 by (pair_induct_tac "y" [is_exec_frag_def] 1);
   213 by (strip_tac 1);
   213 by (strip_tac 1);
   214 by (Seq_case_simp_tac "xa" 1);
   214 by (Seq_case_simp_tac "xa" 1);
   215 by (pair_tac "a" 1);
   215 by (pair_tac "a" 1);
   216 by (Auto_tac());
   216 by Auto_tac;
   217 qed"execfrag_prefixclosed";
   217 qed"execfrag_prefixclosed";
   218 
   218 
   219 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   219 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   220 
   220 
   221 
   221 
   224 goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
   224 goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
   225 by (pair_induct_tac "x" [is_exec_frag_def] 1);
   225 by (pair_induct_tac "x" [is_exec_frag_def] 1);
   226 by (strip_tac 1);
   226 by (strip_tac 1);
   227 by (Seq_case_simp_tac "s" 1);
   227 by (Seq_case_simp_tac "s" 1);
   228 by (pair_tac "a" 1);
   228 by (pair_tac "a" 1);
   229 by (Auto_tac());
   229 by Auto_tac;
   230 qed_spec_mp"exec_prefix2closed";
   230 qed_spec_mp"exec_prefix2closed";
   231 
   231