Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/Metis/src/ (Wiener Entwicklungsmethode ^©) Datei vom 16.11.2025 mit Größe 9 kB

Quelle Constrains.thy Sprache: Isabelle

(*  Title:      HOL/UNITY/Constrains.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Weak safety relations: restricted to the set of reachable states.
*)

section\<open>Weak Safety\<close>

theory Constrains imports UNITY begin

  (*Initial states and program => (final state, reversed trace to it)...
    Arguments MUST be curried in an inductive definition*)

inductive_set
  traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
  for init :: "'a set" and acts :: "('a * 'a)set set"
  where
         (*Initial trace is empty*)
    Init:  "s \ init ==> (s,[]) \ traces init acts"

  | Acts:  "[| act \ acts; (s,evs) \ traces init acts; (s,s') \ act |]
            ==> (s', s#evs) \ traces init acts"

inductive_set
  reachable :: "'a program => 'a set"
  for F :: "'a program"
  where
    Init:  "s \ Init F ==> s \ reachable F"

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

definition Constrains :: "['a set, 'a set] => 'a program set" (infixl \<open>Co\<close> 60) where
    "A Co B == {F. F \ (reachable F \ A) co B}"

definition Unless  :: "['a set, 'a set] => 'a program set" (infixl \<open>Unless\<close> 60) where
    "A Unless B == (A-B) Co (A \ B)"

definition Stable     :: "'a set => 'a program set" where
    "Stable A == A Co A"

  (*Always is the weak form of "invariant"*)
definition Always :: "'a set => 'a program set" where
    "Always A == {F. Init F \ A} \ Stable A"

  (*Polymorphic in both states and the meaning of \<le> *)
definition Increasing :: "['a => 'b::{order}] => 'a program set" where
    "Increasing f == \z. Stable {s. z \ f s}"

subsection\<open>traces and reachable\<close>

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

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

lemma stable_reachable [intro!,simp]:
     "Acts G \ Acts F ==> G \ stable (reachable F)"
by (blast intro: stableI constrainsI reachable.intros)

(*The set of all reachable states is an invariant...*)
lemma invariant_reachable: "F \ invariant (reachable F)"
apply (simp add: invariant_def)
apply (blast intro: reachable.intros)
done

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

subsection\<open>Co\<close>

(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
lemmas constrains_reachable_Int =
    subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]

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

lemma constrains_imp_Constrains: "F \ A co A' ==> F \ A Co A'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_L)
done

lemma stable_imp_Stable: "F \ stable A ==> F \ Stable A"
apply (unfold stable_def Stable_def)
apply (erule constrains_imp_Constrains)
done

lemma ConstrainsI:
    "(!!act s s'. [| act \ Acts F; (s,s') \ act; s \ A |] ==> s' \ A')
     ==> F \<in> A Co A'"
apply (rule constrains_imp_Constrains)
apply (blast intro: constrainsI)
done

lemma Constrains_empty [iff]: "F \ {} Co B"
by (unfold Constrains_def constrains_def, blast)

lemma Constrains_UNIV [iff]: "F \ A Co UNIV"
by (blast intro: ConstrainsI)

lemma Constrains_weaken_R:
    "[| F \ A Co A'; A'<=B' |] ==> F \ A Co B'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_R)
done

lemma Constrains_weaken_L:
    "[| F \ A Co A'; B \ A |] ==> F \ B Co A'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_L)
done

lemma Constrains_weaken:
   "[| F \ A Co A'; B \ A; A'<=B' |] ==> F \ B Co B'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken)
done

(** Union **)

lemma Constrains_Un:
    "[| F \ A Co A'; F \ B Co B' |] ==> F \ (A \ B) Co (A' \ B')"
apply (unfold Constrains_def)
apply (blast intro: constrains_Un [THEN constrains_weaken])
done

lemma Constrains_UN:
  assumes Co: "!!i. i \ I ==> F \ (A i) Co (A' i)"
  shows "F \ (\i \ I. A i) Co (\i \ I. A' i)"
apply (unfold Constrains_def)
apply (rule CollectI)
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN,
                THEN constrains_weaken],   auto)
done

(** Intersection **)

lemma Constrains_Int:
    "[| F \ A Co A'; F \ B Co B' |] ==> F \ (A \ B) Co (A' \ B')"
apply (unfold Constrains_def)
apply (blast intro: constrains_Int [THEN constrains_weaken])
done

lemma Constrains_INT:
  assumes Co: "!!i. i \ I ==> F \ (A i) Co (A' i)"
  shows "F \ (\i \ I. A i) Co (\i \ I. A' i)"
apply (unfold Constrains_def)
apply (rule CollectI)
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT,
                THEN constrains_weaken],   auto)
done

lemma Constrains_imp_subset: "F \ A Co A' ==> reachable F \ A \ A'"
by (simp add: constrains_imp_subset Constrains_def)

lemma Constrains_trans: "[| F \ A Co B; F \ B Co C |] ==> F \ A Co C"
apply (simp add: Constrains_eq_constrains)
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 (simp add: Constrains_eq_constrains constrains_def)
apply best
done

subsection\<open>Stable\<close>

