src/ZF/UNITY/Constrains.ML

Comments

(*  Title:      ZF/UNITY/Constrains.ML
    ID:         $Id \\<in> Constrains.ML,v 1.10 2003/06/20 10:10:45 paulson Exp $
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Safety relations \\<in> restricted to the set of reachable states.

Proofs ported from HOL.
*)

(*** traces and reachable ***)

Goal  "reachable(F) <= state";
by (cut_inst_tac [("F", "F")] Init_type 1);
by (cut_inst_tac [("F", "F")] Acts_type 1);
by (cut_inst_tac [("F", "F")] reachable.dom_subset 1);
by (Blast_tac 1);
qed "reachable_type";

Goalw [st_set_def] "st_set(reachable(F))";
by (rtac reachable_type 1);
qed "st_set_reachable";
AddIffs [st_set_reachable];

Goal "reachable(F) Int state = reachable(F)";
by (cut_facts_tac [reachable_type] 1);
by Auto_tac;
qed "reachable_Int_state";
AddIffs [reachable_Int_state];

Goal "state Int reachable(F) = reachable(F)";
by (cut_facts_tac [reachable_type] 1);
by Auto_tac;
qed "state_Int_reachable";
AddIffs [state_Int_reachable];

Goal 
"F \\<in> program ==> reachable(F)={s \\<in> state. \\<exists>evs. <s,evs>:traces(Init(F), Acts(F))}";
by (rtac equalityI 1);
by Safe_tac;
by (blast_tac (claset() addDs [reachable_type RS subsetD]) 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 \\<in> program; G \\<in> program; \
\   Acts(G) <= Acts(F)  |] ==> G \\<in> stable(reachable(F))";
by (blast_tac (claset() 
   addIs [stableI, constrainsI, st_setI,
          reachable_type RS subsetD] @ 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 \\<in> program ==> F \\<in> invariant(reachable(F))";
by (blast_tac (claset() addIs [reachable_type RS subsetD]@reachable.intrs) 1);
qed "invariant_reachable";

(*...in fact the strongest invariant!*)
Goal "F \\<in> invariant(A) ==> reachable(F) <= A";
by (cut_inst_tac [("F", "F")] Acts_type 1);
by (cut_inst_tac [("F", "F")] Init_type 1);
by (cut_inst_tac [("F", "F")] reachable_type 1);
by (full_simp_tac (simpset() addsimps [stable_def, constrains_def, 
                                       invariant_def, initially_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 ***)

Goal "F \\<in> B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')";
by (forward_tac [constrains_type RS subsetD] 1);
by (forward_tac [[asm_rl, asm_rl, subset_refl] MRS stable_reachable] 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [stable_def, constrains_Int])));
qed "constrains_reachable_Int";

(*Resembles the previous definition of Constrains*)
Goalw [Constrains_def]
"A Co B = {F \\<in> program. F:(reachable(F) Int A) co (reachable(F)  Int  B)}";
by (blast_tac (claset() addDs [constrains_reachable_Int, 
                                      constrains_type RS subsetD]
                        addIs [constrains_weaken]) 1);
qed "Constrains_eq_constrains";
val Constrains_def2 =  Constrains_eq_constrains RS  eq_reflection;

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

val prems = Goalw [Constrains_def, constrains_def, st_set_def]
"[|(!!act s s'. [| act \\<in> Acts(F); <s,s'>:act; s \\<in> A |] ==> s':A'); F \\<in> program|]==>F \\<in> A Co A'";
by (auto_tac (claset(), simpset() addsimps prems));
by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1);
qed "ConstrainsI";

Goalw [Constrains_def] 
 "A Co B <= program";
by (Blast_tac 1);
qed "Constrains_type";

Goal "F \\<in> 0 Co B <-> F \\<in> program";
by (auto_tac (claset() addDs [Constrains_type RS subsetD]
                       addIs [constrains_imp_Constrains], simpset()));
qed "Constrains_empty";
AddIffs [Constrains_empty];

Goalw [Constrains_def] "F \\<in> A Co state <-> F \\<in> program";
by (auto_tac (claset() addDs [Constrains_type RS subsetD]
                       addIs [constrains_imp_Constrains], simpset()));
qed "Constrains_state";
AddIffs [Constrains_state];

Goalw  [Constrains_def2] 
        "[| F \\<in> A Co A'; A'<=B' |] ==> F \\<in> A Co B'";
by (blast_tac (claset()  addIs [constrains_weaken_R]) 1);
qed "Constrains_weaken_R";

Goalw  [Constrains_def2] 
    "[| F \\<in> A Co A'; B<=A |] ==> F \\<in> B Co A'";
by (blast_tac (claset() addIs [constrains_weaken_L, st_set_subset]) 1);
qed "Constrains_weaken_L";  

Goalw [Constrains_def2]
   "[| F \\<in> A Co A'; B<=A; A'<=B' |] ==> F \\<in> B Co B'";
by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1);
qed "Constrains_weaken";

