Theory Canton_Transaction_Tree

theory Canton_Transaction_Tree imports
  Inclusion_Proof_Construction
begin

section ‹Canton's hierarchical transaction trees›

typedecl view_data
typedecl view_metadata
typedecl common_metadata
typedecl participant_metadata

datatype view = View view_metadata view_data (subviews: "view list")

datatype transaction = Transaction common_metadata participant_metadata (views: "view list")

subsection ‹Views as authenticated data structures›

type_synonym view_metadata⇩h = "view_metadata blindable⇩h"
type_synonym view_data⇩h = "view_data blindable⇩h"

datatype view⇩h = View⇩h "((view_metadata⇩h ×⇩h view_data⇩h) ×⇩h view⇩h list⇩h) blindable⇩h"

type_synonym view_metadata⇩m = "(view_metadata, view_metadata) blindable⇩m"
type_synonym view_data⇩m = "(view_data, view_data) blindable⇩m"

datatype view⇩m = View⇩m 
  "((view_metadata⇩m ×⇩m view_data⇩m) ×⇩m view⇩m list⇩m,
    (view_metadata⇩h ×⇩h view_data⇩h) ×⇩h view⇩h list⇩h) blindable⇩m"

abbreviation (input) hash_view_data :: "(view_data⇩m, view_data⇩h) hash" where
  "hash_view_data ≡ hash_blindable id"
abbreviation (input) blinding_of_view_data :: "view_data⇩m blinding_of" where
  "blinding_of_view_data ≡ blinding_of_blindable id (=)"
abbreviation (input) merge_view_data :: "view_data⇩m merge" where
  "merge_view_data ≡ merge_blindable id merge_discrete"

lemma merkle_view_data:
  "merkle_interface hash_view_data blinding_of_view_data merge_view_data"
  by unfold_locales

abbreviation (input) hash_view_metadata :: "(view_metadata⇩m, view_metadata⇩h) hash" where
  "hash_view_metadata ≡ hash_blindable id"
abbreviation (input) blinding_of_view_metadata :: "view_metadata⇩m blinding_of" where
  "blinding_of_view_metadata ≡ blinding_of_blindable id (=)"
abbreviation (input) merge_view_metadata :: "view_metadata⇩m merge" where
  "merge_view_metadata ≡ merge_blindable id merge_discrete"

lemma merkle_view_metadata:
  "merkle_interface hash_view_metadata blinding_of_view_metadata merge_view_metadata"
  by unfold_locales

type_synonym view_content = "view_metadata × view_data"
type_synonym view_content⇩h = "view_metadata⇩h ×⇩h view_data⇩h"
type_synonym view_content⇩m = "view_metadata⇩m ×⇩m view_data⇩m"

locale view_merkle begin

type_synonym view⇩h' = "view_content⇩h rose_tree⇩h"

primrec from_view⇩h :: "view⇩h ⇒ view⇩h'" where
  "from_view⇩h (View⇩h x) = Tree⇩h (map_blindable⇩h (map_prod id (map from_view⇩h)) x)"

primrec to_view⇩h :: "view⇩h' ⇒ view⇩h" where
  "to_view⇩h (Tree⇩h x) = View⇩h (map_blindable⇩h (map_prod id (map to_view⇩h)) x)"

lemma from_to_view⇩h [simp]: "from_view⇩h (to_view⇩h x) = x"
  apply(induction x)
  apply(simp add: blindable⇩h.map_comp o_def prod.map_comp)
  apply(simp cong: blindable⇩h.map_cong prod.map_cong list.map_cong add: blindable⇩h.map_id[unfolded id_def])
  done

lemma to_from_view⇩h [simp]: "to_view⇩h (from_view⇩h x) = x"
  apply(induction x)
  apply(simp add: blindable⇩h.map_comp o_def prod.map_comp)
  apply(simp cong: blindable⇩h.map_cong prod.map_cong list.map_cong add: blindable⇩h.map_id[unfolded id_def])
  done

lemma iso_view⇩h: "type_definition from_view⇩h to_view⇩h UNIV"
  by unfold_locales simp_all

setup_lifting iso_view⇩h

lemma cr_view⇩h_Grp: "cr_view⇩h = Grp UNIV to_view⇩h"
  by(simp add: cr_view⇩h_def Grp_def fun_eq_iff)(transfer, auto)

