Quelle  Constrains.thy   Sprache: Isabelle

(*  Title:      ZF/UNITY/Constrains.thy
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge
*)

section‹Weak Safety Properties›

theory Constrains
imports UNITY
begin

consts traces :: "[i, i] \ i"
  (* Initial states and program \<Rightarrow> (final state, reversed trace to it)... 
      the domain may also be state*list(state) *)
inductive 
  domains 
     "traces(init, acts)" <=
         "(init \ (\act\acts. field(act)))*list(\act\acts. field(act))"
  intros 
         (*Initial trace is empty*)
    Init: "s: init \ \ traces(init,acts)"

    Acts: "\act:acts; \s,evs\ \ traces(init,acts); : act\
           ==> <s', Cons(s,evs)> \ traces(init, acts)"
  
  type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1


consts reachable :: "i\i"
inductive
  domains
  "reachable(F)" ⊆ "Init(F) \ (\act\Acts(F). field(act))"
  intros 
    Init: "s:Init(F) \ s:reachable(F)"

    Acts: "\act: Acts(F); s:reachable(F); : act\
           ==> s':reachable(F)"

  type_intros UnI1 UnI2 fieldI2 UN_I

  
definition
  Constrains :: "[i,i] \ i"  (infixl ‹Co› 60)  where
  "A Co B \ {F:program. F:(reachable(F) \ A) co B}"

definition
  op_Unless  :: "[i, i] \ i"  (infixl ‹Unless› 60)  where
  "A Unless B \ (A-B) Co (A \ B)"

definition
  Stable     :: "i \ i"  where
  "Stable(A) \ A Co A"

definition
  (*Always is the weak form of "invariant"*)
  Always :: "i \ i"  where
  "Always(A) \ initially(A) \ Stable(A)"


(*** traces and reachable ***)

lemma reachable_type: "reachable(F) \ state"
apply (cut_tac F = F in Init_type)
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = F in reachable.dom_subset, blast)
done

lemma st_set_reachable: "st_set(reachable(F))"
  unfolding st_set_def
apply (rule reachable_type)
done
declare st_set_reachable [iff]

lemma reachable_Int_state: "reachable(F) \ state = reachable(F)"
by (cut_tac reachable_type, auto)
declare reachable_Int_state [iff]

lemma state_Int_reachable: "state \ reachable(F) = reachable(F)"
by (cut_tac reachable_type, auto)
declare state_Int_reachable [iff]

lemma reachable_equiv_traces: 
"F \ program \ reachable(F)={s \ state. \evs. \s,evs\:traces(Init(F), Acts(F))}"
apply (rule equalityI, safe)
apply (blast dest: reachable_type [THEN subsetD])
apply (erule_tac [2] traces.induct)
apply (erule reachable.induct)
apply (blast intro: reachable.intros traces.intros)+
done

lemma Init_into_reachable: "Init(F) \ reachable(F)"
by (blast intro: reachable.intros)

lemma stable_reachable: "\F \ program; G \ program;
    Acts(G) ⊆ Acts(F)] ==> G ∈ stable(reachable(F))"
apply (blast intro: stableI constrainsI st_setI
             reachable_type [THEN subsetD] reachable.intros)
done

declare stable_reachable [intro!]
declare stable_reachable [simp]

(*The set of all reachable states is an invariant...*)
lemma invariant_reachable: 
   "F \ program \ F \ invariant(reachable(F))"
  unfolding invariant_def initially_def
apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
done

(*...in fact the strongest invariant!*)
lemma invariant_includes_reachable: "F \ invariant(A) \ reachable(F) \ A"
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = F in Init_type)
apply (cut_tac F = F in reachable_type)
apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def)
apply (rule subsetI)
apply (erule reachable.induct)
apply (blast intro: reachable.intros)+
done

(*** Co ***)

lemma constrains_reachable_Int: "F \ B co B'\F:(reachable(F) \ B) co (reachable(F) \ B')"
apply (frule constrains_type [THEN subsetD])
apply (frule stable_reachable [OF _ _ subset_refl])
apply (simp_all add: stable_def constrains_Int)
done

(*Resembles the previous definition of Constrains*)
lemma Constrains_eq_constrains: 
"A Co B = {F \ program. F:(reachable(F) \ A) co (reachable(F) \ B)}"
  unfolding Constrains_def
apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
             intro: constrains_weaken)
done

lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]

lemma constrains_imp_Constrains: "F \ A co A' \ F \ A Co A'"
  unfolding Constrains_def
apply (blast intro: constrains_weaken_L dest: constrainsD2)
done

lemma ConstrainsI: 
    "\\act s s'. \act \ Acts(F); :act; s \ A\ \ s':A';
       F ∈ program]
     ==> F ∈ A Co A'"
apply (auto simp add: Constrains_def constrains_def st_set_def)
apply (blast dest: reachable_type [THEN subsetD])
done

lemma Constrains_type: 
 "A Co B \ program"
apply (unfold Constrains_def, blast)
done

lemma Constrains_empty: "F \ 0 Co B \ F \ program"
by (auto dest: Constrains_type [THEN subsetD]
            intro: constrains_imp_Constrains)
declare Constrains_empty [iff]

lemma Constrains_state: "F \ A Co state \ F \ program"
  unfolding Constrains_def
apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
done
declare Constrains_state [iff]

lemma Constrains_weaken_R: 
        "\F \ A Co A'; A'<=B'\ \ F \ A Co B'"
  unfolding Constrains_def2
apply (blast intro: constrains_weaken_R)
done

lemma Constrains_weaken_L: 
    "\F \ A Co A'; B<=A\ \ F \ B Co A'"
  unfolding Constrains_def2
apply (blast intro: constrains_weaken_L st_set_subset)
done

lemma Constrains_weaken: 
   "\F \ A Co A'; B<=A; A'<=B'\ \ F \ B Co B'"
  unfolding Constrains_def2
apply (blast intro: constrains_weaken st_set_subset)
done

(** Union **)
lemma Constrains_Un: 
    "\F \ A Co A'; F \ B Co B'\ \ F \ (A \ B) Co (A' \ B')"
apply (unfold Constrains_def2, auto)
apply (simp add: Int_Un_distrib)
apply (blast intro: constrains_Un)
done

lemma Constrains_UN: 
    "\(\i. i \ I\F \ A(i) Co A'(i)); F \ program\
     ==> F:(∪i ∈ I. A(i)) Co (∪i ∈ I. A'(i))"
by (auto intro: constrains_UN simp del: UN_simps 
         simp add: Constrains_def2 Int_UN_distrib)


(** Intersection **)

lemma Constrains_Int: 
    "\F \ A Co A'; F \ B Co B'\\ F:(A \ B) Co (A' \ B')"
  unfolding Constrains_def
apply (subgoal_tac "reachable (F) \ (A \ B) = (reachable (F) \ A) \ (reachable (F) \ B) ")
apply (auto intro: constrains_Int)
done

lemma Constrains_INT: 
    "\(\i. i \ I \F \ A(i) Co A'(i)); F \ program\
     ==> F:(∩i ∈ I. A(i)) Co (∩i ∈ I. A'(i))"
apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps)
apply (rule constrains_INT)
apply (auto simp add: Constrains_def)
done

lemma Constrains_imp_subset: "F \ A Co A' \ reachable(F) \ A \ A'"
  unfolding Constrains_def
apply (blast dest: constrains_imp_subset)
done

lemma Constrains_trans: 
 "\F \ A Co B; F \ B Co C\ \ F \ A Co C"
  unfolding Constrains_def2
apply (blast intro: constrains_trans constrains_weaken)
done

lemma Constrains_cancel: 
"\F \ A Co (A' \ B); F \ B Co B'\ \ F \ A Co (A' \ B')"
  unfolding Constrains_def2
apply (simp (no_asm_use) add: Int_Un_distrib)
apply (blast intro: constrains_cancel)
done

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

lemma stable_imp_Stable: 
"F \ stable(A) \ F \ Stable(A)"

  unfolding stable_def Stable_def
apply (erule constrains_imp_Constrains)
done

lemma Stable_eq: "\F \ Stable(A); A = B\ \ F \ Stable(B)"
by blast

lemma Stable_eq_stable: 
"F \ Stable(A) \ (F \ stable(reachable(F) \ A))"
apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2)
done

lemma StableI: "F \ A Co A \ F \ Stable(A)"
by (unfold Stable_def, assumption)

lemma StableD: "F \ Stable(A) \ F \ A Co A"
by (unfold Stable_def, assumption)

