src/HOLCF/IOA/ABP/Correctness.ML
changeset 14401 477380c74c1d
parent 13898 9410d2eb9563
child 14981 e73f8140af78
     1.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -41,26 +41,26 @@
     1.4  
     1.5  Goal "(reduce(l)=[]) = (l=[])";  
     1.6  by (induct_tac "l" 1);
     1.7 -by (auto_tac (claset(), simpset() addsplits [list.split]));
     1.8 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
     1.9  val l_iff_red_nil = result();
    1.10  
    1.11  Goal "s~=[] --> hd(s)=hd(reduce(s))";
    1.12  by (induct_tac "s" 1);
    1.13 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    1.14 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    1.15  qed"hd_is_reduce_hd";
    1.16  
    1.17  (* to be used in the following Lemma *)
    1.18  Goal "l~=[] --> reverse(reduce(l))~=[]";
    1.19  by (induct_tac "l" 1);
    1.20 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    1.21 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    1.22  qed_spec_mp "rev_red_not_nil";
    1.23  
    1.24  (* shows applicability of the induction hypothesis of the following Lemma 1 *)
    1.25  Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    1.26   by (Simp_tac 1);
    1.27 - by (asm_full_simp_tac (list_ss addsplits [list.split]
    1.28 + by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"]
    1.29                                  addsimps [reverse_Cons,hd_append,
    1.30 -					  rev_red_not_nil])  1);
    1.31 +					  rev_red_not_nil]));
    1.32  qed"last_ind_on_first";
    1.33  
    1.34  val impl_ss = simpset() delsimps [reduce_Cons];
    1.35 @@ -106,7 +106,7 @@
    1.36  by (cut_inst_tac [("l","s")] cons_not_nil 1);
    1.37  by (Asm_full_simp_tac 1);
    1.38  by (REPEAT (etac exE 1));
    1.39 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    1.40 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    1.41  val reduce_tl =result();
    1.42  
    1.43  
    1.44 @@ -145,12 +145,12 @@
    1.45  Addsplits [split_if]; 
    1.46  
    1.47  Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
    1.48 -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    1.49 +by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    1.50   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    1.51  qed"sender_abstraction";
    1.52  
    1.53  Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
    1.54 -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    1.55 +by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    1.56   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    1.57  qed"receiver_abstraction";
    1.58