(** Union **)
Goalw [Constrains_def2] 
"[| F \\<in> A Co A'; F \\<in> B Co B' |] ==> F \\<in> (A Un B) Co (A' Un B')";
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "Constrains_Un";

val [major, minor] = Goalw [Constrains_def2]
"[|(!!i. i \\<in> I==>F \\<in> A(i) Co A'(i)); F \\<in> program|] ==> F:(\\<Union>i \\<in> I. A(i)) Co (\\<Union>i \\<in> I. A'(i))";
by (cut_facts_tac [minor] 1);
by (auto_tac (claset() addDs [major]
                       addIs [constrains_UN],
              simpset() delsimps UN_simps addsimps [Int_UN_distrib]));
qed "Constrains_UN";

(** Intersection **)

Goalw [Constrains_def]
"[| F \\<in> A Co A'; F \\<in> B Co B'|]==> F:(A Int B) Co (A' Int B')";
by (subgoal_tac "reachable(F) Int (A Int B) = \
              \ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
by (ALLGOALS(force_tac (claset() addIs [constrains_Int], simpset())));
qed "Constrains_Int";

val [major,minor] = Goal 
"[| (!!i. i \\<in> I ==>F \\<in> A(i) Co A'(i)); F \\<in> program  |] \
\  ==> F:(\\<Inter>i \\<in> I. A(i)) Co (\\<Inter>i \\<in> I. A'(i))";
by (cut_facts_tac [minor] 1);
by (asm_simp_tac (simpset() delsimps INT_simps
	  	 	    addsimps [Constrains_def]@INT_extend_simps) 1);
by (rtac constrains_INT 1);
by (dtac major 1);
by (auto_tac (claset(), simpset() addsimps [Constrains_def])); 
qed "Constrains_INT";

Goalw [Constrains_def] "F \\<in> A Co A' ==> reachable(F) Int A <= A'";
by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
qed "Constrains_imp_subset";

Goalw [Constrains_def2]
 "[| F \\<in> A Co B; F \\<in> B Co C |] ==> F \\<in> A Co C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";

Goalw [Constrains_def2]
"[| F \\<in> A Co (A' Un B); F \\<in> B Co B' |] ==> F \\<in> A Co (A' Un B')";
by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [constrains_cancel]) 1);
qed "Constrains_cancel";

