Quelle  UNITY.thy

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

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 ≡ {:
               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) ≡
    ∩ 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 🍋‹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 🍋‹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); ∈ 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‹Simplification rules involving 🍋‹state›, 🍋‹Init›, 
  🍋‹Acts›, and 🍋‹AllowedActs›\<close>

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 🍋‹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 ≡ { ∈ A*B. P(s, s')}]
      ==> ( ∈ act) ⟷ ( ∈ 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); ∈ 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

(* 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"
  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 🍋‹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 🍋‹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 🍋‹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)

(* \<lbrakk>F \<in> stable(C); F  \<in> (C \<inter> A) co A\<rbrakk> \<Longrightarrow> F \<in> stable(C \<inter> A) *)
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]

subsection‹The Operator 🍋‹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
  🍋‹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›

(** 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 🍋‹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