Theory Tuple17_LLVM

theory Tuple17_LLVM
  imports Tuple17 IsaSAT_Literals_LLVM
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN


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

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

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

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

  instance
    apply standard
    unfolding from_val_tuple17_def to_val_tuple17_def struct_of_tuple17_def init_tuple17_def comp_def tuple17.case_distrib
    subgoal
      by (auto simp: init_zero fun_eq_iff from_val_tuple17_def split: tuple17.splits)
    subgoal for v
      by (cases v) (auto split: list.splits tuple17.splits)
    subgoal for v
      by (cases v)
       (simp add: LLVM_Shallow.null_def to_val_ptr_def split: tuple17.splits)
    subgoal
      by (simp add: LLVM_Shallow.null_def to_val_ptr_def to_val_word_def init_zero split: tuple17.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, 'p, 'q) tuple17) = 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),
  struct_of TYPE('q::llvm_rep)]"
  by (auto)

text ‹This is the old version of the declaration:›
lemma "to_val x = LL_STRUCT [
  to_val (Tuple17_get_a x),
  to_val (Tuple17_get_b x),
  to_val (Tuple17_get_c x),
  to_val (Tuple17_get_d x),
  to_val (Tuple17_get_e x),
  to_val (Tuple17_get_f x),
  to_val (Tuple17_get_g x),
  to_val (Tuple17_get_h x),
  to_val (Tuple17_get_i x),
  to_val (Tuple17_get_j x),
  to_val (Tuple17_get_k x),
  to_val (Tuple17_get_l x),
  to_val (Tuple17_get_m x),
  to_val (Tuple17_get_n x),
  to_val (Tuple17_get_o x),
  to_val (Tuple17_get_p x),
  to_val (Tuple17_get_q x)]"
  apply (cases x)
  apply (auto simp: to_val_tuple17_def)
  done

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

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

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

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

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

lemmas [llvm_inline] =
  tuple17.Tuple17_get_a_def
  tuple17.Tuple17_get_b_def
  tuple17.Tuple17_get_c_def
  tuple17.Tuple17_get_d_def
  tuple17.Tuple17_get_e_def
  tuple17.Tuple17_get_f_def
  tuple17.Tuple17_get_g_def
  tuple17.Tuple17_get_h_def
  tuple17.Tuple17_get_i_def
  tuple17.Tuple17_get_j_def
  tuple17.Tuple17_get_l_def
  tuple17.Tuple17_get_k_def
  tuple17.Tuple17_get_m_def
  tuple17.Tuple17_get_n_def
  tuple17.Tuple17_get_o_def
  tuple17.Tuple17_get_p_def
  tuple17.Tuple17_get_q_def

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


locale isasat_state_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
    q_assn :: ‹'q ⇒ 'xq:: 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
    q_default :: 'q and
    q :: ‹'xq llM›
begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


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


end

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

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

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

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

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

locale isasat_state =
  isasat_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 p_assn q_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
  q_default q
  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
    q_assn :: ‹'q ⇒ 'xq:: 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
    q_default :: 'q and
    q :: ‹'xq 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› and
    q_free :: ‹'xq ⇒ 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
    q: ‹(uncurry0 q, uncurry0 (RETURN q_default)) ∈ unit_assn⇧k →⇩a q_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›and
    q_free: ‹MK_FREE q_assn q_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 q_default]]
begin

lemmas [sepref_comb_rules] = hn_case_tuple17'[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 q_assn,
  unfolded isasat_assn_def[symmetric]]

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

lemma [sepref_frame_match_rules]:
  ‹ hn_ctxt
     (tuple17_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) (invalid_assn q_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 tuple17.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_tuple17_inverse: ‹RETURN
      (let _ = M
         in ff) =
      (do {_ ← mop_free M;
         RETURN (ff)})›
    by (auto intro!: ext simp: mop_free_def split: tuple17.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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_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 tuple17.case_distrib comp_def RETURN_case_tuple17_inverse
  by sepref

sepref_def update_q_code
  is ‹uncurry (RETURN oo update_q)›
  :: ‹q_assn⇧d *⇩a isasat_assn⇧d →⇩a isasat_assn›
  supply [[goals_limit=1]]
  unfolding update_q_def tuple17.case_distrib comp_def RETURN_case_tuple17_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_tuple17_iff entails_def;
    auto simp: Exists_eq_simp ex_tuple17_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_tuple17_invers: ‹(RETURN ∘∘ case_tuple17)
   (λx1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17.
  ff x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17) =
  case_tuple17
   (λx1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17.
  RETURN (ff x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17))›
  by (auto intro!: ext split: tuple17.splits)

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

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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_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_tuple17_invers
  by sepref

sepref_definition remove_q_code
  is ‹RETURN o remove_q›
  :: ‹ isasat_assn⇧d →⇩a q_assn ×⇩a isasat_assn›
  unfolding remove_q_def RETURN_case_tuple17_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)
  }›and
  remove_q_code_alt_def: ‹remove_q_code xi = do⇩M {
              M ← ll_extract_value xi 16;
              x ← q;
              x ← ll_insert_value xi x 16;
              return⇩M (M, x)
  }›
  supply [simp] = llvm_extract_value_def
    ll_extract_value_def to_val_tuple17_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 remove_q_code_def
  by (solves ‹cases xi, rewrite in ‹Mreturn (_, ⌑)› llvm_rep_class.from_to_id'[symmetric],
    simp flip: from_val_tuple17_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)
  }›and
  update_q_code_alt_def: ‹⋀x. update_q_code x xi = do⇩M {
              M ← ll_extract_value xi 16; q_free M;
              x ← ll_insert_value xi x 16;
              return⇩M (x)
  }›
  supply [simp] = llvm_extract_value_def
    ll_extract_value_def to_val_tuple17_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 update_q_code_def
    comp_def
  by (solves ‹cases xi, rewrite in ‹Mreturn (⌑)› llvm_rep_class.from_to_id'[symmetric],
    simp flip: from_val_tuple17_def›)+

end


context isasat_state
begin
lemma reconstruct_isasat[sepref_frame_match_rules]:
  ‹hn_ctxt
     (tuple17_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) q_assn) ax bx ⊢ hn_ctxt isasat_assn ax bx›
    unfolding isasat_assn_def
    apply (auto split: prod.split tuple17.splits elim: is_pureE
      simp: sep_algebra_simps pure_part_pure_conj_eq)
      done

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

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

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

context
  fixes P
  assumes trail_read[sepref_fr_rules]: ‹(uncurry16 read_all_code, uncurry16 read_all) ∈
      [uncurry16 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  *⇩a q_assn⇧k  → x_assn›
  notes [[sepref_register_adhoc read_all]]
begin
sepref_definition read_all_code_tmp
  is read_all_st
  :: ‹[case_tuple17 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, tuple17_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
  update_q_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
  remove_q_def

end

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

end