Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Constrains.thy Sprache: Isabelle

Original von: Isabelle^©

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

section\<open>Weak Safety Properties\<close>

theory Constrains
imports UNITY
begin

consts traces :: "[i, i] => i"
  (* Initial states and program => (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; \ 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)" \<subseteq> "Init(F) \<union> (\<Union>act\<in>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 \<open>Co\<close> 60)  where
  "A Co B == {F:program. F:(reachable(F) \ A) co B}"

definition
  op_Unless  :: "[i, i] => i"  (infixl \<open>Unless\<close> 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))"
apply (unfold 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. :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) \<subseteq> Acts(F)  |] ==> G \<in> 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))"
apply (unfold 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)}"
apply (unfold 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'"
apply (unfold 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 \<in> program|]
     ==> F \<in> 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"
apply (unfold 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'"
apply (unfold Constrains_def2)
apply (blast intro: constrains_weaken_R)
done

lemma Constrains_weaken_L:
    "[| F \ A Co A'; B<=A |] ==> F \ B Co A'"
apply (unfold 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'"
apply (unfold 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:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> 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')"
apply (unfold 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:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> 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'"
apply (unfold Constrains_def)
apply (blast dest: constrains_imp_subset)
done

lemma Constrains_trans:
"[| F \ A Co B; F \ B Co C |] ==> F \ A Co C"
apply (unfold 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')"
apply (unfold 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)"

apply (unfold 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')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Un)
done

lemma Stable_Int:
    "[| F \ Stable(A); F \ Stable(A') |] ==> F \ Stable (A \ A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Int)
done

lemma Stable_Constrains_Un:
    "[| F \ Stable(C); F \ A Co (C \ A') |]
     ==> F \<in> (C \<union> A) Co (C \<union> A')"
apply (unfold 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 \<in> (C \<inter> A) Co (C \<inter> A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
done

lemma Stable_UN:
    "[| (!!i. i \ I ==> F \ Stable(A(i))); F \ program |]
     ==> F \<in> Stable (\<Union>i \<in> 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 \<in> Stable (\<Inter>i \<in> 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"
apply (unfold Stable_def)
apply (rule Constrains_type)
done

(*** 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. ***)

lemma Elimination:
    "[| \m \ M. F \ ({s \ A. x(s) = m}) Co (B(m)); F \ program |]
     ==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> 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 \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))"
apply (blast intro: Elimination)
done

(** Unless **)

lemma Unless_type: "A Unless B <=program"
apply (unfold 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)"

apply (unfold 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)"
apply (unfold 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])

(* [| F \<in> Always(I);  F \<in> A Co A' |] ==> 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
\<open>
(*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 addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 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;
\<close>

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

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

end

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.