src/HOL/IOA/Solve.ML
changeset 4772 8c7e7eaffbdf
parent 4681 a331c1f5a23e
child 4799 82b0ed20c2cb
     1.1 --- a/src/HOL/IOA/Solve.ML	Thu Apr 02 13:49:04 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Thu Apr 02 17:19:02 1998 +0200
     1.3 @@ -16,16 +16,17 @@
     1.4  
     1.5    by (simp_tac(simpset() addsimps [has_trace_def])1);
     1.6    by Safe_tac;
     1.7 +  by (rename_tac "f ex1 ex2" 1);
     1.8  
     1.9    (* choose same trace, therefore same NF *)
    1.10 -  by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
    1.11 +  by (res_inst_tac[("x","mk_trace  C ex1")] exI 1);
    1.12    by (Asm_full_simp_tac 1);
    1.13  
    1.14    (* give execution of abstract automata *)
    1.15 -  by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
    1.16 +  by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1);
    1.17  
    1.18    (* Traces coincide *)
    1.19 -  by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
    1.20 +   by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
    1.21  
    1.22    (* Use lemma *)
    1.23    by (forward_tac [states_of_exec_reachable] 1);
    1.24 @@ -42,8 +43,8 @@
    1.25    by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
    1.26    by Safe_tac;
    1.27  
    1.28 -  by (eres_inst_tac [("x","snd ex n")] allE 1);
    1.29 -  by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
    1.30 +  by (eres_inst_tac [("x","ex2 n")] allE 1);
    1.31 +  by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1);
    1.32    by (eres_inst_tac [("x","a")] allE 1);
    1.33    by (Asm_full_simp_tac 1);
    1.34  qed "trace_inclusion";
    1.35 @@ -73,7 +74,7 @@
    1.36  \    %i. fst (snd ex i))")]  bexI 1);
    1.37  (* fst(s) is in projected execution *)
    1.38   by (Simp_tac 1);
    1.39 - by (fast_tac (claset() delWrapper "split_all_tac") 1);
    1.40 + by (fast_tac (claset() delSWrapper "split_all_tac") 1);
    1.41  (* projected execution is indeed an execution *)
    1.42  by (asm_full_simp_tac
    1.43        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.44 @@ -93,7 +94,7 @@
    1.45  \    %i. snd (snd ex i))")]  bexI 1);
    1.46  (* fst(s) is in projected execution *)
    1.47   by (Simp_tac 1);
    1.48 - by (fast_tac (claset() delWrapper "split_all_tac") 1);
    1.49 + by (fast_tac (claset() delSWrapper "split_all_tac") 1);
    1.50  (* projected execution is indeed an execution *)
    1.51  by (asm_full_simp_tac
    1.52        (simpset() addsimps [executions_def,is_execution_fragment_def,