src/HOL/IOA/ABP/Correctness.ML

 (* 3 thms that do not hold generally! The lucky restriction here is 
    the absence of internal actions. *)
 goal Correctness.thy 
       "is_weak_pmap (%id.id) sender_ioa sender_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
-(* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)

 
 (* 2 copies of before *)
 goal Correctness.thy 
       "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
- (* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)

 qed"receiver_unchanged";
 
 goal Correctness.thy 
       "is_weak_pmap (%id.id) env_ioa env_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
-(* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)