src/HOLCF/IOA/ex/TrivEx.ML
changeset 6470 f3015fd68d66
child 8600 a466c687c726
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Thu Apr 22 11:06:35 1999 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1995  TU Muenchen
     1.8 +
     1.9 +Trivial Abstraction Example
    1.10 +*)
    1.11 +
    1.12 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    1.13 +  by (fast_tac (claset() addDs prems) 1);
    1.14 +qed "imp_conj_lemma";
    1.15 +
    1.16 +
    1.17 +Goalw [is_abstraction_def] 
    1.18 +"is_abstraction h_abs C_ioa A_ioa";
    1.19 +by (rtac conjI 1);
    1.20 +(* ------------- start states ------------ *)
    1.21 +by (simp_tac (simpset() addsimps 
    1.22 +    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
    1.23 +(* -------------- step case ---------------- *)
    1.24 +by (REPEAT (rtac allI 1));
    1.25 +by (rtac imp_conj_lemma 1);
    1.26 +by (simp_tac (simpset() addsimps [trans_of_def,
    1.27 +        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    1.28 +by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    1.29 +by (induct_tac "a" 1);
    1.30 +by Auto_tac;
    1.31 +qed"h_abs_is_abstraction";
    1.32 +
    1.33 +
    1.34 +Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
    1.35 +by (rtac AbsRuleT1 1);
    1.36 +by (rtac h_abs_is_abstraction 1);
    1.37 +by (rtac MC_result 1);
    1.38 +by (abstraction_tac 1);
    1.39 +by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
    1.40 +qed"TrivEx_abstraction";
    1.41 +
    1.42 +