Quelle UNITY.thy Sprache: Isabelle

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

The basic UNITY theory (revised version, based upon the "co"
operator).

From Misra, "A Logic for Concurrent Programming", 1994.
*)

section \<open>The Basic UNITY Theory\<close>

theory UNITY imports Main begin

definition
  "Program =
    {(init:: 'a set, acts :: ('a * 'a)set set,
      allowed :: ('a * 'a)set set). Id \<in> acts & Id \<in> allowed}"

typedef 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
  morphisms Rep_Program Abs_Program
  unfolding Program_def by blast

definition Acts :: "'a program => ('a * 'a)set set" where
    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"

definition "constrains" :: "['a set, 'a set] => 'a program set"  (infixl \<open>co\<close>     60) where
    "A co B == {F. \act \ Acts F. act``A \ 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 mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
                   => 'a program" where
    "mk_program == %(init, acts, allowed).
                      Abs_Program (init, insert Id acts, insert Id allowed)"

definition Init :: "'a program => 'a set" where
    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"

definition AllowedActs :: "'a program => ('a * 'a)set set" where
    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"

definition Allowed :: "'a program => 'a program set" where
    "Allowed F == {G. Acts G \ AllowedActs F}"

definition stable     :: "'a set => 'a program set" where
    "stable A == A co A"

definition strongest_rhs :: "['a program, 'a set] => 'a set" where
    "strongest_rhs F A == \{B. F \ A co B}"

definition invariant :: "'a set => 'a program set" where
    "invariant A == {F. Init F \ A} \ stable A"

definition increasing :: "['a => 'b::{order}] => 'a program set" where
    \<comment> \<open>Polymorphic in both states and the meaning of \<open>\<le>\<close>\<close>
    "increasing f == \z. stable {s. z \ f s}"

subsubsection\<open>The abstract type of programs\<close>

lemmas program_typedef =
     Rep_Program Rep_Program_inverse Abs_Program_inverse
     Program_def Init_def Acts_def AllowedActs_def mk_program_def

lemma Id_in_Acts [iff]: "Id \ Acts F"
apply (cut_tac x = F in Rep_Program)
apply (auto simp add: program_typedef)
done

lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
by (simp add: insert_absorb)

lemma Acts_nonempty [simp]: "Acts F \ {}"
by auto

lemma Id_in_AllowedActs [iff]: "Id \ AllowedActs F"
apply (cut_tac x = F in Rep_Program)
apply (auto simp add: program_typedef)
done

lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
by (simp add: insert_absorb)

subsubsection\<open>Inspectors for type "program"\<close>

lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
by (simp add: program_typedef)

lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
by (simp add: program_typedef)

lemma AllowedActs_eq [simp]:
     "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
by (simp add: program_typedef)

subsubsection\<open>Equality for UNITY programs\<close>

lemma surjective_mk_program [simp]:
     "mk_program (Init F, Acts F, AllowedActs F) = F"
apply (cut_tac x = F in Rep_Program)
apply (auto simp add: program_typedef)
apply (drule_tac f = Abs_Program in arg_cong)+
apply (simp add: program_typedef insert_absorb)
done

lemma program_equalityI:
     "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]
      ==> F = G"
apply (rule_tac t = F in surjective_mk_program [THEN subst])
apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
done

lemma program_equalityE:
     "[| F = G;
         [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]
         ==> P |] ==> P"
by simp

