(*  Title:      HOLCF/IOA/TrivEx.thy

     ID:         $Id$

     Author:     Olaf Mueller

     Copyright   1995  TU Muenchen

 Trivial Abstraction Example

 *)

 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";

   by (fast_tac (claset() addDs prems) 1);

 qed "imp_conj_lemma";

 Goalw [is_abstraction_def] 

 "is_abstraction h_abs C_ioa A_ioa";

 by (rtac conjI 1);

 (* ------------- start states ------------ *)

 by (simp_tac (simpset() addsimps 

     [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);

 (* -------------- step case ---------------- *)

 by (REPEAT (rtac allI 1));

 by (rtac imp_conj_lemma 1);

 by (simp_tac (simpset() addsimps [trans_of_def,

         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);

 by (induct_tac "a" 1);

 by (simp_tac (simpset() addsimps [h_abs_def]) 1);

 qed"h_abs_is_abstraction";

 Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";

 by (rtac AbsRuleT1 1);

 by (rtac h_abs_is_abstraction 1);

 by (rtac MC_result 1);

 by (abstraction_tac 1);

 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);

 qed"TrivEx_abstraction";