# File TrivEx2.ML

    (*  Title:      HOLCF/IOA/TrivEx.thy
        ID:         $Id: TrivEx2.ML,v 1.5 2004/06/21 08:26:09 kleing Exp $
        Author:     Olaf Müller

    Trivial Abstraction Example.
    *)

    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))))";

    *)