src/HOL/UNITY/Traces.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5423 c57c87628bb4
     1.1 --- a/src/HOL/UNITY/Traces.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -16,59 +16,7 @@
     1.4  by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
     1.5  qed "reachable_equiv_traces";
     1.6  
     1.7 -Goal "stable (Acts prg) (reachable prg)";
     1.8 +Goal "acts <= Acts prg ==> stable acts (reachable prg)";
     1.9  by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
    1.10  qed "stable_reachable";
    1.11  
    1.12 -(*The set of all reachable states is an invariant...*)
    1.13 -Goal "invariant prg (reachable prg)";
    1.14 -by (simp_tac (simpset() addsimps [invariant_def]) 1);
    1.15 -by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
    1.16 -qed "invariant_reachable";
    1.17 -
    1.18 -(*...in fact the strongest invariant!*)
    1.19 -Goal "invariant prg A ==> reachable prg <= A";
    1.20 -by (full_simp_tac 
    1.21 -    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
    1.22 -by (rtac subsetI 1);
    1.23 -by (etac reachable.induct 1);
    1.24 -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
    1.25 -qed "invariant_includes_reachable";
    1.26 -
    1.27 -
    1.28 -(** Natural deduction rules for "invariant prg A" **)
    1.29 -
    1.30 -Goal "[| (Init prg)<=A;  stable (Acts prg) A |] ==> invariant prg A";
    1.31 -by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
    1.32 -qed "invariantI";
    1.33 -
    1.34 -Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
    1.35 -by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
    1.36 -qed "invariantD";
    1.37 -
    1.38 -bind_thm ("invariantE", invariantD RS conjE);
    1.39 -
    1.40 -
    1.41 -(** Conjoining invariants **)
    1.42 -
    1.43 -Goal "[| invariant prg A;  invariant prg B |] \
    1.44 -\     ==> invariant prg (A Int B)";
    1.45 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1);
    1.46 -by Auto_tac;
    1.47 -qed "invariant_Int";
    1.48 -
    1.49 -(*Delete the nearest invariance assumption (which will be the second one
    1.50 -  used by invariant_Int) *)
    1.51 -val invariant_thin =
    1.52 -    read_instantiate_sg (sign_of thy)
    1.53 -                [("V", "invariant ?Prg ?A")] thin_rl;
    1.54 -
    1.55 -(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    1.56 -val invariant_Int_tac = dtac invariant_Int THEN' 
    1.57 -                        assume_tac THEN'
    1.58 -			etac invariant_thin;
    1.59 -
    1.60 -(*Combines two invariance THEOREMS into one.*)
    1.61 -val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int);
    1.62 -
    1.63 -