src/HOL/UNITY/Traces.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
open Traces;
paulson@4776
     2
paulson@4776
     3
goal thy "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}";
paulson@4776
     4
by (rtac subsetI 1);
paulson@4776
     5
be reachable.induct 1;
paulson@4776
     6
by (REPEAT (blast_tac (claset() addIs traces.intrs) 1));
paulson@4776
     7
val lemma1 = result();
paulson@4776
     8
paulson@4776
     9
goal thy "!!evs. evs : traces Init Acts \
paulson@4776
    10
\                ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts";
paulson@4776
    11
be traces.induct 1;
paulson@4776
    12
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
paulson@4776
    13
val lemma2 = normalize_thm [RSmp, RSspec] (result());
paulson@4776
    14
paulson@4776
    15
goal thy "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts";
paulson@4776
    16
by (blast_tac (claset() addIs [lemma2]) 1);
paulson@4776
    17
val lemma3 = result();
paulson@4776
    18
paulson@4776
    19
goal thy "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}";
paulson@4776
    20
by (rtac ([lemma1,lemma3] MRS equalityI) 1);
paulson@4776
    21
qed "reachable_eq_traces";
paulson@4776
    22
paulson@4776
    23
paulson@4776
    24
(*Could/should this be proved?*)
paulson@4776
    25
goal thy "reachable Init Acts = (UN evs: traces Init Acts. set evs)";
paulson@4776
    26
paulson@4776
    27
paulson@4776
    28
(*The strongest invariant is the set of all reachable states!*)
paulson@4776
    29
goalw thy [stable_def, constrains_def]
paulson@4776
    30
    "!!A. [| Init<=A;  stable Acts A |] ==> reachable Init Acts <= A";
paulson@4776
    31
by (rtac subsetI 1);
paulson@4776
    32
be reachable.induct 1;
paulson@4776
    33
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
paulson@4776
    34
qed "strongest_invariant";
paulson@4776
    35
paulson@4776
    36
goal thy "stable Acts (reachable Init Acts)";
paulson@4776
    37
by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
paulson@4776
    38
				addIs reachable.intrs) 1));
paulson@4776
    39
qed "stable_reachable";