lemma Stable_Un: 
    "\F \ Stable(A); F \ Stable(A')\ \ F \ Stable(A \ A')"
  unfolding Stable_def
apply (blast intro: Constrains_Un)
done

lemma Stable_Int: 
    "\F \ Stable(A); F \ Stable(A')\ \ F \ Stable (A \ A')"
  unfolding Stable_def
apply (blast intro: Constrains_Int)
done

lemma Stable_Constrains_Un: 
    "\F \ Stable(C); F \ A Co (C \ A')\
     ==> F ∈ (C ∪ A) Co (C ∪ A')"
  unfolding Stable_def
apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
done

lemma Stable_Constrains_Int: 
    "\F \ Stable(C); F \ (C \ A) Co A'\
     ==> F ∈ (C ∩ A) Co (C ∩ A')"
  unfolding Stable_def
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
done

lemma Stable_UN: 
    "\(\i. i \ I \ F \ Stable(A(i))); F \ program\
     ==> F ∈ Stable (∪i ∈ I. A(i))"
apply (simp add: Stable_def)
apply (blast intro: Constrains_UN)
done

lemma Stable_INT: 
    "\(\i. i \ I \ F \ Stable(A(i))); F \ program\
     ==> F ∈ Stable (∩i ∈ I. A(i))"
apply (simp add: Stable_def)
apply (blast intro: Constrains_INT)
done

lemma Stable_reachable: "F \ program \F \ Stable (reachable(F))"
apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb)
done

lemma Stable_type: "Stable(A) \ program"
  unfolding Stable_def
apply (rule Constrains_type)
done

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

lemma Elimination: 
    "\\m \ M. F \ ({s \ A. x(s) = m}) Co (B(m)); F \ program\
     ==> F ∈ ({s ∈ A. x(s):M}) Co (∪m ∈ M. B(m))"
apply (unfold Constrains_def, auto)
apply (rule_tac A1 = "reachable (F) \ A" 
        in UNITY.elimination [THEN constrains_weaken_L])
apply (auto intro: constrains_weaken_L)
done

(* As above, but for the special case of A=state *)
lemma Elimination2: 
 "\\m \ M. F \ {s \ state. x(s) = m} Co B(m); F \ program\
     ==> F ∈ {s ∈ state. x(s):M} Co (∪m ∈ M. B(m))"
apply (blast intro: Elimination)
done

(** Unless **)

lemma Unless_type: "A Unless B <=program"
  unfolding op_Unless_def
apply (rule Constrains_type)
done

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

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

lemma AlwaysI: 
"\Init(F)<=A; F \ Stable(A)\ \ F \ Always(A)"

  unfolding Always_def initially_def
apply (frule Stable_type [THEN subsetD], auto)
done

lemma AlwaysD: "F \ Always(A) \ Init(F)<=A \ F \ Stable(A)"
by (simp add: Always_def initially_def)

lemmas AlwaysE = AlwaysD [THEN conjE]
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]

(*The set of all reachable states is Always*)
lemma Always_includes_reachable: "F \ Always(A) \ reachable(F) \ A"
apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def)
apply (rule subsetI)
apply (erule reachable.induct)
apply (blast intro: reachable.intros)+
done

lemma invariant_imp_Always: 
     "F \ invariant(A) \ F \ Always(A)"
  unfolding Always_def invariant_def Stable_def stable_def
apply (blast intro: constrains_imp_Constrains)
done

lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]

lemma Always_eq_invariant_reachable: "Always(A) = {F \ program. F \ invariant(reachable(F) \ A)}"
apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
apply (rule equalityI, auto) 
apply (blast intro: reachable.intros reachable_type)
done

(*the RHS is the traditional definition of the "always" operator*)
lemma Always_eq_includes_reachable: "Always(A) = {F \ program. reachable(F) \ A}"
apply (rule equalityI, safe)
apply (auto dest: invariant_includes_reachable 
   simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable)
done

lemma Always_type: "Always(A) \ program"
by (unfold Always_def initially_def, auto)

lemma Always_state_eq: "Always(state) = program"
apply (rule equalityI)
apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD]
            simp add: Always_eq_includes_reachable)
done
declare Always_state_eq [simp]

