Theory Generic_ADS_Construction

(* Author: Andreas Lochbihler, Digital Asset
   Author: Ognjen Maric, Digital Asset *)

theory Generic_ADS_Construction imports
  "Merkle_Interface"
  "HOL-Library.BNF_Axiomatization"
begin

section ‹Generic construction of authenticated data structures›

subsection ‹Functors›

subsubsection ‹Source functor›

text ‹

We want to allow ADSs of arbitrary ADTs, which we call "source trees". The ADTs we are interested in can
in general be represented as the least fixpoints of some bounded natural (bi-)functor (BNF) ‹('a, 'b) F›, where
@{typ 'a} is the type of "source" data, and @{typ 'b} is a recursion "handle".
However, Isabelle's type system does not support higher kinds, necessary to parameterize our definitions
over functors.
Instead, we first develop a general theory of ADSs over an arbitrary, but fixed functor,
and its least fixpoint. We show that the theory is compositional, in that the functor's least fixed point
can then be reused as the "source" data of another functor.

We start by defining the arbitrary fixed functor, its fixpoints, and showing how composition can be
done. A higher-level explanation is found in the paper.
›


bnf_axiomatization ('a, 'b) F [wits: "'a ⇒ ('a, 'b) F"]

context notes [[typedef_overloaded]] begin
datatype 'a T = T "('a, 'a T) F"
end

subsubsection ‹Base Merkle functor›

text ‹
This type captures the ADS hashes.
›

bnf_axiomatization ('a, 'b) F⇩h [wits: "'a ⇒ ('a, 'b) F⇩h"]

text ‹
It intuitively contains mixed garbage and source values.
The functor's recursive handle @{typ 'b} might contain partial garbage.
›


text ‹
This type captures the ADS inclusion proofs.
The functor ‹('a, 'a', 'b, 'b') F⇩m› has all type variables doubled.
This type represents all values including the information which parts are blinded.
The original type variable @{typ 'a} now represents the source data, which for compositionality can contain blindable positions.
The type @{typ 'b} is a recursive handle to inclusion sub-proofs (which can be partialy blinded). 
The type @{typ 'a'} represent "hashes" of the source data in @{typ 'a}, i.e., a mix of source values and garbage.
The type @{typ 'b'} is a recursive handle to ADS hashes of subtrees.

The corresponding type of recursive authenticated trees is then a fixpoint of this functor.
›

bnf_axiomatization ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) F⇩m [wits: "'a⇩m ⇒ 'a⇩h ⇒ 'b⇩h ⇒ ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) F⇩m"]

subsubsection ‹Least fixpoint›

context notes [[typedef_overloaded]] begin
datatype 'a⇩h T⇩h = T⇩h "('a⇩h, 'a⇩h T⇩h) F⇩h"
end

context notes [[typedef_overloaded]] begin
datatype ('a⇩m, 'a⇩h) T⇩m = T⇩m (the_T⇩m: "('a⇩m, 'a⇩h, ('a⇩m, 'a⇩h) T⇩m, 'a⇩h T⇩h) F⇩m")
end


subsubsection ‹ Composition ›

text ‹
Finally, we show how to compose two Merkle functors.
For simplicity, we reuse @{typ ‹('a, 'b) F›} and @{typ ‹'a T›}.
›

context notes [[typedef_overloaded]] begin

datatype ('a, 'b) G = G "('a T, 'b) F"

datatype ('a⇩h, 'b⇩h) G⇩h = G⇩h (the_G⇩h: "('a⇩h T⇩h, 'b⇩h) F⇩h")

datatype ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) G⇩m = G⇩m (the_G⇩m: "(('a⇩m, 'a⇩h) T⇩m, 'a⇩h T⇩h, 'b⇩m, 'b⇩h) F⇩m")

end


subsection ‹Root hash›

subsubsection ‹Base functor›

text ‹
The root hash of an authenticated value is modelled as a blindable value of type @{typ "('a', 'b') F⇩h"}.
(Actually, we want to use an abstract datatype for root hashes, but we omit this distinction here for simplicity.)
›

consts root_hash_F' :: "(('a⇩h, 'a⇩h, 'b⇩h, 'b⇩h) F⇩m, ('a⇩h, 'b⇩h) F⇩h) hash"
  ― ‹Root hash operation where we assume that all atoms have already been replaced by root hashes.
     This assumption is reflected in the equality of the type parameters of @{type F⇩m} ›

type_synonym ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) hash_F =
  "('a⇩m, 'a⇩h) hash ⇒ ('b⇩m, 'b⇩h) hash ⇒ (('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) F⇩m, ('a⇩h, 'b⇩h) F⇩h) hash"
definition root_hash_F :: "('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) hash_F" where
  "root_hash_F rha rhb = root_hash_F' ∘ map_F⇩m rha id rhb id"

subsubsection ‹Least fixpoint›

primrec root_hash_T' :: "(('a⇩h, 'a⇩h) T⇩m, 'a⇩h T⇩h) hash" where
  "root_hash_T' (T⇩m x) = T⇩h (root_hash_F' (map_F⇩m id id root_hash_T' id x))"

