# Theory Lift_prog

Up to index of Isabelle/HOL/UNITY

theory Lift_prog
imports Rename
begin

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

    lift_prog, etc: replication of components and arrays of processes.
    *)

    header{*Replication of Components*}

    theory Lift_prog imports Rename begin

    constdefs

      insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)"
        "insert_map i z f k == if k<i then f k
                               else if k=i then z
                               else f(k - 1)"

      delete_map :: "[nat, nat=>'b] => (nat=>'b)"
        "delete_map i g k == if k<i then g k else g (Suc k)"

      lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c"
        "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"

      drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)"
        "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"

      lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
        "lift_set i A == lift_map i ` A"

      lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
        "lift i == rename (lift_map i)"

      (*simplifies the expression of specifications*)
      sub :: "['a, 'a=>'b] => 'b"
        "sub == %i f. f i"

    declare insert_map_def [simp] delete_map_def [simp]

    lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
    by (rule ext, simp)

    lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
    apply (rule ext)
    apply (auto split add: nat_diff_split)
    done

    subsection{*Injectiveness proof*}

    lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
    by (drule_tac x = i in fun_cong, simp)

    lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
    apply (drule_tac f = "delete_map i" in arg_cong)
    apply (simp add: insert_map_inverse)
    done

    lemma insert_map_inject':
         "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"
    by (blast dest: insert_map_inject1 insert_map_inject2)

    lemmas insert_map_inject = insert_map_inject' [THEN conjE, elim!]

    (*The general case: we don't assume i=i'*)
    lemma lift_map_eq_iff [iff]:
         "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))
          = (uu = uu' & insert_map i s f = insert_map i' s' f')"
    by (unfold lift_map_def, auto)

    (*The !!s allows the automatic splitting of the bound variable*)
    lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
    apply (unfold lift_map_def drop_map_def)
    apply (force intro: insert_map_inverse)
    done

    lemma inj_lift_map: "inj (lift_map i)"
    apply (unfold lift_map_def)
    apply (rule inj_onI, auto)
    done

    subsection{*Surjectiveness proof*}

    lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
    apply (unfold lift_map_def drop_map_def)
    apply (force simp add: insert_map_delete_map_eq)
    done

    lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
    by (drule_tac f = "lift_map i" in arg_cong, simp)

    lemma surj_lift_map: "surj (lift_map i)"
    apply (rule surjI)
    apply (rule lift_map_drop_map_eq)
    done

    lemma bij_lift_map [iff]: "bij (lift_map i)"
    by (simp add: bij_def inj_lift_map surj_lift_map)

    lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
    by (rule inv_equality, auto)

    lemma inv_drop_map_eq [simp]: "inv (drop_map i) = lift_map i"
    by (rule inv_equality, auto)

    lemma bij_drop_map [iff]: "bij (drop_map i)"
    by (simp del: inv_lift_map_eq add: inv_lift_map_eq [symmetric] bij_imp_bij_inv)

    (*sub's main property!*)
    lemma sub_apply [simp]: "sub i f = f i"
    by (simp add: sub_def)

    lemma all_total_lift: "all_total F ==> all_total (lift i F)"
    by (simp add: lift_def rename_def Extend.all_total_extend)

    lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
    by (rule ext, auto)

    lemma insert_map_upd:
         "(insert_map j t f)(i := s) =
          (if i=j then insert_map i s f
           else if i<j then insert_map j t (f(i:=s))
           else insert_map j t (f(i - Suc 0 := s)))"
    apply (rule ext)
    apply (simp split add: nat_diff_split)
     txt{*This simplification is VERY slow*}
    done

    lemma insert_map_eq_diff:
         "[| insert_map i s f = insert_map j t g;  i≠j |]
          ==> ∃g'. insert_map i s' f = insert_map j t g'"
    apply (subst insert_map_upd_same [symmetric])
    apply (erule ssubst)
    apply (simp only: insert_map_upd if_False split: split_if, blast)
    done

    lemma lift_map_eq_diff:
         "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i≠j |]
          ==> ∃g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
    apply (unfold lift_map_def, auto)
    apply (blast dest: insert_map_eq_diff)
    done

    subsection{*The Operator @{term lift_set}*}

    lemma lift_set_empty [simp]: "lift_set i {} = {}"
    by (unfold lift_set_def, auto)

    lemma lift_set_iff: "(lift_map i x ∈ lift_set i A) = (x ∈ A)"
    apply (unfold lift_set_def)
    apply (rule inj_lift_map [THEN inj_image_mem_iff])
    done

    (*Do we really need both this one and its predecessor?*)
    lemma lift_set_iff2 [iff]:
         "((f,uu) ∈ lift_set i A) = ((f i, (delete_map i f, uu)) ∈ A)"
    by (simp add: lift_set_def mem_rename_set_iff drop_map_def)

    lemma lift_set_mono: "A ⊆ B ==> lift_set i A ⊆ lift_set i B"
    apply (unfold lift_set_def)
    apply (erule image_mono)
    done

    lemma lift_set_Un_distrib: "lift_set i (A ∪ B) = lift_set i A ∪ lift_set i B"
    by (simp add: lift_set_def image_Un)

    lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
    apply (unfold lift_set_def)
    apply (rule inj_lift_map [THEN image_set_diff])
    done

    subsection{*The Lattice Operations*}

    lemma bij_lift [iff]: "bij (lift i)"
    by (simp add: lift_def)

    lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
    by (simp add: lift_def)

    lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
    by (simp add: lift_def)

    lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i ∈ I. lift j (F i))"
    by (simp add: lift_def)

    subsection{*Safety: constrains, stable, invariant*}

    lemma lift_constrains:
         "(lift i F ∈ (lift_set i A) co (lift_set i B)) = (F ∈ A co B)"
    by (simp add: lift_def lift_set_def rename_constrains)

    lemma lift_stable:
         "(lift i F ∈ stable (lift_set i A)) = (F ∈ stable A)"
    by (simp add: lift_def lift_set_def rename_stable)

    lemma lift_invariant:
         "(lift i F ∈ invariant (lift_set i A)) = (F ∈ invariant A)"
    by (simp add: lift_def lift_set_def rename_invariant)

    lemma lift_Constrains:
         "(lift i F ∈ (lift_set i A) Co (lift_set i B)) = (F ∈ A Co B)"
    by (simp add: lift_def lift_set_def rename_Constrains)

    lemma lift_Stable:
         "(lift i F ∈ Stable (lift_set i A)) = (F ∈ Stable A)"
    by (simp add: lift_def lift_set_def rename_Stable)

    lemma lift_Always:
         "(lift i F ∈ Always (lift_set i A)) = (F ∈ Always A)"
    by (simp add: lift_def lift_set_def rename_Always)

    subsection{*Progress: transient, ensures*}

    lemma lift_transient:
         "(lift i F ∈ transient (lift_set i A)) = (F ∈ transient A)"
    by (simp add: lift_def lift_set_def rename_transient)

    lemma lift_ensures:
         "(lift i F ∈ (lift_set i A) ensures (lift_set i B)) =
          (F ∈ A ensures B)"
    by (simp add: lift_def lift_set_def rename_ensures)

    lemma lift_leadsTo:
         "(lift i F ∈ (lift_set i A) leadsTo (lift_set i B)) =
          (F ∈ A leadsTo B)"
    by (simp add: lift_def lift_set_def rename_leadsTo)

    lemma lift_LeadsTo:
         "(lift i F ∈ (lift_set i A) LeadsTo (lift_set i B)) =
          (F ∈ A LeadsTo B)"
    by (simp add: lift_def lift_set_def rename_LeadsTo)

    (** guarantees **)

    lemma lift_lift_guarantees_eq:
         "(lift i F ∈ (lift i ` X) guarantees (lift i ` Y)) =
          (F ∈ X guarantees Y)"
    apply (unfold lift_def)
    apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
    apply (simp add: o_def)
    done

    lemma lift_guarantees_eq_lift_inv:
         "(lift i F ∈ X guarantees Y) =
          (F ∈ (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
    by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)

    (*To preserve snd means that the second component is there just to allow
      guarantees properties to be stated.  Converse fails, for lift i F can
      change function components other than i*)
    lemma lift_preserves_snd_I: "F ∈ preserves snd ==> lift i F ∈ preserves snd"
    apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
    apply (simp add: lift_def rename_preserves)
    apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
    done

    lemma delete_map_eqE':
         "(delete_map i g) = (delete_map i g') ==> ∃x. g = g'(i:=x)"
    apply (drule_tac f = "insert_map i (g i) " in arg_cong)
    apply (simp add: insert_map_delete_map_eq)
    apply (erule exI)
    done

    lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]

    lemma delete_map_neq_apply:
         "[| delete_map j g = delete_map j g';  i≠j |] ==> g i = g' i"
    by force

    (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)

    lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
    by auto

    lemma vimage_sub_eq_lift_set [simp]:
         "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
    by auto

    lemma mem_lift_act_iff [iff]:
         "((s,s') ∈ extend_act (%(x,u::unit). lift_map i x) act) =
          ((drop_map i s, drop_map i s') ∈ act)"
    apply (unfold extend_act_def, auto)
    apply (rule bexI, auto)
    done

    lemma preserves_snd_lift_stable:
         "[| F ∈ preserves snd;  i≠j |]
          ==> lift j F ∈ stable (lift_set i (A <*> UNIV))"
    apply (auto simp add: lift_def lift_set_def stable_def constrains_def
                          rename_def extend_def mem_rename_set_iff)
    apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
    apply (drule_tac x = i in fun_cong, auto)
    done

    (*If i≠j then lift j F  does nothing to lift_set i, and the
      premise ensures A ⊆ B.*)
    lemma constrains_imp_lift_constrains:
        "[| F i ∈ (A <*> UNIV) co (B <*> UNIV);
            F j ∈ preserves snd |]
         ==> lift j (F j) ∈ (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
    apply (case_tac "i=j")
    apply (simp add: lift_def lift_set_def rename_constrains)
    apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
           assumption)
    apply (erule constrains_imp_subset [THEN lift_set_mono])
    done

    (*USELESS??*)
    lemma lift_map_image_Times:
         "lift_map i ` (A <*> UNIV) =
          (\<Union>s ∈ A. \<Union>f. {insert_map i s f}) <*> UNIV"
    apply (auto intro!: bexI image_eqI simp add: lift_map_def)
    apply (rule split_conv [symmetric])
    done

    lemma lift_preserves_eq:
         "(lift i F ∈ preserves v) = (F ∈ preserves (v o lift_map i))"
    by (simp add: lift_def rename_preserves)

    (*A useful rewrite.  If o, sub have been rewritten out already then can also
      use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
    lemma lift_preserves_sub:
         "F ∈ preserves snd
          ==> lift i F ∈ preserves (v o sub j o fst) =
              (if i=j then F ∈ preserves (v o fst) else True)"
    apply (drule subset_preserves_o [THEN subsetD])
    apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
    apply (auto cong del: if_weak_cong
           simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
    done

    subsection{*Lemmas to Handle Function Composition (o) More Consistently*}

    (*Lets us prove one version of a theorem and store others*)
    lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
    by (simp add: expand_fun_eq o_def)

    lemma o_equiv_apply: "f o g = h ==> ∀x. f(g x) = h x"
    by (simp add: expand_fun_eq o_def)

    lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
    apply (rule ext)
    apply (auto simp add: o_def lift_map_def sub_def)
    done

    lemma snd_o_lift_map: "snd o lift_map i = snd o snd"
    apply (rule ext)
    apply (auto simp add: o_def lift_map_def)
    done

    subsection{*More lemmas about extend and project*}

    text{*They could be moved to theory Extend or Project*}

    lemma extend_act_extend_act:
         "extend_act h' (extend_act h act) =
          extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
    apply (auto elim!: rev_bexI simp add: extend_act_def, blast)
    done

    lemma project_act_project_act:
         "project_act h (project_act h' act) =
          project_act (%(x,(y,y')). h'(h(x,y),y')) act"
    by (auto elim!: rev_bexI simp add: project_act_def)

    lemma project_act_extend_act:
         "project_act h (extend_act h' act) =
            {(x,x'). ∃s s' y y' z. (s,s') ∈ act &
                     h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
    by (simp add: extend_act_def project_act_def, blast)

    subsection{*OK and "lift"*}

    lemma act_in_UNION_preserves_fst:
         "act ⊆ {(x,x'). fst x = fst x'} ==> act ∈ UNION (preserves fst) Acts"
    apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
    apply (auto simp add: preserves_def stable_def constrains_def)
    done

    lemma UNION_OK_lift_I:
         "[| ∀i ∈ I. F i ∈ preserves snd;
             ∀i ∈ I. UNION (preserves fst) Acts ⊆ AllowedActs (F i) |]
          ==> OK I (%i. lift i (F i))"
    apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
    apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
    apply (rename_tac "act")
    apply (subgoal_tac
           "{(x, x'). ∃s f u s' f' u'.
                        ((s, f, u), s', f', u') ∈ act &
                        lift_map j x = lift_map i (s, f, u) &
                        lift_map j x' = lift_map i (s', f', u') }
                    ⊆ { (x,x') . fst x = fst x'}")
    apply (blast intro: act_in_UNION_preserves_fst, clarify)
    apply (drule_tac x = j in fun_cong)+
    apply (drule_tac x = i in bspec, assumption)
    apply (frule preserves_imp_eq, auto)
    done

    lemma OK_lift_I:
         "[| ∀i ∈ I. F i ∈ preserves snd;
             ∀i ∈ I. preserves fst ⊆ Allowed (F i) |]
          ==> OK I (%i. lift i (F i))"
    by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)

    lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
    by (simp add: lift_def Allowed_rename)

    lemma lift_image_preserves:
         "lift i ` preserves v = preserves (v o drop_map i)"
    by (simp add: rename_image_preserves lift_def inv_lift_map_eq)

    end

lemma insert_map_inverse:

      delete_map i (insert_map i x f) = f

lemma insert_map_delete_map_eq:

      insert_map i x (delete_map i g) = g(i := x)

### Injectiveness proof

lemma insert_map_inject1:

      insert_map i x f = insert_map i y g ==> x = y

lemma insert_map_inject2:

      insert_map i x f = insert_map i y g ==> f = g

lemma insert_map_inject':

      insert_map i x f = insert_map i y g ==> x = y ∧ f = g

lemmas insert_map_inject:

      [| insert_map i1 x1 f1 = insert_map i1 y1 g1; [| x1 = y1; f1 = g1 |] ==> R |]
      ==> R

lemmas insert_map_inject:

      [| insert_map i1 x1 f1 = insert_map i1 y1 g1; [| x1 = y1; f1 = g1 |] ==> R |]
      ==> R

lemma lift_map_eq_iff:

      (lift_map i (s, f, uu) = lift_map i' (s', f', uu')) =
      (uu = uu' ∧ insert_map i s f = insert_map i' s' f')

lemma drop_map_lift_map_eq:

      drop_map i (lift_map i s) = s

lemma inj_lift_map:

      inj (lift_map i)

### Surjectiveness proof

lemma lift_map_drop_map_eq:

      lift_map i (drop_map i s) = s

lemma drop_map_inject:

      drop_map i s = drop_map i s' ==> s = s'

lemma surj_lift_map:

      surj (lift_map i)

lemma bij_lift_map:

      bij (lift_map i)

lemma inv_lift_map_eq:

      inv (lift_map i) = drop_map i

lemma inv_drop_map_eq:

      inv (drop_map i) = lift_map i

lemma bij_drop_map:

      bij (drop_map i)

lemma sub_apply:

      sub i f = f i

lemma all_total_lift:

      all_total F ==> all_total (lift i F)

lemma insert_map_upd_same:

      (insert_map i t f)(i := s) = insert_map i s f

lemma insert_map_upd:

      (insert_map j t f)(i := s) =
      (if i = j then insert_map i s f
       else if i < j then insert_map j t (f(i := s))
            else insert_map j t (f(i - Suc 0 := s)))

lemma insert_map_eq_diff:

      [| insert_map i s f = insert_map j t g; i ≠ j |]
      ==> ∃g'. insert_map i s' f = insert_map j t g'

lemma lift_map_eq_diff:

      [| lift_map i (s, f, uu) = lift_map j (t, g, vv); i ≠ j |]
      ==> ∃g'. lift_map i (s', f, uu) = lift_map j (t, g', vv)

### The Operator @{term lift_set}

lemma lift_set_empty:

      lift_set i {} = {}

lemma lift_set_iff:

      (lift_map i x ∈ lift_set i A) = (x ∈ A)

lemma lift_set_iff2:

      ((f, uu) ∈ lift_set i A) = ((f i, delete_map i f, uu) ∈ A)

lemma lift_set_mono:

      A ⊆ B ==> lift_set i A ⊆ lift_set i B

lemma lift_set_Un_distrib:

      lift_set i (A ∪ B) = lift_set i A ∪ lift_set i B

lemma lift_set_Diff_distrib:

      lift_set i (A - B) = lift_set i A - lift_set i B

### The Lattice Operations

lemma bij_lift:

      bij (lift i)

lemma lift_SKIP:

      lift i SKIP = SKIP

lemma lift_Join:

      lift i (F Join G) = lift i F Join lift i G

lemma lift_JN:

      lift j (JOIN I F) = (JN i:I. lift j (F i))

### Safety: constrains, stable, invariant

lemma lift_constrains:

      (lift i F ∈ lift_set i A co lift_set i B) = (F ∈ A co B)

lemma lift_stable:

      (lift i F ∈ stable (lift_set i A)) = (F ∈ stable A)

lemma lift_invariant:

      (lift i F ∈ invariant (lift_set i A)) = (F ∈ invariant A)

lemma lift_Constrains:

      (lift i F ∈ lift_set i A Co lift_set i B) = (F ∈ A Co B)

lemma lift_Stable:

      (lift i F ∈ Stable (lift_set i A)) = (F ∈ Stable A)

lemma lift_Always:

      (lift i F ∈ Always (lift_set i A)) = (F ∈ Always A)

### Progress: transient, ensures

lemma lift_transient:

      (lift i F ∈ transient (lift_set i A)) = (F ∈ transient A)

lemma lift_ensures:

      (lift i F ∈ lift_set i A ensures lift_set i B) = (F ∈ A ensures B)

lemma lift_leadsTo:

      (lift i F ∈ lift_set i A leadsTo lift_set i B) = (F ∈ A leadsTo B)

lemma lift_LeadsTo:

      (lift i F ∈ lift_set i A LeadsTo lift_set i B) = (F ∈ A LeadsTo B)

lemma lift_lift_guarantees_eq:

      (lift i F ∈ lift i ` X guarantees lift i ` Y) = (F ∈ X guarantees Y)

lemma lift_guarantees_eq_lift_inv:

      (lift i F ∈ X guarantees Y) =
      (F ∈ rename (drop_map i) ` X guarantees rename (drop_map i) ` Y)

lemma lift_preserves_snd_I:

      F ∈ preserves snd ==> lift i F ∈ preserves snd

lemma delete_map_eqE':

      delete_map i g = delete_map i g' ==> ∃x. g = g'(i := x)

lemmas delete_map_eqE:

      [| delete_map i1 g1 = delete_map i1 g'1; !!x. g1 = g'1(i1 := x) ==> Q |] ==> Q

lemmas delete_map_eqE:

      [| delete_map i1 g1 = delete_map i1 g'1; !!x. g1 = g'1(i1 := x) ==> Q |] ==> Q

lemma delete_map_neq_apply:

      [| delete_map j g = delete_map j g'; i ≠ j |] ==> g i = g' i

lemma vimage_o_fst_eq:

      (f o fst) -` A = f -` A × UNIV

lemma vimage_sub_eq_lift_set:

      sub i -` A × UNIV = lift_set i (A × UNIV)

lemma mem_lift_act_iff:

      ((s, s') ∈ extend_act (%(x, u). lift_map i x) act) =
      ((drop_map i s, drop_map i s') ∈ act)

lemma preserves_snd_lift_stable:

      [| F ∈ preserves snd; i ≠ j |] ==> lift j F ∈ stable (lift_set i (A × UNIV))

lemma constrains_imp_lift_constrains:

      [| F i ∈ A × UNIV co B × UNIV; F j ∈ preserves snd |]
      ==> lift j (F j) ∈ lift_set i (A × UNIV) co lift_set i (B × UNIV)

lemma lift_map_image_Times:

      lift_map i ` (A × UNIV) = (UN s:A. UN f. {insert_map i s f}) × UNIV

lemma lift_preserves_eq:

      (lift i F ∈ preserves v) = (F ∈ preserves (v o lift_map i))

lemma lift_preserves_sub:

      F ∈ preserves snd
      ==> (lift i F ∈ preserves (v o sub j o fst)) =
          (if i = j then F ∈ preserves (v o fst) else True)

### Lemmas to Handle Function Composition (o) More Consistently

lemma o_equiv_assoc:

      f o g = h ==> f' o f o g = f' o h

lemma o_equiv_apply:

      f o g = h ==> ∀x. f (g x) = h x

lemma fst_o_lift_map:

      sub i o fst o lift_map i = fst

lemma snd_o_lift_map:

      snd o lift_map i = snd o snd

### More lemmas about extend and project

lemma extend_act_extend_act:

      extend_act h' (extend_act h act) =
      extend_act (%(x, y, y'). h' (h (x, y), y')) act

lemma project_act_project_act:

      project_act h (project_act h' act) =
      project_act (%(x, y, y'). h' (h (x, y), y')) act

lemma project_act_extend_act:

      project_act h (extend_act h' act) =
      {(x, x').
       ∃s s' y y' z. (s, s') ∈ act ∧ h (x, y) = h' (s, z) ∧ h (x', y') = h' (s', z)}

### OK and "lift"

lemma act_in_UNION_preserves_fst:

      act ⊆ {(x, x'). fst x = fst x'} ==> act ∈ UNION (preserves fst) Acts

lemma UNION_OK_lift_I:

      [| ∀i∈I. F i ∈ preserves snd;
         ∀i∈I. UNION (preserves fst) Acts ⊆ AllowedActs (F i) |]
      ==> OK I (%i. lift i (F i))

lemma OK_lift_I:

      [| ∀i∈I. F i ∈ preserves snd; ∀i∈I. preserves fst ⊆ Allowed (F i) |]
      ==> OK I (%i. lift i (F i))

lemma Allowed_lift:

      Allowed (lift i F) = lift i ` Allowed F

lemma lift_image_preserves:

      lift i ` preserves v = preserves (v o drop_map i)