# Theory Table

Up to index of Isabelle/HOL/Bali

theory Table
imports Basis
begin

    (*  Title:      HOL/Bali/Table.thy
        ID:         $Id: Table.thy,v 1.12 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb
    *)
    header {* Abstract tables and their implementation as lists *}

    theory Table imports Basis begin

    text {*
    design issues:
    \begin{itemize}
    \item definition of table: infinite map vs. list vs. finite set
          list chosen, because:
      \begin{itemize}
      \item[+]  a priori finite
      \item[+]  lookup is more operational than for finite set
      \item[-]  not very abstract, but function table converts it to abstract
                mapping
      \end{itemize}
    \item coding of lookup result: Some/None vs. value/arbitrary
       Some/None chosen, because:
      \begin{itemize}
      \item[++] makes definedness check possible (applies also to finite set),
         which is important for the type standard, hiding/overriding, etc.
         (though it may perhaps be possible at least for the operational semantics
          to treat programs as infinite, i.e. where classes, fields, methods etc.
          of any name are considered to be defined)
      \item[-]  sometimes awkward case distinctions, alleviated by operator 'the'
      \end{itemize}
    \end{itemize}
    *}

    types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
          = "'a \<rightharpoonup> 'b"
          ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
          = "'a => 'b set"

    section "map of / table of"

    syntax
      table_of      :: "('a × 'b) list => ('a, 'b) table"   --{* concrete table *}

    translations
      "table_of" == "map_of"

      (type)"'a \<rightharpoonup> 'b"       <= (type)"'a => 'b Option.option"
      (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"

    (* ### To map *)
    lemma map_add_find_left[simp]:
    "n k = None ==> (m ++ n) k = m k"
    by (simp add: map_add_def)

    section {* Conditional Override *}
    constdefs
    cond_override::
      "('b =>'b => bool) => ('a, 'b)table => ('a, 'b)table => ('a, 'b) table"

    --{* when merging tables old and new, only override an entry of table old when
       the condition cond holds *}
    "cond_override cond old new ≡
     λ k.
      (case new k of
         None         => old k
       | Some new_val => (case old k of
                            None         => Some new_val
                          | Some old_val => (if cond new_val old_val
                                             then Some new_val
                                             else Some old_val)))"

    lemma cond_override_empty1[simp]: "cond_override c empty t = t"
    by (simp add: cond_override_def expand_fun_eq)

    lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    by (simp add: cond_override_def expand_fun_eq)

    lemma cond_override_None[simp]:
     "old k = None ==> (cond_override c old new) k = new k"
    by (simp add: cond_override_def)

    lemma cond_override_override:
     "[|old k = Some ov;new k = Some nv; C nv ov|]
      ==> (cond_override C old new) k = Some nv"
    by (auto simp add: cond_override_def)

    lemma cond_override_noOverride:
     "[|old k = Some ov;new k = Some nv; ¬ (C nv ov)|]
      ==> (cond_override C old new) k = Some ov"
    by (auto simp add: cond_override_def)

    lemma dom_cond_override: "dom (cond_override C s t) ⊆ dom s ∪ dom t"
    by (auto simp add: cond_override_def dom_def)

    lemma finite_dom_cond_override:
     "[| finite (dom s); finite (dom t) |] ==> finite (dom (cond_override C s t))"
    apply (rule_tac B="dom s ∪ dom t" in finite_subset)
    apply (rule dom_cond_override)
    by (rule finite_UnI)

    section {* Filter on Tables *}

    constdefs
    filter_tab:: "('a => 'b => bool) => ('a, 'b) table => ('a, 'b) table"
    "filter_tab c t ≡ λ k. (case t k of
                               None   => None
                             | Some x => if c k x then Some x else None)"

    lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
    by (simp add: filter_tab_def empty_def)

    lemma filter_tab_True[simp]: "filter_tab (λx y. True) t = t"
    by (simp add: expand_fun_eq filter_tab_def)

    lemma filter_tab_False[simp]: "filter_tab (λx y. False) t = empty"
    by (simp add: expand_fun_eq filter_tab_def empty_def)

    lemma filter_tab_ran_subset: "ran (filter_tab c t) ⊆ ran t"
    by (auto simp add: filter_tab_def ran_def)

    lemma filter_tab_range_subset: "range (filter_tab c t) ⊆ range t ∪ {None}"
    apply (auto simp add: filter_tab_def)
    apply (drule sym, blast)
    done

    lemma finite_range_filter_tab:
      "finite (range t) ==> finite (range (filter_tab c t))"
    apply (rule_tac B="range t ∪ {None} " in finite_subset)
    apply (rule filter_tab_range_subset)
    apply (auto intro: finite_UnI)
    done

    lemma filter_tab_SomeD[dest!]:
    "filter_tab c t k = Some x ==> (t k = Some x) ∧ c k x"
    by (auto simp add: filter_tab_def)

    lemma filter_tab_SomeI: "[|t k = Some x;C k x|] ==>filter_tab C t k = Some x"
    by (simp add: filter_tab_def)

    lemma filter_tab_all_True:
     "∀ k y. t k = Some y --> p k y ==>filter_tab p t = t"
    apply (auto simp add: filter_tab_def expand_fun_eq)
    done

    lemma filter_tab_all_True_Some:
     "[|∀ k y. t k = Some y --> p k y; t k = Some v|] ==> filter_tab p t k = Some v"
    by (auto simp add: filter_tab_def expand_fun_eq)

    lemma filter_tab_all_False:
     "∀ k y. t k = Some y --> ¬ p k y ==>filter_tab p t = empty"
    by (auto simp add: filter_tab_def expand_fun_eq)

    lemma filter_tab_None: "t k = None ==> filter_tab p t k = None"
    apply (simp add: filter_tab_def expand_fun_eq)
    done

    lemma filter_tab_dom_subset: "dom (filter_tab C t) ⊆ dom t"
    by (auto simp add: filter_tab_def dom_def)

    lemma filter_tab_eq: "[|a=b|] ==> filter_tab C a = filter_tab C b"
    by (auto simp add: expand_fun_eq filter_tab_def)

    lemma finite_dom_filter_tab:
    "finite (dom t) ==> finite (dom (filter_tab C t))"
    apply (rule_tac B="dom t" in finite_subset)
    by (rule filter_tab_dom_subset)

    lemma filter_tab_weaken:
    "[|∀ a ∈ t k: ∃ b ∈ s k: P a b;
      !! k x y. [|t k = Some x;s k = Some y|] ==> cond k x --> cond k y
     |] ==> ∀ a ∈ filter_tab cond t k: ∃ b ∈ filter_tab cond s k: P a b"
    apply (force simp add: filter_tab_def)
    done

    lemma cond_override_filter:
      "[|!! k old new. [|s k = Some new; t k = Some old|]
        ==> (¬ overC new old -->  ¬ filterC k new) ∧
            (overC new old --> filterC k old --> filterC k new)
       |] ==>
        cond_override overC (filter_tab filterC t) (filter_tab filterC s)
        = filter_tab filterC (cond_override overC t s)"
    by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )

    section {* Misc. *}

    lemma Ball_set_table: "(∀ (x,y)∈ set l. P x y) ==> ∀ x. ∀ y∈ map_of l x: P x y"
    apply (erule make_imp)
    apply (induct l)
    apply simp
    apply (simp (no_asm))
    apply auto
    done

    lemma Ball_set_tableD:
      "[|(∀ (x,y)∈ set l. P x y); x ∈ o2s (table_of l xa)|] ==> P xa x"
    apply (frule Ball_set_table)
    by auto

    declare map_of_SomeD [elim]

    lemma table_of_Some_in_set:
    "table_of l k = Some x ==> (k,x) ∈ set l"
    by auto

    lemma set_get_eq:
      "unique l ==> (k, the (table_of l k)) ∈ set l = (table_of l k ≠ None)"
    apply safe
    apply (fast dest!: weak_map_of_SomeI)
    apply auto
    done

    lemma inj_Pair_const2: "inj (λk. (k, C))"
    apply (rule inj_onI)
    apply auto
    done

    lemma table_of_mapconst_SomeI:
      "[|table_of t k = Some y'; snd y=y'; fst y=c|] ==>
       table_of (map (λ(k,x). (k,c,x)) t) k = Some y"
    apply (induct t)
    apply auto
    done

    lemma table_of_mapconst_NoneI:
      "[|table_of t k = None|] ==>
       table_of (map (λ(k,x). (k,c,x)) t) k = None"
    apply (induct t)
    apply auto
    done

    lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]

    lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x -->
       table_of (map (λ(k,x). (k, f x)) t) k = Some (f x)"
    apply (induct_tac "t")
    apply auto
    done

    lemma table_of_remap_SomeD [rule_format (no_asm)]:
      "table_of (map (λ((k,k'),x). (k,(k',x))) t) k = Some (k',x) -->
      table_of t (k, k') = Some x"
    apply (induct_tac "t")
    apply  auto
    done

    lemma table_of_mapf_Some [rule_format (no_asm)]: "∀x y. f x = f y --> x = y ==>
      table_of (map (λ(k,x). (k,f x)) t) k = Some (f x) --> table_of t k = Some x"
    apply (induct_tac "t")
    apply  auto
    done

    lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]:
    "table_of (map (λ(k,x). (k, f x)) t) k = Some z --> (∃y∈table_of t k: z=f y)"
    apply (induct_tac "t")
    apply  auto
    done

    lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]:
    "table_of (map (λ(k,x). (k, f x)) t) k = None --> (table_of t k = None)"
    apply (induct_tac "t")
    apply auto
    done

    lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]:
      "table_of (map (λ(k,x). ((k,C),x)) t) (k,D) = Some x --> C = D ∧ table_of t k = Some x"
    apply (induct_tac "t")
    apply  auto
    done
    lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]:
      "table_of (map (λ(k,x). ((k,C),x)) t) ek = Some x
       --> C = snd ek ∧ table_of t (fst ek) = Some x"
    apply (induct_tac "t")
    apply  auto
    done

    lemma table_append_Some_iff: "table_of (xs@ys) k = Some z =
     (table_of xs k = Some z ∨ (table_of xs k = None ∧ table_of ys k = Some z))"
    apply (simp)
    apply (rule map_add_Some_iff)
    done

    lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
      "table_of (filter P xs) k = Some z ==> unique xs --> table_of xs k = Some z"
    apply (induct xs)
    apply (auto del: map_of_SomeD intro!: map_of_SomeD)
    done

    consts
      Un_tables      :: "('a, 'b) tables set => ('a, 'b) tables"
      overrides_t    :: "('a, 'b) tables     => ('a, 'b) tables =>
                         ('a, 'b) tables"             (infixl "⊕⊕" 100)
      hidings_entails:: "('a, 'b) tables => ('a, 'c) tables =>
                         ('b => 'c => bool) => bool"   ("_ hidings _ entails _" 20)
      --{* variant for unique table: *}
      hiding_entails :: "('a, 'b) table  => ('a, 'c) table  =>
                         ('b => 'c => bool) => bool"   ("_ hiding _ entails _"  20)
      --{* variant for a unique table and conditional overriding: *}
      cond_hiding_entails :: "('a, 'b) table  => ('a, 'c) table
                              => ('b => 'c => bool) => ('b => 'c => bool) => bool"
                              ("_ hiding _ under _ entails _"  20)

    defs
      Un_tables_def:       "Un_tables ts    ≡ λk. \<Union>t∈ts. t k"
      overrides_t_def:     "s ⊕⊕ t        ≡ λk. if t k = {} then s k else t k"
      hidings_entails_def: "t hidings s entails R ≡ ∀k. ∀x∈t k. ∀y∈s k. R x y"
      hiding_entails_def:  "t hiding  s entails R ≡ ∀k. ∀x∈t k: ∀y∈s k: R x y"
      cond_hiding_entails_def: "t hiding  s under C entails R
                                ≡ ∀k. ∀x∈t k: ∀y∈s k: C x y --> R x y"

    section "Untables"

    lemma Un_tablesI [intro]:  "!!x. [|t ∈ ts; x ∈ t k|] ==> x ∈ Un_tables ts k"
    apply (simp add: Un_tables_def)
    apply auto
    done

    lemma Un_tablesD [dest!]: "!!x. x ∈ Un_tables ts k ==> ∃t. t ∈ ts ∧ x ∈ t k"
    apply (simp add: Un_tables_def)
    apply auto
    done

    lemma Un_tables_empty [simp]: "Un_tables {} = (λk. {})"
    apply (unfold Un_tables_def)
    apply (simp (no_asm))
    done

    section "overrides"

    lemma empty_overrides_t [simp]: "(λk. {}) ⊕⊕ m = m"
    apply (unfold overrides_t_def)
    apply (simp (no_asm))
    done
    lemma overrides_empty_t [simp]: "m ⊕⊕ (λk. {}) = m"
    apply (unfold overrides_t_def)
    apply (simp (no_asm))
    done

    lemma overrides_t_Some_iff:
     "(x ∈ (s ⊕⊕ t) k) = (x ∈ t k ∨ t k = {} ∧ x ∈ s k)"
    by (simp add: overrides_t_def)

    lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]

    lemma overrides_t_right_empty [simp]: "n k = {} ==> (m ⊕⊕ n) k = m k"
    by (simp add: overrides_t_def)

    lemma overrides_t_find_right [simp]: "n k ≠ {} ==> (m ⊕⊕ n) k = n k"
    by (simp add: overrides_t_def)

    section "hiding entails"

    lemma hiding_entailsD:
      "[|t hiding s entails R; t k = Some x; s k = Some y|] ==> R x y"
    by (simp add: hiding_entails_def)

    lemma empty_hiding_entails: "empty hiding s entails R"
    by (simp add: hiding_entails_def)

    lemma hiding_empty_entails: "t hiding empty entails R"
    by (simp add: hiding_entails_def)
    declare empty_hiding_entails [simp] hiding_empty_entails [simp]

    section "cond hiding entails"

    lemma cond_hiding_entailsD:
    "[|t hiding s under C entails R; t k = Some x; s k = Some y; C x y|] ==> R x y"
    by (simp add: cond_hiding_entails_def)

    lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
    by (simp add: cond_hiding_entails_def)

    lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
    by (simp add: cond_hiding_entails_def)

    lemma hidings_entailsD: "[|t hidings s entails R; x ∈ t k; y ∈ s k|] ==> R x y"
    by (simp add: hidings_entails_def)

    lemma hidings_empty_entails: "t hidings (λk. {}) entails R"
    apply (unfold hidings_entails_def)
    apply (simp (no_asm))
    done

    lemma empty_hidings_entails:
      "(λk. {}) hidings s entails R"apply (unfold hidings_entails_def)
    by (simp (no_asm))
    declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]

    (*###TO Map?*)
    consts
      atleast_free :: "('a ~=> 'b) => nat => bool"
    primrec
     "atleast_free m 0       = True"
     atleast_free_Suc:
     "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"

    lemma atleast_free_weaken [rule_format (no_asm)]:
      "!m. atleast_free m (Suc n) --> atleast_free m n"
    apply (induct_tac "n")
    apply (simp (no_asm))
    apply clarify
    apply (simp (no_asm))
    apply (drule atleast_free_Suc [THEN iffD1])
    apply fast
    done

    lemma atleast_free_SucI:
    "[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
    by force

    declare fun_upd_apply [simp del]
    lemma atleast_free_SucD_lemma [rule_format (no_asm)]:
    " !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->
      (!b d. a ~= b --> atleast_free (m(b|->d)) n)"
    apply (induct_tac "n")
    apply  auto
    apply (rule_tac x = "a" in exI)
    apply  (rule conjI)
    apply  (force simp add: fun_upd_apply)
    apply (erule_tac V = "m a = None" in thin_rl)
    apply clarify
    apply (subst fun_upd_twist)
    apply  (erule not_sym)
    apply (rename_tac "ba")
    apply (drule_tac x = "ba" in spec)
    apply clarify
    apply (tactic "smp_tac 2 1")
    apply (erule (1) notE impE)
    apply (case_tac "aa = b")
    apply fast+
    done
    declare fun_upd_apply [simp]

    lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
    apply auto
    apply (case_tac "aa = a")
    apply auto
    apply (erule atleast_free_SucD_lemma)
    apply auto
    done

    declare atleast_free_Suc [simp del]
    end

## map of / table of

lemma map_add_find_left:

      n k = None ==> (m ++ n) k = m k

## Conditional Override

lemma cond_override_empty1:

      cond_override c empty t = t

lemma cond_override_empty2:

      cond_override c t empty = t

lemma cond_override_None:

      old k = None ==> cond_override c old new k = new k

lemma cond_override_override:

      [| old k = Some ov; new k = Some nv; C nv ov |]
      ==> cond_override C old new k = Some nv

lemma cond_override_noOverride:

      [| old k = Some ov; new k = Some nv; ¬ C nv ov |]
      ==> cond_override C old new k = Some ov

lemma dom_cond_override:

      dom (cond_override C s t) ⊆ dom s ∪ dom t

lemma finite_dom_cond_override:

      [| finite (dom s); finite (dom t) |] ==> finite (dom (cond_override C s t))

## Filter on Tables

lemma filter_tab_empty:

      filter_tab c empty = empty

lemma filter_tab_True:

      filter_tab (%x y. True) t = t

lemma filter_tab_False:

      filter_tab (%x y. False) t = empty

lemma filter_tab_ran_subset:

      ran (filter_tab c t) ⊆ ran t

lemma filter_tab_range_subset:

      range (filter_tab c t) ⊆ range t ∪ {None}

lemma finite_range_filter_tab:

      finite (range t) ==> finite (range (filter_tab c t))

lemma filter_tab_SomeD:

      filter_tab c t k = Some x ==> t k = Some x ∧ c k x

lemma filter_tab_SomeI:

      [| t k = Some x; C k x |] ==> filter_tab C t k = Some x

lemma filter_tab_all_True:

      ∀k y. t k = Some y --> p k y ==> filter_tab p t = t

lemma filter_tab_all_True_Some:

      [| ∀k y. t k = Some y --> p k y; t k = Some v |] ==> filter_tab p t k = Some v

lemma filter_tab_all_False:

      ∀k y. t k = Some y --> ¬ p k y ==> filter_tab p t = empty

lemma filter_tab_None:

      t k = None ==> filter_tab p t k = None

lemma filter_tab_dom_subset:

      dom (filter_tab C t) ⊆ dom t

lemma filter_tab_eq:

      a = b ==> filter_tab C a = filter_tab C b

lemma finite_dom_filter_tab:

      finite (dom t) ==> finite (dom (filter_tab C t))

lemma filter_tab_weaken:

      [| ! a:t k: ? b:s k: P a b;
         !!k x y. [| t k = Some x; s k = Some y |] ==> cond k x --> cond k y |]
      ==> ! a:filter_tab cond t k: ? b:filter_tab cond s k: P a b

lemma cond_override_filter:

      (!!k old new.
          [| s k = Some new; t k = Some old |]
          ==> (¬ overC new old --> ¬ filterC k new) ∧
              (overC new old --> filterC k old --> filterC k new))
      ==> cond_override overC (filter_tab filterC t) (filter_tab filterC s) =
          filter_tab filterC (cond_override overC t s)

## Misc.

lemma Ball_set_table:

      ∀(x, y)∈set l. P x y ==> ∀x. ! y:table_of l x: P x y

lemma Ball_set_tableD:

      [| ∀(x, y)∈set l. P x y; x ∈ o2s (table_of l xa) |] ==> P xa x

lemma table_of_Some_in_set:

      table_of l k = Some x ==> (k, x) ∈ set l

lemma set_get_eq:

      unique l ==> ((k, the (table_of l k)) ∈ set l) = (table_of l k ≠ None)

lemma inj_Pair_const2:

      inj (%k. (k, C))

lemma table_of_mapconst_SomeI:

      [| table_of t k = Some y'; snd y = y'; fst y = c |]
      ==> table_of (map (%(k, x). (k, c, x)) t) k = Some y

lemma table_of_mapconst_NoneI:

      table_of t k = None ==> table_of (map (%(k, x). (k, c, x)) t) k = None

lemmas table_of_map2_SomeI:

      table_of t k = Some x
      ==> table_of (map (%(k, y). ((k, C), y)) t) (k, C) = Some x

lemmas table_of_map2_SomeI:

      table_of t k = Some x
      ==> table_of (map (%(k, y). ((k, C), y)) t) (k, C) = Some x

lemma table_of_map_SomeI:

      table_of t k = Some x ==> table_of (map (%(k, x). (k, f x)) t) k = Some (f x)

lemma table_of_remap_SomeD:

      table_of (map (%((k, k'), x). (k, k', x)) t) k = Some (k', x)
      ==> table_of t (k, k') = Some x

lemma table_of_mapf_Some:

      [| ∀x y. f x = f y --> x = y;
         table_of (map (%(k, x). (k, f x)) t) k = Some (f x) |]
      ==> table_of t k = Some x

lemma table_of_mapf_SomeD:

      table_of (map (%(k, x). (k, f x)) t) k = Some z ==> ? y:table_of t k: z = f y

lemma table_of_mapf_NoneD:

      table_of (map (%(k, x). (k, f x)) t) k = None ==> table_of t k = None

lemma table_of_mapkey_SomeD:

      table_of (map (%(k, y). ((k, C), y)) t) (k, D) = Some x
      ==> C = D ∧ table_of t k = Some x

lemma table_of_mapkey_SomeD2:

      table_of (map (%(k, y). ((k, C), y)) t) ek = Some x
      ==> C = snd ek ∧ table_of t (fst ek) = Some x

lemma table_append_Some_iff:

      (table_of (xs @ ys) k = Some z) =
      (table_of xs k = Some z ∨ table_of xs k = None ∧ table_of ys k = Some z)

lemma table_of_filter_unique_SomeD:

      [| table_of (filter P xs) k = Some z; unique xs |] ==> table_of xs k = Some z

## Untables

lemma Un_tablesI:

      [| t ∈ ts; x ∈ t k |] ==> x ∈ Un_tables ts k

lemma Un_tablesD:

      x ∈ Un_tables ts k ==> ∃t. t ∈ ts ∧ x ∈ t k

lemma Un_tables_empty:

      Un_tables {} = (%k. {})

## overrides

lemma empty_overrides_t:

      (%k. {}) ⊕⊕ m = m

lemma overrides_empty_t:

      m ⊕⊕ (%k. {}) = m

lemma overrides_t_Some_iff:

      (x ∈ (s ⊕⊕ t) k) = (x ∈ t k ∨ t k = {} ∧ x ∈ s k)

lemmas overrides_t_SomeD:

      x1 ∈ (s1 ⊕⊕ t1) k1 ==> x1 ∈ t1 k1 ∨ t1 k1 = {} ∧ x1 ∈ s1 k1

lemmas overrides_t_SomeD:

      x1 ∈ (s1 ⊕⊕ t1) k1 ==> x1 ∈ t1 k1 ∨ t1 k1 = {} ∧ x1 ∈ s1 k1

lemma overrides_t_right_empty:

      n k = {} ==> (m ⊕⊕ n) k = m k

lemma overrides_t_find_right:

      n k ≠ {} ==> (m ⊕⊕ n) k = n k

## hiding entails

lemma hiding_entailsD:

      [| t hiding s entails R; t k = Some x; s k = Some y |] ==> R x y

lemma empty_hiding_entails:

      empty hiding s entails R

lemma hiding_empty_entails:

      t hiding empty entails R

## cond hiding entails

lemma cond_hiding_entailsD:

      [| t hiding s under C entails R; t k = Some x; s k = Some y; C x y |] ==> R x y

lemma empty_cond_hiding_entails:

      empty hiding s under C entails R

lemma cond_hiding_empty_entails:

      t hiding empty under C entails R

lemma hidings_entailsD:

      [| t hidings s entails R; x ∈ t k; y ∈ s k |] ==> R x y

lemma hidings_empty_entails:

      t hidings %k. {} entails R

lemma empty_hidings_entails:

      %k. {} hidings s entails R

lemma atleast_free_weaken:

      atleast_free m (Suc n) ==> atleast_free m n

lemma atleast_free_SucI:

      [| h a = None; ∀obj. atleast_free (h(a |-> obj)) n |] ==> atleast_free h (Suc n)

lemma atleast_free_SucD_lemma:

      [| m a = None; ∀c. atleast_free (m(a |-> c)) n; a ≠ b |]
      ==> atleast_free (m(b |-> d)) n

lemma atleast_free_SucD:

      atleast_free h (Suc n) ==> atleast_free (h(a |-> b)) n