definition root_hash_T :: "('a⇩m, 'a⇩h) hash ⇒ (('a⇩m, 'a⇩h) T⇩m, 'a⇩h T⇩h) hash" where
  "root_hash_T rha = root_hash_T' ∘ map_T⇩m rha id"

lemma root_hash_T_simps [simp]:
  "root_hash_T rha (T⇩m x) = T⇩h (root_hash_F rha (root_hash_T rha) x)"
  by(simp add: root_hash_T_def F⇩m.map_comp root_hash_F_def T⇩h.map_id0)

subsubsection ‹Composition›

primrec root_hash_G' :: "(('a⇩h, 'a⇩h, 'b⇩h, 'b⇩h) G⇩m, ('a⇩h, 'b⇩h) G⇩h) hash" where
  "root_hash_G' (G⇩m x) = G⇩h (root_hash_F' (map_F⇩m root_hash_T' id id id x))"

definition root_hash_G :: "('a⇩m, 'a⇩h) hash ⇒ ('b⇩m, 'b⇩h) hash ⇒ (('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) G⇩m, ('a⇩h, 'b⇩h) G⇩h) hash" where
  "root_hash_G rha rhb = root_hash_G' ∘ map_G⇩m rha id rhb id"

lemma root_hash_G_unfold:
  "root_hash_G rha rhb = G⇩h ∘ root_hash_F (root_hash_T rha) rhb ∘ the_G⇩m"
  apply(rule ext)
  subgoal for x
    by(cases x)(simp add: root_hash_G_def fun_eq_iff root_hash_F_def root_hash_T_def F⇩m.map_comp T⇩m.map_comp o_def T⇩h.map_id id_def[symmetric])
  done

lemma root_hash_G_simps [simp]:
  "root_hash_G rha rhb (G⇩m x) = G⇩h (root_hash_F (root_hash_T rha) rhb x)"
  by(simp add: root_hash_G_def root_hash_T_def F⇩m.map_comp root_hash_F_def T⇩h.map_id0)


subsection ‹Blinding relation›

text ‹
The blinding relation determines whether one ADS value is a blinding of another.
›

subsubsection ‹ Blinding on the base functor (@{type F⇩m}) ›

type_synonym ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) blinding_of_F =
  "('a⇩m, 'a⇩h) hash ⇒ 'a⇩m blinding_of ⇒ ('b⇩m, 'b⇩h) hash ⇒ 'b⇩m blinding_of ⇒ ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) F⇩m blinding_of"

― ‹ Computes whether a partially blinded ADS is a blinding of another one ›
axiomatization blinding_of_F :: "('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) blinding_of_F" where
  blinding_of_F_mono: "⟦ boa ≤ boa'; bob ≤ bob' ⟧
    ⟹ blinding_of_F rha boa rhb bob ≤ blinding_of_F rha boa' rhb bob'"
    ― ‹ Monotonicity must be unconditional (without the assumption @{text "blinding_of_on"}) 
         such that we can justify the recursive definition for the least fixpoint. ›
  and blinding_respects_hashes_F [locale_witness]:
  "⟦ blinding_respects_hashes rha boa; blinding_respects_hashes rhb bob ⟧
   ⟹ blinding_respects_hashes (root_hash_F rha rhb) (blinding_of_F rha boa rhb bob)"
  and blinding_of_on_F [locale_witness]:
  "⟦ blinding_of_on A rha boa; blinding_of_on B rhb bob ⟧
   ⟹ blinding_of_on {x. set1_F⇩m x ⊆ A ∧ set3_F⇩m x ⊆ B} (root_hash_F rha rhb) (blinding_of_F rha boa rhb bob)"

