src/ZF/UNITY/Constrains.ML

new ZF/UNITY theory

(*  Title:      ZF/UNITY/Constrains.ML
    ID:         $Id$
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Safety relations: restricted to the set of reachable states.

Proofs ported from HOL.
*)

(*** traces and reachable ***)

Goalw [condition_def]
  "reachable(F):condition";
by (auto_tac (claset() addSDs [reachable.dom_subset RS subsetD]
                       addDs [InitD, ActsD], simpset()));
qed "reachable_type";
Addsimps [reachable_type];
AddIs [reachable_type];

Goal "x:reachable(F) ==> x:state";
by (cut_inst_tac [("F", "F")] reachable_type 1);
by (auto_tac (claset(), simpset() addsimps [condition_def]));
qed "reachableD";

Goal "F:program ==> \
\   reachable(F) = {s:state. EX evs. <s,evs>: traces(Init(F), Acts(F))}";
by (rtac equalityI 1);
by Safe_tac;
by (blast_tac (claset() addDs [reachableD]) 1);
by (etac traces.induct 2);
by (etac reachable.induct 1);
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
qed "reachable_equiv_traces";

Goal "Init(F) <= reachable(F)";
by (blast_tac (claset() addIs reachable.intrs) 1);
qed "Init_into_reachable";

Goal "[| F:program; G:program; \
\   Acts(G) <= Acts(F)  |] ==> G:stable(reachable(F))";
by (blast_tac (claset() 
   addIs [stableI, constrainsI, reachable_type] @ reachable.intrs) 1);
qed "stable_reachable";

AddSIs [stable_reachable];
Addsimps [stable_reachable];

(*The set of all reachable states is an invariant...*)
Goalw [invariant_def, initially_def]
   "F:program ==> F:invariant(reachable(F))";
by (blast_tac (claset() addIs [reachable_type]@reachable.intrs) 1);
qed "invariant_reachable";

(*...in fact the strongest invariant!*)
Goal "F : invariant(A) ==> reachable(F) <= 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";

(*** Co ***)

(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
val lemma = subset_refl RSN (3, rewrite_rule 
            [stable_def] stable_reachable RS constrains_Int);
Goal "F:B co B' ==> F: (reachable(F) Int B) co (reachable(F) Int B')";
by (blast_tac (claset() addSIs [lemma]
                        addDs [constrainsD2]) 1);
qed "constrains_reachable_Int";

(*Resembles the previous definition of Constrains*)
Goalw [Constrains_def]
     "A Co B = \
\ {F:program. F : (reachable(F)  Int  A) co (reachable(F)  Int  B) & \
\  A:condition & B:condition}";
by (rtac equalityI 1);
by (ALLGOALS(Clarify_tac));
by (subgoal_tac "reachable(x) Int B:condition" 2);
by (blast_tac (claset() addDs [constrains_reachable_Int]
                        addIs [constrains_weaken]) 2);
by (subgoal_tac "reachable(x) Int B:condition" 1);
by (blast_tac (claset() addDs [constrains_reachable_Int]
                        addIs [constrains_weaken]) 1);
by (REPEAT(blast_tac (claset() addIs [reachable_type]) 1));
qed "Constrains_eq_constrains";

Goalw [Constrains_def] 
 "F : A co A' ==> F : A Co A'";
by (blast_tac (claset() addIs [constrains_weaken_L]
                        addDs [constrainsD2]) 1);
qed "constrains_imp_Constrains";

Goalw [stable_def, Stable_def] 
"F : stable(A) ==> F : Stable(A)";
by (etac constrains_imp_Constrains 1);
qed "stable_imp_Stable";


val prems = Goal
    "[|(!!act s s'. [| act: Acts(F);  <s,s'>:act; s:A |] \
\  ==> s':A');  F:program; A:condition; A':condition |]  ==> F:A Co A'";
by (rtac constrains_imp_Constrains 1);
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
qed "ConstrainsI";

Goalw [Constrains_def] 
 "F:A Co B ==> F:program & A:condition & B:condition";
by (Blast_tac 1);
qed "ConstrainsD";

Goal "[| F:program; B:condition |] ==> F : 0 Co B";
by (blast_tac (claset() addIs 
        [constrains_imp_Constrains, constrains_empty]) 1);
qed "Constrains_empty";

Goal "[| F:program; A:condition |] ==> F : A Co state";
by (blast_tac (claset() addIs 
       [constrains_imp_Constrains, constrains_state2]) 1);
qed "Constrains_state";
Addsimps [Constrains_empty, Constrains_state];

val Constrains_def2 =  Constrains_eq_constrains RS  eq_reflection;

Goalw  [Constrains_def2] 
        "[| F : A Co A'; A'<=B'; B':condition |] ==> F : A Co B'";
by (Clarify_tac 1);
by (blast_tac (claset() 
     addIs [reachable_type, constrains_weaken_R]) 1);
qed "Constrains_weaken_R";


Goalw [condition_def]
   "[| A<=B; B:condition |] ==>A:condition";
by (Blast_tac 1);
qed "condition_subset_mono";


Goalw  [Constrains_def2] 
    "[| F : A Co A'; B<=A |] ==> F : B Co A'";
by (Clarify_tac 1);
by (forward_tac [condition_subset_mono] 1);
by (assume_tac 1);
by (blast_tac (claset() 
     addIs [reachable_type, constrains_weaken_L]) 1);
qed "Constrains_weaken_L";  

Goalw [Constrains_def]
   "[| F : A Co A'; B<=A; A'<=B'; B':condition |] ==> F : B Co B'";
by (Clarify_tac 1);
by (forward_tac [condition_subset_mono] 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [reachable_type, constrains_weaken]) 1);
qed "Constrains_weaken";

