Theory Data_Tuple

section ‹Data: Tuple›

theory Data_Tuple
  imports
    Type_Classes
    Data_Bool
begin

subsection ‹Datatype definitions›

domain Unit ("⟨⟩") = Unit ("⟨⟩")

domain ('a, 'b) Tuple2 ("⟨_, _⟩") =
  Tuple2 (lazy fst :: "'a") (lazy snd :: "'b") ("⟨_, _⟩")

notation Tuple2 ("⟨,⟩")

fixrec uncurry :: "('a → 'b → 'c) → ⟨'a, 'b⟩ → 'c"
  where "uncurry⋅f⋅p = f⋅(fst⋅p)⋅(snd⋅p)"

fixrec curry :: "(⟨'a, 'b⟩  → 'c) → 'a → 'b → 'c"
  where "curry⋅f⋅a⋅b = f⋅⟨a, b⟩"

domain ('a, 'b, 'c) Tuple3 ("⟨_, _, _⟩") =
  Tuple3 (lazy "'a") (lazy "'b") (lazy "'c") ("⟨_, _, _⟩")

notation Tuple3 ("⟨,,⟩")

subsection ‹Type class instances›

instantiation Unit :: Ord_linear
begin

definition
  "eq = (Λ ⟨⟩ ⟨⟩. TT)"

definition
  "compare = (Λ ⟨⟩ ⟨⟩. EQ)"

instance
  apply standard
        apply (unfold eq_Unit_def compare_Unit_def)
        apply simp
       apply (rename_tac x, case_tac x, simp, simp)
      apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
     apply (rename_tac x y, case_tac x, case_tac y, simp, simp, case_tac y, simp, simp)
    apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
   apply (rename_tac x, case_tac x, simp, simp)
  apply (rename_tac x y z, case_tac x, simp, case_tac y, simp, case_tac z, simp, simp)
  done

end

instantiation Tuple2 :: (Eq, Eq) Eq_strict
begin

definition
  "eq = (Λ ⟨x1, y1⟩ ⟨x2, y2⟩. eq⋅x1⋅x2 andalso eq⋅y1⋅y2)"

instance proof
  fix x :: "⟨'a, 'b⟩"
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_Tuple2_def by (cases x, simp_all)
  show "eq⋅⊥⋅x = ⊥"
    unfolding eq_Tuple2_def by simp
qed

end

lemma eq_Tuple2_simps [simp]:
  "eq⋅⟨x1, y1⟩⋅⟨x2, y2⟩ = (eq⋅x1⋅x2 andalso eq⋅y1⋅y2)"
  unfolding eq_Tuple2_def by simp

instance Tuple2 :: (Eq_sym, Eq_sym) Eq_sym
proof
  fix x y :: "⟨'a, 'b⟩"
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_Tuple2_def
    by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
qed

instance Tuple2 :: (Eq_equiv, Eq_equiv) Eq_equiv
proof
  fix x y z :: "⟨'a, 'b⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  show "eq⋅x⋅z = TT" if "eq⋅x⋅y = TT" and "eq⋅y⋅z = TT"
    using that
    by (cases x, simp, cases y, simp, cases z, simp, simp,
        fast intro: eq_trans)
qed

instance Tuple2 :: (Eq_eq, Eq_eq) Eq_eq
proof
  fix x y :: "⟨'a, 'b⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  show "x = y" if "eq⋅x⋅y = TT"
    using that by (cases x, simp, cases y, simp, simp, fast)
qed

instantiation Tuple2 :: (Ord, Ord) Ord_strict
begin

definition
  "compare = (Λ ⟨x1, y1⟩ ⟨x2, y2⟩.
    thenOrdering⋅(compare⋅x1⋅x2)⋅(compare⋅y1⋅y2))"

instance
  by standard (simp add: compare_Tuple2_def,
      rename_tac x, case_tac x, simp_all add: compare_Tuple2_def)

end

lemma compare_Tuple2_simps [simp]:
  "compare⋅⟨x1, y1⟩⋅⟨x2, y2⟩ = thenOrdering⋅(compare⋅x1⋅x2)⋅(compare⋅y1⋅y2)"
  unfolding compare_Tuple2_def by simp