lemma blinding_of_F_mono_inductive:
  assumes a: "⋀x y. boa x y ⟶ boa' x y"
    and b: "⋀x y. bob x y ⟶ bob' x y"
  shows "blinding_of_F rha boa rhb bob x y ⟶ blinding_of_F rha boa' rhb bob' x y"
  using assms by(blast intro: blinding_of_F_mono[THEN predicate2D, OF predicate2I predicate2I])

subsubsection ‹ Blinding on least fixpoints ›

context
  fixes rh :: "('a⇩m, 'a⇩h) hash"
    and bo :: "'a⇩m blinding_of"
begin

inductive blinding_of_T :: "('a⇩m, 'a⇩h) T⇩m blinding_of" where
  "blinding_of_T (T⇩m x) (T⇩m y)" if 
  "blinding_of_F rh bo (root_hash_T rh) blinding_of_T x y"
monos blinding_of_F_mono_inductive

end

lemma blinding_of_T_mono:
  assumes "bo ≤ bo'"
  shows "blinding_of_T rh bo ≤ blinding_of_T rh bo'"
  by(rule predicate2I; erule blinding_of_T.induct)
    (blast intro: blinding_of_T.intros blinding_of_F_mono[THEN predicate2D, OF assms, rotated -1])

lemma blinding_of_T_root_hash:
  assumes "bo ≤ vimage2p rh rh (=)"
  shows "blinding_of_T rh bo ≤ vimage2p (root_hash_T rh) (root_hash_T rh) (=)"
  apply(rule predicate2I vimage2pI)+
  apply(erule blinding_of_T.induct)
  apply simp
  apply(drule blinding_respects_hashes_F[unfolded blinding_respects_hashes_def, THEN predicate2D, rotated -1])
    apply(rule assms)
   apply(blast intro: vimage2pI)
  apply(simp add: vimage2p_def)
  done

lemma blinding_respects_hashes_T [locale_witness]:
  "blinding_respects_hashes rh bo ⟹ blinding_respects_hashes (root_hash_T rh) (blinding_of_T rh bo)"
  unfolding blinding_respects_hashes_def by(rule blinding_of_T_root_hash)

lemma blinding_of_on_T [locale_witness]:
  assumes "blinding_of_on A rh bo"
  shows "blinding_of_on {x. set1_T⇩m x ⊆ A} (root_hash_T rh) (blinding_of_T rh bo)"
  (is "blinding_of_on ?A ?h ?bo")
proof -
  interpret a: blinding_of_on A rh bo by fact
  show ?thesis
  proof
    have "?bo x x ∧ (?bo x y ⟶ ?bo y z ⟶ ?bo x z) ∧ (?bo x y ⟶ ?bo y x ⟶ x = y)" 
      if "x ∈ ?A" for x y z using that
    proof(induction x arbitrary: y z)
      case (T⇩m x)
      interpret blinding_of_on 
        "{a. set1_F⇩m a ⊆ A ∧ set3_F⇩m a ⊆ set3_F⇩m x}" 
        "root_hash_F rh ?h" 
        "blinding_of_F rh bo ?h ?bo"
        apply(rule blinding_of_on_F[OF assms])
        apply unfold_locales
        subgoal using T⇩m.IH T⇩m.prems by(force simp add: eq_onp_def)
        subgoal for a b c using T⇩m.IH[of a b c] T⇩m.prems by auto
        subgoal for a b using T⇩m.IH[of a b] T⇩m.prems by auto
        done
      show ?case using T⇩m.prems
        apply(intro conjI)
        subgoal by(auto intro: blinding_of_T.intros refl)
        subgoal by(auto elim!: blinding_of_T.cases trans intro!: blinding_of_T.intros)
        subgoal by(auto elim!: blinding_of_T.cases dest: antisym)
        done
    qed
    then show "x ∈ ?A ⟹ ?bo x x" 
      and "⟦ ?bo x y; ?bo y z; x ∈ ?A ⟧ ⟹ ?bo x z"
      and "⟦ ?bo x y; ?bo y x; x ∈ ?A ⟧ ⟹ x = y"
      for x y z by blast+
  qed
