Theory Tuple15

theory Tuple15
  imports
    More_Sepref.WB_More_Refinement IsaSAT_Literals
begin

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


We define 3 sort of operations:

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

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

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

›

datatype ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 = Tuple15
  (Tuple15_a: 'a)
  (Tuple15_b: 'b)
  (Tuple15_c: 'c)
  (Tuple15_d: 'd)
  (Tuple15_e: 'e)
  (Tuple15_f: 'f)
  (Tuple15_g: 'g)
  (Tuple15_h: 'h)
  (Tuple15_i: 'i)
  (Tuple15_j: 'j)
  (Tuple15_k: 'k)
  (Tuple15_l: 'l)
  (Tuple15_m: 'm)
  (Tuple15_n: 'n)
  (Tuple15_o: 'o)

context
begin

qualified fun set_a :: ‹'a ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ _› where
  ‹set_a M (Tuple15 _ N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_b :: ‹'b ⇒ _ ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_b N (Tuple15 M _ D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_c :: ‹'c ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_c D (Tuple15 M N _ i W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_d :: ‹'d ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_d i (Tuple15 M N D _ W ivmtf icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_e :: ‹'e ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_e W (Tuple15 M N D i _ ivmtf icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_f :: ‹'f ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_f ivmtf (Tuple15 M N D i W _ icount ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_g :: ‹'g ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_g icount (Tuple15 M N D i W ivmtf _ ccach lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_h :: ‹'h ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_h ccach (Tuple15 M N D i W ivmtf icount _ lbd outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_i :: ‹'i ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_i lbd (Tuple15 M N D i W ivmtf icount ccach _ outl heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_j :: ‹'j ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_j outl (Tuple15 M N D i W ivmtf icount ccach lbd _ heur stats aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_l :: ‹'l ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_l heur (Tuple15 M N D i W ivmtf icount ccach lbd outl stats _ aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts)›

qualified fun set_k :: ‹'k ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_k stats (Tuple15 M N D i W ivmtf icount ccach lbd outl _ heur aivdom clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts)›

qualified fun set_m :: ‹'m ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_m aivdom (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats _ clss opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_n :: ‹'n ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_n clss (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom _ opts) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

qualified fun set_o :: ‹'o ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15 ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o) tuple15› where
  ‹set_o opts (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss _) = (Tuple15 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts)›

end

lemma lambda_comp_true: ‹(λS. True) ∘ f = (λ_. True)› ‹uncurry (λa b. True) = (λ_. True)›  ‹uncurry2 (λa b c. True) = (λ_. True)›
  ‹case_tuple15 (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. True) = (λ_. True)›
  by (auto intro!: ext split: Tuple15.tuple15.splits)

named_theorems Tuple15_state_simp ‹Simplify the state setter and extractors›
lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_a a S) = a›
  ‹Tuple15_b (Tuple15.set_a b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_a b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_a b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_a b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_a b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_a b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_a b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_a b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_a b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_a b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_a b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_a b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_a b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_a b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_b b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_b b S) = b›
  ‹Tuple15_c (Tuple15.set_b b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_b b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_b b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_b b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_b b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_b b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_b b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_b b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_b b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_b b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_b b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_b b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_b b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_c b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_c b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_c b S) = b›
  ‹Tuple15_d (Tuple15.set_c b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_c b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_c b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_c b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_c b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_c b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_c b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_c b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_c b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_c b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_c b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_c b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_d b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_d b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_d b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_d b S) = b›
  ‹Tuple15_e (Tuple15.set_d b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_d b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_d b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_d b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_d b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_d b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_d b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_d b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_d b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_d b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_d b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_e b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_e b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_e b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_e b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_e b S) = b›
  ‹Tuple15_f (Tuple15.set_e b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_e b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_e b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_e b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_e b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_e b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_e b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_e b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_e b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_e b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_f b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_f b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_f b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_f b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_f b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_f b S) = b›
  ‹Tuple15_g (Tuple15.set_f b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_f b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_f b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_f b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_f b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_f b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_f b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_f b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_f b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_g b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_g b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_g b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_g b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_g b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_g b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_g b S) = b›
  ‹Tuple15_h (Tuple15.set_g b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_g b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_g b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_g b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_g b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_g b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_g b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_g b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_h b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_h b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_h b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_h b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_h b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_h b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_h b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_h b S) = b›
  ‹Tuple15_i (Tuple15.set_h b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_h b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_h b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_h b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_h b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_h b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_h b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_i b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_i b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_i b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_i b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_i b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_i b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_i b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_i b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_i b S) = b›
  ‹Tuple15_j (Tuple15.set_i b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_i b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_i b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_i b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_i b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_i b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_j b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_j b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_j b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_j b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_j b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_j b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_j b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_j b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_j b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_j b S) = b›
  ‹Tuple15_k (Tuple15.set_j b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_j b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_j b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_j b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_j b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_k b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_k b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_k b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_k b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_k b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_k b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_k b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_k b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_k b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_k b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_k b S) = b›
  ‹Tuple15_l (Tuple15.set_k b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_k b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_k b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_k b S) = Tuple15_o S›
  by (cases S; auto; fail)+
 
lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_l b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_l b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_l b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_l b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_l b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_l b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_l b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_l b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_l b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_l b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_l b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_l b S) = b›
  ‹Tuple15_m (Tuple15.set_l b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_l b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_l b S) = Tuple15_o S›
  by (cases S; auto; fail)+


lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_m b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_m b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_m b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_m b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_m b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_m b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_m b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_m b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_m b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_m b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_m b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_m b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_m b S) = b›
  ‹Tuple15_n (Tuple15.set_m b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_m b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_n b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_n b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_n b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_n b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_n b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_n b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_n b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_n b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_n b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_n b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_n b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_n b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_n b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_n b S) = b›
  ‹Tuple15_o (Tuple15.set_n b S) = Tuple15_o S›
  by (cases S; auto; fail)+

lemma [Tuple15_state_simp]:
  ‹Tuple15_a (Tuple15.set_o b S) = Tuple15_a S›
  ‹Tuple15_b (Tuple15.set_o b S) = Tuple15_b S›
  ‹Tuple15_c (Tuple15.set_o b S) = Tuple15_c S›
  ‹Tuple15_d (Tuple15.set_o b S) = Tuple15_d S›
  ‹Tuple15_e (Tuple15.set_o b S) = Tuple15_e S›
  ‹Tuple15_f (Tuple15.set_o b S) = Tuple15_f S›
  ‹Tuple15_g (Tuple15.set_o b S) = Tuple15_g S›
  ‹Tuple15_h (Tuple15.set_o b S) = Tuple15_h S›
  ‹Tuple15_i (Tuple15.set_o b S) = Tuple15_i S›
  ‹Tuple15_j (Tuple15.set_o b S) = Tuple15_j S›
  ‹Tuple15_k (Tuple15.set_o b S) = Tuple15_k S›
  ‹Tuple15_l (Tuple15.set_o b S) = Tuple15_l S›
  ‹Tuple15_m (Tuple15.set_o b S) = Tuple15_m S›
  ‹Tuple15_n (Tuple15.set_o b S) = Tuple15_n S›
  ‹Tuple15_o (Tuple15.set_o b S) = b›
  by (cases S; auto; fail)+

declare Tuple15_state_simp[simp]
end