(*Useful because there's no Stable_weaken.  [Tanja Vos]*)
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))"
by (simp add: Stable_def Constrains_eq_constrains stable_def)

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])
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 \ Stable (\i \ I. A i)"
by (simp add: Stable_def Constrains_UN)

lemma Stable_INT:
    "(!!i. i \ I ==> F \ Stable (A i)) ==> F \ Stable (\i \ I. A i)"
by (simp add: Stable_def Constrains_INT)

lemma Stable_reachable: "F \ Stable (reachable F)"
by (simp add: Stable_eq_stable)

subsection\<open>Increasing\<close>

lemma IncreasingD:
     "F \ Increasing f ==> F \ Stable {s. x \ f s}"
by (unfold Increasing_def, blast)

lemma mono_Increasing_o:
     "mono g ==> Increasing f \ Increasing (g o f)"
apply (simp add: Increasing_def Stable_def Constrains_def stable_def
                 constrains_def)
apply (blast intro: monoD order_trans)
done

lemma strict_IncreasingD:
     "!!z::nat. F \ Increasing f ==> F \ Stable {s. z < f s}"
by (simp add: Increasing_def Suc_le_eq [symmetric])

lemma increasing_imp_Increasing:
     "F \ increasing f ==> F \ Increasing f"
apply (unfold increasing_def Increasing_def)
apply (blast intro: stable_imp_Stable)
done

lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]

subsection\<open>The Elimination Theorem\<close>

(*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. F \ {s. s x = m} Co (B m) |]
     ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)"
by (unfold Constrains_def constrains_def, blast)

(*As above, but for the trivial case of a one-variable state, in which the
  state is identified with its one variable.*)
lemma Elimination_sing:
    "(\m. F \ {m} Co (B m)) ==> F \ M Co (\m \ M. B m)"
by (unfold Constrains_def constrains_def, blast)

subsection\<open>Specialized laws for handling Always\<close>

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

lemma AlwaysI: "[| Init F \ A; F \ Stable A |] ==> F \ Always A"
by (simp add: Always_def)

lemma AlwaysD: "F \ Always A ==> Init F \ A & F \ Stable A"
by (simp add: Always_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 add: Stable_def Constrains_def constrains_def Always_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. F \ invariant (reachable F \ A)}"
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
                 stable_def)
apply (blast intro: reachable.intros)
done

(*the RHS is the traditional definition of the "always" operator*)
lemma Always_eq_includes_reachable: "Always A = {F. reachable F \ A}"
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)

lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
by (auto simp add: Always_eq_includes_reachable)

lemma UNIV_AlwaysI: "UNIV \ A ==> F \ Always A"
by (auto simp add: Always_eq_includes_reachable)

lemma Always_eq_UN_invariant: "Always A = (\I \ Pow A. invariant I)"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD]
                    invariant_includes_reachable [THEN subsetD])
done

lemma Always_weaken: "[| F \ Always A; A \ B |] ==> F \ Always B"
by (auto simp add: Always_eq_includes_reachable)

subsection\<open>"Co" rules involving Always\<close>

lemma Always_Constrains_pre:
     "F \ Always INV ==> (F \ (INV \ A) Co A') = (F \ A Co A')"
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def
              Int_assoc [symmetric])

lemma Always_Constrains_post:
     "F \ Always INV ==> (F \ A Co (INV \ A')) = (F \ A Co A')"
by (simp add: Always_includes_reachable [THEN Int_absorb2]
              Constrains_eq_constrains Int_assoc [symmetric])

(* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]

(* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<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 \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]
      ==> F \<in> B Co B'"
apply (rule Always_ConstrainsI, assumption)
apply (drule Always_ConstrainsD, assumption)
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)

lemma Always_INT_distrib: "Always (\(A ` I)) = (\i \ I. Always (A i))"
by (auto simp add: Always_eq_includes_reachable)

lemma Always_Int_I:
     "[| F \ Always A; F \ Always B |] ==> F \ Always (A \ B)"
by (simp add: Always_Int_distrib)

(*Allows a kind of "implication introduction"*)
lemma Always_Compl_Un_eq:
     "F \ Always A ==> (F \ Always (-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

subsection\<open>Totalize\<close>

lemma reachable_imp_reachable_tot:
      "s \ reachable F ==> s \ reachable (totalize F)"
apply (erule reachable.induct)
apply (rule reachable.Init)
apply simp
apply (rule_tac act = "totalize_act act" in reachable.Acts)
apply (auto simp add: totalize_act_def)
done

lemma reachable_tot_imp_reachable:
      "s \ reachable (totalize F) ==> s \ reachable F"
apply (erule reachable.induct)
apply (rule reachable.Init, simp)
apply (force simp add: totalize_act_def intro: reachable.Acts)
done

lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F"
by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable)

lemma totalize_Constrains_iff [simp]: "(totalize F \ A Co B) = (F \ A Co B)"
by (simp add: Constrains_def)

lemma totalize_Stable_iff [simp]: "(totalize F \ Stable A) = (F \ Stable A)"
by (simp add: Stable_def)

lemma totalize_Always_iff [simp]: "(totalize F \ Always A) = (F \ Always A)"
by (simp add: Always_def)

end

quality99%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.