--- a/src/HOLCF/IOA/ex/TrivEx2.ML Sat May 27 21:00:31 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(* Title: HOLCF/IOA/TrivEx.thy
- ID: $Id$
- Author: Olaf Mueller
-
-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))))";
-
-*)
-