Theory Tuple15_LLVM

theory Tuple15_LLVM
  imports Tuple15 IsaSAT_Literals_LLVM
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN

text ‹
This is the setup for accessing and modifying the state as an abstract tuple of 15 elements.
 The construction is kept generic 
(even if still targetting only our state). There is a lot of copy-paste that would be nice to automate
at some point.


We define 3 sort of operations:

  ▸ extracting an element, replacing it by an default element. Modifies the state. The name starts 
with \<^text>‹exctr›

  ▸ reinserting an element, freeing the current one. Modifies the state. The name starts with
 \<^text>‹update›

  ▸ in-place reading a value, possibly with pure parameters. Does not modify the state. The name
starts with \<^text>‹read›

›

instantiation tuple15 ::
  (llvm_rep,llvm_rep,llvm_rep,llvm_rep,
  llvm_rep,llvm_rep,llvm_rep,llvm_rep,
  llvm_rep,llvm_rep,llvm_rep,llvm_rep,
  llvm_rep,llvm_rep,llvm_rep) llvm_rep
begin
  definition to_val_tuple15 where
    ‹to_val_tuple15 ≡ (λS. case S of
     Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts ⇒ LL_STRUCT [to_val M, to_val N, to_val D, to_val i, to_val W, to_val ivmtf,
       to_val icount, to_val ccach, to_val lbd,
       to_val outl, to_val stats, to_val heur, to_val aivdom,  to_val clss, to_val opts])›

  definition from_val_tuple15 :: ‹llvm_val ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
    ‹from_val_tuple15 ≡ (λp. case llvm_val.the_fields p of
   [M, N, D, i, W, ivmtf, icount, ccach, lbd, outl, stats, heur, aivdom, clss, opts] ⇒
     Tuple15 (from_val M) (from_val N) (from_val D) (from_val i) (from_val W) (from_val ivmtf) (from_val icount) (from_val ccach) (from_val lbd)
       (from_val outl) (from_val stats) (from_val heur) (from_val aivdom) (from_val clss) (from_val opts))›

  definition [simp]: "struct_of_tuple15 (_ :: ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 itself) ≡
     VS_STRUCT [struct_of TYPE('a), struct_of TYPE('b), struct_of TYPE('c),
      struct_of TYPE('d), struct_of TYPE('e), struct_of TYPE('f), struct_of TYPE('g), struct_of TYPE('h),
      struct_of TYPE('i), struct_of TYPE('j), struct_of TYPE('k), struct_of TYPE('l),
      struct_of TYPE('m), struct_of TYPE('n), struct_of TYPE('o)]"

  definition [simp]: "init_tuple15 :: ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ≡ Tuple15 init init init init init init init init init init init init init init init"

  instance
    apply standard
    unfolding from_val_tuple15_def to_val_tuple15_def struct_of_tuple15_def init_tuple15_def comp_def tuple15.case_distrib
    subgoal
      by (auto simp: init_zero fun_eq_iff from_val_tuple15_def split: tuple15.splits)
    subgoal for v
      by (cases v) (auto split: list.splits tuple15.splits)
    subgoal for v
      by (cases v)
       (simp add: LLVM_Shallow.null_def to_val_ptr_def split: tuple15.splits)
    subgoal
      by (simp add: LLVM_Shallow.null_def to_val_ptr_def to_val_word_def init_zero split: tuple15.splits)
    done
end

subsubsection ‹Setup for LLVM code export›
text ‹Declare structure to code generator.›
lemma to_val_tuple17[ll_struct_of]: "struct_of TYPE(('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15) = VS_STRUCT [
  struct_of TYPE('a::llvm_rep),
  struct_of TYPE('b::llvm_rep),
  struct_of TYPE('c::llvm_rep),
  struct_of TYPE('d::llvm_rep),
  struct_of TYPE('e::llvm_rep),
  struct_of TYPE('f::llvm_rep),
  struct_of TYPE('g::llvm_rep),
  struct_of TYPE('h::llvm_rep),
  struct_of TYPE('i::llvm_rep),
  struct_of TYPE('j::llvm_rep),
  struct_of TYPE('k::llvm_rep),
  struct_of TYPE('l::llvm_rep),
  struct_of TYPE('m::llvm_rep),
  struct_of TYPE('n::llvm_rep),
  struct_of TYPE('o::llvm_rep)]"
  by (auto)

lemma node_insert_value:
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) M' 0 = Mreturn (Tuple15 M' N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) N' (Suc 0) = Mreturn (Tuple15 M N' D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) D' 2 = Mreturn (Tuple15 M N D' i W ivmtf icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) i' 3 = Mreturn (Tuple15 M N D i' W ivmtf icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) W' 4 = Mreturn (Tuple15 M N D i W' ivmtf icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) ivmtf' 5 = Mreturn (Tuple15 M N D i W ivmtf' icount ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) icount' 6 = Mreturn (Tuple15 M N D i W ivmtf icount' ccach lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) ccach' 7 = Mreturn (Tuple15 M N D i W ivmtf icount ccach' lbd outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) lbd' 8 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd' outl stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) outl' 9 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl' stats heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) stats' 10 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl stats' heur aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) heur' 11 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur' aivdom clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) aivdom' 12 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom' clss opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) clss' 13 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss' opts)"
  "ll_insert_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) opts' 14 = Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts')"
  by (simp_all add: ll_insert_value_def llvm_insert_value_def Let_def checked_from_val_def
                to_val_tuple15_def from_val_tuple15_def)

lemma node_extract_value:
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 0 = Mreturn M"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) (Suc 0) = Mreturn N"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 2 = Mreturn D"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 3 = Mreturn i"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 4 = Mreturn W"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 5 = Mreturn ivmtf"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 6 = Mreturn icount"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 7 = Mreturn ccach"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 8 = Mreturn lbd"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 9 = Mreturn outl"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 10 = Mreturn stats"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 11 = Mreturn heur"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 12 = Mreturn aivdom"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 13 = Mreturn clss"
  "ll_extract_value (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts) 14 = Mreturn opts"
  apply (simp_all add: ll_extract_value_def llvm_extract_value_def Let_def checked_from_val_def
                to_val_tuple15_def from_val_tuple15_def)
  done

text ‹Lemmas to translate node construction and destruction›
lemma inline_return_node[llvm_pre_simp]: "Mreturn (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = doM {
    r ← ll_insert_value init M 0;
    r ← ll_insert_value r N 1;
    r ← ll_insert_value r D 2;
    r ← ll_insert_value r i 3;
    r ← ll_insert_value r W 4;
    r ← ll_insert_value r ivmtf 5;
    r ← ll_insert_value r icount 6;
    r ← ll_insert_value r ccach 7;
    r ← ll_insert_value r lbd 8;
    r ← ll_insert_value r outl 9;
    r ← ll_insert_value r heur 10;
    r ← ll_insert_value r stats 11;
    r ← ll_insert_value r aivdom 12;
    r ← ll_insert_value r clss 13;
    r ← ll_insert_value r opts 14;
    Mreturn r
  }"
  apply (auto simp: node_insert_value)
  done

lemma inline_node_case[llvm_pre_simp]: "(case r of (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = doM {
    M ← ll_extract_value r 0;
    N ← ll_extract_value r 1;
    D ← ll_extract_value r 2;
    i ← ll_extract_value r 3;
    W ← ll_extract_value r 4;
    ivmtf ← ll_extract_value r 5;
    icount ← ll_extract_value r 6;
    ccach ← ll_extract_value r 7;
    lbd ← ll_extract_value r 8;
    outl ← ll_extract_value r 9;
    heur ← ll_extract_value r 10;
    stats ← ll_extract_value r 11;
    aivdom ← ll_extract_value r 12;
    clss ← ll_extract_value r 13;
    opts ← ll_extract_value r 14;
  f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done

lemma inline_return_node_case[llvm_pre_simp]: "doM {Mreturn (case r of (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)} = doM {
    M ← ll_extract_value r 0;
    N ← ll_extract_value r 1;
    D ← ll_extract_value r 2;
    i ← ll_extract_value r 3;
    W ← ll_extract_value r 4;
    ivmtf ← ll_extract_value r 5;
    icount ← ll_extract_value r 6;
    ccach ← ll_extract_value r 7;
    lbd ← ll_extract_value r 8;
    outl ← ll_extract_value r 9;
    heur ← ll_extract_value r 10;
    stats ← ll_extract_value r 11;
    aivdom ← ll_extract_value r 12;
    clss ← ll_extract_value r 13;
    opts ← ll_extract_value r 14;
  Mreturn (f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done
lemma inline_direct_return_node_case[llvm_pre_simp]: "doM {(case r of (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)} = doM {
    M ← ll_extract_value r 0;
    N ← ll_extract_value r 1;
    D ← ll_extract_value r 2;
    i ← ll_extract_value r 3;
    W ← ll_extract_value r 4;
    ivmtf ← ll_extract_value r 5;
    icount ← ll_extract_value r 6;
    ccach ← ll_extract_value r 7;
    lbd ← ll_extract_value r 8;
    outl ← ll_extract_value r 9;
    heur ← ll_extract_value r 10;
    stats ← ll_extract_value r 11;
    aivdom ← ll_extract_value r 12;
    clss ← ll_extract_value r 13;
    opts ← ll_extract_value r 14;
   (f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done

lemmas [llvm_inline] =
  tuple15.Tuple15_a_def
  tuple15.Tuple15_b_def
  tuple15.Tuple15_c_def
  tuple15.Tuple15_d_def
  tuple15.Tuple15_e_def
  tuple15.Tuple15_f_def
  tuple15.Tuple15_g_def
  tuple15.Tuple15_h_def
  tuple15.Tuple15_i_def
  tuple15.Tuple15_j_def
  tuple15.Tuple15_k_def
  tuple15.Tuple15_l_def
  tuple15.Tuple15_m_def
  tuple15.Tuple15_n_def
  tuple15.Tuple15_o_def

fun tuple15_assn :: ‹
  ('a ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('b ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('c ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('d ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('e ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('f ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('g ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('h ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('i ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('j ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('k ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('l ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('m ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('n ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('o ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ _ ⇒ assn› where
  ‹tuple15_assn a_assn b_assn' c_assn d_assn e_assn f_assn g_assn h_assn i_assn j_assn k_assn l_assn m_assn n_assn o_assn S T =
   (case (S, T) of
  (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts,
   Tuple15 M' N' D' i' W' ivmtf' icount' ccach' lbd' outl' heur' stats' aivdom' clss' opts')
     ⇒
 (a_assn M (M') ∧* b_assn' N (N') ∧* c_assn D (D')  ∧* d_assn i (i') ∧*
 e_assn W (W') ∧* f_assn ivmtf (ivmtf') ∧* g_assn icount (icount')  ∧* h_assn ccach (ccach') ∧*
 i_assn lbd (lbd') ∧* j_assn outl (outl') ∧* k_assn heur (heur')  ∧* l_assn stats (stats') ∧*
 m_assn aivdom (aivdom') ∧* n_assn clss (clss') ∧* o_assn opts (opts')))
  ›

locale tuple15_state_ops =
  fixes
    a_assn :: ‹'a ⇒ 'xa ⇒ assn› and
    b_assn :: ‹'b ⇒ 'xb ⇒ assn› and
    c_assn :: ‹'c ⇒ 'xc ⇒ assn› and
    d_assn :: ‹'d ⇒ 'xd ⇒ assn› and
    e_assn :: ‹'e ⇒ 'xe ⇒ assn› and
    f_assn :: ‹'f ⇒ 'xf ⇒ assn› and
    g_assn :: ‹'g ⇒ 'xg ⇒ assn› and
    h_assn :: ‹'h ⇒ 'xh ⇒ assn› and
    i_assn :: ‹'i ⇒ 'xi ⇒ assn› and
    j_assn :: ‹'j ⇒ 'xj ⇒ assn› and
    k_assn :: ‹'k ⇒ 'xk ⇒ assn› and
    l_assn :: ‹'l ⇒ 'xl ⇒ assn› and
    m_assn :: ‹'m ⇒ 'xm ⇒ assn› and
    n_assn :: ‹'n ⇒ 'xn ⇒ assn› and
    o_assn :: ‹'o ⇒ 'xo ⇒ assn› and
    a_default :: 'a and
    a :: ‹'xa llM› and
    b_default :: 'b and
    b :: ‹'xb llM› and
    c_default :: 'c and
    c :: ‹'xc llM› and
    d_default :: 'd and
    d :: ‹'xd llM› and
    e_default :: 'e and
    e :: ‹'xe llM› and
    f_default :: 'f and
    f :: ‹'xf llM› and
    g_default :: 'g and
    g :: ‹'xg llM› and
    h_default :: 'h and
    h :: ‹'xh llM› and
    i_default :: 'i and
    i :: ‹'xi llM› and
    j_default :: 'j and
    j :: ‹'xj llM› and
    k_default :: 'k and
    k :: ‹'xk llM› and
    l_default :: 'l and
    l :: ‹'xl llM› and
    m_default :: 'm and
    m :: ‹'xm llM› and
    n_default :: 'n and
    n :: ‹'xn llM› and
    ko_default :: 'o and
    ko :: ‹'xo llM›
begin

definition tuple15_int_assn :: ‹_ ⇒ _ ⇒ assn› where
‹tuple15_int_assn = tuple15_assn
  a_assn b_assn c_assn d_assn
  e_assn f_assn g_assn h_assn
  i_assn j_assn k_assn l_assn
  m_assn n_assn o_assn›

definition remove_a :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'a × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_a tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x1, Tuple15 a_default x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_b :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'b × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_b tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x2, Tuple15 x1 b_default x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_c :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ _ × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_c tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x3, Tuple15 x1 x2 c_default x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_d :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ _ × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_d tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x4, Tuple15 x1 x2 x3 d_default x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_e :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'e × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_e tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x5, Tuple15 x1 x2 x3 x4 e_default x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_f :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'f × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_f tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x6, Tuple15 x1 x2 x3 x4 x5 f_default x7 x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_g :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'g × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_g tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x7, Tuple15 x1 x2 x3 x4 x5 x6 g_default x8 x9 x10 x11 x12 x13 x14 x15))›

definition remove_h :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'h × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_h tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x8, Tuple15 x1 x2 x3 x4 x5 x6 x7 h_default x9 x10 x11 x12 x13 x14 x15))›

definition remove_i :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'i × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_i tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x9, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 i_default x10 x11 x12 x13 x14 x15))›

definition remove_j :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'j × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_j tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x10, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 j_default x11 x12 x13 x14 x15))›

definition remove_k :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'k × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_k tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x11, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 k_default x12 x13 x14 x15))›

definition remove_l :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'l × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_l tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x12, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 l_default x13 x14 x15))›

definition remove_m :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'm × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_m tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x13, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 m_default x14 x15))›

definition remove_n :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'n × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_n tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x14, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 n_default x15))›

definition remove_o :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ 'o × ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹remove_o tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
      (x15, Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ko_default))›

definition update_a :: ‹'a ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_a x1 tuple15 = (case tuple15 of Tuple15 M x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_b :: ‹'b ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_b x2 tuple15 = (case tuple15 of Tuple15 x1 M x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_c :: ‹'c ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_c x3 tuple15 = (case tuple15 of Tuple15 x1 x2 M x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_d :: ‹'d ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_d x4 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 M x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_e :: ‹'e ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_e x5 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 M x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_f :: ‹'f ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_f x6 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 M x7 x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_g :: ‹'g ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_g x7 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 M x8 x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_h :: ‹'h ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_h x8 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 M x9 x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_i :: ‹'i ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_i x9 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 M x10 x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_j :: ‹'j ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_j x10 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 M x11 x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_k :: ‹'k ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_k x11 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 M x12 x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_l :: ‹'l ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_l x12 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 M x13 x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_m :: ‹'m ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_m x13 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 M x14 x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_n :: ‹'n ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_n x14 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 M x15 ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›

definition update_o :: ‹'o ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹update_o x15 tuple15 = (case tuple15 of Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 M ⇒
    let _ = M in
    Tuple15 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)›


end
 
lemma tuple15_assn_conv[simp]: 
  "tuple15_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 (Tuple15 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)
  (Tuple15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15') =
  (P1 a1 a1' ∧*
  P2 a2 a2' ∧*
  P3 a3 a3' ∧*
  P4 a4 a4' ∧*
  P5 a5 a5' ∧*
  P6 a6 a6' ∧*
  P7 a7 a7' ∧*
  P8 a8 a8' ∧* P9 a9 a9' ∧* P10 a10 a10' ∧* P11 a11 a11' ∧* P12 a12 a12' ∧* P13 a13 a13' ∧* P14 a14 a14' ∧* P15 a15 a15')"
  unfolding tuple15_assn.simps by auto
lemma tuple15_assn_ctxt:
  ‹tuple15_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 (Tuple15 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)
  (Tuple15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15') = z ⟹
  hn_ctxt (tuple15_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15) (Tuple15 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)
  (Tuple15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15')= z›
  by (simp add: hn_ctxt_def)

lemma hn_case_tuple15'[sepref_comb_rules]:
  assumes FR: ‹Γ ⊢ hn_ctxt (tuple15_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15) p' p ** Γ1›
  assumes Pair: "⋀a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15'.
        ⟦p'=Tuple15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15'⟧
    ⟹ hn_refine (hn_ctxt P1 a1' a1 ∧* hn_ctxt P2 a2' a2 ∧* hn_ctxt P3 a3' a3 ∧* hn_ctxt P4 a4' a4 ∧*
       hn_ctxt P5 a5' a5 ∧* hn_ctxt P6 a6' a6 ∧* hn_ctxt P7 a7' a7 ∧* hn_ctxt P8 a8' a8 ∧*
       hn_ctxt P9 a9' a9 ∧* hn_ctxt P10 a10' a10 ∧* hn_ctxt P11 a11' a11 ∧* hn_ctxt P12 a12' a12 ∧*
       hn_ctxt P13 a13' a13 ∧* hn_ctxt P14 a14' a14 ∧* hn_ctxt P15 a15' a15 ∧* Γ1)
          (f a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)
          (Γ2 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15') R
          (CP a1 a2  a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)
         (f' a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15')"
  assumes FR2: ‹⋀a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15'.
       Γ2 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' ⊢
       hn_ctxt P1' a1' a1 ** hn_ctxt P2' a2' a2 ** hn_ctxt P3' a3' a3 ** hn_ctxt P4' a4' a4 **
       hn_ctxt P5' a5' a5 ** hn_ctxt P6' a6' a6 ** hn_ctxt P7' a7' a7 ** hn_ctxt P8' a8' a8 **
       hn_ctxt P9' a9' a9 ** hn_ctxt P10' a10' a10 ** hn_ctxt P11' a11' a11 ** hn_ctxt P12' a12' a12 **
       hn_ctxt P13' a13' a13 ** hn_ctxt P14' a14' a14 ** hn_ctxt P15' a15' a15 ** Γ1'›
  shows ‹hn_refine Γ (case_tuple15 f p) (hn_ctxt (tuple15_assn P1' P2' P3' P4' P5' P6' P7' P8' P9' P10' P11' P12' P13' P14' P15') p' p ** Γ1')
    R (case_tuple15 CP p) (case_tuple15$(λ⇩2a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15. f' a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)$p')› (is ‹?G Γ›)
  unfolding autoref_tag_defs PROTECT2_def
  apply1 (rule hn_refine_cons_pre[OF FR])
    apply1 (cases p; cases p'; simp add: tuple15_assn_conv[THEN tuple15_assn_ctxt])
  unfolding CP_SPLIT_def prod.simps
  apply (rule hn_refine_cons[OF _ Pair _ entails_refl])
  applyS (simp add: hn_ctxt_def)
  applyS simp using FR2
  by (simp add: hn_ctxt_def)


lemma case_tuple15_arity[sepref_monadify_arity]:
  ‹case_tuple15 ≡ λ⇩2fp p. SP case_tuple15$(λ⇩2a b. fp$a$b)$p›
  by (simp_all only: SP_def APP_def PROTECT2_def RCALL_def)

lemma case_tuple15_comb[sepref_monadify_comb]:
  ‹⋀fp p. case_tuple15$fp$p ≡ Refine_Basic.bind$(EVAL$p)$(λ⇩2p. (SP case_tuple15$fp$p))›
  by (simp_all)

lemma case_tuple15_plain_comb[sepref_monadify_comb]:
  "EVAL$(case_tuple15$(λ⇩2a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15. fp a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)$p) ≡
    Refine_Basic.bind$(EVAL$p)$(λ⇩2p. case_tuple15$(λ⇩2a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15. EVAL$(fp a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15))$p)"
  apply (rule eq_reflection, simp split: list.split prod.split option.split tuple15.split)+
  done

lemma ho_tuple15_move[sepref_preproc]: ‹case_tuple15 (λa1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 x. f x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15) =
  (λp x. case_tuple15 (f x) p)›
  by (auto split: tuple15.splits)

locale tuple15_state =
  tuple15_state_ops a_assn b_assn c_assn d_assn e_assn
  f_assn g_assn h_assn i_assn j_assn
  k_assn l_assn m_assn n_assn o_assn
  a_default a
  b_default b
  c_default c
  d_default d
  e_default e
  f_default f
  g_default g
  h_default h
  i_default i
  j_default j
  k_default k
  l_default l
  m_default m
  n_default n
  ko_default ko
  for
    a_assn :: ‹'a ⇒ 'xa ⇒ assn› and
    b_assn :: ‹'b ⇒ 'xb ⇒ assn› and
    c_assn :: ‹'c ⇒ 'xc ⇒ assn› and
    d_assn :: ‹'d ⇒ 'xd ⇒ assn› and
    e_assn :: ‹'e ⇒ 'xe ⇒ assn› and
    f_assn :: ‹'f ⇒ 'xf ⇒ assn› and
    g_assn :: ‹'g ⇒ 'xg ⇒ assn› and
    h_assn :: ‹'h ⇒ 'xh ⇒ assn› and
    i_assn :: ‹'i ⇒ 'xi ⇒ assn› and
    j_assn :: ‹'j ⇒ 'xj ⇒ assn› and
    k_assn :: ‹'k ⇒ 'xk ⇒ assn› and
    l_assn :: ‹'l ⇒ 'xl ⇒ assn› and
    m_assn :: ‹'m ⇒ 'xm ⇒ assn› and
    n_assn :: ‹'n ⇒ 'xn ⇒ assn› and
    o_assn :: ‹'o ⇒ 'xo ⇒ assn› and
    a_default :: 'a and
    a :: ‹'xa llM› and
    b_default :: 'b and
    b :: ‹'xb llM› and
    c_default :: 'c and
    c :: ‹'xc llM› and
    d_default :: 'd and
    d :: ‹'xd llM› and
    e_default :: 'e and
    e :: ‹'xe llM› and
    f_default :: 'f and
    f :: ‹'xf llM› and
    g_default :: 'g and
    g :: ‹'xg llM› and
    h_default :: 'h and
    h :: ‹'xh llM› and
    i_default :: 'i and
    i :: ‹'xi llM› and
    j_default :: 'j and
    j :: ‹'xj llM› and
    k_default :: 'k and
    k :: ‹'xk llM› and
    l_default :: 'l and
    l :: ‹'xl llM› and
    m_default :: 'm and
    m :: ‹'xm llM› and
    n_default :: 'n and
    n :: ‹'xn llM› and
    ko_default :: 'o and
    ko :: ‹'xo llM› and
    a_free :: ‹'xa ⇒ unit llM› and
    b_free :: ‹'xb ⇒ unit llM› and
    c_free :: ‹'xc ⇒ unit llM› and
    d_free :: ‹'xd ⇒ unit llM› and
    e_free :: ‹'xe ⇒ unit llM› and
    f_free :: ‹'xf ⇒ unit llM› and
    g_free :: ‹'xg ⇒ unit llM› and
    h_free :: ‹'xh ⇒ unit llM› and
    i_free :: ‹'xi ⇒ unit llM› and
    j_free :: ‹'xj ⇒ unit llM› and
    k_free :: ‹'xk ⇒ unit llM› and
    l_free :: ‹'xl ⇒ unit llM› and
    m_free :: ‹'xm ⇒ unit llM› and
    n_free :: ‹'xn ⇒ unit llM› and
    o_free :: ‹'xo ⇒ unit llM› +
  assumes
    a: ‹(uncurry0 a, uncurry0  (RETURN a_default)) ∈ unit_assn⇧k →⇩a a_assn› and
    b: ‹(uncurry0 b, uncurry0  (RETURN b_default)) ∈ unit_assn⇧k →⇩a b_assn› and
    c: ‹(uncurry0 c, uncurry0  (RETURN c_default)) ∈ unit_assn⇧k →⇩a c_assn› and
    d: ‹(uncurry0 d, uncurry0  (RETURN d_default)) ∈ unit_assn⇧k →⇩a d_assn› and
    e: ‹(uncurry0 e, uncurry0  (RETURN e_default)) ∈ unit_assn⇧k →⇩a e_assn› and
    f: ‹(uncurry0 f, uncurry0  (RETURN f_default)) ∈ unit_assn⇧k →⇩a f_assn› and
    g: ‹(uncurry0 g, uncurry0  (RETURN g_default)) ∈ unit_assn⇧k →⇩a g_assn› and
    h: ‹(uncurry0 h, uncurry0  (RETURN h_default)) ∈ unit_assn⇧k →⇩a h_assn› and
    i: ‹(uncurry0 i, uncurry0  (RETURN i_default)) ∈ unit_assn⇧k →⇩a i_assn› and
    j: ‹(uncurry0 j, uncurry0  (RETURN j_default)) ∈ unit_assn⇧k →⇩a j_assn› and
    k: ‹(uncurry0 k, uncurry0  (RETURN k_default)) ∈ unit_assn⇧k →⇩a k_assn› and
    l: ‹(uncurry0 l, uncurry0  (RETURN l_default)) ∈ unit_assn⇧k →⇩a l_assn› and
    m: ‹(uncurry0 m, uncurry0  (RETURN m_default)) ∈ unit_assn⇧k →⇩a m_assn› and
    n: ‹(uncurry0 n, uncurry0  (RETURN n_default)) ∈ unit_assn⇧k →⇩a n_assn› and
    o: ‹(uncurry0 ko, uncurry0  (RETURN ko_default)) ∈ unit_assn⇧k →⇩a o_assn›and
    a_free: ‹MK_FREE a_assn a_free› and
    b_free: ‹MK_FREE b_assn b_free›and
    c_free: ‹MK_FREE c_assn c_free›and
    d_free: ‹MK_FREE d_assn d_free›and
    e_free: ‹MK_FREE e_assn e_free›and
    f_free: ‹MK_FREE f_assn f_free›and
    g_free: ‹MK_FREE g_assn g_free›and
    h_free: ‹MK_FREE h_assn h_free›and
    i_free: ‹MK_FREE i_assn i_free›and
    j_free: ‹MK_FREE j_assn j_free›and
    k_free: ‹MK_FREE k_assn k_free›and
    l_free: ‹MK_FREE l_assn l_free›and
    m_free: ‹MK_FREE m_assn m_free›and
    n_free: ‹MK_FREE n_assn n_free›and
    o_free: ‹MK_FREE o_assn o_free›
  notes [[sepref_register_adhoc a_default b_default c_default d_default e_default f_default g_default h_default
  i_default j_default k_default l_default m_default n_default ko_default p_default]]
begin

lemmas [sepref_comb_rules] = hn_case_tuple15'[of _ a_assn b_assn c_assn d_assn e_assn f_assn
  g_assn h_assn i_assn j_assn k_assn l_assn m_assn n_assn o_assn,
  unfolded tuple15_int_assn_def[symmetric]]

lemma ex_tuple15_iff: "(∃b :: (_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)tuple15. P b) ⟷
  (∃a b  c d e f g h i j k l m n ko. P (Tuple15 a b  c d e f g h i j k l m n ko))"
  apply auto
    apply (case_tac b)
  by force

lemmas [sepref_frame_free_rules] = a_free b_free c_free d_free e_free f_free g_free h_free i_free
  j_free k_free l_free m_free n_free o_free
sepref_register
  ‹Tuple15›
lemma [sepref_fr_rules]: ‹(uncurry14 (Mreturn o⇩1⇩5 Tuple15), uncurry14 (RETURN o⇩1⇩5 Tuple15))
  ∈ a_assn⇧d *⇩a b_assn⇧d *⇩a c_assn⇧d *⇩a d_assn⇧d *⇩a
  e_assn⇧d *⇩a f_assn⇧d *⇩a g_assn⇧d *⇩a h_assn⇧d *⇩a
  i_assn⇧d *⇩a j_assn⇧d *⇩a k_assn⇧d *⇩a l_assn⇧d *⇩a
  m_assn⇧d *⇩a n_assn⇧d *⇩a o_assn⇧d
  →⇩a tuple15_int_assn›
  unfolding tuple15_int_assn_def
  apply sepref_to_hoare
  apply vcg
  unfolding ex_tuple15_iff
  apply vcg'
  done

lemma [sepref_frame_match_rules]:
  ‹ hn_ctxt
     (tuple15_assn (invalid_assn a_assn) (invalid_assn b_assn) (invalid_assn c_assn) (invalid_assn d_assn) (invalid_assn e_assn)
    (invalid_assn f_assn) (invalid_assn g_assn) (invalid_assn h_assn) (invalid_assn i_assn) (invalid_assn j_assn) (invalid_assn k_assn)
   (invalid_assn l_assn) (invalid_assn m_assn) (invalid_assn n_assn) (invalid_assn o_assn)) ax bx ⊢ hn_val UNIV ax bx›
    unfolding hn_ctxt_def invalid_assn_def tuple15_int_assn_def entails_def
    apply (auto split: prod.split tuple15.splits elim: is_pureE 
      simp: sep_algebra_simps pure_part_pure_conj_eq)
    apply (auto simp: pure_part_def)
      apply (auto simp: pure_def pure_true_conv)
    done

lemma RETURN_case_tuple15_inverse: ‹RETURN
      (let _ = M
         in ff) =
      (do {_ ← mop_free M;
         RETURN (ff)})›
    by (auto intro!: ext simp: mop_free_def split: tuple15.splits)

sepref_definition update_a_code
  is ‹uncurry (RETURN oo update_a)›
  :: ‹a_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=5]]
  unfolding update_a_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_b_code
  is ‹uncurry (RETURN oo update_b)›
  :: ‹b_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_b_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_c_code
  is ‹uncurry (RETURN oo update_c)›
  :: ‹c_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_c_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_d_code
  is ‹uncurry (RETURN oo update_d)›
  :: ‹d_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_d_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_e_code
  is ‹uncurry (RETURN oo update_e)›
  :: ‹e_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_e_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_f_code
  is ‹uncurry (RETURN oo update_f)›
  :: ‹f_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_f_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_g_code
  is ‹uncurry (RETURN oo update_g)›
  :: ‹g_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_g_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_h_code
  is ‹uncurry (RETURN oo update_h)›
  :: ‹h_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_h_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_i_code
  is ‹uncurry (RETURN oo update_i)›
  :: ‹i_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_i_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_j_code
  is ‹uncurry (RETURN oo update_j)›
  :: ‹j_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_j_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_k_code
  is ‹uncurry (RETURN oo update_k)›
  :: ‹k_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_k_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_l_code
  is ‹uncurry (RETURN oo update_l)›
  :: ‹l_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_l_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_m_code
  is ‹uncurry (RETURN oo update_m)›
  :: ‹m_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_m_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_n_code
  is ‹uncurry (RETURN oo update_n)›
  :: ‹n_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_n_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

sepref_definition update_o_code
  is ‹uncurry (RETURN oo update_o)›
  :: ‹o_assn⇧d *⇩a tuple15_int_assn⇧d →⇩a tuple15_int_assn›
  supply [[goals_limit=1]]
  unfolding update_o_def tuple15.case_distrib comp_def RETURN_case_tuple15_inverse
  by sepref

lemma RETURN_case_tuple15_invers: ‹(RETURN ∘∘ case_tuple15)
   (λx1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.
  ff x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) =
  case_tuple15
   (λx1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.
  RETURN (ff x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15))›
  by (auto intro!: ext split: tuple15.splits)

lemmas [sepref_fr_rules] = a b c d e f g h i j k l m n o

sepref_definition remove_a_code
  is ‹RETURN o remove_a›
  :: ‹ tuple15_int_assn⇧d →⇩a a_assn ×⇩a tuple15_int_assn›
  unfolding remove_a_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_b_code
  is ‹RETURN o remove_b›
  :: ‹ tuple15_int_assn⇧d →⇩a b_assn ×⇩a tuple15_int_assn›
  unfolding remove_b_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_c_code
  is ‹RETURN o remove_c›
  :: ‹ tuple15_int_assn⇧d →⇩a c_assn ×⇩a tuple15_int_assn›
  unfolding remove_c_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_d_code
  is ‹RETURN o remove_d›
  :: ‹ tuple15_int_assn⇧d →⇩a d_assn ×⇩a tuple15_int_assn›
  unfolding remove_d_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_e_code
  is ‹RETURN o remove_e›
  :: ‹ tuple15_int_assn⇧d →⇩a e_assn ×⇩a tuple15_int_assn›
  unfolding remove_e_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_f_code
  is ‹RETURN o remove_f›
  :: ‹ tuple15_int_assn⇧d →⇩a f_assn ×⇩a tuple15_int_assn›
  unfolding remove_f_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_g_code
  is ‹RETURN o remove_g›
  :: ‹ tuple15_int_assn⇧d →⇩a g_assn ×⇩a tuple15_int_assn›
  unfolding remove_g_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_h_code
  is ‹RETURN o remove_h›
  :: ‹ tuple15_int_assn⇧d →⇩a h_assn ×⇩a tuple15_int_assn›
  unfolding remove_h_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_i_code
  is ‹RETURN o remove_i›
  :: ‹ tuple15_int_assn⇧d →⇩a i_assn ×⇩a tuple15_int_assn›
  unfolding remove_i_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_j_code
  is ‹RETURN o remove_j›
  :: ‹ tuple15_int_assn⇧d →⇩a j_assn ×⇩a tuple15_int_assn›
  unfolding remove_j_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_k_code
  is ‹RETURN o remove_k›
  :: ‹ tuple15_int_assn⇧d →⇩a k_assn ×⇩a tuple15_int_assn›
  unfolding remove_k_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_l_code
  is ‹RETURN o remove_l›
  :: ‹ tuple15_int_assn⇧d →⇩a l_assn ×⇩a tuple15_int_assn›
  unfolding remove_l_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_m_code
  is ‹RETURN o remove_m›
  :: ‹ tuple15_int_assn⇧d →⇩a m_assn ×⇩a tuple15_int_assn›
  unfolding remove_m_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_n_code
  is ‹RETURN o remove_n›
  :: ‹ tuple15_int_assn⇧d →⇩a n_assn ×⇩a tuple15_int_assn›
  unfolding remove_n_def RETURN_case_tuple15_invers
  by sepref

sepref_definition remove_o_code
  is ‹RETURN o remove_o›
  :: ‹ tuple15_int_assn⇧d →⇩a o_assn ×⇩a tuple15_int_assn›
  unfolding remove_o_def RETURN_case_tuple15_invers
  by sepref

lemmas separation_rules =
  remove_a_code.refine
  remove_b_code.refine
  remove_c_code.refine
  remove_d_code.refine
  remove_e_code.refine
  remove_f_code.refine
  remove_g_code.refine
  remove_h_code.refine
  remove_i_code.refine
  remove_j_code.refine
  remove_k_code.refine
  remove_l_code.refine
  remove_m_code.refine
  remove_n_code.refine
  remove_o_code.refine
  update_a_code.refine
  update_b_code.refine
  update_c_code.refine
  update_d_code.refine
  update_e_code.refine
  update_f_code.refine
  update_g_code.refine
  update_h_code.refine
  update_i_code.refine
  update_j_code.refine
  update_k_code.refine
  update_l_code.refine
  update_m_code.refine
  update_n_code.refine
  update_o_code.refine

lemmas code_rules =
  remove_a_code_def
  remove_b_code_def
  remove_c_code_def
  remove_d_code_def
  remove_e_code_def
  remove_f_code_def
  remove_g_code_def
  remove_h_code_def
  remove_i_code_def
  remove_j_code_def
  remove_k_code_def
  remove_l_code_def
  remove_m_code_def
  remove_n_code_def
  remove_o_code_def
  update_a_code_def
  update_b_code_def
  update_c_code_def
  update_d_code_def
  update_e_code_def
  update_f_code_def
  update_g_code_def
  update_h_code_def
  update_i_code_def
  update_j_code_def
  update_k_code_def
  update_l_code_def
  update_m_code_def
  update_n_code_def
  update_o_code_def

lemmas setter_and_getters_def =
   update_a_def remove_a_def
   update_b_def remove_b_def
   update_c_def remove_c_def
   update_d_def remove_d_def
   update_e_def remove_e_def
   update_f_def remove_f_def
   update_g_def remove_g_def
   update_h_def remove_h_def
   update_i_def remove_i_def
   update_j_def remove_j_def
   update_k_def remove_k_def
   update_l_def remove_l_def
   update_m_def remove_m_def
   update_n_def remove_n_def
   update_o_def remove_o_def

end


context tuple15_state
begin
lemma reconstruct_isasat[sepref_frame_match_rules]:
  ‹hn_ctxt
     (tuple15_assn (a_assn) (b_assn) (c_assn) (d_assn) (e_assn)
    (f_assn) (g_assn) (h_assn) (i_assn) (j_assn) (k_assn)
   (l_assn) (m_assn) (n_assn) (o_assn)) ax bx ⊢ hn_ctxt tuple15_int_assn ax bx›
    unfolding tuple15_int_assn_def
    apply (auto split: prod.split tuple15.splits elim: is_pureE 
      simp: sep_algebra_simps pure_part_pure_conj_eq)
      done

context
  fixes x_assn :: ‹'r ⇒ 'q ⇒ assn› and
    read_all_code :: ‹'xa ⇒ 'xb ⇒ 'xc ⇒ 'xd ⇒ 'xe ⇒ 'xf ⇒ 'xg ⇒ 'xh ⇒ 'xi ⇒ 'xj ⇒ 'xk ⇒ 'xl ⇒ 'xm ⇒ 'xn ⇒ 'xo ⇒ 'q llM› and
    read_all :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'g ⇒ 'h ⇒ 'i ⇒ 'j ⇒ 'k ⇒ 'l ⇒ 'm ⇒ 'n ⇒ 'o ⇒ 'r nres›
begin

definition read_all_st_code :: ‹_› where
  ‹read_all_st_code xi = (case xi of
  Tuple15 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 ⇒
    read_all_code a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15)›

definition read_all_st :: ‹('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o) tuple15 ⇒ _› where
  ‹read_all_st tuple15 = (case tuple15 of Tuple15 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15a16 ⇒
  read_all a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15a16)›

context
  fixes P
  assumes trail_read[sepref_fr_rules]: ‹(uncurry14 read_all_code, uncurry14 read_all) ∈
      [uncurry14 P]⇩a a_assn⇧k *⇩a b_assn⇧k *⇩a c_assn⇧k *⇩a d_assn⇧k *⇩a e_assn⇧k *⇩a f_assn⇧k *⇩a
          g_assn⇧k *⇩a h_assn⇧k *⇩a i_assn⇧k *⇩a j_assn⇧k *⇩a k_assn⇧k *⇩a l_assn⇧k *⇩a
          m_assn⇧k *⇩a n_assn⇧k *⇩a o_assn⇧k → x_assn›
  notes [[sepref_register_adhoc read_all]]
begin
sepref_definition read_all_st_code_tmp
  is read_all_st
  :: ‹[case_tuple15 P]⇩a tuple15_int_assn⇧k → x_assn›
   unfolding read_all_st_def
   by sepref

lemmas read_all_st_code_refine =
  read_all_st_code_tmp.refine[unfolded read_all_st_code_tmp_def
    read_all_st_code_def[symmetric]]
end

end

end

lemma Mreturn_comp_Tuple15:
  ‹(Mreturn o⇩1⇩5 Tuple15) a b c d e f g h i j k l m n ko =
  Mreturn (Tuple15 a b c d e f g h i j k l m n ko)›
  by auto

lemma tuple15_free[sepref_frame_free_rules]:
  assumes
  ‹MK_FREE A freea› ‹MK_FREE B freeb› ‹MK_FREE C freec› ‹MK_FREE D freed›
  ‹MK_FREE E freee› ‹MK_FREE F freef› ‹MK_FREE G freeg› ‹MK_FREE H freeh›
  ‹MK_FREE I freei› ‹MK_FREE J freej› ‹MK_FREE K freek› ‹MK_FREE L freel›
  ‹MK_FREE M freem› ‹MK_FREE N freen› ‹MK_FREE KO freeko›
  shows
  ‹
  MK_FREE (tuple15_assn A B C D E F G H I J K L M N KO) (λS. case S of Tuple15 a b c d e f g h i j k l m n ko ⇒ do⇩M {
  freea a; freeb b; freec c; freed d; freee e; freef f; freeg g; freeh h; freei i; freej j;
  freek k; freel l; freem m; freen n; freeko ko
  })›
  supply [vcg_rules] = assms[THEN MK_FREED]
  apply (rule)+
  apply (clarsimp split: tuple15.splits)
  by vcg'

end