Theory Tuple16_LLVM

theory Tuple16_LLVM
  imports Tuple16 IsaSAT_Literals_LLVM
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN


instantiation tuple16 ::
  (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) llvm_rep
begin
  definition to_val_tuple16 where
    ‹to_val_tuple16 ≡ (λS. case S of
     Tuple16 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena ⇒ 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, to_val arena])›

  definition from_val_tuple16 :: ‹llvm_val ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16› where
    ‹from_val_tuple16 ≡ (λp. case llvm_val.the_fields p of
   [M, N, D, i, W, ivmtf, icount, ccach, lbd, outl, stats, heur, aivdom, clss, opts, arena] ⇒
     Tuple16 (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) (from_val arena))›

  definition [simp]: "struct_of_tuple16 (_ :: ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 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), struct_of TYPE('p)]"

  definition [simp]: "init_tuple16 :: ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ≡ Tuple16 init init init init init init init init init init init init init init init init"

  instance
    apply standard
    unfolding from_val_tuple16_def to_val_tuple16_def struct_of_tuple16_def init_tuple16_def comp_def tuple16.case_distrib
    subgoal
      by (auto simp: init_zero fun_eq_iff from_val_tuple16_def split: tuple16.splits)
    subgoal for v
      by (cases v) (auto split: list.splits tuple16.splits)
    subgoal for v
      by (cases v)
       (simp add: LLVM_Shallow.null_def to_val_ptr_def split: tuple16.splits)
    subgoal
      by (simp add: LLVM_Shallow.null_def to_val_ptr_def to_val_word_def init_zero split: tuple16.splits)
    done
end

subsubsection ‹Setup for LLVM code export›
text ‹Declare structure to code generator.›

lemma to_val_tuple16[ll_struct_of]: "struct_of TYPE(('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16) = 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),
  struct_of TYPE('p::llvm_rep)]"
  by (auto)


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

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

text ‹Lemmas to translate node construction and destruction›
lemma inline_return_node[llvm_pre_simp]: "Mreturn (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = 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;
    r ← ll_insert_value r arena 15;
    Mreturn r
  }"
  apply (auto simp: node_insert_value)
  done

lemma inline_node_case[llvm_pre_simp]: "(case r of (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = 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;
    arena ← ll_extract_value r 15;
  f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done

lemma inline_return_node_case[llvm_pre_simp]: "doM {Mreturn (case r of (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)} = 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;
    arena ← ll_extract_value r 15;
  Mreturn (f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done
lemma inline_direct_return_node_case[llvm_pre_simp]: "doM {(case r of (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) ⇒ f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)} = 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;
    arena ← ll_extract_value r 15;
   (f M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)
}"
  apply (cases r)
  apply (auto simp: node_extract_value)
  done

lemmas [llvm_inline] =
  tuple16.Tuple16_get_a_def
  tuple16.Tuple16_get_b_def
  tuple16.Tuple16_get_c_def
  tuple16.Tuple16_get_d_def
  tuple16.Tuple16_get_e_def
  tuple16.Tuple16_get_f_def
  tuple16.Tuple16_get_g_def
  tuple16.Tuple16_get_h_def
  tuple16.Tuple16_get_i_def
  tuple16.Tuple16_get_j_def
  tuple16.Tuple16_get_l_def
  tuple16.Tuple16_get_k_def
  tuple16.Tuple16_get_m_def
  tuple16.Tuple16_get_n_def
  tuple16.Tuple16_get_o_def
  tuple16.Tuple16_get_p_def

fun tuple16_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) ⇒
  ('p ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒
  ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j,
     'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _ ⇒ assn› where
  ‹tuple16_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 p_assn S T =
   (case (S, T) of
  (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena,
   Tuple16 M' N' D' i' W' ivmtf' icount' ccach' lbd' outl' heur' stats' aivdom' clss' opts' arena')
     ⇒
 (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')  ∧* p_assn arena (arena')))
  ›