lemma program_equality_iff:
     "(F=G) =
      (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
by (blast intro: program_equalityI program_equalityE)

subsubsection\<open>co\<close>

lemma constrainsI:
    "(!!act s s'. [| act \ Acts F; (s,s') \ act; s \ A |] ==> s' \ A')
     ==> F \<in> A co A'"
by (simp add: constrains_def, blast)

lemma constrainsD:
    "[| F \ A co A'; act \ Acts F; (s,s') \ act; s \ A |] ==> s' \ A'"
by (unfold constrains_def, blast)

lemma constrains_empty [iff]: "F \ {} co B"
by (unfold constrains_def, blast)

lemma constrains_empty2 [iff]: "(F \ A co {}) = (A={})"
by (unfold constrains_def, blast)

lemma constrains_UNIV [iff]: "(F \ UNIV co B) = (B = UNIV)"
by (unfold constrains_def, blast)

lemma constrains_UNIV2 [iff]: "F \ A co UNIV"
by (unfold constrains_def, blast)

text\<open>monotonic in 2nd argument\<close>
lemma constrains_weaken_R:
    "[| F \ A co A'; A'<=B' |] ==> F \ A co B'"
by (unfold constrains_def, blast)

text\<open>anti-monotonic in 1st argument\<close>
lemma constrains_weaken_L:
    "[| F \ A co A'; B \ A |] ==> F \ B co A'"
by (unfold constrains_def, blast)

lemma constrains_weaken:
   "[| F \ A co A'; B \ A; A'<=B' |] ==> F \ B co B'"
by (unfold constrains_def, blast)

subsubsection\<open>Union\<close>

lemma constrains_Un:
    "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')"
by (unfold constrains_def, blast)

lemma constrains_UN:
    "(!!i. i \ I ==> F \ (A i) co (A' i))
     ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
by (unfold constrains_def, blast)

lemma constrains_Un_distrib: "(A \ B) co C = (A co C) \ (B co C)"
by (unfold constrains_def, blast)

lemma constrains_UN_distrib: "(\i \ I. A i) co B = (\i \ I. A i co B)"
by (unfold constrains_def, blast)

lemma constrains_Int_distrib: "C co (A \ B) = (C co A) \ (C co B)"
by (unfold constrains_def, blast)

lemma constrains_INT_distrib: "A co (\i \ I. B i) = (\i \ I. A co B i)"
by (unfold constrains_def, blast)

subsubsection\<open>Intersection\<close>

lemma constrains_Int:
    "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')"
by (unfold constrains_def, blast)

lemma constrains_INT:
    "(!!i. i \ I ==> F \ (A i) co (A' i))
     ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
by (unfold constrains_def, blast)

lemma constrains_imp_subset: "F \ A co A' ==> A \ A'"
by (unfold constrains_def, auto)

text\<open>The reasoning is by subsets since "co" refers to single actions
  only.  So this rule isn't that useful.\
lemma constrains_trans:
    "[| F \ A co B; F \ B co C |] ==> F \ A co C"
by (unfold constrains_def, blast)

lemma constrains_cancel:
   "[| F \ A co (A' \ B); F \ B co B' |] ==> F \ A co (A' \ B')"
by (unfold constrains_def, clarify, blast)

subsubsection\<open>unless\<close>

lemma unlessI: "F \ (A-B) co (A \ B) ==> F \ A unless B"
by (unfold unless_def, assumption)

lemma unlessD: "F \ A unless B ==> F \ (A-B) co (A \ B)"
by (unfold unless_def, assumption)

subsubsection\<open>stable\<close>

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_UNIV [simp]: "stable UNIV = UNIV"
by (unfold stable_def constrains_def, auto)

subsubsection\<open>Union\<close>

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_UN:
    "(!!i. i \ I ==> F \ stable (A i)) ==> F \ stable (\i \ I. A i)"
apply (unfold stable_def)
apply (blast intro: constrains_UN)
done

lemma stable_Union:
    "(!!A. A \ X ==> F \ stable A) ==> F \ stable (\X)"
by (unfold stable_def constrains_def, blast)

subsubsection\<open>Intersection\<close>

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_INT:
    "(!!i. i \ I ==> F \ stable (A i)) ==> F \ stable (\i \ I. A i)"
apply (unfold stable_def)
apply (blast intro: constrains_INT)
done

lemma stable_Inter:
    "(!!A. A \ X ==> F \ stable A) ==> F \ stable (\X)"
by (unfold stable_def constrains_def, blast)

lemma stable_constrains_Un:
    "[| F \ stable C; F \ A co (C \ A') |] ==> F \ (C \ A) co (C \ A')"
by (unfold stable_def constrains_def, blast)

lemma stable_constrains_Int:
  "[| F \ stable C; F \ (C \ A) co A' |] ==> F \ (C \ A) co (C \ A')"
by (unfold stable_def constrains_def, blast)

(*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]

subsubsection\<open>invariant\<close>

lemma invariantI: "[| Init F \ A; F \ stable A |] ==> F \ invariant A"
by (simp add: invariant_def)

text\<open>Could also say \<^term>\<open>invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)\<close>\<close>
lemma invariant_Int:
     "[| F \ invariant A; F \ invariant B |] ==> F \ invariant (A \ B)"
by (auto simp add: invariant_def stable_Int)

subsubsection\<open>increasing\<close>

lemma increasingD:
     "F \ increasing f ==> F \ stable {s. z \ f s}"
by (unfold increasing_def, blast)

lemma increasing_constant [iff]: "F \ increasing (%s. c)"
by (unfold increasing_def stable_def, auto)

lemma mono_increasing_o:
     "mono g ==> increasing f \ increasing (g o f)"
apply (unfold increasing_def stable_def constrains_def, auto)
apply (blast intro: monoD order_trans)
done