lemma state_AlwaysI: "F \ program \ F \ Always(state)"
by (auto dest: reachable_type [THEN subsetD]
            simp add: Always_eq_includes_reachable)

lemma Always_eq_UN_invariant: "st_set(A) \ Always(A) = (\I \ Pow(A). invariant(I))"
apply (simp (no_asm) add: Always_eq_includes_reachable)
apply (rule equalityI, auto) 
apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable] 
                    rev_subsetD [OF _ invariant_includes_reachable]  
             dest: invariant_type [THEN subsetD])+
done

lemma Always_weaken: "\F \ Always(A); A \ B\ \ F \ Always(B)"
by (auto simp add: Always_eq_includes_reachable)


(*** "Co" rules involving Always ***)
lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp]

lemma Always_Constrains_pre: "F \ Always(I) \ (F:(I \ A) Co A') \ (F \ A Co A')"
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric])
done

lemma Always_Constrains_post: "F \ Always(I) \ (F \ A Co (I \ A')) \(F \ A Co A')"
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric])
done

lemma Always_ConstrainsI: "\F \ Always(I); F \ (I \ A) Co A'\ \ F \ A Co A'"
by (blast intro: Always_Constrains_pre [THEN iffD1])

(* \<lbrakk>F \<in> Always(I);  F \<in> A Co A'\<rbrakk> \<Longrightarrow> F \<in> A Co (I \<inter> A') *)
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]

(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
lemma Always_Constrains_weaken: 
"\F \ Always(C); F \ A Co A'; C \ B<=A; C \ A'<=B'\\F \ B Co B'"
apply (rule Always_ConstrainsI)
apply (drule_tac [2] Always_ConstrainsD, simp_all) 
apply (blast intro: Constrains_weaken)
done

(** Conjoining Always properties **)
lemma Always_Int_distrib: "Always(A \ B) = Always(A) \ Always(B)"
by (auto simp add: Always_eq_includes_reachable)

(* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *)
lemma Always_INT_distrib: "i \ I\Always(\i \ I. A(i)) = (\i \ I. Always(A(i)))"
apply (rule equalityI)
apply (auto simp add: Inter_iff Always_eq_includes_reachable)
done


lemma Always_Int_I: "\F \ Always(A); F \ Always(B)\ \ F \ Always(A \ B)"
apply (simp (no_asm_simp) add: Always_Int_distrib)
done

(*Allows a kind of "implication introduction"*)
lemma Always_Diff_Un_eq: "\F \ Always(A)\ \ (F \ Always(C-A \ B)) \ (F \ Always(B))"
by (auto simp add: Always_eq_includes_reachable)

(*Delete the nearest invariance assumption (which will be the second one
  used by Always_Int_I) *)
lemmas Always_thin = thin_rl [of "F \ Always(A)"] for F A

(*To allow expansion of the program's definition when appropriate*)
named_theorems program "program definitions"

ML
‹
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
fun Always_Int_tac ctxt =
  dresolve_tac ctxt @{thms Always_Int_I} THEN'
  assume_tac ctxt THEN'
  eresolve_tac ctxt @{thms Always_thin};

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

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

fun constrains_tac ctxt =
   SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac ctxt 1),
              REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
                      ORELSE
                      resolve_tac ctxt [@{thm StableI}, @{thm stableI},
                                   @{thm constrains_imp_Constrains}] 1),
              resolve_tac ctxt @{thms constrainsI} 1,
              (* Three subgoals *)
              rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
              REPEAT (force_tac ctxt 2),
              full_simp_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt 🍋‹program›)) 1,
              ALLGOALS (clarify_tac ctxt),
              REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
              ALLGOALS (clarify_tac ctxt),
              REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
              ALLGOALS (clarify_tac ctxt),
              ALLGOALS (asm_full_simp_tac ctxt),
              ALLGOALS (clarify_tac ctxt)]);

(*For proving invariants*)
fun always_tac ctxt i =
  resolve_tac ctxt @{thms AlwaysI} i THEN
  force_tac ctxt i
  THEN constrains_tac ctxt i;
›

method_setup safety = ‹
  Scan.succeed (SIMPLE_METHOD' o constrains_tac)\
  "for proving safety properties"

method_setup always = ‹
  Scan.succeed (SIMPLE_METHOD' o always_tac)\
  "for proving invariants"

end