locale tuple16_ops =
  fixes
    a_assn :: ‹'a ⇒ 'xa :: llvm_rep ⇒ assn› and
    b_assn :: ‹'b ⇒ 'xb:: llvm_rep ⇒ assn› and
    c_assn :: ‹'c ⇒ 'xc:: llvm_rep ⇒ assn› and
    d_assn :: ‹'d ⇒ 'xd:: llvm_rep ⇒ assn› and
    e_assn :: ‹'e ⇒ 'xe:: llvm_rep ⇒ assn› and
    f_assn :: ‹'f ⇒ 'xf:: llvm_rep ⇒ assn› and
    g_assn :: ‹'g ⇒ 'xg:: llvm_rep ⇒ assn› and
    h_assn :: ‹'h ⇒ 'xh:: llvm_rep ⇒ assn› and
    i_assn :: ‹'i ⇒ 'xi:: llvm_rep ⇒ assn› and
    j_assn :: ‹'j ⇒ 'xj:: llvm_rep ⇒ assn› and
    k_assn :: ‹'k ⇒ 'xk:: llvm_rep ⇒ assn› and
    l_assn :: ‹'l ⇒ 'xl:: llvm_rep ⇒ assn› and
    m_assn :: ‹'m ⇒ 'xm:: llvm_rep ⇒ assn› and
    n_assn :: ‹'n ⇒ 'xn:: llvm_rep ⇒ assn› and
    o_assn :: ‹'o ⇒ 'xo:: llvm_rep ⇒ assn› and
    p_assn :: ‹'p ⇒ 'xp:: llvm_rep ⇒ 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
    p_default :: 'p and
    p :: ‹'xp llM›
begin

definition isasat_assn :: ‹_ ⇒ _ ⇒ assn› where
‹isasat_assn = tuple16_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 p_assn›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


end

lemma tuple16_assn_conv[simp]:
  "tuple16_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16 (Tuple16 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)
  (Tuple16 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' a16') =
  (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' ∧* P16 a16 a16')"
  unfolding tuple16_assn.simps by auto
lemma tuple16_assn_ctxt:
  ‹tuple16_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16 (Tuple16 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)
  (Tuple16 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' a16') = z ⟹
  hn_ctxt (tuple16_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16) (Tuple16 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)
  (Tuple16 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' a16')= z›
  by (simp add: hn_ctxt_def)