(*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
lemma strict_increasingD:
     "!!z::nat. F \ increasing f ==> F \ stable {s. z < f s}"
by (simp add: increasing_def Suc_le_eq [symmetric])

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

text\<open>As above, but for the trivial case of a one-variable state, in which the
  state is identified with its one variable.\<close>
lemma elimination_sing:
    "(\m \ M. F \ {m} co (B m)) ==> F \ M co (\m \ M. B m)"
by (unfold constrains_def, blast)

subsubsection\<open>Theoretical Results from Section 6\<close>

lemma constrains_strongest_rhs:
    "F \ A co (strongest_rhs F A )"
by (unfold constrains_def strongest_rhs_def, blast)

lemma strongest_rhs_is_strongest:
    "F \ A co B ==> strongest_rhs F A \ B"
by (unfold constrains_def strongest_rhs_def, blast)

subsubsection\<open>Ad-hoc set-theory rules\<close>

lemma Un_Diff_Diff [simp]: "A \ B - (A - B) = B"
by blast

lemma Int_Union_Union: "\B \ A = \((%C. C \ A)`B)"
by blast

text\<open>Needed for WF reasoning in WFair.thy\<close>

lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
by blast

lemma Image_inverse_less_than [simp]: "less_than\ `` {k} = lessThan k"
by blast

subsection\<open>Partial versus Total Transitions\<close>

definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
    "totalize_act act == act \ Id_on (-(Domain act))"

definition totalize :: "'a program => 'a program" where
    "totalize F == mk_program (Init F,
                               totalize_act ` Acts F,
                               AllowedActs F)"

definition mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
                   => 'a program" where
    "mk_total_program args == totalize (mk_program args)"

definition all_total :: "'a program => bool" where
    "all_total F == \act \ Acts F. Domain act = UNIV"

lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
by (blast intro: sym [THEN image_eqI])

subsubsection\<open>Basic properties\<close>

lemma totalize_act_Id [simp]: "totalize_act Id = Id"
by (simp add: totalize_act_def)

lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
by (auto simp add: totalize_act_def)

lemma Init_totalize [simp]: "Init (totalize F) = Init F"
by (unfold totalize_def, auto)

lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
by (simp add: totalize_def insert_Id_image_Acts)

lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
by (simp add: totalize_def)

lemma totalize_constrains_iff [simp]: "(totalize F \ A co B) = (F \ A co B)"
by (simp add: totalize_def totalize_act_def constrains_def, blast)

lemma totalize_stable_iff [simp]: "(totalize F \ stable A) = (F \ stable A)"
by (simp add: stable_def)

lemma totalize_invariant_iff [simp]:
     "(totalize F \ invariant A) = (F \ invariant A)"
by (simp add: invariant_def)

lemma all_total_totalize: "all_total (totalize F)"
by (simp add: totalize_def all_total_def)

lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
by (force simp add: totalize_act_def)

lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
apply (simp add: all_total_def totalize_def)
apply (rule program_equalityI)
  apply (simp_all add: Domain_iff_totalize_act image_def)
done

lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
apply (rule iffI)
apply (erule all_total_imp_totalize)
apply (erule subst)
apply (rule all_total_totalize)
done

lemma mk_total_program_constrains_iff [simp]:
     "(mk_total_program args \ A co B) = (mk_program args \ A co B)"
by (simp add: mk_total_program_def)

subsection\<open>Rules for Lazy Definition Expansion\<close>

text\<open>They avoid expanding the full program, which is a large expression\<close>

lemma def_prg_Init:
     "F = mk_total_program (init,acts,allowed) ==> Init F = init"
by (simp add: mk_total_program_def)

lemma def_prg_Acts:
     "F = mk_total_program (init,acts,allowed)
      ==> Acts F = insert Id (totalize_act ` acts)"
by (simp add: mk_total_program_def)

lemma def_prg_AllowedActs:
     "F = mk_total_program (init,acts,allowed)
      ==> AllowedActs F = insert Id allowed"
by (simp add: mk_total_program_def)

text\<open>An action is expanded if a pair of states is being tested against it\<close>
lemma def_act_simp:
     "act = {(s,s'). P s s'} ==> ((s,s') \ act) = P s s'"
by (simp add: mk_total_program_def)

text\<open>A set is expanded only if an element is being tested against it\<close>
lemma def_set_simp: "A = B ==> (x \ A) = (x \ B)"
by (simp add: mk_total_program_def)

subsubsection\<open>Inspectors for type "program"\<close>

lemma Init_total_eq [simp]:
     "Init (mk_total_program (init,acts,allowed)) = init"
by (simp add: mk_total_program_def)

lemma Acts_total_eq [simp]:
    "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
by (simp add: mk_total_program_def)

lemma AllowedActs_total_eq [simp]:
     "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
by (auto simp add: mk_total_program_def)

end

quality100%

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

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.