Theory UNITY

theory UNITY
imports State
(*  Title:      ZF/UNITY/UNITY.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
*)


header {*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.*}


consts
"constrains" :: "[i, i] => i" (infixl "co" 60)
op_unless :: "[i, i] => i" (infixl "unless" 60)

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
stable :: "i=>i" where
"stable(A) == A co A"

definition
strongest_rhs :: "[i, i] => i" where
"strongest_rhs(F, A) == \<Inter>({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"

defs
constrains_def:
"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 *}


unless_def: "A unless B == (A - B) co (A ∪ B)"


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))"
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{*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 @{text "∩ 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 ∈ (\<Union>i ∈ I. A(i)) co (\<Union>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 ==> (\<Union>i ∈ I. A(i)) co B = (\<Inter>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 (\<Inter>i ∈ I. B(i)) = (\<Inter>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 ∈ (\<Inter>i ∈ I. A(i)) co (\<Inter>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

(* 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 ∈ 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 (\<Union>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 (\<Inter>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)
apply (simp add: stable_Int, blast)
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 (\<Union>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 (\<Union>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