src/HOL/UNITY/Traces.ML

Constant "invariant" and new constrains_tac, ensures_tac

(*  Title:      HOL/UNITY/Traces
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Definitions of
  * traces: the possible execution traces
  * reachable: the set of reachable states

*)

(****
Now simulate the inductive definition (illegal due to paired arguments)

inductive "reachable(Init,Acts)"
  intrs 
    Init  "s: Init ==> s : reachable(Init,Acts)"

    Acts  "[| act: Acts;  s : reachable(Init,Acts);  (s,s'): act |]
	   ==> s' : reachable(Init,Acts)"

This amounts to an equivalence proof for the definition actually used, 
****)


(** reachable: Deriving the Introduction rules **)

Goal "s: Init ==> s : reachable(Init,Acts)";
by (simp_tac (simpset() addsimps [reachable_def]) 1);
by (blast_tac (claset() addIs traces.intrs) 1);
qed "reachable_Init";


Goal "[| act: Acts;  s : reachable(Init,Acts) |] \
\     ==> (s,s'): act --> s' : reachable(Init,Acts)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac exE 1);
by (etac traces.induct 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (blast_tac (claset() addIs traces.intrs)));
qed_spec_mp "reachable_Acts";


val major::prems = 
Goalw [reachable_def] 
  "[| za : reachable(Init,Acts);  \
\     !!s. s : Init ==> P s;      \
\     !!act s s'.  \
\        [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |]  \
\        ==> P s' |] \
\  ==> P za";
by (cut_facts_tac [major] 1);
by Auto_tac;
by (etac traces.induct 1);
by (ALLGOALS (blast_tac (claset() addIs prems)));
qed "reachable_induct";

structure reachable = 
  struct 
  val Init = reachable_Init
  val Acts = reachable_Acts
  val intrs = [reachable_Init, reachable_Acts]
  val induct = reachable_induct
  end;



Goal "stable Acts (reachable(Init,Acts))";
by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
qed "stable_reachable";

(*The set of all reachable states is an invariant...*)
Goal "invariant (Init,Acts) (reachable(Init,Acts))";
by (simp_tac (simpset() addsimps [invariant_def]) 1);
by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
qed "invariant_reachable";

(*...in fact the strongest invariant!*)
Goal "invariant (Init,Acts) A ==> reachable(Init,Acts) <= A";
by (full_simp_tac 
    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
by (rtac subsetI 1);
by (etac reachable.induct 1);
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "invariant_includes_reachable";

(*If "A" includes the initial states and is stable then "A" is invariant.
  Result is trivial from the definition, but it is handy.*)
Goal "[| Init<=A;  stable Acts A |] ==> invariant (Init,Acts) A";
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
qed "invariantI";


(** Conjoining invariants **)

Goal "[| invariant (Init,Acts) A;  invariant (Init,Acts) B |] \
\     ==> invariant (Init,Acts) (A Int B)";
by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1);
by Auto_tac;
qed "invariant_Int";

(*Delete the nearest invariance assumption (which will be the second one
  used by invariant_Int) *)
val invariant_thin =
    read_instantiate_sg (sign_of thy)
                [("V", "invariant ?Prg ?A")] thin_rl;

(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
val invariant_Int_tac = dtac invariant_Int THEN' 
                        assume_tac THEN'
			etac invariant_thin;

(*Combines two invariance THEOREMS into one.*)
val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int);