|
(* 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 "co" 60) where
"A co B == {F. \act \ Acts F. act``A \ B}"
definition unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 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
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