lemma View⇩h_transfer [transfer_rule]: includes lifting_syntax shows
  "(rel_blindable⇩h (rel_prod (=) (list_all2 pcr_view⇩h)) ===> pcr_view⇩h) Tree⇩h View⇩h"
  by(simp add: rel_fun_def view⇩h.pcr_cr_eq cr_view⇩h_Grp list.rel_Grp eq_alt prod.rel_Grp blindable⇩h.rel_Grp)
    (simp add: Grp_def)

type_synonym view⇩m' = "(view_content⇩m, view_content⇩h) rose_tree⇩m"

primrec from_view⇩m :: "view⇩m ⇒ view⇩m'" where
  "from_view⇩m (View⇩m x) = Tree⇩m (map_blindable⇩m (map_prod id (map from_view⇩m)) (map_prod id (map from_view⇩h)) x)"

primrec to_view⇩m :: "view⇩m' ⇒ view⇩m" where
  "to_view⇩m (Tree⇩m x) = View⇩m (map_blindable⇩m (map_prod id (map to_view⇩m)) (map_prod id (map to_view⇩h)) x)"

lemma from_to_view⇩m [simp]: "from_view⇩m (to_view⇩m x) = x"
  apply(induction x)
  apply(simp add: blindable⇩m.map_comp o_def prod.map_comp)
  apply(simp cong: blindable⇩m.map_cong prod.map_cong list.map_cong add: blindable⇩m.map_id[unfolded id_def])
  done

lemma to_from_view⇩m [simp]: "to_view⇩m (from_view⇩m x) = x"
  apply(induction x)
  apply(simp add: blindable⇩m.map_comp o_def prod.map_comp)
  apply(simp cong: blindable⇩m.map_cong prod.map_cong list.map_cong add: blindable⇩m.map_id[unfolded id_def])
  done

lemma iso_view⇩m: "type_definition from_view⇩m to_view⇩m UNIV"
  by unfold_locales simp_all

setup_lifting iso_view⇩m

lemma cr_view⇩m_Grp: "cr_view⇩m = Grp UNIV to_view⇩m"
  by(simp add: cr_view⇩m_def Grp_def fun_eq_iff)(transfer, auto)

lemma View⇩m_transfer [transfer_rule]: includes lifting_syntax shows
  "(rel_blindable⇩m (rel_prod (=) (list_all2 pcr_view⇩m)) (rel_prod (=) (list_all2 pcr_view⇩h)) ===> pcr_view⇩m) Tree⇩m View⇩m"
  by(simp add: rel_fun_def view⇩h.pcr_cr_eq view⇩m.pcr_cr_eq cr_view⇩h_Grp cr_view⇩m_Grp list.rel_Grp eq_alt prod.rel_Grp blindable⇩m.rel_Grp)
    (simp add: Grp_def)

end

code_datatype View⇩h
code_datatype View⇩m

context begin
interpretation view_merkle .

abbreviation (input) hash_view_content :: "(view_content⇩m, view_content⇩h) hash" where
  "hash_view_content ≡ hash_prod hash_view_metadata hash_view_data"

abbreviation (input) blinding_of_view_content :: "view_content⇩m blinding_of" where
  "blinding_of_view_content ≡ blinding_of_prod blinding_of_view_metadata blinding_of_view_data"

abbreviation (input) merge_view_content :: "view_content⇩m merge" where
  "merge_view_content ≡ merge_prod merge_view_metadata merge_view_data"

lift_definition hash_view :: "(view⇩m, view⇩h) hash" is
  "hash_tree hash_view_content" .

lift_definition blinding_of_view :: "view⇩m blinding_of" is
  "blinding_of_tree hash_view_content blinding_of_view_content" .

lift_definition merge_view :: "view⇩m merge" is
  "merge_tree hash_view_content merge_view_content" .

lemma merkle_view [locale_witness]: "merkle_interface hash_view blinding_of_view merge_view"
  by transfer unfold_locales

lemma hash_view_simps [simp]:
  "hash_view (View⇩m x) = 
   View⇩h (hash_blindable (hash_prod hash_view_content (hash_list hash_view)) x)"
  by transfer(simp add: hash_rt_F⇩m_def prod.map_comp hash_blindable_def blindable⇩m.map_id)