lemma hn_case_tuple16'[sepref_comb_rules]:
  assumes FR: ‹Γ ⊢ hn_ctxt (tuple16_assn P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 P12 P13 P14 P15 P16) 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' a16'.
        ⟦p'=Tuple16 a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' a16'⟧
    ⟹ 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 ∧* hn_ctxt P16 a16' a16 ∧* Γ1)
          (f a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)
          (Γ2 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' a16') R
          (CP a1 a2  a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)
         (f' a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12' a13' a14' a15' a16')"
  assumes FR2: ‹⋀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' a16'.
       Γ2 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' a16' ⊢
       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 ** hn_ctxt P16' a16' a16 ** Γ1'›
  shows ‹hn_refine Γ (case_tuple16 f p) (hn_ctxt (tuple16_assn P1' P2' P3' P4' P5' P6' P7' P8' P9' P10' P11' P12' P13' P14' P15' P16') p' p ** Γ1')
    R (case_tuple16 CP p) (case_tuple16$(λ⇩2a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16. f' a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16)$p')› (is ‹?G Γ›)
  unfolding autoref_tag_defs PROTECT2_def
  apply1 (rule hn_refine_cons_pre[OF FR])
    apply1 (cases p; cases p'; simp add: tuple16_assn_conv[THEN tuple16_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_tuple16_arity[sepref_monadify_arity]:
  ‹case_tuple16 ≡ λ⇩2fp p. SP case_tuple16$(λ⇩2a b. fp$a$b)$p›
  by (simp_all only: SP_def APP_def PROTECT2_def RCALL_def)

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

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

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

locale tuple16 =
  tuple16_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 p_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
  p_default p
  for
    a_assn :: ‹'a ⇒ 'xa:: llvm_rep ⇒ assn› and
    b_assn :: ‹'b ⇒ 'xb:: llvm_rep ⇒ assn› and
    c_assn :: ‹'c ⇒ 'xc:: llvm_rep ⇒ assn› and
    d_assn :: ‹'d ⇒ 'xd:: llvm_rep ⇒ assn› and
    e_assn :: ‹'e ⇒ 'xe:: llvm_rep ⇒ assn› and
    f_assn :: ‹'f ⇒ 'xf:: llvm_rep ⇒ assn› and
    g_assn :: ‹'g ⇒ 'xg:: llvm_rep ⇒ assn› and
    h_assn :: ‹'h ⇒ 'xh:: llvm_rep ⇒ assn› and
    i_assn :: ‹'i ⇒ 'xi:: llvm_rep ⇒ assn› and
    j_assn :: ‹'j ⇒ 'xj:: llvm_rep ⇒ assn› and
    k_assn :: ‹'k ⇒ 'xk:: llvm_rep ⇒ assn› and
    l_assn :: ‹'l ⇒ 'xl:: llvm_rep ⇒ assn› and
    m_assn :: ‹'m ⇒ 'xm:: llvm_rep ⇒ assn› and
    n_assn :: ‹'n ⇒ 'xn:: llvm_rep ⇒ assn› and
    o_assn :: ‹'o ⇒ 'xo:: llvm_rep ⇒ assn› and
    p_assn :: ‹'p ⇒ 'xp:: llvm_rep ⇒ 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
    p_default :: 'p and
    p :: ‹'xp 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› and
    p_free :: ‹'xp ⇒ 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
    p: ‹(uncurry0 p, uncurry0 (RETURN p_default)) ∈ unit_assn⇧k →⇩a p_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›and
    p_free: ‹MK_FREE p_assn p_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_tuple16'[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 p_assn,
  unfolded isasat_assn_def[symmetric]]

lemma ex_tuple16_iff: "(∃b :: (_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)tuple16. P b) ⟷
  (∃a b  c d e f g h i j k l m n ko p. P (Tuple16 a b  c d e f g h i j k l m n ko p))"
  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 p_free
sepref_register
  ‹Tuple16›
lemma [sepref_fr_rules]: ‹(uncurry15 (Mreturn o⇩1⇩6 Tuple16), uncurry15 (RETURN o⇩1⇩6 Tuple16))
  ∈ 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 p_assn⇧d
  →⇩a isasat_assn›
  unfolding isasat_assn_def
  apply sepref_to_hoare
  apply vcg
  unfolding ex_tuple16_iff
  apply vcg'
  done

lemma [sepref_frame_match_rules]:
  ‹ hn_ctxt
     (tuple16_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) (invalid_assn p_assn)) ax bx ⊢ hn_val UNIV ax bx›
    unfolding hn_ctxt_def invalid_assn_def isasat_assn_def entails_def
    apply (auto split: prod.split tuple16.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_tuple16_inverse: ‹RETURN
      (let _ = M
         in ff) =
      (do {_ ← mop_free M;
         RETURN (ff)})›
    by (auto intro!: ext simp: mop_free_def split: tuple16.splits)

sepref_def update_a_code
  is ‹uncurry (RETURN oo update_a)›
  :: ‹a_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=5]]
  unfolding update_a_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_b_code
  is ‹uncurry (RETURN oo update_b)›
  :: ‹b_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_b_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_c_code
  is ‹uncurry (RETURN oo update_c)›
  :: ‹c_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_c_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_d_code
  is ‹uncurry (RETURN oo update_d)›
  :: ‹d_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_d_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_e_code
  is ‹uncurry (RETURN oo update_e)›
  :: ‹e_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_e_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_f_code
  is ‹uncurry (RETURN oo update_f)›
  :: ‹f_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_f_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_g_code
  is ‹uncurry (RETURN oo update_g)›
  :: ‹g_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_g_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_h_code
  is ‹uncurry (RETURN oo update_h)›
  :: ‹h_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_h_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_i_code
  is ‹uncurry (RETURN oo update_i)›
  :: ‹i_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_i_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_j_code
  is ‹uncurry (RETURN oo update_j)›
  :: ‹j_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_j_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_k_code
  is ‹uncurry (RETURN oo update_k)›
  :: ‹k_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_k_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_l_code
  is ‹uncurry (RETURN oo update_l)›
  :: ‹l_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_l_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_m_code
  is ‹uncurry (RETURN oo update_m)›
  :: ‹m_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_m_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_n_code
  is ‹uncurry (RETURN oo update_n)›
  :: ‹n_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_n_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_o_code
  is ‹uncurry (RETURN oo update_o)›
  :: ‹o_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_o_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

sepref_def update_p_code
  is ‹uncurry (RETURN oo update_p)›
  :: ‹p_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_p_def tuple16.case_distrib comp_def RETURN_case_tuple16_inverse
  by sepref

