Theory Metric_Point_Structure

```theory Metric_Point_Structure
imports Interval
begin

(* Conversion from the abstract time domain (Definition 4.1) introduced
in the paper ``Specifying Real-Time Properties with Metric Temporal Logic''
(Koymans, 1990) to our time-stamps. *)

(* Metric domain. *)

class metric_domain = plus + zero + ord +
assumes Δ1: "x + x' = x' + x"
and Δ2: "(x + x') + x'' = x + (x' + x'')"
and Δ3: "x + 0 = x"
and Δ3': "x = 0 + x"
and Δ4: "x + x' = x + x'' ⟹ x' = x''"
and Δ4': "x + x'' = x' + x'' ⟹ x = x'"
and Δ5: "x + x' = 0 ⟹ x = 0"
and Δ5': "x + x' = 0 ⟹ x' = 0"
and Δ6: "∃x''. x = x' + x'' ∨ x' = x + x''"
and metric_domain_le_def: "x ≤ x' ⟷ (∃x''. x' = x + x'')"
and metric_domain_lt_def: "x < x' ⟷ (∃x''. x'' ≠ 0 ∧ x' = x + x'')"
begin

lemma metric_domain_pos: "x ≥ 0"
using Δ3' local.metric_domain_le_def by auto

lemma less_eq_le_neq: "x < x' ⟷ (x ≤ x' ∧ x ≠ x')"
apply (auto simp: metric_domain_le_def metric_domain_lt_def)
apply (metis Δ3 Δ4)
apply (metis Δ3)
done

end

(* Metric domain extended with embedding of natural numbers and syntactically extended with sup, tfin. *)

class metric_domain_timestamp = metric_domain + sup + embed_nat + tfin +
assumes metric_domain_sup_def: "sup x x' = (if x ≤ x' then x' else x)"
and metric_domain_ι_mono: "⋀i j. i ≤ j ⟹ ι i ≤ ι j"
and metric_domain_ι_progressing: "∃j. ¬ι j ≤ ι i + x"
and metric_domain_tfin_def: "tfin = UNIV"

subclass (in metric_domain_timestamp) timestamp
apply unfold_locales
apply (auto simp: Δ2)[1]
apply (auto simp: Δ1)[1]
apply (auto simp: Δ3'[symmetric])[1]
subgoal for x y
apply (auto simp: metric_domain_le_def metric_domain_lt_def)
apply (metis Δ2 Δ3 Δ4 Δ5)
apply (metis Δ2 Δ3)
done
using Δ6 apply (auto simp: metric_domain_le_def)[1]
using Δ2 apply (auto simp: metric_domain_le_def)[1]
subgoal for x y
apply (auto simp: metric_domain_le_def metric_domain_lt_def)
apply (metis Δ2 Δ3 Δ4 Δ5)
done
using Δ6 apply (fastforce simp: metric_domain_le_def metric_domain_sup_def)
using Δ6 apply (fastforce simp: metric_domain_le_def metric_domain_sup_def)
apply (auto simp: metric_domain_le_def metric_domain_sup_def)[1]
using metric_domain_ι_mono apply (auto simp: metric_domain_le_def)[1]
apply (auto simp: metric_domain_tfin_def)[1]
using metric_domain_ι_progressing apply (auto simp: metric_domain_le_def)[1]
apply (auto simp: metric_domain_tfin_def)[2]
using Δ2 apply (auto simp: metric_domain_le_def)[1]
using Δ1 Δ3 apply (auto simp: metric_domain_lt_def)
done

(* Metric point structure.
We map Koymans' time-stamps t in a trace to d t0 t, where t0 is the initial time-stamp of the trace.
Because Koymans assumes the strict precedence relation on time-stamps to be
``transitive, irreflexive and comparable'', the precedence relation is actually a partial order. *)

locale metric_point_structure =
fixes d :: "'t :: {order} ⇒ 't ⇒ 'd :: metric_domain_timestamp"
assumes d1: "d t t' = 0 ⟷ t = t'"
and d2: "d t t' = d t' t"
and d3: "t < t' ⟹ t' < t'' ⟹ d t t'' = d t t' + d t' t''"
and d3': "t < t' ⟹ t' < t'' ⟹ d t'' t = d t'' t' + d t' t"
begin

lemma metric_point_structure_memL_aux: "t0 ≤ t ⟹ t ≤ t' ⟹ x ≤ d t t' ⟷ (d t0 t + x ≤ d t0 t')"
apply (rule iffI)
apply (cases "t0 < t"; cases "t < t'")
apply (auto simp: metric_domain_le_def)
apply (metis Δ3' d1)
done

lemma metric_point_structure_memL_strict_aux: "t0 ≤ t ⟹ t ≤ t' ⟹ x < d t t' ⟷ (d t0 t + x < d t0 t')"
using metric_point_structure_memL_aux[of t0 t t' x]
apply auto
apply (metis (no_types, lifting) Δ1 Δ3 Δ4 antisym_conv2 d1 d3)
apply (metis Δ1 add_0 d1 d3 order.order_iff_strict order_less_irrefl)
done

lemma metric_point_structure_memR_aux: "t0 ≤ t ⟹ t ≤ t' ⟹ d t t' ≤ x ⟷ (d t0 t' ≤ d t0 t + x)"
apply auto
apply (metis Δ1 Δ3 d1 d3 order_le_less add_mono)
apply (smt (verit, ccfv_threshold) Δ1 Δ2 Δ3 Δ4 d1 d3 metric_domain_le_def order_le_less)
done

lemma metric_point_structure_memR_strict_aux: "t0 ≤ t ⟹ t ≤ t' ⟹ d t t' < x ⟷ (d t0 t' < d t0 t + x)"
by (auto simp add: metric_point_structure_memL_aux metric_point_structure_memR_aux less_le_not_le)

lemma metric_point_structure_le_mem: "t0 ≤ t ⟹ t ≤ t' ⟹ d t t' ≤ x ⟷ mem (d t0 t) (d t0 t') (interval 0 x True True)"
unfolding mem_def
apply (transfer fixing: d)
using metric_point_structure_memR_aux
apply (auto simp: metric_domain_le_def metric_domain_tfin_def)
done

lemma metric_point_structure_lt_mem: "t0 ≤ t ⟹ t ≤ t' ⟹ 0 < x ⟹ d t t' < x ⟷ mem (d t0 t) (d t0 t') (interval 0 x True False)"
unfolding mem_def
apply (transfer fixing: d)
using metric_point_structure_memR_strict_aux
apply (auto simp: metric_domain_tfin_def)
apply (metis Δ3 metric_domain_pos metric_point_structure_memL_aux)
done

lemma metric_point_structure_eq_mem: "t0 ≤ t ⟹ t ≤ t' ⟹ d t t' = x ⟷ mem (d t0 t) (d t0 t') (interval x x True True)"
unfolding mem_def
apply (transfer fixing: d)
subgoal for t0 t t' x
using metric_point_structure_memL_aux[of t0 t t' x] metric_point_structure_memR_aux[of t0 t t' x] metric_domain_pos
by (auto simp: metric_domain_tfin_def)
done

lemma metric_point_structure_ge_mem: "t0 ≤ t ⟹ t ≤ t' ⟹ x ≤ d t t' ⟷ mem (Some (d t0 t)) (Some (d t0 t')) (interval (Some x) None True True)"
unfolding mem_def
apply (transfer fixing: d)
using metric_point_structure_memL_aux by (auto simp: tfin_option_def zero_option_def plus_option_def less_eq_option_def metric_domain_le_def metric_domain_tfin_def split: option.splits)

lemma metric_point_structure_gt_mem: "t0 ≤ t ⟹ t ≤ t' ⟹ x < d t t' ⟷ mem (Some (d t0 t)) (Some (d t0 t')) (interval (Some x) None False True)"
unfolding mem_def
apply (transfer fixing: d)
using metric_point_structure_memL_strict_aux by (auto simp: tfin_option_def zero_option_def plus_option_def less_option_def less_eq_option_def metric_domain_le_def metric_domain_tfin_def split: option.splits)

end

instantiation nat :: metric_domain_timestamp
begin

instance
apply standard
apply auto[8]
apply (meson less_eqE timestamp_total)
apply (auto simp: sup_max)[1]
apply (auto simp: ι_nat_def)[1]
subgoal for i x
apply (auto simp: ι_nat_def)