--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ex/TrivEx.ML Thu Apr 22 11:06:35 1999 +0200
@@ -0,0 +1,39 @@
+(* 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 (induct_tac "a" 1);
+by Auto_tac;
+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";
+
+