src/HOLCF/IOA/ex/TrivEx.ML
author wenzelm
Thu Nov 15 23:25:46 2001 +0100 (2001-11-15)
changeset 12218 6597093b77e7
parent 8600 a466c687c726
child 13524 604d0f3622d6
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/IOA/TrivEx.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Trivial Abstraction Example.
     7 *)
     8 
     9 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    10   by (fast_tac (claset() addDs prems) 1);
    11 qed "imp_conj_lemma";
    12 
    13 
    14 Goalw [is_abstraction_def] 
    15 "is_abstraction h_abs C_ioa A_ioa";
    16 by (rtac conjI 1);
    17 (* ------------- start states ------------ *)
    18 by (simp_tac (simpset() addsimps 
    19     [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
    20 (* -------------- step case ---------------- *)
    21 by (REPEAT (rtac allI 1));
    22 by (rtac imp_conj_lemma 1);
    23 by (simp_tac (simpset() addsimps [trans_of_def,
    24         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    25 by (induct_tac "a" 1);
    26 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    27 qed"h_abs_is_abstraction";
    28 
    29 
    30 Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
    31 by (rtac AbsRuleT1 1);
    32 by (rtac h_abs_is_abstraction 1);
    33 by (rtac MC_result 1);
    34 by (abstraction_tac 1);
    35 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
    36 qed"TrivEx_abstraction";
    37 
    38