src/HOL/TLA/Buffer/Buffer.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14396 011a2a49d303
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (* 
     2     File:        Buffer.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Simple FIFO buffer (theorems and proofs)
     7 *)
     8 
     9 (* ---------------------------- Data lemmas ---------------------------- *)
    10 
    11 (*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
    12 Goal "xs ~= [] --> tl xs ~= xs";
    13 by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
    14 qed_spec_mp "tl_not_self";
    15 context Buffer.thy;
    16 
    17 Addsimps [tl_not_self];
    18 
    19 (* ---------------------------- Action lemmas ---------------------------- *)
    20 
    21 (* Dequeue is visible *)
    22 Goalw [angle_def,Deq_def] "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
    23 by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
    24 qed "Deq_visible";
    25 
    26 (* Enabling condition for dequeue -- NOT NEEDED *)
    27 Goalw [temp_rewrite Deq_visible]
    28    "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])";
    29 by (force_tac (claset() addSEs [base_enabled,enabledE], 
    30                simpset() addsimps [Deq_def]) 1);
    31 qed "Deq_enabled";
    32 
    33 (* For the left-to-right implication, we don't need the base variable stuff *)
    34 Goalw [temp_rewrite Deq_visible] 
    35    "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])";
    36 by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def]));
    37 qed "Deq_enabledE";