(** Union **)

Goalw [Constrains_def2]
    "[| F : A Co A'; F : B Co B' |]   \
\    ==> F : (A Un B) Co (A' Un B')";
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "Constrains_Un";

Goalw [Constrains_def2]
     "[| F:program; \
\     ALL i:I. F : A(i) Co A'(i)  |] \
\     ==> F : (UN i:I. A(i)) Co (UN i:I. A'(i))";
by (rtac CollectI 1);
by Safe_tac;
by (simp_tac (simpset() addsimps [Int_UN_distrib]) 1);
by (blast_tac (claset() addIs [constrains_UN, CollectD2 RS conjunct1]) 1);
by (rewrite_goals_tac [condition_def]);
by (ALLGOALS(Blast_tac));
qed "Constrains_UN";

(** Intersection **)

Goal "A Int (B Int C) = (A Int B) Int (A Int C)";
by (Blast_tac 1);
qed "Int_duplicate";

Goalw [Constrains_def]
    "[| F : A Co A'; F : B Co B' |]   \
\    ==> F : (A Int B) Co (A' Int B')";
by (Step_tac 1);
by (subgoal_tac "reachable(F) Int (A Int B) = \
                 \ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
by (Blast_tac 2);
by (Asm_simp_tac 1);
by (rtac constrains_Int  1);
by (ALLGOALS(Asm_simp_tac));
qed "Constrains_Int";

Goal 
     "[| F:program; \
\         ALL i:I. F: A(i) Co A'(i)  |] \
\     ==> F : (INT i:I. A(i)) Co (INT i:I. A'(i))";
by (case_tac "I=0" 1);
by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 2);
by (Blast_tac 2);
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (Step_tac 1);
by (rtac constrains_INT 1);
by (ALLGOALS(Asm_full_simp_tac));
by (ALLGOALS(Blast_tac));
qed "Constrains_INT";

Goal "F : A Co A' ==> reachable(F) Int A <= A'";
by (asm_full_simp_tac (simpset() addsimps 
          [Constrains_def, reachable_type]) 1);
by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
qed "Constrains_imp_subset";

Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";

Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
by (full_simp_tac (simpset()
    addsimps [Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1);
by (Step_tac 1);
by (blast_tac (claset() addIs [constrains_cancel]) 1);
qed "Constrains_cancel";

(*** Stable ***)

(*Useful because there's no Stable_weaken.  [Tanja Vos]*)
Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)";
by (Blast_tac 1);
qed "Stable_eq";

Goal "A:condition ==> F : Stable(A) <->  (F : stable(reachable(F) Int A))";
by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, 
                                  stable_def]) 1);
