(*  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";

 (*

 Goalw [xt2_def,plift,option_lift]

   "(xt2 (plift afun)) (s,a,t) = (afun a)";

 (* !!!!!!!!!!!!! Occurs check !!!! *)

 by (induct_tac "a" 1);

 *)

 Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,

            C_trans_def,trans_of_def] 

 "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";

 by Auto_tac;

 qed"Enabled_implication";

 Goalw [is_live_abstraction_def]

 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";

 by Auto_tac;

 (* is_abstraction *)

 by (rtac h_abs_is_abstraction 1);

 (* temp_weakening *)

 by (abstraction_tac 1);

 by (etac Enabled_implication 1);

 qed"h_abs_is_liveabstraction";

 Goalw [C_live_ioa_def]

 "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";

 by (rtac AbsRuleT2 1);

 by (rtac h_abs_is_liveabstraction 1);

 by (rtac MC_result 1);

 by (abstraction_tac 1);

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

 qed"TrivEx2_abstraction";

 (*

 Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) 

 IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";

 *)