src/HOL/UNITY/Traces.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5423 c57c87628bb4
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     1 (*  Title:      HOL/UNITY/Traces
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Definitions of
     7   * traces: the possible execution traces
     8   * reachable: the set of reachable states
     9 
    10 *)
    11 
    12 Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
    13 by Safe_tac;
    14 by (etac traces.induct 2);
    15 be reachable.induct 1;
    16 by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
    17 qed "reachable_equiv_traces";
    18 
    19 Goal "acts <= Acts prg ==> stable acts (reachable prg)";
    20 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
    21 qed "stable_reachable";
    22