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