# Theory Timestamp_Lex

```theory Timestamp_Lex
imports Timestamp
begin

instantiation prod :: (timestamp_total_strict, timestamp_total_strict) timestamp_total_strict
begin

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

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) = (if a < c then (c, d) else if c < a then (a, b) else (a, sup b d))"

fun less_eq_prod :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
"less_eq_prod (a, b) (c, d) ⟷ a < c ∨ (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: zero_prod_def less_prod_def)[2]
subgoal for x y z
using order.strict_trans
by (cases x; cases y; cases z) auto
subgoal for x y
by (cases x; cases y) auto
subgoal for x y
by (cases x; cases y) (auto simp add: sup.commute sup.strict_order_iff)
subgoal for x y
apply (cases x; cases y)
apply (auto simp add: sup.commute sup.strict_order_iff)
apply (metis sup.absorb_iff2 sup.order_iff timestamp_total)
done
subgoal for y x z
by (cases x; cases y; cases z) auto
subgoal for i j
using ι_mono less_le
apply (auto 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)
apply (auto simp: ι_prod_def tfin_prod_def)
apply (metis ι_progressing dual_order.refl order_less_le)
done
apply (auto simp: tfin_prod_def tfin_closed)[1]
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
subgoal for a c
apply (cases a; cases c)
apply (auto simp: tfin_prod_def zero_prod_def)
done
subgoal for c d a
apply (cases c; cases d; cases a)
subgoal for a b
apply (cases a; cases b)
apply (auto)
apply (metis antisym_conv1 timestamp_total)
apply (metis antisym_conv1 timestamp_total)
apply (metis antisym_conv1 timestamp_total)
apply (metis timestamp_total)
done
subgoal for a b
apply (cases a; cases b)
apply (auto simp: zero_prod_def tfin_prod_def order_less_le timestamp_tfin_le_not_tfin)
done
done

end

end```