# Theory Extend

Up to index of Isabelle/HOL/UNITY

theory Extend
imports Guar
begin

    (*  Title:      HOL/UNITY/Extend.thy
        ID:         $Id: Extend.thy,v 1.21 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Extending of state setsExtending of state sets
      function f (forget)    maps the extended state to the original state
      function g (forgotten) maps the extended state to the "extending part"
    *)

    header{*Extending State Sets*}

    theory Extend imports Guar begin

    constdefs

      (*MOVE to Relation.thy?*)
      Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
        "Restrict A r == r ∩ (A <*> UNIV)"

      good_map :: "['a*'b => 'c] => bool"
        "good_map h == surj h & (∀x y. fst (inv h (h (x,y))) = x)"
         (*Using the locale constant "f", this is  f (h (x,y))) = x*)

      extend_set :: "['a*'b => 'c, 'a set] => 'c set"
        "extend_set h A == h ` (A <*> UNIV)"

      project_set :: "['a*'b => 'c, 'c set] => 'a set"
        "project_set h C == {x. ∃y. h(x,y) ∈ C}"

      extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
        "extend_act h == %act. \<Union>(s,s') ∈ act. \<Union>y. {(h(s,y), h(s',y))}"

      project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
        "project_act h act == {(x,x'). ∃y y'. (h(x,y), h(x',y')) ∈ act}"

      extend :: "['a*'b => 'c, 'a program] => 'c program"
        "extend h F == mk_program (extend_set h (Init F),
                                   extend_act h ` Acts F,
                                   project_act h -` AllowedActs F)"

      (*Argument C allows weak safety laws to be projected*)
      project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
        "project h C F ==
           mk_program (project_set h (Init F),
                       project_act h ` Restrict C ` Acts F,
                       {act. Restrict (project_set h C) act :
                             project_act h ` Restrict C ` AllowedActs F})"

    locale Extend =
      fixes f     :: "'c => 'a"
        and g     :: "'c => 'b"
        and h     :: "'a*'b => 'c"    (*isomorphism between 'a * 'b and 'c *)
        and slice :: "['c set, 'b] => 'a set"
      assumes
        good_h:  "good_map h"
      defines f_def: "f z == fst (inv h z)"
          and g_def: "g z == snd (inv h z)"
          and slice_def: "slice Z y == {x. h(x,y) ∈ Z}"

    (** These we prove OUTSIDE the locale. **)

    subsection{*Restrict*}
    (*MOVE to Relation.thy?*)

    lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x ∈ A)"
    by (unfold Restrict_def, blast)

    lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
    apply (rule ext)
    apply (auto simp add: Restrict_def)
    done

    lemma Restrict_empty [simp]: "Restrict {} r = {}"
    by (auto simp add: Restrict_def)

    lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A ∩ B) r"
    by (unfold Restrict_def, blast)

    lemma Restrict_triv: "Domain r ⊆ A ==> Restrict A r = r"
    by (unfold Restrict_def, auto)

    lemma Restrict_subset: "Restrict A r ⊆ r"
    by (unfold Restrict_def, auto)

    lemma Restrict_eq_mono:
         "[| A ⊆ B;  Restrict B r = Restrict B s |]
          ==> Restrict A r = Restrict A s"
    by (unfold Restrict_def, blast)

    lemma Restrict_imageI:
         "[| s ∈ RR;  Restrict A r = Restrict A s |]
          ==> Restrict A r ∈ Restrict A ` RR"
    by (unfold Restrict_def image_def, auto)

    lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A ∩ Domain r"
    by blast

    lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A ∩ B)"
    by blast

    (*Possibly easier than reasoning about "inv h"*)
    lemma good_mapI:
         assumes surj_h: "surj h"
             and prem:   "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'"
         shows "good_map h"
    apply (simp add: good_map_def)
    apply (safe intro!: surj_h)
    apply (rule prem)
    apply (subst surjective_pairing [symmetric])
    apply (subst surj_h [THEN surj_f_inv_f])
    apply (rule refl)
    done

    lemma good_map_is_surj: "good_map h ==> surj h"
    by (unfold good_map_def, auto)

    (*A convenient way of finding a closed form for inv h*)
    lemma fst_inv_equalityI:
         assumes surj_h: "surj h"
             and prem:   "!! x y. g (h(x,y)) = x"
         shows "fst (inv h z) = g z"
    apply (unfold inv_def)
    apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
    apply (rule someI2)
    apply (drule_tac [2] f = g in arg_cong)
    apply (auto simp add: prem)
    done

    subsection{*Trivial properties of f, g, h*}

    lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x"
    by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])

    lemma (in Extend) h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
    apply (drule_tac f = f in arg_cong)
    apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
    done

    lemma (in Extend) h_f_g_equiv: "h(f z, g z) == z"
    by (simp add: f_def g_def
                good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])

    lemma (in Extend) h_f_g_eq: "h(f z, g z) = z"
    by (simp add: h_f_g_equiv)

    lemma (in Extend) split_extended_all:
         "(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
    proof
       assume allP: "!!z. PROP P z"
       fix u y
       show "PROP P (h (u, y))" by (rule allP)
     next
       assume allPh: "!!u y. PROP P (h(u,y))"
       fix z
       have Phfgz: "PROP P (h (f z, g z))" by (rule allPh)
       show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv])
    qed

    subsection{*@{term extend_set}: basic properties*}

    lemma project_set_iff [iff]:
         "(x ∈ project_set h C) = (∃y. h(x,y) ∈ C)"
    by (simp add: project_set_def)

    lemma extend_set_mono: "A ⊆ B ==> extend_set h A ⊆ extend_set h B"
    by (unfold extend_set_def, blast)

    lemma (in Extend) mem_extend_set_iff [iff]: "z ∈ extend_set h A = (f z ∈ A)"
    apply (unfold extend_set_def)
    apply (force intro: h_f_g_eq [symmetric])
    done

    lemma (in Extend) extend_set_strict_mono [iff]:
         "(extend_set h A ⊆ extend_set h B) = (A ⊆ B)"
    by (unfold extend_set_def, force)

    lemma extend_set_empty [simp]: "extend_set h {} = {}"
    by (unfold extend_set_def, auto)

    lemma (in Extend) extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
    by auto

    lemma (in Extend) extend_set_sing: "extend_set h {x} = {s. f s = x}"
    by auto

    lemma (in Extend) extend_set_inverse [simp]:
         "project_set h (extend_set h C) = C"
    by (unfold extend_set_def, auto)

    lemma (in Extend) extend_set_project_set:
         "C ⊆ extend_set h (project_set h C)"
    apply (unfold extend_set_def)
    apply (auto simp add: split_extended_all, blast)
    done

    lemma (in Extend) inj_extend_set: "inj (extend_set h)"
    apply (rule inj_on_inverseI)
    apply (rule extend_set_inverse)
    done

    lemma (in Extend) extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
    apply (unfold extend_set_def)
    apply (auto simp add: split_extended_all)
    done

    subsection{*@{term project_set}: basic properties*}

    (*project_set is simply image!*)
    lemma (in Extend) project_set_eq: "project_set h C = f ` C"
    by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)

    (*Converse appears to fail*)
    lemma (in Extend) project_set_I: "!!z. z ∈ C ==> f z ∈ project_set h C"
    by (auto simp add: split_extended_all)

    subsection{*More laws*}

    (*Because A and B could differ on the "other" part of the state,
       cannot generalize to
          project_set h (A ∩ B) = project_set h A ∩ project_set h B
    *)
    lemma (in Extend) project_set_extend_set_Int:
         "project_set h ((extend_set h A) ∩ B) = A ∩ (project_set h B)"
    by auto

    (*Unused, but interesting?*)
    lemma (in Extend) project_set_extend_set_Un:
         "project_set h ((extend_set h A) ∪ B) = A ∪ (project_set h B)"
    by auto

    lemma project_set_Int_subset:
         "project_set h (A ∩ B) ⊆ (project_set h A) ∩ (project_set h B)"
    by auto

    lemma (in Extend) extend_set_Un_distrib:
         "extend_set h (A ∪ B) = extend_set h A ∪ extend_set h B"
    by auto

    lemma (in Extend) extend_set_Int_distrib:
         "extend_set h (A ∩ B) = extend_set h A ∩ extend_set h B"
    by auto

    lemma (in Extend) extend_set_INT_distrib:
         "extend_set h (INTER A B) = (\<Inter>x ∈ A. extend_set h (B x))"
    by auto

    lemma (in Extend) extend_set_Diff_distrib:
         "extend_set h (A - B) = extend_set h A - extend_set h B"
    by auto

    lemma (in Extend) extend_set_Union:
         "extend_set h (Union A) = (\<Union>X ∈ A. extend_set h X)"
    by blast

    lemma (in Extend) extend_set_subset_Compl_eq:
         "(extend_set h A ⊆ - extend_set h B) = (A ⊆ - B)"
    by (unfold extend_set_def, auto)

    subsection{*@{term extend_act}*}

    (*Can't strengthen it to
      ((h(s,y), h(s',y')) ∈ extend_act h act) = ((s, s') ∈ act & y=y')
      because h doesn't have to be injective in the 2nd argument*)
    lemma (in Extend) mem_extend_act_iff [iff]:
         "((h(s,y), h(s',y)) ∈ extend_act h act) = ((s, s') ∈ act)"
    by (unfold extend_act_def, auto)

    (*Converse fails: (z,z') would include actions that changed the g-part*)
    lemma (in Extend) extend_act_D:
         "(z, z') ∈ extend_act h act ==> (f z, f z') ∈ act"
    by (unfold extend_act_def, auto)

    lemma (in Extend) extend_act_inverse [simp]:
         "project_act h (extend_act h act) = act"
    by (unfold extend_act_def project_act_def, blast)

    lemma (in Extend) project_act_extend_act_restrict [simp]:
         "project_act h (Restrict C (extend_act h act)) =
          Restrict (project_set h C) act"
    by (unfold extend_act_def project_act_def, blast)

    lemma (in Extend) subset_extend_act_D:
         "act' ⊆ extend_act h act ==> project_act h act' ⊆ act"
    by (unfold extend_act_def project_act_def, force)

    lemma (in Extend) inj_extend_act: "inj (extend_act h)"
    apply (rule inj_on_inverseI)
    apply (rule extend_act_inverse)
    done

    lemma (in Extend) extend_act_Image [simp]:
         "extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
    by (unfold extend_set_def extend_act_def, force)

    lemma (in Extend) extend_act_strict_mono [iff]:
         "(extend_act h act' ⊆ extend_act h act) = (act'<=act)"
    by (unfold extend_act_def, auto)

    declare (in Extend) inj_extend_act [THEN inj_eq, iff]
    (*This theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)

    lemma Domain_extend_act:
        "Domain (extend_act h act) = extend_set h (Domain act)"
    by (unfold extend_set_def extend_act_def, force)

    lemma (in Extend) extend_act_Id [simp]:
        "extend_act h Id = Id"
    apply (unfold extend_act_def)
    apply (force intro: h_f_g_eq [symmetric])
    done

    lemma (in Extend) project_act_I:
         "!!z z'. (z, z') ∈ act ==> (f z, f z') ∈ project_act h act"
    apply (unfold project_act_def)
    apply (force simp add: split_extended_all)
    done

    lemma (in Extend) project_act_Id [simp]: "project_act h Id = Id"
    by (unfold project_act_def, force)

    lemma (in Extend) Domain_project_act:
      "Domain (project_act h act) = project_set h (Domain act)"
    apply (unfold project_act_def)
    apply (force simp add: split_extended_all)
    done

    subsection{*extend*}

    text{*Basic properties*}

    lemma Init_extend [simp]:
         "Init (extend h F) = extend_set h (Init F)"
    by (unfold extend_def, auto)

    lemma Init_project [simp]:
         "Init (project h C F) = project_set h (Init F)"
    by (unfold project_def, auto)

    lemma (in Extend) Acts_extend [simp]:
         "Acts (extend h F) = (extend_act h ` Acts F)"
    by (simp add: extend_def insert_Id_image_Acts)

    lemma (in Extend) AllowedActs_extend [simp]:
         "AllowedActs (extend h F) = project_act h -` AllowedActs F"
    by (simp add: extend_def insert_absorb)

    lemma Acts_project [simp]:
         "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)"
    by (auto simp add: project_def image_iff)

    lemma (in Extend) AllowedActs_project [simp]:
         "AllowedActs(project h C F) =
            {act. Restrict (project_set h C) act
                   ∈ project_act h ` Restrict C ` AllowedActs F}"
    apply (simp (no_asm) add: project_def image_iff)
    apply (subst insert_absorb)
    apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
    done

    lemma (in Extend) Allowed_extend:
         "Allowed (extend h F) = project h UNIV -` Allowed F"
    apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
    apply blast
    done

    lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
    apply (unfold SKIP_def)
    apply (rule program_equalityI, auto)
    done

    lemma project_set_UNIV [simp]: "project_set h UNIV = UNIV"
    by auto

    lemma project_set_Union:
         "project_set h (Union A) = (\<Union>X ∈ A. project_set h X)"
    by blast

    (*Converse FAILS: the extended state contributing to project_set h C
      may not coincide with the one contributing to project_act h act*)
    lemma (in Extend) project_act_Restrict_subset:
         "project_act h (Restrict C act) ⊆
          Restrict (project_set h C) (project_act h act)"
    by (auto simp add: project_act_def)

    lemma (in Extend) project_act_Restrict_Id_eq:
         "project_act h (Restrict C Id) = Restrict (project_set h C) Id"
    by (auto simp add: project_act_def)

    lemma (in Extend) project_extend_eq:
         "project h C (extend h F) =
          mk_program (Init F, Restrict (project_set h C) ` Acts F,
                      {act. Restrict (project_set h C) act
                              ∈ project_act h ` Restrict C `
                                         (project_act h -` AllowedActs F)})"
    apply (rule program_equalityI)
      apply simp
     apply (simp add: image_eq_UN)
    apply (simp add: project_def)
    done

    lemma (in Extend) extend_inverse [simp]:
         "project h UNIV (extend h F) = F"
    apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
              subset_UNIV [THEN subset_trans, THEN Restrict_triv])
    apply (rule program_equalityI)
    apply (simp_all (no_asm))
    apply (subst insert_absorb)
    apply (simp (no_asm) add: bexI [of _ Id])
    apply auto
    apply (rename_tac "act")
    apply (rule_tac x = "extend_act h act" in bexI, auto)
    done

    lemma (in Extend) inj_extend: "inj (extend h)"
    apply (rule inj_on_inverseI)
    apply (rule extend_inverse)
    done

    lemma (in Extend) extend_Join [simp]:
         "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
    apply (rule program_equalityI)
    apply (simp (no_asm) add: extend_set_Int_distrib)
    apply (simp add: image_Un, auto)
    done

    lemma (in Extend) extend_JN [simp]:
         "extend h (JOIN I F) = (\<Squnion>i ∈ I. extend h (F i))"
    apply (rule program_equalityI)
      apply (simp (no_asm) add: extend_set_INT_distrib)
     apply (simp add: image_UN, auto)
    done

    (** These monotonicity results look natural but are UNUSED **)

    lemma (in Extend) extend_mono: "F ≤ G ==> extend h F ≤ extend h G"
    by (force simp add: component_eq_subset)

    lemma (in Extend) project_mono: "F ≤ G ==> project h C F ≤ project h C G"
    by (simp add: component_eq_subset, blast)

    lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
    by (simp add: all_total_def Domain_extend_act)

    subsection{*Safety: co, stable*}

    lemma (in Extend) extend_constrains:
         "(extend h F ∈ (extend_set h A) co (extend_set h B)) =
          (F ∈ A co B)"
    by (simp add: constrains_def)

    lemma (in Extend) extend_stable:
         "(extend h F ∈ stable (extend_set h A)) = (F ∈ stable A)"
    by (simp add: stable_def extend_constrains)

    lemma (in Extend) extend_invariant:
         "(extend h F ∈ invariant (extend_set h A)) = (F ∈ invariant A)"
    by (simp add: invariant_def extend_stable)

    (*Projects the state predicates in the property satisfied by  extend h F.
      Converse fails: A and B may differ in their extra variables*)
    lemma (in Extend) extend_constrains_project_set:
         "extend h F ∈ A co B ==> F ∈ (project_set h A) co (project_set h B)"
    by (auto simp add: constrains_def, force)

    lemma (in Extend) extend_stable_project_set:
         "extend h F ∈ stable A ==> F ∈ stable (project_set h A)"
    by (simp add: stable_def extend_constrains_project_set)

    subsection{*Weak safety primitives: Co, Stable*}

    lemma (in Extend) reachable_extend_f:
         "p ∈ reachable (extend h F) ==> f p ∈ reachable F"
    apply (erule reachable.induct)
    apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
    done

    lemma (in Extend) h_reachable_extend:
         "h(s,y) ∈ reachable (extend h F) ==> s ∈ reachable F"
    by (force dest!: reachable_extend_f)

    lemma (in Extend) reachable_extend_eq:
         "reachable (extend h F) = extend_set h (reachable F)"
    apply (unfold extend_set_def)
    apply (rule equalityI)
    apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify)
    apply (erule reachable.induct)
    apply (force intro: reachable.intros)+
    done

    lemma (in Extend) extend_Constrains:
         "(extend h F ∈ (extend_set h A) Co (extend_set h B)) =
          (F ∈ A Co B)"
    by (simp add: Constrains_def reachable_extend_eq extend_constrains
                  extend_set_Int_distrib [symmetric])

    lemma (in Extend) extend_Stable:
         "(extend h F ∈ Stable (extend_set h A)) = (F ∈ Stable A)"
    by (simp add: Stable_def extend_Constrains)

    lemma (in Extend) extend_Always:
         "(extend h F ∈ Always (extend_set h A)) = (F ∈ Always A)"
    by (simp (no_asm_simp) add: Always_def extend_Stable)

    (** Safety and "project" **)

    (** projection: monotonicity for safety **)

    lemma project_act_mono:
         "D ⊆ C ==>
          project_act h (Restrict D act) ⊆ project_act h (Restrict C act)"
    by (auto simp add: project_act_def)

    lemma (in Extend) project_constrains_mono:
         "[| D ⊆ C; project h C F ∈ A co B |] ==> project h D F ∈ A co B"
    apply (auto simp add: constrains_def)
    apply (drule project_act_mono, blast)
    done

    lemma (in Extend) project_stable_mono:
         "[| D ⊆ C;  project h C F ∈ stable A |] ==> project h D F ∈ stable A"
    by (simp add: stable_def project_constrains_mono)

    (*Key lemma used in several proofs about project and co*)
    lemma (in Extend) project_constrains:
         "(project h C F ∈ A co B)  =
          (F ∈ (C ∩ extend_set h A) co (extend_set h B) & A ⊆ B)"
    apply (unfold constrains_def)
    apply (auto intro!: project_act_I simp add: ball_Un)
    apply (force intro!: project_act_I dest!: subsetD)
    (*the <== direction*)
    apply (unfold project_act_def)
    apply (force dest!: subsetD)
    done

    lemma (in Extend) project_stable:
         "(project h UNIV F ∈ stable A) = (F ∈ stable (extend_set h A))"
    apply (unfold stable_def)
    apply (simp (no_asm) add: project_constrains)
    done

    lemma (in Extend) project_stable_I:
         "F ∈ stable (extend_set h A) ==> project h C F ∈ stable A"
    apply (drule project_stable [THEN iffD2])
    apply (blast intro: project_stable_mono)
    done

    lemma (in Extend) Int_extend_set_lemma:
         "A ∩ extend_set h ((project_set h A) ∩ B) = A ∩ extend_set h B"
    by (auto simp add: split_extended_all)

    (*Strange (look at occurrences of C) but used in leadsETo proofs*)
    lemma project_constrains_project_set:
         "G ∈ C co B ==> project h C G ∈ project_set h C co project_set h B"
    by (simp add: constrains_def project_def project_act_def, blast)

    lemma project_stable_project_set:
         "G ∈ stable C ==> project h C G ∈ stable (project_set h C)"
    by (simp add: stable_def project_constrains_project_set)

    subsection{*Progress: transient, ensures*}

    lemma (in Extend) extend_transient:
         "(extend h F ∈ transient (extend_set h A)) = (F ∈ transient A)"
    by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)

    lemma (in Extend) extend_ensures:
         "(extend h F ∈ (extend_set h A) ensures (extend_set h B)) =
          (F ∈ A ensures B)"
    by (simp add: ensures_def extend_constrains extend_transient
            extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])

    lemma (in Extend) leadsTo_imp_extend_leadsTo:
         "F ∈ A leadsTo B
          ==> extend h F ∈ (extend_set h A) leadsTo (extend_set h B)"
    apply (erule leadsTo_induct)
      apply (simp add: leadsTo_Basis extend_ensures)
     apply (blast intro: leadsTo_Trans)
    apply (simp add: leadsTo_UN extend_set_Union)
    done

    subsection{*Proving the converse takes some doing!*}

    lemma (in Extend) slice_iff [iff]: "(x ∈ slice C y) = (h(x,y) ∈ C)"
    by (simp (no_asm) add: slice_def)

    lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x ∈ S. slice x y)"
    by auto

    lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
    by auto

    lemma (in Extend) project_set_is_UN_slice:
         "project_set h A = (\<Union>y. slice A y)"
    by auto

    lemma (in Extend) extend_transient_slice:
         "extend h F ∈ transient A ==> F ∈ transient (slice A y)"
    by (unfold transient_def, auto)

    (*Converse?*)
    lemma (in Extend) extend_constrains_slice:
         "extend h F ∈ A co B ==> F ∈ (slice A y) co (slice B y)"
    by (auto simp add: constrains_def)

    lemma (in Extend) extend_ensures_slice:
         "extend h F ∈ A ensures B ==> F ∈ (slice A y) ensures (project_set h B)"
    apply (auto simp add: ensures_def extend_constrains extend_transient)
    apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
    apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
    done

    lemma (in Extend) leadsTo_slice_project_set:
         "∀y. F ∈ (slice B y) leadsTo CU ==> F ∈ (project_set h B) leadsTo CU"
    apply (simp (no_asm) add: project_set_is_UN_slice)
    apply (blast intro: leadsTo_UN)
    done

    lemma (in Extend) extend_leadsTo_slice [rule_format]:
         "extend h F ∈ AU leadsTo BU
          ==> ∀y. F ∈ (slice AU y) leadsTo (project_set h BU)"
    apply (erule leadsTo_induct)
      apply (blast intro: extend_ensures_slice leadsTo_Basis)
     apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
    apply (simp add: leadsTo_UN slice_Union)
    done

    lemma (in Extend) extend_leadsTo:
         "(extend h F ∈ (extend_set h A) leadsTo (extend_set h B)) =
          (F ∈ A leadsTo B)"
    apply safe
    apply (erule_tac [2] leadsTo_imp_extend_leadsTo)
    apply (drule extend_leadsTo_slice)
    apply (simp add: slice_extend_set)
    done

    lemma (in Extend) extend_LeadsTo:
         "(extend h F ∈ (extend_set h A) LeadsTo (extend_set h B)) =
          (F ∈ A LeadsTo B)"
    by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
                  extend_set_Int_distrib [symmetric])

    subsection{*preserves*}

    lemma (in Extend) project_preserves_I:
         "G ∈ preserves (v o f) ==> project h C G ∈ preserves v"
    by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)

    (*to preserve f is to preserve the whole original state*)
    lemma (in Extend) project_preserves_id_I:
         "G ∈ preserves f ==> project h C G ∈ preserves id"
    by (simp add: project_preserves_I)

    lemma (in Extend) extend_preserves:
         "(extend h G ∈ preserves (v o f)) = (G ∈ preserves v)"
    by (auto simp add: preserves_def extend_stable [symmetric]
                       extend_set_eq_Collect)

    lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G ∈ preserves g)"
    by (auto simp add: preserves_def extend_def extend_act_def stable_def
                       constrains_def g_def)

    subsection{*Guarantees*}

    lemma (in Extend) project_extend_Join:
         "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
    apply (rule program_equalityI)
      apply (simp add: project_set_extend_set_Int)
     apply (simp add: image_eq_UN UN_Un, auto)
    done

    lemma (in Extend) extend_Join_eq_extend_D:
         "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
    apply (drule_tac f = "project h UNIV" in arg_cong)
    apply (simp add: project_extend_Join)
    done

    (** Strong precondition and postcondition; only useful when
        the old and new state sets are in bijection **)

    lemma (in Extend) ok_extend_imp_ok_project:
         "extend h F ok G ==> F ok project h UNIV G"
    apply (auto simp add: ok_def)
    apply (drule subsetD)
    apply (auto intro!: rev_image_eqI)
    done

    lemma (in Extend) ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
    apply (simp add: ok_def, safe)
    apply (force+)
    done

    lemma (in Extend) OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
    apply (unfold OK_def, safe)
    apply (drule_tac x = i in bspec)
    apply (drule_tac [2] x = j in bspec)
    apply (force+)
    done

    lemma (in Extend) guarantees_imp_extend_guarantees:
         "F ∈ X guarantees Y ==>
          extend h F ∈ (extend h ` X) guarantees (extend h ` Y)"
    apply (rule guaranteesI, clarify)
    apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D
                       guaranteesD)
    done

    lemma (in Extend) extend_guarantees_imp_guarantees:
         "extend h F ∈ (extend h ` X) guarantees (extend h ` Y)
          ==> F ∈ X guarantees Y"
    apply (auto simp add: guar_def)
    apply (drule_tac x = "extend h G" in spec)
    apply (simp del: extend_Join
                add: extend_Join [symmetric] ok_extend_iff
                     inj_extend [THEN inj_image_mem_iff])
    done

    lemma (in Extend) extend_guarantees_eq:
         "(extend h F ∈ (extend h ` X) guarantees (extend h ` Y)) =
          (F ∈ X guarantees Y)"
    by (blast intro: guarantees_imp_extend_guarantees
                     extend_guarantees_imp_guarantees)

    end