method stuff_pre =
    sepref_to_hoare;
    case_tac x;
    vcg;
    unfold wpa_return;
    subst (asm)(2) sep_algebra_class.sep_conj_empty'[symmetric];
    rule apply_htriple_rule

method stuff_post1 =
    rule POSTCONDI;
    rule STATE_monoI

method stuff_post2 =
    unfold ex_tuple16_iff entails_def;
    auto simp: Exists_eq_simp ex_tuple16_iff  entails_def entails_eq_iff pure_true_conv sep_conj_left_commute;
    smt (z3) entails_def entails_eq_iff pure_true_conv sep_conj_aci(4) sep_conj_aci(5) sep_conj_left_commute

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

sepref_definition remove_p_code
  is ‹RETURN o remove_p›
  :: ‹ isasat_assn⇧d →⇩a p_assn ×⇩a isasat_assn›
  unfolding remove_p_def RETURN_case_tuple16_invers
  by sepref


lemma remove_a_code_alt_def: ‹remove_a_code xi = do⇩M {
              M ← ll_extract_value xi 0;
              x ← a;
              x ← ll_insert_value xi x 0;
              return⇩M (M, x)
  }› and
  remove_b_code_alt_def: ‹remove_b_code xi = do⇩M {
              M ← ll_extract_value xi 1;
              x ← b;
              x ← ll_insert_value xi x 1;
              return⇩M (M, x)
  }›and
  remove_c_code_alt_def: ‹remove_c_code xi = do⇩M {
              M ← ll_extract_value xi 2;
              x ← c;
              x ← ll_insert_value xi x 2;
              return⇩M (M, x)
  }›and
  remove_d_code_alt_def: ‹remove_d_code xi = do⇩M {
              M ← ll_extract_value xi 3;
              x ← d;
              x ← ll_insert_value xi x 3;
              return⇩M (M, x)
  }›and
  remove_e_code_alt_def: ‹remove_e_code xi = do⇩M {
              M ← ll_extract_value xi 4;
              x ← e;
              x ← ll_insert_value xi x 4;
              return⇩M (M, x)
  }›and
  remove_f_code_alt_def: ‹remove_f_code xi = do⇩M {
              M ← ll_extract_value xi 5;
              x ← f;
              x ← ll_insert_value xi x 5;
              return⇩M (M, x)
  }›and
  remove_g_code_alt_def: ‹remove_g_code xi = do⇩M {
              M ← ll_extract_value xi 6;
              x ← g;
              x ← ll_insert_value xi x 6;
              return⇩M (M, x)
  }›and
  remove_h_code_alt_def: ‹remove_h_code xi = do⇩M {
              M ← ll_extract_value xi 7;
              x ← h;
              x ← ll_insert_value xi x 7;
              return⇩M (M, x)
  }›and
  remove_i_code_alt_def: ‹remove_i_code xi = do⇩M {
              M ← ll_extract_value xi 8;
              x ← i;
              x ← ll_insert_value xi x 8;
              return⇩M (M, x)
  }›and
  remove_j_code_alt_def: ‹remove_j_code xi = do⇩M {
              M ← ll_extract_value xi 9;
              x ← j;
              x ← ll_insert_value xi x 9;
              return⇩M (M, x)
  }›and
  remove_k_code_alt_def: ‹remove_k_code xi = do⇩M {
              M ← ll_extract_value xi 10;
              x ← k;
              x ← ll_insert_value xi x 10;
              return⇩M (M, x)
  }›and
  remove_l_code_alt_def: ‹remove_l_code xi = do⇩M {
              M ← ll_extract_value xi 11;
              x ← l;
              x ← ll_insert_value xi x 11;
              return⇩M (M, x)
  }›and
  remove_m_code_alt_def: ‹remove_m_code xi = do⇩M {
              M ← ll_extract_value xi 12;
              x ← m;
              x ← ll_insert_value xi x 12;
              return⇩M (M, x)
  }›and
  remove_n_code_alt_def: ‹remove_n_code xi = do⇩M {
              M ← ll_extract_value xi 13;
              x ← n;
              x ← ll_insert_value xi x 13;
              return⇩M (M, x)
  }›and
  remove_o_code_alt_def: ‹remove_o_code xi = do⇩M {
              M ← ll_extract_value xi 14;
              x ← ko;
              x ← ll_insert_value xi x 14;
              return⇩M (M, x)
  }›and
  remove_p_code_alt_def: ‹remove_p_code xi = do⇩M {
              M ← ll_extract_value xi 15;
              x ← p;
              x ← ll_insert_value xi x 15;
              return⇩M (M, x)
  }›
  supply [simp] = llvm_extract_value_def
    ll_extract_value_def to_val_tuple16_def
    checked_from_val_def ll_insert_value_def
    llvm_insert_value_def
  unfolding remove_a_code_def remove_b_code_def inline_direct_return_node_case
    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 remove_p_code_def
  by (solves ‹cases xi, rewrite in ‹Mreturn (_, ⌑)› llvm_rep_class.from_to_id'[symmetric],
    simp flip: from_val_tuple16_def›)+