lemma blinding_of_view_iff [simp]:
  "blinding_of_view (View⇩m x) (View⇩m y) ⟷
   blinding_of_blindable (hash_prod hash_view_content (hash_list hash_view))
     (blinding_of_prod blinding_of_view_content (blinding_of_list blinding_of_view)) x y"
  by transfer simp

lemma blinding_of_view_induct [consumes 1, induct pred: blinding_of_view]:
  assumes "blinding_of_view x y"
    and "⋀x y. blinding_of_blindable (hash_prod hash_view_content (hash_list hash_view))
             (blinding_of_prod blinding_of_view_content (blinding_of_list (λx y. blinding_of_view x y ∧ P x y))) x y
         ⟹ P (View⇩m x) (View⇩m y)"
  shows "P x y"
  using assms by transfer(rule blinding_of_tree.induct)

lemma merge_view_simps [simp]:
  "merge_view (View⇩m x) (View⇩m y) =
   map_option View⇩m (merge_rt_F⇩m hash_view_content merge_view_content hash_view merge_view x y)"
  by transfer simp

end

subsection ‹Transaction trees as authenticated data structures›

type_synonym common_metadata⇩h = "common_metadata blindable⇩h"
type_synonym common_metadata⇩m = "(common_metadata, common_metadata) blindable⇩m"

type_synonym participant_metadata⇩h = "participant_metadata blindable⇩h"
type_synonym participant_metadata⇩m = "(participant_metadata, participant_metadata) blindable⇩m"

datatype transaction⇩h = Transaction⇩h 
  (the_Transaction⇩h: "((common_metadata⇩h ×⇩h participant_metadata⇩h) ×⇩h view⇩h list⇩h) blindable⇩h")

datatype transaction⇩m = Transaction⇩m 
  (the_Transaction⇩m: "((common_metadata⇩m ×⇩m participant_metadata⇩m) ×⇩m view⇩m list⇩m,
    (common_metadata⇩h ×⇩h participant_metadata⇩h) ×⇩h view⇩h list⇩h) blindable⇩m")

abbreviation (input) hash_common_metadata :: "(common_metadata⇩m, common_metadata⇩h) hash" where
  "hash_common_metadata ≡ hash_blindable id"
abbreviation (input) blinding_of_common_metadata :: "common_metadata⇩m blinding_of" where
  "blinding_of_common_metadata ≡ blinding_of_blindable id (=)"
abbreviation (input) merge_common_metadata :: "common_metadata⇩m merge" where
  "merge_common_metadata ≡ merge_blindable id merge_discrete"

abbreviation (input) hash_participant_metadata :: "(participant_metadata⇩m, participant_metadata⇩h) hash" where
  "hash_participant_metadata ≡ hash_blindable id"
abbreviation (input) blinding_of_participant_metadata :: "participant_metadata⇩m blinding_of" where
  "blinding_of_participant_metadata ≡ blinding_of_blindable id (=)"
abbreviation (input) merge_participant_metadata :: "participant_metadata⇩m merge" where
  "merge_participant_metadata ≡ merge_blindable id merge_discrete"

locale transaction_merkle begin

lemma iso_transaction⇩h: "type_definition the_Transaction⇩h Transaction⇩h UNIV"
  by unfold_locales simp_all

setup_lifting iso_transaction⇩h

lemma Transaction⇩h_transfer [transfer_rule]: includes lifting_syntax shows
  "((=) ===> pcr_transaction⇩h) id Transaction⇩h"
  by(simp add: transaction⇩h.pcr_cr_eq cr_transaction⇩h_def rel_fun_def)

lemma iso_transaction⇩m: "type_definition the_Transaction⇩m Transaction⇩m UNIV"
  by unfold_locales simp_all

setup_lifting iso_transaction⇩m

lemma Transaction⇩m_transfer [transfer_rule]: includes lifting_syntax shows
  "((=) ===> pcr_transaction⇩m) id Transaction⇩m"
  by(simp add: transaction⇩m.pcr_cr_eq cr_transaction⇩m_def rel_fun_def)

end

code_datatype Transaction⇩h
code_datatype Transaction⇩m

context begin
interpretation transaction_merkle .

lift_definition hash_transaction :: "(transaction⇩m, transaction⇩h) hash" is
  "hash_blindable (hash_prod (hash_prod hash_common_metadata hash_participant_metadata) (hash_list hash_view))" .