### Restrict

lemma Restrict_iff:

      ((x, y) ∈ Restrict A r) = ((x, y) ∈ r ∧ x ∈ A)

lemma Restrict_UNIV:

      Restrict UNIV = id

lemma Restrict_empty:

      Restrict {} r = {}

lemma Restrict_Int:

      Restrict A (Restrict B r) = Restrict (A ∩ B) r

lemma Restrict_triv:

      Domain r ⊆ A ==> Restrict A r = r

lemma Restrict_subset:

      Restrict A r ⊆ r

lemma Restrict_eq_mono:

      [| A ⊆ B; Restrict B r = Restrict B s |] ==> Restrict A r = Restrict A s

lemma Restrict_imageI:

      [| s ∈ RR; Restrict A r = Restrict A s |] ==> Restrict A r ∈ Restrict A ` RR

lemma Domain_Restrict:

      Domain (Restrict A r) = A ∩ Domain r

lemma Image_Restrict:

      Restrict A r `` B = r `` (A ∩ B)

lemma good_mapI:

      [| surj h; !!x x' y y'. h (x, y) = h (x', y') ==> x = x' |] ==> good_map h

lemma good_map_is_surj:

      good_map h ==> surj h

lemma fst_inv_equalityI:

      [| surj h; !!x y. g (h (x, y)) = x |] ==> fst (inv h z) = g z

### Trivial properties of f, g, h

lemma f_h_eq:

      Extend h ==> fst (inv h (h (x, y))) = x

lemma h_inject1:

      [| Extend h; h (x, y) = h (x', y') |] ==> x = x'

lemma h_f_g_equiv:

      Extend h ==> h (fst (inv h z), snd (inv h z)) == z

lemma h_f_g_eq:

      Extend h ==> h (fst (inv h z), snd (inv h z)) = z

lemma split_extended_all:

      Extend h ==> (!!z. PROP P z) == (!!u y. PROP P (h (u, y)))

### @{term extend_set}: basic properties

lemma project_set_iff:

      (x ∈ project_set h C) = (∃y. h (x, y) ∈ C)

lemma extend_set_mono:

      A ⊆ B ==> extend_set h A ⊆ extend_set h B

lemma mem_extend_set_iff:

      Extend h ==> (z ∈ extend_set h A) = (fst (inv h z) ∈ A)

lemma extend_set_strict_mono:

      Extend h ==> (extend_set h A ⊆ extend_set h B) = (A ⊆ B)

lemma extend_set_empty:

      extend_set h {} = {}

lemma extend_set_eq_Collect:

      Extend h ==> extend_set h {s. P s} = {s. P (fst (inv h s))}

lemma extend_set_sing:

      Extend h ==> extend_set h {x} = {s. fst (inv h s) = x}

lemma extend_set_inverse:

      Extend h ==> project_set h (extend_set h C) = C

lemma extend_set_project_set:

      Extend h ==> C ⊆ extend_set h (project_set h C)

lemma inj_extend_set:

      Extend h ==> inj (extend_set h)

lemma extend_set_UNIV_eq:

      Extend h ==> extend_set h UNIV = UNIV

### @{term project_set}: basic properties

lemma project_set_eq:

      Extend h ==> project_set h C = (%z. fst (inv h z)) ` C

