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 (metis Δ1 add_0 add_mono_comm d1 d3 order_le_less)
  apply (cases "t0 < t"; cases "t < t'")
     apply (auto simp: metric_domain_le_def)
     apply (metis Δ4 ab_semigroup_add_class.add_ac(1) d3)
    apply (metis comm_monoid_add_class.add_0 group_cancel.add1 metric_domain_lt_def nless_le)
   apply (metis Δ3' d1)
  apply (metis add_0 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)
  apply (metis add.right_neutral d3 order.order_iff_strict)
  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)
  using nat_le_iff_add apply blast
  using less_imp_add_positive apply auto[1]
     apply (auto simp: sup_max)[1]
    apply (auto simp: ι_nat_def)[1]
  subgoal for i x
    apply (auto simp: ι_nat_def)
    using add_le_same_cancel1 by blast
  apply (auto simp: tfin_nat_def)
  done

end

interpretation nat_metric_point_structure: metric_point_structure "λt :: nat. λt'. if t ≤ t' then t' - t else t - t'"
  by unfold_locales auto

end