(*** Stable ***)
(* Useful because there's no Stable_weaken.  [Tanja Vos] *)

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

Goal "[| F \\<in> Stable(A); A = B |] ==> F \\<in> Stable(B)";
by (Blast_tac 1);
qed "Stable_eq";

Goal
"F \\<in> Stable(A) <->  (F \\<in> stable(reachable(F) Int A))";
by (auto_tac (claset() addDs [constrainsD2], 
              simpset() addsimps [Stable_def, stable_def, Constrains_def2]));
qed "Stable_eq_stable";

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

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

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

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

Goalw [Stable_def]
    "[| F \\<in> Stable(C); F \\<in> A Co (C Un A') |]   \
\    ==> F \\<in> (C Un A) Co (C Un A')";
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
qed "Stable_Constrains_Un";

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

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

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

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

Goalw [Stable_def]
"Stable(A) <= program";
by (rtac Constrains_type 1);
qed "Stable_type";

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

Goalw [Constrains_def]  
"[| \\<forall>m \\<in> M. F \\<in> ({s \\<in> A. x(s) = m}) Co (B(m)); F \\<in> program |] \
\    ==> F \\<in> ({s \\<in> A. x(s):M}) Co (\\<Union>m \\<in> M. B(m))";
by Auto_tac;
by (res_inst_tac [("A1","reachable(F)Int A")] (elimination RS constrains_weaken_L) 1);
by (auto_tac (claset() addIs [constrains_weaken_L], simpset()));
qed "Elimination";

(* As above, but for the special case of A=state *)
Goal
 "[| \\<forall>m \\<in> M. F \\<in> {s \\<in> state. x(s) = m} Co B(m); F \\<in> program |] \
\    ==> F \\<in> {s \\<in> state. x(s):M} Co (\\<Union>m \\<in> M. B(m))";
by (blast_tac (claset() addIs [Elimination]) 1);
qed "Elimination2";

(** Unless **)

Goalw [Unless_def] "A Unless B <=program";
by (rtac Constrains_type 1);
qed "Unless_type";

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

(** Natural deduction rules for "Always A" **)

Goalw [Always_def, initially_def]
"[| Init(F)<=A;  F \\<in> Stable(A) |] ==> F \\<in> Always(A)";
by (forward_tac [Stable_type RS subsetD] 1);
by Auto_tac;
qed "AlwaysI";

Goal "F \\<in> Always(A) ==> Init(F)<=A & F \\<in> Stable(A)";
by (asm_full_simp_tac (simpset() addsimps [Always_def, initially_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 \\<in> Always(A) ==> reachable(F) <= A";
by (full_simp_tac (simpset() addsimps 
        [Stable_def, Constrains_def, constrains_def, Always_def, initially_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_def, invariant_def, Stable_def, stable_def]
     "F \\<in> invariant(A) ==> F \\<in> 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 \\<in> program. F \\<in> invariant(reachable(F) Int A)}";
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 
                                  Constrains_def2, stable_def, initially_def]) 1);
by (rtac equalityI 1);
by (ALLGOALS(Clarify_tac));
by (REPEAT(blast_tac (claset() 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 \\<in> program. reachable(F) <= A}";
by (rtac 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, initially_def] "Always(A) <= program";
by Auto_tac;
qed "Always_type";

Goal "Always(state) = program";
by (rtac equalityI 1);
by (auto_tac (claset() addDs [Always_type RS subsetD, 
                              reachable_type RS subsetD], 
              simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_state_eq";
Addsimps [Always_state_eq];

Goal "F \\<in> program ==> F \\<in> Always(state)";
by (auto_tac (claset() addDs [reachable_type RS subsetD], simpset() 
    addsimps [Always_eq_includes_reachable]));
qed "state_AlwaysI";

Goal "st_set(A) ==> Always(A) = (\\<Union>I \\<in> 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 [invariant_type RS subsetD]) 1));
qed "Always_eq_UN_invariant";

Goal "[| F \\<in> Always(A); A <= B |] ==> F \\<in> 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 \\<in> Always(I) ==> (F:(I Int A) Co A') <-> (F \\<in> A Co A')";
by (asm_simp_tac
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
                         Constrains_def, Int_assoc RS sym]) 1);
qed "Always_Constrains_pre";

Goal "F \\<in> Always(I) ==> (F \\<in> A Co (I Int A')) <->(F \\<in> A Co A')";
by (asm_simp_tac
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
                         Constrains_eq_constrains, Int_assoc RS sym]) 1);
qed "Always_Constrains_post";

Goal "[| F \\<in> Always(I);  F \\<in> (I Int A) Co A' |] ==> F \\<in> A Co A'";
by (blast_tac (claset() addIs [Always_Constrains_pre RS iffD1]) 1);
qed "Always_ConstrainsI";

(* [| F \\<in> Always(I);  F \\<in> A Co A' |] ==> F \\<in> A Co (I Int A') *)
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);

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

(** Conjoining Always properties **)
Goal "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 \\<in> I is need since \\<Inter>is formally not defined for I=0 *)
Goal "i \\<in> I==>Always(\\<Inter>i \\<in> I. A(i)) = (\\<Inter>i \\<in> I. Always(A(i)))";
by (rtac equalityI 1);
by (auto_tac (claset(), simpset() addsimps
              [Inter_iff, Always_eq_includes_reachable]));
qed "Always_INT_distrib";


Goal "[| F \\<in> Always(A);  F \\<in> Always(B) |] ==> F \\<in> Always(A Int B)";
by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1);
qed "Always_Int_I";

(*Allows a kind of "implication introduction"*)
Goal "[| F \\<in> Always(A) |] ==> (F \\<in> Always(C-A Un B)) <-> (F \\<in> Always(B))";
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_Diff_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 \\<in> 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);

(*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 gen_constrains_tac(cs,ss) 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,
              (* Three subgoals *)
              rewrite_goal_tac [st_set_def] 3,
              REPEAT (Force_tac 2),
              full_simp_tac (ss addsimps !program_defs_ref) 1,
              ALLGOALS (clarify_tac cs),
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS Clarify_tac,
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS (clarify_tac cs),
              ALLGOALS (asm_full_simp_tac ss),
              ALLGOALS (clarify_tac cs)]) i;

fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;

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