# Theory UNITY

theory UNITY
imports Main
```(*  Title:      HOL/UNITY/UNITY.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

The basic UNITY theory (revised version, based upon the "co"
operator).

From Misra, "A Logic for Concurrent Programming", 1994.
*)

section ‹The Basic UNITY Theory›

theory UNITY imports Main begin

definition
"Program =
{(init:: 'a set, acts :: ('a * 'a)set set,
allowed :: ('a * 'a)set set). Id ∈ acts & Id ∈ 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
― ‹Polymorphic in both states and the meaning of ‹≤››
"increasing f == ⋂z. stable {s. z ≤ f s}"

subsubsection‹The abstract type of programs›

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

lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"

lemma Acts_nonempty [simp]: "Acts F ≠ {}"
by auto

lemma Id_in_AllowedActs [iff]: "Id ∈ AllowedActs F"
apply (cut_tac x = F in Rep_Program)
done

lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"

subsubsection‹Inspectors for type "program"›

lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"

lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"

lemma AllowedActs_eq [simp]:
"AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"

subsubsection‹Equality for UNITY programs›

lemma surjective_mk_program [simp]:
"mk_program (Init F, Acts F, AllowedActs F) = F"
apply (cut_tac x = F in Rep_Program)
apply (drule_tac f = Abs_Program in arg_cong)+
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‹co›

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

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‹monotonic in 2nd argument›
lemma constrains_weaken_R:
"[| F ∈ A co A'; A'<=B' |] ==> F ∈ A co B'"
by (unfold constrains_def, blast)

text‹anti-monotonic in 1st argument›
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‹Union›

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 ∈ (⋃i ∈ I. A i) co (⋃i ∈ 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‹Intersection›

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 ∈ (⋂i ∈ I. A i) co (⋂i ∈ I. A' i)"
by (unfold constrains_def, blast)

lemma constrains_imp_subset: "F ∈ A co A' ==> A ⊆ A'"
by (unfold constrains_def, auto)

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, 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‹unless›

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‹stable›

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‹Union›

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‹Intersection›

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 ∈ stable C; F ∈  (C ∩ A) co A |] ==> F ∈ stable (C ∩ A) *)
lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]

subsubsection‹invariant›

lemma invariantI: "[| Init F ⊆ A;  F ∈ stable A |] ==> F ∈ invariant A"

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)"
by (auto simp add: invariant_def stable_Int)

subsubsection‹increasing›

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 ⊆ 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 ∀m ?  Would make it harder to use
in forward proof. **)

lemma elimination:
"[| ∀m ∈ M. F ∈ {s. s x = m} co (B m) |]
==> F ∈ {s. s x ∈ M} co (⋃m ∈ M. B m)"
by (unfold constrains_def, blast)

text‹As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.›
lemma elimination_sing:
"(∀m ∈ M. F ∈ {m} co (B m)) ==> F ∈ M co (⋃m ∈ M. B m)"
by (unfold constrains_def, blast)

subsubsection‹Theoretical Results from Section 6›

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)

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‹Needed for WF reasoning in WFair.thy›

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‹Partial versus Total Transitions›

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‹Basic properties›

lemma totalize_act_Id [simp]: "totalize_act Id = Id"

lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"

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

lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"

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

lemma totalize_invariant_iff [simp]:
"(totalize F ∈ invariant A) = (F ∈ invariant A)"

lemma all_total_totalize: "all_total (totalize F)"

lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"

lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
apply (rule program_equalityI)
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)"

subsection‹Rules for Lazy Definition Expansion›

text‹They avoid expanding the full program, which is a large expression›

lemma def_prg_Init:
"F = mk_total_program (init,acts,allowed) ==> Init F = init"

lemma def_prg_Acts:
"F = mk_total_program (init,acts,allowed)
==> Acts F = insert Id (totalize_act ` acts)"

lemma def_prg_AllowedActs:
"F = mk_total_program (init,acts,allowed)
==> AllowedActs F = insert Id allowed"

text‹An action is expanded if a pair of states is being tested against it›
lemma def_act_simp:
"act = {(s,s'). P s s'} ==> ((s,s') ∈ act) = P s s'"

text‹A set is expanded only if an element is being tested against it›
lemma def_set_simp: "A = B ==> (x ∈ A) = (x ∈ B)"

subsubsection‹Inspectors for type "program"›

lemma Init_total_eq [simp]:
"Init (mk_total_program (init,acts,allowed)) = init"