lemma project_set_I:

      [| Extend h; z ∈ C |] ==> fst (inv h z) ∈ project_set h C

### More laws

lemma project_set_extend_set_Int:

      Extend h ==> project_set h (extend_set h A ∩ B) = A ∩ project_set h B

lemma project_set_extend_set_Un:

      Extend h ==> project_set h (extend_set h A ∪ B) = A ∪ project_set h B

lemma project_set_Int_subset:

      project_set h (A ∩ B) ⊆ project_set h A ∩ project_set h B

lemma extend_set_Un_distrib:

      Extend h ==> extend_set h (A ∪ B) = extend_set h A ∪ extend_set h B

lemma extend_set_Int_distrib:

      Extend h ==> extend_set h (A ∩ B) = extend_set h A ∩ extend_set h B

lemma extend_set_INT_distrib:

      Extend h ==> extend_set h (INTER A B) = (INT x:A. extend_set h (B x))

lemma extend_set_Diff_distrib:

      Extend h ==> extend_set h (A - B) = extend_set h A - extend_set h B

lemma extend_set_Union:

      Extend h ==> extend_set h (Union A) = (UN X:A. extend_set h X)

lemma extend_set_subset_Compl_eq:

      Extend h ==> (extend_set h A ⊆ - extend_set h B) = (A ⊆ - B)

