# HG changeset patch # User mueller # Date 908796859 -7200 # Node ID 5e7d9455de96567549c98a7bd7a2991098881695 # Parent f5d9caafc3bd8488ad556c648761f782655cf53e solved conflict by taking newest version; diff -r f5d9caafc3bd -r 5e7d9455de96 src/HOLCF/IOA/meta_theory/Abstraction.ML --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Mon Oct 19 11:26:46 1998 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Mon Oct 19 13:34:19 1998 +0200 @@ -69,7 +69,7 @@ by (forward_tac [reachable.reachable_n] 1); by (assume_tac 1); by (Asm_full_simp_tac 1); -qed"exec_frag_abstraction"; +qed_spec_mp"exec_frag_abstraction"; Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h"; @@ -80,7 +80,7 @@ by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1); (* is-execution-fragment *) -by (etac (exec_frag_abstraction RS spec RS mp) 1); +by (etac exec_frag_abstraction 1); by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); qed"abs_is_weakening"; @@ -185,6 +185,8 @@ by (pair_induct_tac "xs" [] 1); qed"traces_coincide_abs"; +(* +FIX: Is this needed anywhere? Goalw [cex_abs_def] "!!f.[| is_abstraction h C A |] ==>\ @@ -205,6 +207,7 @@ by (assume_tac 1); by (Asm_full_simp_tac 1); qed_spec_mp"correp_is_exec_abs"; +*) (* Does not work with abstraction_is_ref_map as proof of abs_safety, because is_live_abstraction includes temp_strengthening which is necessarily based @@ -232,7 +235,7 @@ by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1); (* is-execution-fragment *) - by (etac correp_is_exec_abs 1); + by (etac exec_frag_abstraction 1); by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); (* Liveness *) @@ -376,8 +379,8 @@ \ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"; by (rtac impI 1); by (Seq_Finite_induct_tac 1); +by (Blast_tac 1); (* main case *) -by (Blast_tac 1); by (clarify_tac set_cs 1); by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); @@ -489,7 +492,6 @@ by Auto_tac; qed"TLex2seq"; - Goal "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); @@ -497,7 +499,7 @@ by (Seq_case_simp_tac "s" 1); by (pair_tac "a" 1); qed"ex2seqUUTL"; - + Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1);