src/HOLCF/IOA/ABP/Correctness.ML

  by (rtac (split_list_case RS iffD2) 1);
  by (Asm_full_simp_tac 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
  by (hyp_subst_tac 1);
- by (stac expand_if 1);
+ by (stac split_if 1);
  by (Asm_full_simp_tac 1);
  by (Asm_full_simp_tac 1);
 val l_iff_red_nil = result();
 
 goal Correctness.thy "s~=[] --> hd(s)=hd(reduce(s))";

 by (Simp_tac 1);
 by (rtac (split_list_case RS iffD2) 1);
 by (asm_full_simp_tac list_ss 1);
 by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
-by (stac expand_if 1);
+by (stac split_if 1);
 by (REPEAT(hyp_subst_tac 1));
 by (etac subst 1);
 by (Simp_tac 1);
 qed"hd_is_reduce_hd";
 

 by (Asm_full_simp_tac 1);
 by (cut_inst_tac [("l","list")] cons_not_nil 1); 
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
 by (Asm_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
 qed"rev_red_not_nil";
 
 (* shows applicability of the induction hypothesis of the following Lemma 1 *)

  by (Simp_tac 1);
  by (rtac (split_list_case RS iffD2) 1);
  by (asm_full_simp_tac list_ss 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
- by (stac expand_if 1);
+ by (stac split_if 1);
  by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
                           (rev_red_not_nil RS mp)])  1);
 qed"last_ind_on_first";
 
 val impl_ss = simpset() delsimps [reduce_Cons];

 (* Main Lemma 1 for S_pkt in showing that reduce is refinement  *) 
 goal Correctness.thy 
    "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
 \      reduce(l@[x])=reduce(l) else                  \
 \      reduce(l@[x])=reduce(l)@[x]"; 
-by (stac expand_if 1);
+by (stac split_if 1);
 by (rtac conjI 1);
 (* --> *)
 by (List.list.induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);

 by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
 by (List.list.induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);
 by (cut_inst_tac [("l","list")] cons_not_nil 2);
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (auto_tac (claset(), 
 	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
-                      setloop split_tac [expand_if]));
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+                      setloop split_tac [split_if]));
+by (Asm_full_simp_tac 1);
 qed"reduce_hd";
 
 
 (* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
 goal Correctness.thy 

 \      reduce(tl(s))=tl(reduce(s))"; 
 by (cut_inst_tac [("l","s")] cons_not_nil 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
 by (Asm_full_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
 by (rtac conjI 1);
 by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
 by (Step_tac 1);
 by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
 by (Auto_tac);

 
 (*******************************************************************
           C h a n n e l   A b s t r a c t i o n
  *******************************************************************)
 
-Delsplits [expand_if];
+Delsplits [split_if];
 goal Correctness.thy 
       "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
 (* ---------------- main-part ------------------- *)
 by (REPEAT (rtac allI 1));

 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"sender_unchanged";
 
 (* 2 copies of before *)
 goal Correctness.thy 
       "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";

 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"receiver_unchanged";
 
 goal Correctness.thy 
       "is_weak_ref_map (%id. id) env_ioa env_ioa";
 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);

 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"env_unchanged";
-Addsplits [expand_if];
+Addsplits [split_if];
 
 goal Correctness.thy "compatible srch_ioa rsch_ioa"; 
 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
 by (rtac set_ext 1);
 by (Action.action.induct_tac "x" 1);