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
paulson@5111
     1
(*  Title:      HOL/UNITY/Traces
paulson@5111
     2
    ID:         $Id$
paulson@5111
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5111
     4
    Copyright   1998  University of Cambridge
paulson@5111
     5
paulson@5111
     6
Definitions of
paulson@5111
     7
  * traces: the possible execution traces
paulson@5111
     8
  * reachable: the set of reachable states
paulson@5111
     9
paulson@5111
    10
*)
paulson@5111
    11
paulson@5253
    12
Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
paulson@5253
    13
by Safe_tac;
paulson@5253
    14
by (etac traces.induct 2);
paulson@5253
    15
be reachable.induct 1;
paulson@5253
    16
by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
paulson@5253
    17
qed "reachable_equiv_traces";
paulson@4776
    18
paulson@5313
    19
Goal "acts <= Acts prg ==> stable acts (reachable prg)";
paulson@5240
    20
by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
paulson@5240
    21
qed "stable_reachable";
paulson@5240
    22