# Theory UNITY

theory UNITY
imports State
```(*  Title:      ZF/UNITY/UNITY.thy
Author:     Sidi O Ehmety, Computer Laboratory
*)

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
―‹The definition yields a program thanks to the coercions
init ∩ state, acts ∩ Pow(state*state), etc.›
"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))"

(* 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 "co" 60)  where
"A co B == {F ∈ program. (∀act ∈ Acts(F). act``A⊆B) & st_set(A)}"
―‹the condition @{term "st_set(A)"} makes the definition slightly
stronger than the HOL one›

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)"

(* meta-function composition *)
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"

lemma programify_in_program [iff,TC]: "programify(F) ∈ program"

text‹Collapsing rules: to remove programify from expressions›
lemma programify_idem [simp]: "programify(programify(F))=programify(F)"

lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"

lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"

lemma AllowedActs_programify [simp]:
"AllowedActs(programify(F)) = AllowedActs(F)"

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)"

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)"

lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"

lemma cons_id_AllowedActs [simp]:
"cons(id(state), AllowedActs(F)) = AllowedActs(F)"

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"

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)"

lemma AllowedActs_type: "AllowedActs(F) ⊆ Pow(state*state)"

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"

lemma Acts_eq [simp]:
"Acts(mk_program(init, acts, allowed)) =
cons(id(state), acts  ∩ Pow(state*state))"

lemma AllowedActs_eq [simp]:
"AllowedActs(mk_program(init, acts, allowed))=
cons(id(state), allowed ∩ Pow(state*state))"

text‹Init, Acts, and AlowedActs  of SKIP›

lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"

lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"

lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"

lemma Init_SKIP [simp]: "Init(SKIP) = state"

lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"

lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"

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"

lemma constrainsI:
"[|(!!act s s'. [| act: Acts(F);  <s,s'> ∈ act; s ∈ A|] ==> s' ∈ A');
F ∈ program; st_set(A) |]  ==> F ∈ A co A'"

lemma constrainsD:
"F ∈ A co B ==> ∀act ∈ Acts(F). act``A⊆B"

lemma constrainsD2: "F ∈ A co B ==> F ∈ program & st_set(A)"

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 (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 (⋂z. A i) co (⋂z. B i) *)
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"
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‹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')"
apply (unfold 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))"
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 ∈ stable (⋂i ∈ 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 ∈ stable({s ∈ state. ∀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 ∈ stable(C); F  ∈ (C ∩ A) co A |] ==> F ∈ stable(C ∩ A) *)
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]

subsection‹The Operator @{term invariant}›

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‹Could also say
@{term "invariant(A) ∩ invariant(B) ⊆ invariant (A ∩ B)"}›
lemma invariant_Int:
"[| F ∈ invariant(A);  F ∈ invariant(B) |] ==> F ∈ invariant(A ∩ B)"
apply (unfold invariant_def initially_def)
done

subsection‹The Elimination Theorem›

(** The "free" m has become universally quantified!
Should the premise be !!m instead of ∀m ? Would make it harder
to use in forward proof. **)

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
```