(* 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 (simp_tac (simpset() addsimps [h_abs_def]) 1);
by (action.induct_tac "a" 1);
auto();
qed"h_abs_is_abstraction";
(*
Goalw [xt2_def,plift,option_lift]
"(xt2 (plift afun)) (s,a,t) = (afun a)";
(* !!!!!!!!!!!!! Occurs check !!!! *)
by (option.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";
auto();
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})";
auto();
(* is_abstraction *)
br h_abs_is_abstraction 1;
(* temp_weakening *)
by (abstraction_tac 1);
be Enabled_implication 1;
qed"h_abs_is_liveabstraction";
Goalw [C_live_ioa_def]
"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
br AbsRuleT2 1;
br h_abs_is_liveabstraction 1;
br 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))))";
*)