lemma update_a_code_alt_def: ‹⋀x. update_a_code x xi = do⇩M {
              M ← ll_extract_value xi 0; a_free M;
              x ← ll_insert_value xi x 0;
              return⇩M (x)
  }› and
  update_b_code_alt_def: ‹⋀x. update_b_code x xi = do⇩M {
              M ← ll_extract_value xi 1; b_free M;
              x ← ll_insert_value xi x 1;
              return⇩M (x)
  }›and
  update_c_code_alt_def: ‹⋀x. update_c_code x xi = do⇩M {
              M ← ll_extract_value xi 2; c_free M;
              x ← ll_insert_value xi x 2;
              return⇩M (x)
  }›and
  update_d_code_alt_def: ‹⋀x. update_d_code x xi = do⇩M {
              M ← ll_extract_value xi 3; d_free M;
              x ← ll_insert_value xi x 3;
              return⇩M (x)
  }›and
  update_e_code_alt_def: ‹⋀x. update_e_code x xi = do⇩M {
              M ← ll_extract_value xi 4; e_free M;
              x ← ll_insert_value xi x 4;
              return⇩M (x)
  }›and
  update_f_code_alt_def: ‹⋀x. update_f_code x xi = do⇩M {
              M ← ll_extract_value xi 5; f_free M;
              x ← ll_insert_value xi x 5;
              return⇩M (x)
  }›and
  update_g_code_alt_def: ‹⋀x. update_g_code x xi = do⇩M {
              M ← ll_extract_value xi 6; g_free M;
              x ← ll_insert_value xi x 6;
              return⇩M (x)
  }›and
  update_h_code_alt_def: ‹⋀x. update_h_code x xi = do⇩M {
              M ← ll_extract_value xi 7; h_free M;
              x ← ll_insert_value xi x 7;
              return⇩M (x)
  }›and
  update_i_code_alt_def: ‹⋀x. update_i_code x xi = do⇩M {
              M ← ll_extract_value xi 8; i_free M;
              x ← ll_insert_value xi x 8;
              return⇩M (x)
  }›and
  update_j_code_alt_def: ‹⋀x. update_j_code x xi = do⇩M {
              M ← ll_extract_value xi 9; j_free M;
              x ← ll_insert_value xi x 9;
              return⇩M (x)
  }›and
  update_k_code_alt_def: ‹⋀x. update_k_code x xi = do⇩M {
              M ← ll_extract_value xi 10; k_free M;
              x ← ll_insert_value xi x 10;
              return⇩M (x)
  }›and
  update_l_code_alt_def: ‹⋀x. update_l_code x xi = do⇩M {
              M ← ll_extract_value xi 11; l_free M;
              x ← ll_insert_value xi x 11;
              return⇩M (x)
  }›and
  update_m_code_alt_def: ‹⋀x. update_m_code x xi = do⇩M {
              M ← ll_extract_value xi 12; m_free M;
              x ← ll_insert_value xi x 12;
              return⇩M (x)
  }›and
  update_n_code_alt_def: ‹⋀x. update_n_code x xi = do⇩M {
              M ← ll_extract_value xi 13; n_free M;
              x ← ll_insert_value xi x 13;
              return⇩M (x)
  }›and
  update_o_code_alt_def: ‹⋀x. update_o_code x xi = do⇩M {
              M ← ll_extract_value xi 14; o_free M;
              x ← ll_insert_value xi x 14;
              return⇩M (x)
  }›and
  update_p_code_alt_def: ‹⋀x. update_p_code x xi = do⇩M {
              M ← ll_extract_value xi 15; p_free M;
              x ← ll_insert_value xi x 15;
              return⇩M (x)
  }›
  supply [simp] = llvm_extract_value_def
    ll_extract_value_def to_val_tuple16_def
    checked_from_val_def ll_insert_value_def
    llvm_insert_value_def
  unfolding update_a_code_def update_b_code_def inline_direct_return_node_case
    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 update_p_code_def comp_def
  by (solves ‹cases xi, rewrite in ‹Mreturn (⌑)› llvm_rep_class.from_to_id'[symmetric],
    simp flip: from_val_tuple16_def›)+

