Theory Tuple4

theory Tuple4
  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 4 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) tuple4 = Tuple4
  (Tuple4_a: 'a)
  (Tuple4_b: 'b)
  (Tuple4_c: 'c)
  (Tuple4_d: 'd)

context
begin

qualified fun set_a :: ‹'a ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ _› where
  ‹set_a M (Tuple4 _ N D i) = (Tuple4 M N D i)›

qualified fun set_b :: ‹'b ⇒ _ ⇒ ('a, 'b, 'c, 'd) tuple4› where
  ‹set_b N (Tuple4 M _ D i) = (Tuple4 M N D i)›

qualified fun set_c :: ‹'c ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where
  ‹set_c D (Tuple4 M N _ i) = (Tuple4 M N D i)›

qualified fun set_d :: ‹'d ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where
  ‹set_d i (Tuple4 M N D _) = (Tuple4 M N D i)›

end

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

named_theorems Tuple4_state_simp ‹Simplify the state setter and extractors›
lemma [Tuple4_state_simp]:
  ‹Tuple4_a (Tuple4.set_a a S) = a›
  ‹Tuple4_b (Tuple4.set_a b S) = Tuple4_b S›
  ‹Tuple4_c (Tuple4.set_a b S) = Tuple4_c S›
  ‹Tuple4_d (Tuple4.set_a b S) = Tuple4_d S›
  by (cases S; auto; fail)+

lemma [Tuple4_state_simp]:
  ‹Tuple4_a (Tuple4.set_b b S) = Tuple4_a S›
  ‹Tuple4_b (Tuple4.set_b b S) = b›
  ‹Tuple4_c (Tuple4.set_b b S) = Tuple4_c S›
  ‹Tuple4_d (Tuple4.set_b b S) = Tuple4_d S›
  by (cases S; auto; fail)+

lemma [Tuple4_state_simp]:
  ‹Tuple4_a (Tuple4.set_c b S) = Tuple4_a S›
  ‹Tuple4_b (Tuple4.set_c b S) = Tuple4_b S›
  ‹Tuple4_c (Tuple4.set_c b S) = b›
  ‹Tuple4_d (Tuple4.set_c b S) = Tuple4_d S›
  by (cases S; auto; fail)+

lemma [Tuple4_state_simp]:
  ‹Tuple4_a (Tuple4.set_d b S) = Tuple4_a S›
  ‹Tuple4_b (Tuple4.set_d b S) = Tuple4_b S›
  ‹Tuple4_c (Tuple4.set_d b S) = Tuple4_c S›
  ‹Tuple4_d (Tuple4.set_d b S) = b›
  by (cases S; auto; fail)+

declare Tuple4_state_simp[simp]
end