Theory UNITY
section ‹The Basic UNITY Theory›
theory UNITY imports State begin
text‹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.›
definition
program :: i where
"program ≡ {<init, acts, allowed>:
Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
id(state) ∈ acts ∧ id(state) ∈ allowed}"
definition
mk_program :: "[i,i,i]⇒i" where
"mk_program(init, acts, allowed) ≡
<init ∩ state, cons(id(state), acts ∩ Pow(state*state)),
cons(id(state), allowed ∩ Pow(state*state))>"
definition
SKIP :: i (‹⊥›) where
"SKIP ≡ mk_program(state, 0, Pow(state*state))"
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 ‹co› 60) where
"A co B ≡ {F ∈ program. (∀act ∈ Acts(F). act``A⊆B) ∧ st_set(A)}"
definition unless :: "[i, i] ⇒ i" (infixl ‹unless› 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)"
definition
metacomp :: "[i⇒i, i⇒i] ⇒ (i⇒i)" (infixl ‹comp› 65) where
"f comp g ≡ λx. f(g(x))"
definition
pg_compl :: "i⇒i" where
"pg_compl(X)≡ program - X"
text‹SKIP›
lemma SKIP_in_program [iff,TC]: "SKIP ∈ program"
by (force simp add: SKIP_def program_def mk_program_def)
subsection‹The function \<^term>‹programify›, the coercion from anything to
program›
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‹Collapsing rules: to remove programify from expressions›
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‹The Inspectors for Programs›
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‹Types of the Inspectors›
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))"
unfolding 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‹Needed in Behaviors›
lemma ActsD: "⟦act ∈ Acts(F); <s,s'> ∈ act⟧ ⟹ s ∈ state ∧ s' ∈ state"
by (blast dest: Acts_type [THEN subsetD])
lemma AllowedActsD:
"⟦act ∈ AllowedActs(F); <s,s'> ∈ act⟧ ⟹ s ∈ state ∧ s' ∈ state"
by (blast dest: AllowedActs_type [THEN subsetD])
subsection‹Simplification rules involving \<^term>‹state›, \<^term>‹Init›,
\<^term>‹Acts›, and \<^term>‹AllowedActs››
text‹But are they really needed?›
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‹Eliminating ‹∩ state› from expressions›
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‹The Operator \<^term>‹mk_program››
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 ∩ 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 ∩ 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 ∩ Pow(state*state))"
by (simp add: Acts_def)
lemma AllowedActs_eq [simp]:
"AllowedActs(mk_program(init, acts, allowed))=
cons(id(state), allowed ∩ Pow(state*state))"
by (simp add: AllowedActs_def)
text‹Init, Acts, and AlowedActs of SKIP›
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‹Equality of UNITY programs›
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 ∈ program; G ∈ 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‹These rules allow "lazy" definition expansion›
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 ∩ Pow(state*state))"
by auto
lemma def_prg_AllowedActs:
"F ≡ mk_program (init,acts,allowed)
⟹ AllowedActs(F) = cons(id(state), allowed ∩ Pow(state*state))"
by auto
lemma def_prg_simps:
"⟦F ≡ mk_program (init,acts,allowed)⟧
⟹ Init(F) = init ∩ state ∧
Acts(F) = cons(id(state), acts ∩ Pow(state*state)) ∧
AllowedActs(F) = cons(id(state), allowed ∩ Pow(state*state))"
by auto
text‹An action is expanded only if a pair of states is being tested against it›
lemma def_act_simp:
"⟦act ≡ {<s,s'> ∈ A*B. P(s, s')}⟧
⟹ (<s,s'> ∈ act) ⟷ (<s,s'> ∈ A*B ∧ P(s, s'))"
by auto
text‹A set is expanded only if an element is being tested against it›
lemma def_set_simp: "A ≡ B ⟹ (x ∈ A) ⟷ (x ∈ B)"
by auto
subsection‹The Constrains Operator›
lemma constrains_type: "A co B ⊆ program"
by (force simp add: constrains_def)
lemma constrainsI:
"⟦(⋀act s s'. ⟦act: Acts(F); <s,s'> ∈ act; s ∈ A⟧ ⟹ s' ∈ A');
F ∈ program; st_set(A)⟧ ⟹ F ∈ 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‹monotonic in 2nd argument›
lemma constrains_weaken_R:
"⟦F ∈ A co A'; A'⊆B'⟧ ⟹ F ∈ A co B'"
apply (unfold constrains_def, blast)
done
text‹anti-monotonic in 1st argument›
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‹Constrains and Union›
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 ∈ (⋃i ∈ I. A(i)) co (⋃i ∈ 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‹Constrains and Intersection›
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 ∈ (⋂i ∈ I. A(i)) co (⋂i ∈ 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
lemma constrains_All:
"⟦∀z. F:{s ∈ state. P(s, z)} co {s ∈ state. Q(s, z)}; F ∈ program⟧⟹
F:{s ∈ state. ∀z. P(s, z)} co {s ∈ state. ∀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‹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‹The Unless Operator›
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"
unfolding 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‹The Operator \<^term>‹initially››
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‹The Operator \<^term>‹stable››
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‹Union and Intersection with \<^term>‹stable››
lemma stable_Un:
"⟦F ∈ stable(A); F ∈ stable(A')⟧ ⟹ F ∈ stable(A ∪ A')"
unfolding stable_def
apply (blast intro: constrains_Un)
done
lemma stable_UN:
"⟦⋀i. i∈I ⟹ F ∈ stable(A(i)); F ∈ program⟧
⟹ F ∈ stable (⋃i ∈ I. A(i))"
unfolding stable_def
apply (blast intro: constrains_UN)
done
lemma stable_Int:
"⟦F ∈ stable(A); F ∈ stable(A')⟧ ⟹ F ∈ stable (A ∩ A')"
unfolding stable_def
apply (blast intro: constrains_Int)
done
lemma stable_INT:
"⟦⋀i. i ∈ I ⟹ F ∈ stable(A(i)); F ∈ program⟧
⟹ F ∈ stable (⋂i ∈ I. A(i))"
unfolding stable_def
apply (blast intro: constrains_INT)
done
lemma stable_All:
"⟦∀z. F ∈ stable({s ∈ state. P(s, z)}); F ∈ program⟧
⟹ F ∈ stable({s ∈ state. ∀z. P(s, z)})"
unfolding 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)
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]
subsection‹The Operator \<^term>‹invariant››
lemma invariant_type: "invariant(A) ⊆ program"
unfolding invariant_def
apply (blast dest: stable_type [THEN subsetD])
done
lemma invariantI: "⟦Init(F)⊆A; F ∈ stable(A)⟧ ⟹ F ∈ invariant(A)"
unfolding 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)"
unfolding invariant_def
apply (blast dest: stableD2)
done
text‹Could also say
\<^term>‹invariant(A) ∩ invariant(B) ⊆ invariant (A ∩ B)››
lemma invariant_Int:
"⟦F ∈ invariant(A); F ∈ invariant(B)⟧ ⟹ F ∈ invariant(A ∩ B)"
unfolding invariant_def initially_def
apply (simp add: stable_Int, blast)
done
subsection‹The Elimination Theorem›
text‹The general case is easier to prove than the special case!›
lemma "elimination":
"⟦∀m ∈ M. F ∈ {s ∈ A. x(s) = m} co B(m); F ∈ program⟧
⟹ F ∈ {s ∈ A. x(s) ∈ M} co (⋃m ∈ M. B(m))"
by (auto simp add: constrains_def st_set_def, blast)
text‹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:{s ∈ state. x(s) ∈ M} co (⋃m ∈ M. B(m))"
by (rule UNITY.elimination, auto)
subsection‹The Operator \<^term>‹strongest_rhs››
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 ‹
fun simp_of_act def = def RS @{thm def_act_simp};
fun simp_of_set def = def RS @{thm def_set_simp};
›
end