lift_definition blinding_of_transaction :: "transaction⇩m blinding_of" is
  "blinding_of_blindable 
     (hash_prod (hash_prod hash_common_metadata hash_participant_metadata) (hash_list hash_view))
     (blinding_of_prod (blinding_of_prod blinding_of_common_metadata blinding_of_participant_metadata) (blinding_of_list blinding_of_view))" .

lift_definition merge_transaction :: "transaction⇩m merge" is
  "merge_blindable
     (hash_prod (hash_prod hash_common_metadata hash_participant_metadata) (hash_list hash_view))
     (merge_prod (merge_prod merge_common_metadata merge_participant_metadata) (merge_list merge_view))" .

lemma merkle_transaction [locale_witness]:
  "merkle_interface hash_transaction blinding_of_transaction merge_transaction"
  by transfer unfold_locales

lemmas hash_transaction_simps [simp] = hash_transaction.abs_eq
lemmas blinding_of_transaction_iff [simp] = blinding_of_transaction.abs_eq
lemmas merge_transaction_simps [simp] = merge_transaction.abs_eq

end

interpretation transaction:
  merkle_interface hash_transaction blinding_of_transaction merge_transaction 
  by(rule merkle_transaction)

subsection ‹
Constructing authenticated data structures for views
›

context view_merkle begin

type_synonym view' = "(view_metadata × view_data) rose_tree"

primrec from_view :: "view ⇒ view'" where
  "from_view (View vm vd vs) = Tree ((vm, vd), map from_view vs)"

primrec to_view :: "view' ⇒ view" where
  "to_view (Tree x) = View (fst (fst x)) (snd (fst x)) (snd (map_prod id (map to_view) x))"

lemma from_to_view [simp]: "from_view (to_view x) = x"
  by(induction x)(clarsimp cong: map_cong)

lemma to_from_view [simp]: "to_view (from_view x) = x"
  by(induction x)(clarsimp cong: map_cong)

lemma iso_view: "type_definition from_view to_view UNIV"
  by unfold_locales simp_all

setup_lifting iso_view

definition View' :: "(view_metadata × view_data) × view list ⇒ view" where
  "View' = (λ((vm, vd), vs). View vm vd vs)"