qed

lemmas blinding_of_T [locale_witness] = blinding_of_on_T[where A=UNIV, simplified]

subsubsection ‹ Blinding on composition ›

context
  fixes rha :: "('a⇩m, 'a⇩h) hash"
    and boa :: "'a⇩m blinding_of"
    and rhb :: "('b⇩m, 'b⇩h) hash"
    and bob :: "'b⇩m blinding_of"
begin

inductive blinding_of_G :: "('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) G⇩m blinding_of" where
  "blinding_of_G (G⇩m x) (G⇩m y)" if 
  "blinding_of_F (root_hash_T rha) (blinding_of_T rha boa) rhb bob x y"

lemma blinding_of_G_unfold:
  "blinding_of_G = vimage2p the_G⇩m the_G⇩m (blinding_of_F (root_hash_T rha) (blinding_of_T rha boa) rhb bob)"
  apply(rule ext)+
  subgoal for x y by(cases x; cases y)(simp_all add: blinding_of_G.simps fun_eq_iff vimage2p_def)
  done

end

lemma blinding_of_G_mono:
  assumes "boa ≤ boa'" "bob ≤ bob'"
  shows "blinding_of_G rha boa rhb bob ≤ blinding_of_G rha boa' rhb bob'"
  unfolding blinding_of_G_unfold
  by(rule vimage2p_mono' blinding_of_F_mono blinding_of_T_mono assms)+

lemma blinding_of_G_root_hash:
  assumes "boa ≤ vimage2p rha rha (=)" and "bob ≤ vimage2p rhb rhb (=)"
  shows "blinding_of_G rha boa rhb bob ≤ vimage2p (root_hash_G rha rhb) (root_hash_G rha rhb) (=)"
  unfolding blinding_of_G_unfold root_hash_G_unfold vimage2p_comp o_apply
  apply(rule vimage2p_mono')
  apply(rule order_trans)
   apply(rule blinding_respects_hashes_F[unfolded blinding_respects_hashes_def])
    apply(rule blinding_of_T_root_hash)
    apply(rule assms)+
  apply(rule vimage2p_mono')
  apply(simp add: vimage2p_def)
  done

lemma blinding_of_on_G [locale_witness]:
  assumes "blinding_of_on A rha boa" "blinding_of_on B rhb bob"
  shows "blinding_of_on {x. set1_G⇩m x ⊆ A ∧ set3_G⇩m x ⊆ B} (root_hash_G rha rhb) (blinding_of_G rha boa rhb bob)"
  (is "blinding_of_on ?A ?h ?bo")
proof -
  interpret a: blinding_of_on A rha boa by fact
  interpret b: blinding_of_on B rhb bob by fact
  interpret FT: blinding_of_on 
    "{x. set1_F⇩m x ⊆ {x. set1_T⇩m x ⊆ A} ∧ set3_F⇩m x ⊆ B}" 
    "root_hash_F (root_hash_T rha) rhb"
    "blinding_of_F (root_hash_T rha) (blinding_of_T rha boa) rhb bob"
    ..
  show ?thesis
  proof
    show "?bo ≤ vimage2p ?h ?h (=)"
      using a.hash b.hash
      by(rule blinding_of_G_root_hash)
    show "?bo x x" if "x ∈ ?A" for x using that
      by(cases x; hypsubst)(rule blinding_of_G.intros; rule FT.refl; auto)
    show "?bo x z" if "?bo x y" "?bo y z" "x ∈ ?A" for x y z using that
      by(fastforce elim!: blinding_of_G.cases intro!: blinding_of_G.intros elim!: FT.trans)
    show "x = y" if "?bo x y" "?bo y x" "x ∈ ?A" for x y using that
      by(clarsimp elim!: blinding_of_G.cases)(erule (1) FT.antisym; auto)
  qed
qed

lemmas blinding_of_G [locale_witness] = blinding_of_on_G[where A=UNIV and B=UNIV, simplified]

subsection ‹Merging›

text ‹Two Merkle values with the same root hash can be merged into a less blinded Merkle value.
The operation is unspecified for trees with different root hashes.
›

subsubsection ‹ Merging on the base functor ›

axiomatization merge_F :: "('a⇩m, 'a⇩h) hash ⇒ 'a⇩m merge ⇒ ('b⇩m, 'b⇩h) hash ⇒ 'b⇩m merge 
  ⇒ ('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) F⇩m merge" where
  merge_F_cong [fundef_cong]: 
  "⟦ ⋀a b. a ∈ set1_F⇩m x ⟹ ma a b = ma' a b; ⋀a b. a ∈ set3_F⇩m x ⟹ mb a b = mb' a b ⟧
   ⟹ merge_F rha ma rhb mb x y = merge_F rha ma' rhb mb' x y"
  and
  merge_on_F [locale_witness]:
  "⟦ merge_on A rha boa ma; merge_on B rhb bob mb ⟧
  ⟹ merge_on {x. set1_F⇩m x ⊆ A ∧ set3_F⇩m x ⊆ B} (root_hash_F rha rhb) (blinding_of_F rha boa rhb bob) (merge_F rha ma rhb mb)"

lemmas merge_F [locale_witness] = merge_on_F[where A=UNIV and B=UNIV, simplified]

subsubsection ‹ Merging on the least fixpoint ›

lemma wfP_subterm_T: "wfP (λx y. x ∈ set3_F⇩m (the_T⇩m y))"
  apply(rule wfpUNIVI)
  subgoal premises IH[rule_format] for P x
    by(induct x)(auto intro: IH)
  done

lemma irrefl_subterm_T: "x ∈ set3_F⇩m y ⟹ y ≠ the_T⇩m x"
  using wfP_subterm_T by (auto simp: wfp_def elim!: wf_irrefl)

context
  fixes rh :: "('a⇩m, 'a⇩h) hash"
  fixes m :: "'a⇩m merge"
begin

function merge_T :: "('a⇩m, 'a⇩h) T⇩m merge" where
  "merge_T (T⇩m x) (T⇩m y) = map_option T⇩m (merge_F rh m (root_hash_T rh) merge_T x y)"
  by pat_completeness auto
termination
  apply(relation "{(x, y). x ∈ set3_F⇩m (the_T⇩m y)} <*lex*> {(x, y). x ∈ set3_F⇩m (the_T⇩m y)}")
   apply(auto simp add: wfp_def[symmetric] wfP_subterm_T)
  done

lemma merge_on_T [locale_witness]:
  assumes "merge_on A rh bo m"
  shows "merge_on {x. set1_T⇩m x ⊆ A} (root_hash_T rh) (blinding_of_T rh bo) merge_T"
  (is "merge_on ?A ?h ?bo ?m")
proof -
  interpret a: merge_on A rh bo m by fact
  show ?thesis
  proof
    have "(?h a = ?h b ⟶ (∃ab. ?m a b = Some ab ∧ ?bo a ab ∧ ?bo b ab ∧ (∀u. ?bo a u ⟶ ?bo b u ⟶ ?bo ab u))) ∧
      (?h a ≠ ?h b ⟶ ?m a b = None)"
      if "a ∈ ?A" for a b using that unfolding mem_Collect_eq
    proof(induction a arbitrary: b)
      case (T⇩m x y)
      interpret merge_on "{y. set1_F⇩m y ⊆ A ∧ set3_F⇩m y ⊆ set3_F⇩m x}"
        "root_hash_F rh ?h" "blinding_of_F rh bo ?h ?bo" "merge_F rh m ?h ?m"
      proof
        fix a
        assume a: "a ∈ set3_F⇩m x"
        with T⇩m.prems have a': "set1_T⇩m a ⊆ A" by auto

        fix b
        from T⇩m.IH[OF a a', rule_format, of b]
        show "root_hash_T rh a = root_hash_T rh b
           ⟹ ∃ab. merge_T a b = Some ab ∧ blinding_of_T rh bo a ab ∧ blinding_of_T rh bo b ab ∧
                    (∀u. blinding_of_T rh bo a u ⟶ blinding_of_T rh bo b u ⟶ blinding_of_T rh bo ab u)"
          and "root_hash_T rh a ≠ root_hash_T rh b ⟹ merge_T a b = None"
          by(auto dest: sym)
      qed
      show ?case using T⇩m.prems
        apply(intro conjI strip)
        subgoal by(cases y)(auto dest!: join simp add: blinding_of_T.simps)
        subgoal by(cases y)(auto dest!: undefined)
        done
    qed
    then show
      "?h a = ?h b ⟹ ∃ab. ?m a b = Some ab ∧ ?bo a ab ∧ ?bo b ab ∧ (∀u. ?bo a u ⟶ ?bo b u ⟶ ?bo ab u)"
      "?h a ≠ ?h b ⟹ ?m a b = None"
      if "a ∈ ?A" for a b using that by blast+
  qed
qed

lemmas merge_T [locale_witness] = merge_on_T[where A=UNIV, simplified]

end

lemma merge_T_cong [fundef_cong]:
  assumes "⋀a b. a ∈ set1_T⇩m x ⟹ m a b = m' a b"
  shows "merge_T rh m x y = merge_T rh m' x y"
  using assms
  apply(induction x y rule: merge_T.induct)
  apply simp
  apply(rule arg_cong[where f="map_option _"])
  apply(blast intro: merge_F_cong)
  done

subsubsection ‹ Merging and composition ›

context
  fixes rha :: "('a⇩m, 'a⇩h) hash"
  fixes ma :: "'a⇩m merge"
  fixes rhb :: "('b⇩m, 'b⇩h) hash"
  fixes mb :: "'b⇩m merge"
begin

primrec merge_G :: "('a⇩m, 'a⇩h, 'b⇩m, 'b⇩h) G⇩m merge" where
  "merge_G (G⇩m x) y' = (case y' of G⇩m y ⇒
    map_option G⇩m (merge_F (root_hash_T rha) (merge_T rha ma) rhb mb x y))"

lemma merge_G_simps [simp]:
  "merge_G (G⇩m x) (G⇩m y) = map_option G⇩m (merge_F (root_hash_T rha) (merge_T rha ma) rhb mb x y)"
  by(simp)

declare merge_G.simps [simp del]

lemma merge_on_G:
  assumes a: "merge_on A rha boa ma" and b: "merge_on B rhb bob mb"
  shows "merge_on {x. set1_G⇩m x ⊆ A ∧ set3_G⇩m x ⊆ B} (root_hash_G rha rhb) (blinding_of_G rha boa rhb bob) merge_G"
  (is "merge_on ?A ?h ?bo ?m")
proof -
  interpret a: merge_on A rha boa ma by fact
  interpret b: merge_on B rhb bob mb by fact
  interpret F: merge_on 
    "{x. set1_F⇩m x ⊆ {x. set1_T⇩m x ⊆ A} ∧ set3_F⇩m x ⊆ B}"
    "root_hash_F (root_hash_T rha) rhb"
    "blinding_of_F (root_hash_T rha) (blinding_of_T rha boa) rhb bob"
    "merge_F (root_hash_T rha) (merge_T rha ma) rhb mb"
    ..
  show ?thesis
  proof
    show "∃ab. ?m a b = Some ab ∧ ?bo a ab ∧ ?bo b ab ∧ (∀u. ?bo a u ⟶ ?bo b u ⟶ ?bo ab u)"
      if "?h a = ?h b" "a ∈ ?A" for a b using that
      by(cases a; cases b)(auto dest!: F.join simp add: blinding_of_G.simps)
    show "?m a b = None" if "?h a ≠ ?h b" "a ∈ ?A" for a b using that
      by(cases a; cases b)(auto dest!: F.undefined)
  qed
qed

lemmas merge_G [locale_witness] = merge_on_G[where A=UNIV and B=UNIV, simplified]

end

lemma merge_G_cong [fundef_cong]: 
  "⟦ ⋀a b. a ∈ set1_G⇩m x ⟹ ma a b = ma' a b; ⋀a b. a ∈ set3_G⇩m x ⟹ mb a b = mb' a b ⟧
   ⟹ merge_G rha ma rhb mb x y = merge_G rha ma' rhb mb' x y"
  apply(cases x; cases y; simp)
  apply(rule arg_cong[where f="map_option _"])
  apply(blast intro: merge_F_cong merge_T_cong)
  done

end