Theory Timestamp_Prod

theory Timestamp_Prod
  imports Timestamp
begin

instantiation prod :: (timestamp, timestamp) timestamp
begin

definition tfin_prod :: "('a × 'b) set" where
  "tfin_prod = tfin × tfin"

definition ι_prod :: "nat ⇒ 'a × 'b" where
  "ι_prod n = (ι n, ι n)"

fun sup_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
  "sup_prod (a, b) (c, d) = (sup a c, sup b d)"

fun less_eq_prod :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
  "less_eq_prod (a, b) (c, d) ⟷ a ≤ c ∧ b ≤ d"

definition less_prod :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
  "less_prod x y ⟷ x ≤ y ∧ x ≠ y"

instance
  apply standard
              apply (auto simp: add.commute zero_prod_def less_prod_def)[7]
  subgoal for i j
    using ι_mono ι_mono less_le
    by (fastforce simp: ι_prod_def less_prod_def)
  subgoal for i
    by (auto simp: ι_prod_def tfin_prod_def intro: ι_tfin)
  subgoal for x i
    apply (cases x)
    using ι_progressing
    by (auto simp: tfin_prod_def ι_prod_def)
  apply (auto simp: zero_prod_def tfin_prod_def intro: zero_tfin)[1]
  subgoal for c d
    by (cases c; cases d) (auto simp: tfin_prod_def intro: tfin_closed)
  subgoal for c d a
    by (cases c; cases d; cases a) (auto simp add: add_mono)
  subgoal for a c
    apply (cases a; cases c)
    apply (auto simp: tfin_prod_def zero_prod_def)
    apply (metis add.right_neutral add_pos less_eq_prod.simps less_prod_def order_less_le prod.inject timestamp_class.add_mono)
    done
  done

end

end