(* Title: ZF/UNITY/UNITY.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
*)
section \<open>The Basic UNITY Theory\<close>
theory UNITY imports State begin
text\<open>The basic UNITY theory (revised version, based upon the "co" operator)
From Misra, "A Logic for Concurrent Programming", 1994.
This ZF theory was ported from its HOL equivalent.\<close>
definition
program :: i where
"program == {:
Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
id(state) \<in> acts & id(state) \<in> allowed}"
definition
mk_program :: "[i,i,i]=>i" where
\<comment> \<open>The definition yields a program thanks to the coercions
init \<inter> state, acts \<inter> Pow(state*state), etc.\<close>
"mk_program(init, acts, allowed) ==
<init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
cons(id(state), allowed \<inter> Pow(state*state))>"
definition
SKIP :: i (\<open>\<bottom>\<close>) where
"SKIP == mk_program(state, 0, Pow(state*state))"
(* Coercion from anything to program *)
definition
programify :: "i=>i" where
"programify(F) == if F \ program then F else SKIP"
definition
RawInit :: "i=>i" where
"RawInit(F) == fst(F)"
definition
Init :: "i=>i" where
"Init(F) == RawInit(programify(F))"
definition
RawActs :: "i=>i" where
"RawActs(F) == cons(id(state), fst(snd(F)))"
definition
Acts :: "i=>i" where
"Acts(F) == RawActs(programify(F))"
definition
RawAllowedActs :: "i=>i" where
"RawAllowedActs(F) == cons(id(state), snd(snd(F)))"
definition
AllowedActs :: "i=>i" where
"AllowedActs(F) == RawAllowedActs(programify(F))"
definition
Allowed :: "i =>i" where
"Allowed(F) == {G \ program. Acts(G) \ AllowedActs(F)}"
definition
initially :: "i=>i" where
"initially(A) == {F \ program. Init(F)\A}"
definition "constrains" :: "[i, i] => i" (infixl \<open>co\<close> 60) where
"A co B == {F \ program. (\act \ Acts(F). act``A\B) & st_set(A)}"
\<comment> \<open>the condition \<^term>\<open>st_set(A)\<close> makes the definition slightly
stronger than the HOL one\<close>
definition 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
strongest_rhs :: "[i, i] => i" where
"strongest_rhs(F, A) == \({B \ Pow(state). F \ A co B})"
definition
invariant :: "i => i" where
"invariant(A) == initially(A) \ stable(A)"
(* meta-function composition *)
definition
metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl \<open>comp\<close> 65) where
"f comp g == %x. f(g(x))"
definition
pg_compl :: "i=>i" where
"pg_compl(X)== program - X"
text\<open>SKIP\<close>
lemma SKIP_in_program [iff,TC]: "SKIP \ program"
by (force simp add: SKIP_def program_def mk_program_def)
subsection\<open>The function \<^term>\<open>programify\<close>, the coercion from anything to
program\<close>
lemma programify_program [simp]: "F \ program ==> programify(F)=F"
by (force simp add: programify_def)
lemma programify_in_program [iff,TC]: "programify(F) \ program"
by (force simp add: programify_def)
text\<open>Collapsing rules: to remove programify from expressions\<close>
lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
by (force simp add: programify_def)
lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"
by (simp add: Init_def)
lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"
by (simp add: Acts_def)
lemma AllowedActs_programify [simp]:
"AllowedActs(programify(F)) = AllowedActs(F)"
by (simp add: AllowedActs_def)
subsection\<open>The Inspectors for Programs\<close>
lemma id_in_RawActs: "F \ program ==>id(state) \ RawActs(F)"
by (auto simp add: program_def RawActs_def)
lemma id_in_Acts [iff,TC]: "id(state) \ Acts(F)"
by (simp add: id_in_RawActs Acts_def)
lemma id_in_RawAllowedActs: "F \ program ==>id(state) \ RawAllowedActs(F)"
by (auto simp add: program_def RawAllowedActs_def)
lemma id_in_AllowedActs [iff,TC]: "id(state) \ AllowedActs(F)"
by (simp add: id_in_RawAllowedActs AllowedActs_def)
lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"
by (simp add: cons_absorb)
lemma cons_id_AllowedActs [simp]:
"cons(id(state), AllowedActs(F)) = AllowedActs(F)"
by (simp add: cons_absorb)
subsection\<open>Types of the Inspectors\<close>
lemma RawInit_type: "F \ program ==> RawInit(F)\state"
by (auto simp add: program_def RawInit_def)
lemma RawActs_type: "F \ program ==> RawActs(F)\Pow(state*state)"
by (auto simp add: program_def RawActs_def)
lemma RawAllowedActs_type:
"F \ program ==> RawAllowedActs(F)\Pow(state*state)"
by (auto simp add: program_def RawAllowedActs_def)
lemma Init_type: "Init(F)\state"
by (simp add: RawInit_type Init_def)
lemmas InitD = Init_type [THEN subsetD]
lemma st_set_Init [iff]: "st_set(Init(F))"
apply (unfold st_set_def)
apply (rule Init_type)
done
lemma Acts_type: "Acts(F)\Pow(state*state)"
by (simp add: RawActs_type Acts_def)
lemma AllowedActs_type: "AllowedActs(F) \ Pow(state*state)"
by (simp add: RawAllowedActs_type AllowedActs_def)
text\<open>Needed in Behaviors\<close>
lemma ActsD: "[| act \ Acts(F); \ act |] ==> s \ state & s' \ state"
by (blast dest: Acts_type [THEN subsetD])
lemma AllowedActsD:
"[| act \ AllowedActs(F); \ act |] ==> s \ state & s' \ state"
by (blast dest: AllowedActs_type [THEN subsetD])
subsection\<open>Simplification rules involving \<^term>\<open>state\<close>, \<^term>\<open>Init\<close>,
\<^term>\<open>Acts\<close>, and \<^term>\<open>AllowedActs\<close>\<close>
text\<open>But are they really needed?\<close>
lemma state_subset_is_Init_iff [iff]: "state \ Init(F) \ Init(F)=state"
by (cut_tac F = F in Init_type, auto)
lemma Pow_state_times_state_is_subset_Acts_iff [iff]:
"Pow(state*state) \ Acts(F) \ Acts(F)=Pow(state*state)"
by (cut_tac F = F in Acts_type, auto)
lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]:
"Pow(state*state) \ AllowedActs(F) \ AllowedActs(F)=Pow(state*state)"
by (cut_tac F = F in AllowedActs_type, auto)
subsubsection\<open>Eliminating \<open>\<inter> state\<close> from expressions\<close>
lemma Init_Int_state [simp]: "Init(F) \ state = Init(F)"
by (cut_tac F = F in Init_type, blast)
lemma state_Int_Init [simp]: "state \ Init(F) = Init(F)"
by (cut_tac F = F in Init_type, blast)
lemma Acts_Int_Pow_state_times_state [simp]:
"Acts(F) \ Pow(state*state) = Acts(F)"
by (cut_tac F = F in Acts_type, blast)
lemma state_times_state_Int_Acts [simp]:
"Pow(state*state) \ Acts(F) = Acts(F)"
by (cut_tac F = F in Acts_type, blast)
lemma AllowedActs_Int_Pow_state_times_state [simp]:
"AllowedActs(F) \ Pow(state*state) = AllowedActs(F)"
by (cut_tac F = F in AllowedActs_type, blast)
lemma state_times_state_Int_AllowedActs [simp]:
"Pow(state*state) \ AllowedActs(F) = AllowedActs(F)"
by (cut_tac F = F in AllowedActs_type, blast)
subsubsection\<open>The Operator \<^term>\<open>mk_program\<close>\<close>
lemma mk_program_in_program [iff,TC]:
"mk_program(init, acts, allowed) \ program"
by (auto simp add: mk_program_def program_def)
lemma RawInit_eq [simp]:
"RawInit(mk_program(init, acts, allowed)) = init \ state"
by (auto simp add: mk_program_def RawInit_def)
lemma RawActs_eq [simp]:
"RawActs(mk_program(init, acts, allowed)) =
cons(id(state), acts \<inter> Pow(state*state))"
by (auto simp add: mk_program_def RawActs_def)
lemma RawAllowedActs_eq [simp]:
"RawAllowedActs(mk_program(init, acts, allowed)) =
cons(id(state), allowed \<inter> Pow(state*state))"
by (auto simp add: mk_program_def RawAllowedActs_def)
lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \ state"
by (simp add: Init_def)
lemma Acts_eq [simp]:
"Acts(mk_program(init, acts, allowed)) =
cons(id(state), acts \<inter> Pow(state*state))"
by (simp add: Acts_def)
lemma AllowedActs_eq [simp]:
"AllowedActs(mk_program(init, acts, allowed))=
cons(id(state), allowed \<inter> Pow(state*state))"
by (simp add: AllowedActs_def)
text\<open>Init, Acts, and AlowedActs of SKIP\<close>
lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
by (simp add: SKIP_def)
lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"
by (force simp add: SKIP_def)
lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"
by (force simp add: SKIP_def)
lemma Init_SKIP [simp]: "Init(SKIP) = state"
by (force simp add: SKIP_def)
lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"
by (force simp add: SKIP_def)
lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
by (force simp add: SKIP_def)
text\<open>Equality of UNITY programs\<close>
lemma raw_surjective_mk_program:
"F \ program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def
RawAllowedActs_def, blast+)
done
lemma surjective_mk_program [simp]:
"mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"
by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def)
lemma program_equalityI:
"[|Init(F) = Init(G); Acts(F) = Acts(G);
AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G"
apply (subgoal_tac "programify(F) = programify(G)")
apply simp
apply (simp only: surjective_mk_program [symmetric])
done
lemma program_equalityE:
"[|F = G;
[|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
==> P |]
==> P"
by force
lemma program_equality_iff:
"[| F \ program; G \ program |] ==>(F=G) \
(Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"
by (blast intro: program_equalityI program_equalityE)
subsection\<open>These rules allow "lazy" definition expansion\<close>
lemma def_prg_Init:
"F == mk_program (init,acts,allowed) ==> Init(F) = init \ state"
by auto
lemma def_prg_Acts:
"F == mk_program (init,acts,allowed)
==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))"
by auto
lemma def_prg_AllowedActs:
"F == mk_program (init,acts,allowed)
==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
by auto
lemma def_prg_simps:
"[| F == mk_program (init,acts,allowed) |]
==> Init(F) = init \<inter> state &
Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) &
AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
by auto
text\<open>An action is expanded only if a pair of states is being tested against it\<close>
lemma def_act_simp:
"[| act == { \ A*B. P(s, s')} |]
==> (<s,s'> \ act) \ ( \ A*B & P(s, s'))"
by auto
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 auto
subsection\<open>The Constrains Operator\<close>
lemma constrains_type: "A co B \ program"
by (force simp add: constrains_def)
lemma constrainsI:
"[|(!!act s s'. [| act: Acts(F); \ act; s \ A|] ==> s' \ A');
F \<in> program; st_set(A) |] ==> F \<in> A co A'"
by (force simp add: constrains_def)
lemma constrainsD:
"F \ A co B ==> \act \ Acts(F). act``A\B"
by (force simp add: constrains_def)
lemma constrainsD2: "F \ A co B ==> F \ program & st_set(A)"
by (force simp add: constrains_def)
lemma constrains_empty [iff]: "F \ 0 co B \ F \ program"
by (force simp add: constrains_def st_set_def)
lemma constrains_empty2 [iff]: "(F \ A co 0) \ (A=0 & F \ program)"
by (force simp add: constrains_def st_set_def)
lemma constrains_state [iff]: "(F \ state co B) \ (state\B & F \ program)"
apply (cut_tac F = F in Acts_type)
apply (force simp add: constrains_def st_set_def)
done
lemma constrains_state2 [iff]: "F \ A co state \ (F \ program & st_set(A))"
apply (cut_tac F = F in Acts_type)
apply (force simp add: constrains_def st_set_def)
done
text\<open>monotonic in 2nd argument\<close>
lemma constrains_weaken_R:
"[| F \ A co A'; A'\B' |] ==> F \ A co B'"
apply (unfold constrains_def, blast)
done
text\<open>anti-monotonic in 1st argument\<close>
lemma constrains_weaken_L:
"[| F \ A co A'; B\A |] ==> F \ B co A'"
apply (unfold constrains_def st_set_def, blast)
done
lemma constrains_weaken:
"[| F \ A co A'; B\A; A'\B' |] ==> F \ B co B'"
apply (drule constrains_weaken_R)
apply (drule_tac [2] constrains_weaken_L, blast+)
done
subsection\<open>Constrains and Union\<close>
lemma constrains_Un:
"[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')"
by (auto simp add: constrains_def st_set_def, force)
lemma constrains_UN:
"[|!!i. i \ I ==> F \ A(i) co A'(i); F \ program |]
==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
by (force simp add: constrains_def st_set_def)
lemma constrains_Un_distrib:
"(A \ B) co C = (A co C) \ (B co C)"
by (force simp add: constrains_def st_set_def)
lemma constrains_UN_distrib:
"i \ I ==> (\i \ I. A(i)) co B = (\i \ I. A(i) co B)"
by (force simp add: constrains_def st_set_def)
subsection\<open>Constrains and Intersection\<close>
lemma constrains_Int_distrib: "C co (A \ B) = (C co A) \ (C co B)"
by (force simp add: constrains_def st_set_def)
lemma constrains_INT_distrib:
"x \ I ==> A co (\i \ I. B(i)) = (\i \ I. A co B(i))"
by (force simp add: constrains_def st_set_def)
lemma constrains_Int:
"[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')"
by (force simp add: constrains_def st_set_def)
lemma constrains_INT [rule_format]:
"[| \i \ I. F \ A(i) co A'(i); F \ program|]
==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))"
apply (case_tac "I=0")
apply (simp add: Inter_def)
apply (erule not_emptyE)
apply (auto simp add: constrains_def st_set_def, blast)
apply (drule bspec, assumption, force)
done
(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *)
lemma constrains_All:
"[| \z. F:{s \ state. P(s, z)} co {s \ state. Q(s, z)}; F \ program |]==>
F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}"
by (unfold constrains_def, blast)
lemma constrains_imp_subset:
"[| F \ A co A' |] ==> A \ A'"
by (unfold constrains_def st_set_def, force)
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 st_set_def, auto, blast)
lemma constrains_cancel:
"[| F \ A co (A' \ B); F \ B co B' |] ==> F \ A co (A' \ B')"
apply (drule_tac A = B in constrains_imp_subset)
apply (blast intro: constrains_weaken_R)
done
subsection\<open>The Unless Operator\<close>
lemma unless_type: "A unless B \ program"
by (force simp add: unless_def constrains_def)
lemma unlessI: "[| F \ (A-B) co (A \ B) |] ==> F \ A unless B"
apply (unfold unless_def)
apply (blast dest: constrainsD2)
done
lemma unlessD: "F :A unless B ==> F \ (A-B) co (A \ B)"
by (unfold unless_def, auto)
subsection\<open>The Operator \<^term>\<open>initially\<close>\<close>
lemma initially_type: "initially(A) \ program"
by (unfold initially_def, blast)
lemma initiallyI: "[| F \ program; Init(F)\A |] ==> F \ initially(A)"
by (unfold initially_def, blast)
lemma initiallyD: "F \ initially(A) ==> Init(F)\A"
by (unfold initially_def, blast)
subsection\<open>The Operator \<^term>\<open>stable\<close>\<close>
lemma stable_type: "stable(A)\program"
by (unfold stable_def constrains_def, blast)
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 stableD2: "F \ stable(A) ==> F \ program & st_set(A)"
by (unfold stable_def constrains_def, auto)
lemma stable_state [simp]: "stable(state) = program"
by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD])
lemma stable_unless: "stable(A)= A unless 0"
by (auto simp add: unless_def stable_def)
subsection\<open>Union and Intersection with \<^term>\<open>stable\<close>\<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 \ program |]
==> F \<in> stable (\<Union>i \<in> I. A(i))"
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_INT:
"[| !!i. i \ I ==> F \ stable(A(i)); F \ program |]
==> F \<in> stable (\<Inter>i \<in> I. A(i))"
apply (unfold stable_def)
apply (blast intro: constrains_INT)
done
lemma stable_All:
"[|\z. F \ stable({s \ state. P(s, z)}); F \ program|]
==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
apply (unfold stable_def)
apply (rule constrains_All, auto)
done
lemma stable_constrains_Un:
"[| F \ stable(C); F \ A co (C \ A') |] ==> F \ (C \ A) co (C \ A')"
apply (unfold stable_def constrains_def st_set_def, auto)
apply (blast dest!: bspec)
done
lemma stable_constrains_Int:
"[| F \ stable(C); F \ (C \ A) co A' |] ==> F \ (C \ A) co (C \ A')"
by (unfold stable_def constrains_def st_set_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]
subsection\<open>The Operator \<^term>\<open>invariant\<close>\<close>
lemma invariant_type: "invariant(A) \ program"
apply (unfold invariant_def)
apply (blast dest: stable_type [THEN subsetD])
done
lemma invariantI: "[| Init(F)\A; F \ stable(A) |] ==> F \ invariant(A)"
apply (unfold invariant_def initially_def)
apply (frule stable_type [THEN subsetD], auto)
done
lemma invariantD: "F \ invariant(A) ==> Init(F)\A & F \ stable(A)"
by (unfold invariant_def initially_def, auto)
lemma invariantD2: "F \ invariant(A) ==> F \ program & st_set(A)"
apply (unfold invariant_def)
apply (blast dest: stableD2)
done
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)"
apply (unfold invariant_def initially_def)
apply (simp add: stable_Int, blast)
done
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. **)
text\<open>The general case is easier to prove than the special case!\<close>
lemma "elimination":
"[| \m \ M. F \ {s \ A. x(s) = m} co B(m); F \ program |]
==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
by (auto simp add: constrains_def st_set_def, blast)
text\<open>As above, but for the special case of A=state\<close>
lemma elimination2:
"[| \m \ M. F \ {s \ state. x(s) = m} co B(m); F \ program |]
==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
by (rule UNITY.elimination, auto)
subsection\<open>The Operator \<^term>\<open>strongest_rhs\<close>\<close>
lemma constrains_strongest_rhs:
"[| F \ program; st_set(A) |] ==> F \ A co (strongest_rhs(F,A))"
by (auto simp add: constrains_def strongest_rhs_def st_set_def
dest: Acts_type [THEN subsetD])
lemma strongest_rhs_is_strongest:
"[| F \ A co B; st_set(B) |] ==> strongest_rhs(F,A) \ B"
by (auto simp add: constrains_def strongest_rhs_def st_set_def)
ML \<open>
fun simp_of_act def = def RS @{thm def_act_simp};
fun simp_of_set def = def RS @{thm def_set_simp};
\<close>
end
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
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.
|