### @{term extend_act}

lemma mem_extend_act_iff:

      Extend h ==> ((h (s, y), h (s', y)) ∈ extend_act h act) = ((s, s') ∈ act)

lemma extend_act_D:

      [| Extend h; (z, z') ∈ extend_act h act |]
      ==> (fst (inv h z), fst (inv h z')) ∈ act

lemma extend_act_inverse:

      Extend h ==> project_act h (extend_act h act) = act

lemma project_act_extend_act_restrict:

      Extend h
      ==> project_act h (Restrict C (extend_act h act)) =
          Restrict (project_set h C) act

lemma subset_extend_act_D:

      [| Extend h; act' ⊆ extend_act h act |] ==> project_act h act' ⊆ act

lemma inj_extend_act:

      Extend h ==> inj (extend_act h)

lemma extend_act_Image:

      Extend h ==> extend_act h act `` extend_set h A = extend_set h (act `` A)

lemma extend_act_strict_mono:

      Extend h ==> (extend_act h act' ⊆ extend_act h act) = (act' ⊆ act)

lemma Domain_extend_act:

      Domain (extend_act h act) = extend_set h (Domain act)

lemma extend_act_Id:

      Extend h ==> extend_act h Id = Id

lemma project_act_I:

      [| Extend h; (z, z') ∈ act |]
      ==> (fst (inv h z), fst (inv h z')) ∈ project_act h act

lemma project_act_Id:

      Extend h ==> project_act h Id = Id

lemma Domain_project_act:

      Extend h ==> Domain (project_act h act) = project_set h (Domain act)

### extend

lemma Init_extend:

      Init (extend h F) = extend_set h (Init F)

lemma Init_project:

      Init (project h C F) = project_set h (Init F)

lemma Acts_extend:

      Extend h ==> Acts (extend h F) = extend_act h ` Acts F

lemma AllowedActs_extend:

      Extend h ==> AllowedActs (extend h F) = project_act h -` AllowedActs F

lemma Acts_project:

      Acts (project h C F) = insert Id (project_act h ` Restrict C ` Acts F)

lemma AllowedActs_project:

      Extend h
      ==> AllowedActs (project h C F) =
          {act.
           Restrict (project_set h C) act
           ∈ project_act h ` Restrict C ` AllowedActs F}

lemma Allowed_extend:

      Extend h ==> Allowed (extend h F) = project h UNIV -` Allowed F

lemma extend_SKIP:

      Extend h ==> extend h SKIP = SKIP

lemma project_set_UNIV:

      project_set h UNIV = UNIV

lemma project_set_Union:

      project_set h (Union A) = (UN X:A. project_set h X)

lemma project_act_Restrict_subset:

      Extend h
      ==> project_act h (Restrict C act)
          ⊆ Restrict (project_set h C) (project_act h act)

lemma project_act_Restrict_Id_eq:

      Extend h ==> project_act h (Restrict C Id) = Restrict (project_set h C) Id

lemma project_extend_eq:

      Extend h
      ==> project h C (extend h F) =
          mk_program
           (Init F, Restrict (project_set h C) ` Acts F,
            {act.
             Restrict (project_set h C) act
             ∈ project_act h ` Restrict C ` project_act h -` AllowedActs F})

lemma extend_inverse:

      Extend h ==> project h UNIV (extend h F) = F

lemma inj_extend:

      Extend h ==> inj (extend h)

lemma extend_Join:

      Extend h ==> extend h (F Join G) = extend h F Join extend h G

lemma extend_JN:

      Extend h ==> extend h (JOIN I F) = (JN i:I. extend h (F i))

lemma extend_mono:

      [| Extend h; F ≤ G |] ==> extend h F ≤ extend h G

lemma project_mono:

      [| Extend h; F ≤ G |] ==> project h C F ≤ project h C G

lemma all_total_extend:

      [| Extend h; all_total F |] ==> all_total (extend h F)

### Safety: co, stable

lemma extend_constrains:

      Extend h ==> (extend h F ∈ extend_set h A co extend_set h B) = (F ∈ A co B)

lemma extend_stable:

      Extend h ==> (extend h F ∈ stable (extend_set h A)) = (F ∈ stable A)

lemma extend_invariant:

      Extend h ==> (extend h F ∈ invariant (extend_set h A)) = (F ∈ invariant A)

lemma extend_constrains_project_set:

      [| Extend h; extend h F ∈ A co B |] ==> F ∈ project_set h A co project_set h B

lemma extend_stable_project_set:

      [| Extend h; extend h F ∈ stable A |] ==> F ∈ stable (project_set h A)

### Weak safety primitives: Co, Stable

lemma reachable_extend_f:

      [| Extend h; p ∈ reachable (extend h F) |] ==> fst (inv h p) ∈ reachable F

lemma h_reachable_extend:

      [| Extend h; h (s, y) ∈ reachable (extend h F) |] ==> s ∈ reachable F

lemma reachable_extend_eq:

      Extend h ==> reachable (extend h F) = extend_set h (reachable F)

lemma extend_Constrains:

      Extend h ==> (extend h F ∈ extend_set h A Co extend_set h B) = (F ∈ A Co B)

lemma extend_Stable:

      Extend h ==> (extend h F ∈ Stable (extend_set h A)) = (F ∈ Stable A)

lemma extend_Always:

      Extend h ==> (extend h F ∈ Always (extend_set h A)) = (F ∈ Always A)

lemma project_act_mono:

      D ⊆ C ==> project_act h (Restrict D act) ⊆ project_act h (Restrict C act)

lemma project_constrains_mono:

      [| Extend h; D ⊆ C; project h C F ∈ A co B |] ==> project h D F ∈ A co B

lemma project_stable_mono:

      [| Extend h; D ⊆ C; project h C F ∈ stable A |] ==> project h D F ∈ stable A

lemma project_constrains:

      Extend h
      ==> (project h C F ∈ A co B) =
          (F ∈ C ∩ extend_set h A co extend_set h B ∧ A ⊆ B)

lemma project_stable:

      Extend h ==> (project h UNIV F ∈ stable A) = (F ∈ stable (extend_set h A))

lemma project_stable_I:

      [| Extend h; F ∈ stable (extend_set h A) |] ==> project h C F ∈ stable A

lemma Int_extend_set_lemma:

      Extend h ==> A ∩ extend_set h (project_set h A ∩ B) = A ∩ extend_set h B

lemma project_constrains_project_set:

      G ∈ C co B ==> project h C G ∈ project_set h C co project_set h B

lemma project_stable_project_set:

      G ∈ stable C ==> project h C G ∈ stable (project_set h C)

### Progress: transient, ensures

lemma extend_transient:

      Extend h ==> (extend h F ∈ transient (extend_set h A)) = (F ∈ transient A)

lemma extend_ensures:

      Extend h
      ==> (extend h F ∈ extend_set h A ensures extend_set h B) = (F ∈ A ensures B)

lemma leadsTo_imp_extend_leadsTo:

      [| Extend h; F ∈ A leadsTo B |]
      ==> extend h F ∈ extend_set h A leadsTo extend_set h B

### Proving the converse takes some doing!

lemma slice_iff:

      Extend h ==> (x ∈ {x. h (x, y) ∈ C}) = (h (x, y) ∈ C)

lemma slice_Union:

      Extend h ==> {x. h (x, y) ∈ Union S} = (UN x:S. {xa. h (xa, y) ∈ x})

lemma slice_extend_set:

      Extend h ==> {x. h (x, y) ∈ extend_set h A} = A

lemma project_set_is_UN_slice:

      Extend h ==> project_set h A = (UN y. {x. h (x, y) ∈ A})

lemma extend_transient_slice:

      [| Extend h; extend h F ∈ transient A |] ==> F ∈ transient {x. h (x, y) ∈ A}

lemma extend_constrains_slice:

      [| Extend h; extend h F ∈ A co B |]
      ==> F ∈ {x. h (x, y) ∈ A} co {x. h (x, y) ∈ B}

lemma extend_ensures_slice:

      [| Extend h; extend h F ∈ A ensures B |]
      ==> F ∈ {x. h (x, y) ∈ A} ensures project_set h B

lemma leadsTo_slice_project_set:

      [| Extend h; ∀y. F ∈ {x. h (x, y) ∈ B} leadsTo CU |]
      ==> F ∈ project_set h B leadsTo CU

lemma extend_leadsTo_slice:

      [| Extend h; extend h F ∈ AU leadsTo BU |]
      ==> ∀y. F ∈ {x. h (x, y) ∈ AU} leadsTo project_set h BU

lemma extend_leadsTo:

      Extend h
      ==> (extend h F ∈ extend_set h A leadsTo extend_set h B) = (F ∈ A leadsTo B)

lemma extend_LeadsTo:

      Extend h
      ==> (extend h F ∈ extend_set h A LeadsTo extend_set h B) = (F ∈ A LeadsTo B)

### preserves

lemma project_preserves_I:

      [| Extend h; G ∈ preserves (v o (%z. fst (inv h z))) |]
      ==> project h C G ∈ preserves v

lemma project_preserves_id_I:

      [| Extend h; G ∈ preserves (%z. fst (inv h z)) |]
      ==> project h C G ∈ preserves id

lemma extend_preserves:

      Extend h
      ==> (extend h G ∈ preserves (v o (%z. fst (inv h z)))) = (G ∈ preserves v)

lemma inj_extend_preserves:

      [| Extend h; inj h |] ==> extend h G ∈ preserves (%z. snd (inv h z))

### Guarantees

lemma project_extend_Join:

      Extend h ==> project h UNIV (extend h F Join G) = F Join project h UNIV G

lemma extend_Join_eq_extend_D:

      [| Extend h; extend h F Join G = extend h H |] ==> H = F Join project h UNIV G

lemma ok_extend_imp_ok_project:

      [| Extend h; extend h F ok G |] ==> F ok project h UNIV G

lemma ok_extend_iff:

      Extend h ==> extend h F ok extend h G = F ok G

lemma OK_extend_iff:

      Extend h ==> OK I (%i. extend h (F i)) = OK I F

lemma guarantees_imp_extend_guarantees:

      [| Extend h; F ∈ X guarantees Y |]
      ==> extend h F ∈ extend h ` X guarantees extend h ` Y

lemma extend_guarantees_imp_guarantees:

      [| Extend h; extend h F ∈ extend h ` X guarantees extend h ` Y |]
      ==> F ∈ X guarantees Y

lemma extend_guarantees_eq:

      Extend h
      ==> (extend h F ∈ extend h ` X guarantees extend h ` Y) = (F ∈ X guarantees Y)