solved conflict by taking newest version;
authormueller
Mon Oct 19 13:34:19 1998 +0200 (1998-10-19)
changeset 56705e7d9455de96
parent 5669 f5d9caafc3bd
child 5671 da670b37857e
solved conflict by taking newest version;
src/HOLCF/IOA/meta_theory/Abstraction.ML
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 11:26:46 1998 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Oct 19 13:34:19 1998 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  by (forward_tac [reachable.reachable_n] 1);
     1.5  by (assume_tac 1);
     1.6  by (Asm_full_simp_tac 1);
     1.7 -qed"exec_frag_abstraction";
     1.8 +qed_spec_mp"exec_frag_abstraction";
     1.9  
    1.10  
    1.11  Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
    1.12 @@ -80,7 +80,7 @@
    1.13  by (rtac conjI 1);
    1.14  by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
    1.15  (* is-execution-fragment *)
    1.16 -by (etac (exec_frag_abstraction RS spec RS mp) 1);
    1.17 +by (etac exec_frag_abstraction 1);
    1.18  by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    1.19  qed"abs_is_weakening";
    1.20  
    1.21 @@ -185,6 +185,8 @@
    1.22  by (pair_induct_tac "xs" [] 1);
    1.23  qed"traces_coincide_abs";
    1.24  
    1.25 +(* 
    1.26 +FIX: Is this needed anywhere? 
    1.27  
    1.28  Goalw [cex_abs_def]
    1.29   "!!f.[| is_abstraction h C A |] ==>\
    1.30 @@ -205,6 +207,7 @@
    1.31  by (assume_tac 1);
    1.32  by (Asm_full_simp_tac 1);
    1.33  qed_spec_mp"correp_is_exec_abs";
    1.34 +*) 
    1.35  
    1.36  (* Does not work with abstraction_is_ref_map as proof of abs_safety, because
    1.37     is_live_abstraction includes temp_strengthening which is necessarily based
    1.38 @@ -232,7 +235,7 @@
    1.39    by (rtac conjI 1);
    1.40    by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
    1.41    (* is-execution-fragment *)
    1.42 -  by (etac correp_is_exec_abs 1);
    1.43 +  by (etac exec_frag_abstraction 1);
    1.44    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    1.45  
    1.46   (* Liveness *) 
    1.47 @@ -376,8 +379,8 @@
    1.48  \ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))";
    1.49  by (rtac impI 1);
    1.50  by (Seq_Finite_induct_tac 1);
    1.51 +by (Blast_tac 1);
    1.52  (* main case *)
    1.53 -by (Blast_tac 1);
    1.54  by (clarify_tac set_cs 1);
    1.55  by (pair_tac "ex" 1);
    1.56  by (Seq_case_simp_tac "y" 1);
    1.57 @@ -489,7 +492,6 @@
    1.58  by Auto_tac;
    1.59  qed"TLex2seq";
    1.60  
    1.61 -
    1.62  Goal "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)";
    1.63  by (pair_tac "ex" 1);
    1.64  by (Seq_case_simp_tac "y" 1);
    1.65 @@ -497,7 +499,7 @@
    1.66  by (Seq_case_simp_tac "s" 1);
    1.67  by (pair_tac "a" 1);
    1.68  qed"ex2seqUUTL";
    1.69 -
    1.70 + 
    1.71  Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)";
    1.72  by (pair_tac "ex" 1);
    1.73  by (Seq_case_simp_tac "y" 1);