(* Title: HOLCF/IOA/TrivEx.thy ID: $Id: TrivEx.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"; 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";