by (blast_tac (claset() addDs [constrainsD2]) 1);
qed "Stable_eq_stable";

Goalw [Stable_def] "F : A Co A ==> F : Stable(A)";
by (assume_tac 1);
qed "StableI";

Goalw [Stable_def] "F : Stable(A) ==> F : A Co A";
by (assume_tac 1);
qed "StableD";

Goalw [Stable_def]
    "[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')";
by (blast_tac (claset() addIs [Constrains_Un]) 1);
qed "Stable_Un";

Goalw [Stable_def]
    "[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')";
by (blast_tac (claset() addIs [Constrains_Int]) 1);
qed "Stable_Int";

Goalw [Stable_def]
    "[| F : Stable(C); F : A Co (C Un A') |]   \
\    ==> F : (C Un A) Co (C Un A')";
by (subgoal_tac "C Un A' :condition & C Un A:condition" 1);
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
by (blast_tac (claset() addDs [ConstrainsD]) 1);
qed "Stable_Constrains_Un";


Goalw [Stable_def]
    "[| F : Stable(C); F : (C Int A) Co A' |]   \
\    ==> F : (C Int A) Co (C Int A')";
by (blast_tac (claset() addDs [ConstrainsD]
            addIs [Constrains_Int RS Constrains_weaken]) 1);
qed "Stable_Constrains_Int";

val [major, prem] = Goalw [Stable_def]
    "[| F:program; \
\       (!!i. i:I ==> F : Stable(A(i))) |]==> F : Stable (UN i:I. A(i))";
by (cut_facts_tac [major] 1);
by (blast_tac (claset() addIs [major, Constrains_UN, prem]) 1);
qed "Stable_UN";

val [major, prem] = Goalw [Stable_def]
    "[| F:program; \
\       (!!i. i:I ==> F:Stable(A(i))) |]==> F : Stable (INT i:I. A(i))";
by (cut_facts_tac [major] 1);
by (blast_tac (claset() addIs [major, Constrains_INT, prem]) 1);
qed "Stable_INT";

Goal "F:program ==>F : Stable (reachable(F))";
by (asm_simp_tac (simpset() 
    addsimps [Stable_eq_stable, Int_absorb, subset_refl]) 1);
qed "Stable_reachable";

Goalw [Stable_def]
"F:Stable(A) ==> F:program & A:condition";
by (blast_tac (claset() addDs [ConstrainsD]) 1);
qed "StableD2";

(*** The Elimination Theorem.  The "free" m has become universally quantified!
     Should the premise be !!m instead of ALL m ?  Would make it harder to use
     in forward proof. ***)

Goalw [condition_def]
  "Collect(state,P):condition";
by Auto_tac;
qed "Collect_in_condition";
AddIffs [Collect_in_condition];

Goalw [Constrains_def]  
    "[| ALL m:M. F : {s:S. x(s) = m} Co B(m); F:program |] \
\    ==> F : {s:S. x(s):M} Co (UN m:M. B(m))";
by Safe_tac;
by (res_inst_tac [("S1", "reachable(F) Int S")]
             (elimination RS constrains_weaken_L) 1);
by Auto_tac;
by (rtac constrains_weaken_L 1);
by (auto_tac (claset(), simpset() addsimps [condition_def]));
qed "Elimination";

(* As above, but for the special case of S=state *)

Goal
 "[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \
\    ==> F : {s:state. x(s):M} Co (UN m:M. B(m))";
by (blast_tac (claset() addIs [Elimination]) 1);
qed "Elimination2";

(** Unless **)

Goalw [Unless_def]
"F:A Unless B ==> F:program & A:condition & B:condition";
by (blast_tac (claset() addDs [ConstrainsD]) 1);
qed "UnlessD";

(*** Specialized laws for handling Always ***)

(** Natural deduction rules for "Always A" **)
Goalw [Always_def, initially_def]
      "Always(A) = initially(A) Int Stable(A)";
by (blast_tac (claset() addDs [StableD2]) 1);
qed "Always_eq";

val Always_def2 = Always_eq RS eq_reflection;

Goalw [Always_def]
"[| Init(F)<=A;  F : Stable(A) |] ==> F : Always(A)";
by (asm_simp_tac (simpset() addsimps [StableD2]) 1);
qed "AlwaysI";

Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)";
by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
qed "AlwaysD";