instance Tuple2 :: (Ord_linear, Ord_linear) Ord_linear
proof
  fix x y z :: "⟨'a, 'b⟩"
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
  show "x = y" if "compare⋅x⋅y = EQ"
    using that by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest)
  show "compare⋅x⋅z = LT" if "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT"
    using that
    apply (cases x, simp, cases y, simp, cases z, simp, simp)
    apply (elim disjE conjE)
       apply (fast elim!: compare_LT_trans)
      apply (fast dest: compare_EQ_dest)
     apply (fast dest: compare_EQ_dest)
    apply (drule compare_EQ_dest)
    apply (fast elim!: compare_LT_trans)
    done
  show "compare⋅x⋅x ⊑ EQ"
    by (cases x, simp_all)
qed

instantiation Tuple3 :: (Eq, Eq, Eq) Eq_strict
begin

definition
  "eq = (Λ ⟨x1, y1, z1⟩ ⟨x2, y2, z2⟩.
    eq⋅x1⋅x2 andalso eq⋅y1⋅y2 andalso eq⋅z1⋅z2)"

instance proof
  fix x :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_Tuple3_def by (cases x, simp_all)
  show "eq⋅⊥⋅x = ⊥"
    unfolding eq_Tuple3_def by simp
qed

end

lemma eq_Tuple3_simps [simp]:
  "eq⋅⟨x1, y1, z1⟩⋅⟨x2, y2, z2⟩ = (eq⋅x1⋅x2 andalso eq⋅y1⋅y2 andalso eq⋅z1⋅z2)"
  unfolding eq_Tuple3_def by simp

instance Tuple3 :: (Eq_sym, Eq_sym, Eq_sym) Eq_sym
proof
  fix x y :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_Tuple3_def
    by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
qed

instance Tuple3 :: (Eq_equiv, Eq_equiv, Eq_equiv) Eq_equiv
proof
  fix x y z :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  show "eq⋅x⋅z = TT" if "eq⋅x⋅y = TT" and "eq⋅y⋅z = TT"
    using that
    by (cases x, simp, cases y, simp, cases z, simp, simp,
        fast intro: eq_trans)
qed

instance Tuple3 :: (Eq_eq, Eq_eq, Eq_eq) Eq_eq
proof
  fix x y :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  show "x = y" if "eq⋅x⋅y = TT"
    using that by (cases x, simp, cases y, simp, simp, fast)
qed

instantiation Tuple3 :: (Ord, Ord, Ord) Ord_strict
begin

definition
  "compare = (Λ ⟨x1, y1, z1⟩ ⟨x2, y2, z2⟩.
    thenOrdering⋅(compare⋅x1⋅x2)⋅(thenOrdering⋅(compare⋅y1⋅y2)⋅(compare⋅z1⋅z2)))"

instance
  by standard (simp add: compare_Tuple3_def,
    rename_tac x, case_tac x, simp_all add: compare_Tuple3_def)

end

lemma compare_Tuple3_simps [simp]:
  "compare⋅⟨x1, y1, z1⟩⋅⟨x2, y2, z2⟩ =
    thenOrdering⋅(compare⋅x1⋅x2)⋅
      (thenOrdering⋅(compare⋅y1⋅y2)⋅(compare⋅z1⋅z2))"
  unfolding compare_Tuple3_def by simp

instance Tuple3 :: (Ord_linear, Ord_linear, Ord_linear) Ord_linear
proof
  fix x y z :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
  show "x = y" if "compare⋅x⋅y = EQ"
    using that by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest)
  show "compare⋅x⋅z = LT" if "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT"
    using that
    apply (cases x, simp, cases y, simp, cases z, simp, simp)
    apply (elim disjE conjE)
            apply (fast elim!: compare_LT_trans)
           apply (fast dest: compare_EQ_dest)
          apply (fast dest: compare_EQ_dest)
         apply (fast dest: compare_EQ_dest)
        apply (fast dest: compare_EQ_dest)
       apply (drule compare_EQ_dest)
       apply (fast elim!: compare_LT_trans)
      apply (fast dest: compare_EQ_dest)
     apply (fast dest: compare_EQ_dest)
    apply (fast dest: compare_EQ_dest elim!: compare_LT_trans)
    done
  show "compare⋅x⋅x ⊑ EQ"
    by (cases x, simp_all)
qed

end