lemma View_View': "View = (λvm vd vs. View' ((vm, vd), vs))"
  by(simp add: View'_def)

lemma cr_view_Grp: "cr_view = Grp UNIV to_view"
  by(simp add: cr_view_def Grp_def fun_eq_iff)(transfer, auto)

lemma View'_transfer [transfer_rule]: includes lifting_syntax shows
  "(rel_prod (=) (list_all2 pcr_view) ===> pcr_view) Tree View'"
  by(simp add: view.pcr_cr_eq cr_view_Grp eq_alt prod.rel_Grp rose_tree.rel_Grp list.rel_Grp)
    (auto simp add: Grp_def View'_def)

end

code_datatype View

context begin
interpretation view_merkle .

abbreviation embed_view_content :: "view_metadata × view_data ⇒ view_metadata⇩m × view_data⇩m" where
  "embed_view_content ≡ map_prod Unblinded Unblinded"

lift_definition embed_view :: "view ⇒ view⇩m" is "embed_source_tree embed_view_content" .

lemma embed_view_simps [simp]:
  "embed_view (View vm vd vs) = View⇩m (Unblinded ((Unblinded vm, Unblinded vd), map embed_view vs))"
  unfolding View_View' by transfer simp

end

context transaction_merkle begin

primrec the_Transaction :: "transaction ⇒ (common_metadata × participant_metadata) × view list" where
  "the_Transaction (Transaction cm pm views) = ((cm, pm), views)" for views

definition Transaction' :: "(common_metadata × participant_metadata) × view list ⇒ transaction" where
  "Transaction' = (λ((cm, pm), views). Transaction cm pm views)"

lemma Transaction_Transaction': "Transaction = (λcm pm views. Transaction' ((cm, pm), views))"
  by(simp add: Transaction'_def)

lemma the_Transaction_inverse [simp]: "Transaction' (the_Transaction x) = x" 
  by(cases x)(simp add: Transaction'_def)

lemma Transaction'_inverse [simp]: "the_Transaction (Transaction' x) = x"
  by(simp add: Transaction'_def split_def)

lemma iso_transaction: "type_definition the_Transaction Transaction' UNIV"
  by unfold_locales simp_all

setup_lifting iso_transaction

lemma Transaction'_transfer [transfer_rule]: includes lifting_syntax shows
  "((=) ===> pcr_transaction) id Transaction'"
  by(simp add: transaction.pcr_cr_eq cr_transaction_def rel_fun_def)

end

code_datatype Transaction

context begin
interpretation transaction_merkle .

lift_definition embed_transaction :: "transaction ⇒ transaction⇩m" is
  "Unblinded ∘ map_prod (map_prod Unblinded Unblinded) (map embed_view)" .

lemma embed_transaction_simps [simp]:
  "embed_transaction (Transaction cm pm views) =
   Transaction⇩m (Unblinded ((Unblinded cm, Unblinded pm), map embed_view views))" 
  for views unfolding Transaction_Transaction' by transfer simp

end

subsubsection ‹Inclusion proof for the mediator›

primrec mediator_view :: "view ⇒ view⇩m" where
  "mediator_view (View vm vd vs) =
   View⇩m (Unblinded ((Unblinded vm, Blinded (Content vd)), map mediator_view vs))"

primrec mediator_transaction_tree :: "transaction ⇒ transaction⇩m" where
  "mediator_transaction_tree (Transaction cm pm views) =
   Transaction⇩m (Unblinded ((Unblinded cm, Blinded (Content pm)), map mediator_view views))"
  for views

lemma blinding_of_mediator_view [simp]: "blinding_of_view (mediator_view view) (embed_view view)"
  by(induction view)(auto simp add: list.rel_map intro!: list.rel_refl_strong)

lemma blinding_of_mediator_transaction_tree:
  "blinding_of_transaction (mediator_transaction_tree tt) (embed_transaction tt)"
  by(cases tt)(auto simp add: list.rel_map intro: list.rel_refl_strong)

subsubsection ‹Inclusion proofs for participants›

text ‹Next, we define a function for producing all transaction views from a given view,
  and prove its properties.›

type_synonym view_path_elem = "(view_metadata × view_data) blindable × view list × view list"
type_synonym view_path = "view_path_elem list"
type_synonym view_zipper = "view_path × view"

type_synonym view_path_elem⇩m = "(view_metadata⇩m ×⇩m view_data⇩m) × view⇩m list⇩m × view⇩m list⇩m"
type_synonym view_path⇩m = "view_path_elem⇩m list"
type_synonym view_zipper⇩m = "view_path⇩m × view⇩m"

context begin
interpretation view_merkle .

lift_definition zipper_of_view :: "view ⇒ view_zipper" is zipper_of_tree .
lift_definition view_of_zipper :: "view_zipper ⇒ view" is tree_of_zipper .

lift_definition zipper_of_view⇩m :: "view⇩m ⇒ view_zipper⇩m" is zipper_of_tree⇩m .
lift_definition view_of_zipper⇩m :: "view_zipper⇩m ⇒ view⇩m" is tree_of_zipper⇩m .

lemma view_of_zipper⇩m_Nil [simp]: "view_of_zipper⇩m ([], t) = t"
  by transfer simp

lift_definition blind_view_path_elem :: "view_path_elem ⇒ view_path_elem⇩m" is
  "blind_path_elem embed_view_content hash_view_content" .

lift_definition blind_view_path :: "view_path ⇒ view_path⇩m" is
  "blind_path embed_view_content hash_view_content" .

lift_definition embed_view_path_elem :: "view_path_elem ⇒ view_path_elem⇩m" is
  "embed_path_elem embed_view_content" .

lift_definition embed_view_path :: "view_path ⇒ view_path⇩m" is
  "embed_path embed_view_content" .

lift_definition hash_view_path_elem :: "view_path_elem⇩m ⇒ (view_content⇩h × view⇩h list × view⇩h list)" is
  "hash_path_elem hash_view_content" .

lift_definition zippers_view :: "view_zipper ⇒ view_zipper⇩m list" is
  "zippers_rose_tree embed_view_content hash_view_content" .

lemma embed_view_path_Nil [simp]: "embed_view_path [] = []"
  by transfer(simp add: embed_path_def)

lemma zippers_view_same_hash:
  assumes "z ∈ set (zippers_view (p, t))"
  shows "hash_view (view_of_zipper⇩m z) = hash_view (view_of_zipper⇩m (embed_view_path p, embed_view t))"
  using assms by transfer(rule zippers_rose_tree_same_hash')

lemma zippers_view_blinding_of:
  assumes "z ∈ set (zippers_view (p, t))"
  shows "blinding_of_view (view_of_zipper⇩m z) (view_of_zipper⇩m (blind_view_path p, embed_view t))"
  using assms by transfer(rule zippers_rose_tree_blinding_of, unfold_locales)

end

primrec blind_view :: "view ⇒ view⇩m" where
  "blind_view (View vm vd subviews) = 
   View⇩m (Blinded (Content ((Content vm, Content vd), map (hash_view ∘ embed_view) subviews)))"
  for subviews

lemma hash_blind_view: "hash_view (blind_view view) = hash_view (embed_view view)"
  by(cases view) simp

primrec blind_transaction :: "transaction ⇒ transaction⇩m" where
  "blind_transaction (Transaction cm pm views) = 
   Transaction⇩m (Blinded (Content ((Content cm, Content pm), map (hash_view ∘ blind_view) views)))"
  for views

lemma hash_blind_transaction:
  "hash_transaction (blind_transaction transaction) = hash_transaction (embed_transaction transaction)"
  by(cases transaction)(simp add: hash_blind_view)


typedecl participant
consts recipients :: "view_metadata ⇒ participant list"

fun view_recipients :: "view⇩m ⇒ participant set" where
  "view_recipients (View⇩m (Unblinded ((Unblinded vm, vd), subviews))) = set (recipients vm)" for subviews
| "view_recipients _ = {}" ― ‹Sane default case›

context fixes participant :: participant begin

definition view_trees_for :: "view ⇒ view⇩m list" where
  "view_trees_for view =
   map view_of_zipper⇩m
     (filter (λ(_, t). participant ∈ view_recipients t) 
       (zippers_view ([], view)))"

primrec transaction_views_for :: "transaction ⇒ transaction⇩m list" where
  "transaction_views_for (Transaction cm pm views) =
   map (λview⇩m. Transaction⇩m (Unblinded ((Unblinded cm, Unblinded pm), view⇩m)))
  (concat (map (λ(l, v, r). map (λv⇩m. map blind_view l @ [v⇩m] @ map blind_view r) (view_trees_for v)) (splits views)))"
  for views
   
lemma view_trees_for_same_hash:
  "vt ∈ set (view_trees_for view) ⟹ hash_view vt = hash_view (embed_view view)"
  by(auto simp add: view_trees_for_def dest: zippers_view_same_hash)

lemma transaction_views_for_same_hash:
  "t⇩m ∈ set (transaction_views_for t) ⟹ hash_transaction t⇩m = hash_transaction (embed_transaction t)"
  by(cases t)(clarsimp simp add: splits_iff hash_blind_view view_trees_for_same_hash)

definition transaction_projection_for :: "transaction ⇒ transaction⇩m" where
  "transaction_projection_for t =
   (let tvs = transaction_views_for t
    in if tvs = [] then blind_transaction t else the (transaction.Merge (set tvs)))"

lemma transaction_projection_for_same_hash:
  "hash_transaction (transaction_projection_for t) = hash_transaction (embed_transaction t)"
proof(cases "transaction_views_for t = []")
  case True thus ?thesis by(simp add: transaction_projection_for_def Let_def hash_blind_transaction)
next
  case False
  then have "transaction.Merge (set (transaction_views_for t)) ≠ None"
    by(intro transaction.Merge_defined)(auto simp add: transaction_views_for_same_hash)
  with False show ?thesis
    apply(clarsimp simp add: transaction_projection_for_def neq_Nil_conv simp del: transaction.Merge_insert)
    apply(drule transaction.Merge_hash[symmetric], blast)
    apply(auto intro: transaction_views_for_same_hash)
    done
qed

lemma transaction_projection_for_upper:
  assumes "t⇩m ∈ set (transaction_views_for t)"
  shows "blinding_of_transaction t⇩m (transaction_projection_for t)"
proof -
  from assms have "transaction.Merge (set (transaction_views_for t)) ≠ None"
    by(intro transaction.Merge_defined)(auto simp add: transaction_views_for_same_hash)
  with assms show ?thesis
    by(auto simp add: transaction_projection_for_def Let_def dest: transaction.Merge_upper)
qed

end

end