bind_thm ("AlwaysE", AlwaysD RS conjE);
bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);


(*The set of all reachable states is Always*)
Goal "F : Always(A) ==> reachable(F) <= A";
by (full_simp_tac 
    (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
                         Always_def]) 1);
by (rtac subsetI 1);
by (etac reachable.induct 1);
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "Always_includes_reachable";

Goalw [Always_def2, invariant_def2, Stable_def, stable_def]
     "F : invariant(A) ==> F : Always(A)";
by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
qed "invariant_imp_Always";

bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);

Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A) & A:condition}";
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 
                                  Constrains_eq_constrains, stable_def]) 1);
by (rtac equalityI 1);
by (ALLGOALS(Clarify_tac));
by (REPEAT(blast_tac (claset() addDs [constrainsD] 
                        addIs reachable.intrs@[reachable_type]) 1));
qed "Always_eq_invariant_reachable";

(*the RHS is the traditional definition of the "always" operator*)
Goal "Always(A) = {F:program. reachable(F) <= A & A:condition}";
br equalityI 1;
by (ALLGOALS(Clarify_tac));
by (auto_tac (claset() addDs [invariant_includes_reachable],
              simpset() addsimps [subset_Int_iff, invariant_reachable,
                                  Always_eq_invariant_reachable]));
qed "Always_eq_includes_reachable";

Goalw [Always_def]
"F:Always(A)==> F:program & A:condition";
by (blast_tac (claset() addDs [StableD2]) 1);
qed "AlwaysD2";

Goal "Always(state) = program";
br equalityI 1;
by (ALLGOALS(Clarify_tac));
by (blast_tac (claset() addDs [AlwaysD2]) 1);
by (auto_tac (claset() addDs [reachableD], 
             simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_state_eq";
Addsimps [Always_state_eq];

Goal "[| state <= A; F:program; A:condition |] ==> F : Always(A)";
by (auto_tac (claset(), simpset() 
    addsimps [Always_eq_includes_reachable]));
by (auto_tac (claset() addSDs [reachableD],  
              simpset() addsimps [condition_def]));
qed "state_AlwaysI";

Goal "A:condition ==> Always(A) = (UN I: Pow(A). invariant(I))";
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
by (rtac equalityI 1);
by (ALLGOALS(Clarify_tac));
by (REPEAT(blast_tac (claset() 
         addIs [invariantI, impOfSubs Init_into_reachable, 
         impOfSubs invariant_includes_reachable]
                        addDs [invariantD2]) 1));
qed "Always_eq_UN_invariant";

Goal "[| F : Always(A); A <= B; B:condition |] ==> F : Always(B)";
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_weaken";


(*** "Co" rules involving Always ***)
val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp;

Goal "[| F:Always(INV); A:condition |] \
 \  ==> (F:(INV Int A) Co A') <-> (F : A Co A')";
by (asm_simp_tac
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
                         Constrains_def, Int_assoc RS sym]) 1);
by (blast_tac (claset() addDs [AlwaysD2]) 1);
qed "Always_Constrains_pre";

Goal "[| F : Always(INV); A':condition |] \
\  ==> (F : A Co (INV Int A')) <->(F : A Co A')";
by (asm_simp_tac
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
                         Constrains_eq_constrains, Int_assoc RS sym]) 1);
by (blast_tac (claset() addDs [AlwaysD2]) 1);
qed "Always_Constrains_post";

(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);

(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);

