# 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