lemma tuple15_free[sepref_frame_free_rules]:
  shows
  ‹MK_FREE (tuple16_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 p_assn) (λS. case S of Tuple16 a b c d e f g h i j k l m n ko p ⇒ do⇩M {
  a_free a; b_free b; c_free c; d_free d; e_free e; f_free f; g_free g; h_free h; i_free i; j_free j;
  k_free k; l_free l; m_free m; n_free n; o_free ko; p_free p
  })›
  supply [vcg_rules] = a_free[THEN MK_FREED] b_free[THEN MK_FREED] c_free[THEN MK_FREED] d_free[THEN MK_FREED]
    e_free[THEN MK_FREED] f_free[THEN MK_FREED] g_free[THEN MK_FREED] h_free[THEN MK_FREED]
    i_free[THEN MK_FREED] j_free[THEN MK_FREED] k_free[THEN MK_FREED] l_free[THEN MK_FREED]
    m_free[THEN MK_FREED] n_free[THEN MK_FREED]  o_free[THEN MK_FREED] p_free[THEN MK_FREED]
  apply (rule)+
  apply (clarsimp split: tuple16.splits)
  by vcg'

end


context tuple16
begin
lemma reconstruct_isasat[sepref_frame_match_rules]:
  ‹hn_ctxt
     (tuple16_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) (p_assn)) ax bx ⊢ hn_ctxt isasat_assn ax bx›
    unfolding isasat_assn_def
    apply (auto split: prod.split tuple16.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 ⇒ 'xp ⇒ 'q llM› and
    read_all :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'g ⇒ 'h ⇒ 'i ⇒ 'j ⇒ 'k ⇒ 'l ⇒ 'm ⇒ 'n ⇒ 'o ⇒ 'p ⇒ 'r nres›
begin

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

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

context
  fixes P
  assumes trail_read[sepref_fr_rules]: ‹(uncurry15 read_all_code, uncurry15 read_all) ∈
      [uncurry15 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 *⇩a p_assn⇧k  → x_assn›
  notes [[sepref_register_adhoc read_all]]
begin
sepref_definition read_all_code_tmp
  is read_all_st
  :: ‹[case_tuple16 P]⇩a isasat_assn⇧k → x_assn›
   unfolding read_all_st_def
   by sepref

lemmas read_all_code_refine =
  read_all_code_tmp.refine[unfolded read_all_code_tmp_def
    read_all_st_code_def[symmetric]]
end

end

lemmas [unfolded Let_def, tuple16_getters_setters] =
  update_a_def
  update_b_def
  update_c_def
  update_d_def
  update_e_def
  update_f_def
  update_g_def
  update_h_def
  update_i_def
  update_j_def
  update_k_def
  update_l_def
  update_m_def
  update_n_def
  update_o_def
  update_p_def

  remove_a_def
  remove_b_def
  remove_c_def
  remove_d_def
  remove_e_def
  remove_f_def
  remove_g_def
  remove_h_def
  remove_i_def
  remove_j_def
  remove_k_def
  remove_l_def
  remove_m_def
  remove_n_def
  remove_o_def
  remove_p_def

end

lemmas [tuple16_getters_setters] =
  tuple16_ops.remove_a_def
  tuple16_ops.remove_b_def
  tuple16_ops.remove_c_def
  tuple16_ops.remove_d_def
  tuple16_ops.remove_e_def
  tuple16_ops.remove_f_def
  tuple16_ops.remove_g_def
  tuple16_ops.remove_h_def
  tuple16_ops.remove_i_def
  tuple16_ops.remove_j_def
  tuple16_ops.remove_k_def
  tuple16_ops.remove_l_def
  tuple16_ops.remove_m_def
  tuple16_ops.remove_n_def
  tuple16_ops.remove_o_def
  tuple16_ops.remove_p_def

end