(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
Goal "[| F : Always(C);  F : A Co A';   \
\        C Int B <= A;   C Int A' <= B'; B:condition; B':condition |] \
\     ==> F : B Co B'";
by (rtac Always_ConstrainsI 1);
by (assume_tac 1);
by (assume_tac 1);
by (dtac Always_ConstrainsD 1);
by (assume_tac 2);
by (blast_tac (claset() addDs [ConstrainsD]) 1);
by (blast_tac (claset() addIs [Constrains_weaken]) 1);
qed "Always_Constrains_weaken";


(** Conjoining Always properties **)

Goal "[| A:condition; B:condition |] ==> \
\ Always(A Int B) = Always(A) Int Always(B)";
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_Int_distrib";

(* the premise i:I is need since INT is formally not defined for I=0 *)
Goal "[| i:I; ALL i:I. A(i):condition |] \
\  ==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))";
by (rtac equalityI 1);
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_INT_distrib";


Goal "[| F : Always(A);  F : Always(B) |] ==> F : Always(A Int B)";
by (asm_simp_tac (simpset() addsimps
                 [Always_Int_distrib,AlwaysD2]) 1);
qed "Always_Int_I";

(*Allows a kind of "implication introduction"*)
Goal "F : Always(A) ==> (F : Always (state-A Un B)) <-> (F : Always(B))";
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_Compl_Un_eq";

(*Delete the nearest invariance assumption (which will be the second one
  used by Always_Int_I) *)
val Always_thin =
    read_instantiate_sg (sign_of thy)
                [("V", "?F : Always(?A)")] thin_rl;

(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;

(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);

(*** Increasing ***)

Goalw [Increasing_on_def]
"[| F:Increasing_on(A, f, r); a:A |] ==> F: Stable({s:state. <a,f`s>:r})";
by (Blast_tac 1);
qed "Increasing_onD";

Goalw [Increasing_on_def]
"F:Increasing_on(A, f, r) ==> F:program & f:state->A & part_order(A,r)";
by (auto_tac (claset(), simpset() addsimps [INT_iff]));
qed "Increasing_onD2";

Goalw [Increasing_on_def, Stable_def, Constrains_def, stable_def, constrains_def, part_order_def]
     "!!f. g:mono_map(A,r,A,r) \
\  ==> Increasing_on(A, f, r) <= Increasing_on(A, g O f, r)";
by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
by (force_tac (claset() addSDs [bspec, ActsD],  simpset()) 1);
by (subgoal_tac "xd:state" 1);
by (blast_tac (claset() addSDs [ActsD]) 2);
by (subgoal_tac "f`xe:A & f`xd:A" 1);
by (blast_tac (claset() addDs [apply_type]) 2);
by (rotate_tac 3 1);
by (dres_inst_tac [("x", "f`xe")] bspec 1);
by (Asm_simp_tac 1);
by (REPEAT(etac conjE 1));
by (rotate_tac ~3 1);
by (dres_inst_tac [("x", "xc")] bspec 1);
by (Asm_simp_tac 1);
by (dres_inst_tac [("c", "xd")] subsetD 1);
by (rtac imageI 1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
by (dres_inst_tac [("x", "f`xe")] bspec 1);
by (dres_inst_tac [("x", "f`xd")] bspec 2);
by (ALLGOALS(Asm_simp_tac));
by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
by Auto_tac;
qed "mono_Increasing_on_comp";

Goalw [increasing_on_def, Increasing_on_def]
     "F : increasing_on(A, f,r) ==> F : Increasing_on(A, f,r)";
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
qed "increasing_on_imp_Increasing_on";

bind_thm("Increasing_on_constant",  increasing_on_constant RS increasing_on_imp_Increasing_on);
Addsimps [Increasing_on_constant];

Goalw [Increasing_on_def, nat_order_def]
     "[| F:Increasing_on(nat,f, nat_order); z:nat |] \
\  ==> F: Stable({s:state. z < f`s})";
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
by Safe_tac;
by (dres_inst_tac [("x", "succ(z)")] bspec 1);
by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
by (subgoal_tac "{x: state . f ` x : nat} = state" 1);
by Auto_tac;
qed "strict_Increasing_onD";

(*To allow expansion of the program's definition when appropriate*)
val program_defs_ref = ref ([] : thm list);

(*proves "co" properties when the program is specified*)

fun constrains_tac i = 
   SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac 1),
              REPEAT (etac Always_ConstrainsI 1
                      ORELSE
                      resolve_tac [StableI, stableI,
                                   constrains_imp_Constrains] 1),
              rtac constrainsI 1,
              full_simp_tac (simpset() addsimps !program_defs_ref) 1,
              ALLGOALS Clarify_tac,
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS Clarify_tac,
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS Clarify_tac,
              ALLGOALS Asm_full_simp_tac,
              ALLGOALS Clarify_tac]) i;

(*For proving invariants*)
fun always_tac i = 
    rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;