Quelle  Example_Metric.thy

(*  Title:    Example_Metric.thy
  Author: Maximilian Schäffeler
*)
theory Example_Metric
  imports "HOL-Analysis.Metric_Arith" "HOL-Eisbach.Eisbach_Tools"
begin

text ‹An Eisbach implementation of the method @{method metric}.
  Slower than the Isabelle/ML implementation but arguably more readable.›

declare [[argo_timeout = 20]]

method dist_refl_sym = simp only: simp_thms dist_commute dist_self

method lin_real_arith uses thms = argo thms

method pre_arith uses argo_thms =
  (simp only: metric_pre_arith)?;
  lin_real_arith thms: argo_thms

method elim_sup =
  (simp only: image_insert image_empty)?;
  dist_refl_sym?;
  (simp only: algebra_simps simp_thms)?;
  (simp only: simp_thms Sup_insert_insert cSup_singleton)?;
  (simp only: simp_thms real_abs_dist)?

method ball_simp = simp only: Set.ball_simps(5,7)

lemmas maxdist_thm = maxdist_thm🍋 ‹normalizes indexnames›

method rewr_maxdist for ps::"'a::metric_space set" uses pos_thms =
  match conclusion in
    "?P (dist x y)" (cut) for x y::'a ==> ‹
  simp only: maxdist_thm[where s=ps and x=x and y=y]
  simp_thms finite.emptyI finite_insert empty_iff insert_iff;
  rewr_maxdist ps pos_thms: pos_thms zero_le_dist[of x y]›
  ∣ _ ==> ‹
  ball_simp?;
  dist_refl_sym?;
  elim_sup?;
  pre_arith argo_thms: pos_thms›

lemmas metric_eq_thm = metric_eq_thm🍋 ‹normalizes indexnames›
method rewr_metric_eq for ps::"'a::metric_space set" =
  match conclusion in
    "?P (x = y)" (cut) for x y::'a ==> ‹
  simp only: metric_eq_thm[where s=ps and x=x and y=y] simp_thms empty_iff insert_iff;
  rewr_metric_eq ps›
  ∣ _ ==> ‹-›

method find_points for ps::"'a::metric_space set" and t::bool =
  match (t) in
    "Q p" (cut) for p::'a and Q::"'a==>bool" ==> ‹
  find_points ‹insert p ps› ‹∀p. Q p›\›
  ∣ _ ==> ‹
  rewr_metric_eq ps;
  rewr_maxdist ps›

method basic_metric_arith for p::"'a::metric_space" =
  dist_refl_sym?;
  match conclusion in
    "Q q" (cut) for q::'a and Q ==> ‹
  find_points ‹{q}› ‹∀p. Q p›\›
  ∣ _ ==> ‹
  rewr_metric_eq ‹{}::'a set›;
  rewr_maxdist ‹{}::'a set›\›

method elim_exists_loop for p::"'a::metric_space" =
  match conclusion in
    "∃q::'a. ?P q r" for r::'a ==> ‹
  print_term r;
  rule exI[of _ r];
  elim_exists_loop p›
  ∣ "∀x. ?P x" (cut) ==> ‹
  rule allI;
  elim_exists_loop p›
  ∣ _ ==> ‹-›

method elim_exists for p::"'a::metric_space" =
  elim_exists_loop p;
  basic_metric_arith p

method find_type =
  match conclusion in
  (* exists in front *)
    "∃x::'a::metric_space. ?P x" ==> ‹
  match conclusion in
  "?Q x" (cut) for x::"'a::metric_space" ==> ‹elim_exists x›
      ∣ _ ==> ‹
  rule exI;
  match conclusion in "?Q x" (cut) for x::"'a::metric_space" ==> ‹elim_exists x›\›\
  (* no exists *)
  ∣ "?P (λy. (dist x y))" (cut) for x::"'a::metric_space" ==> ‹elim_exists x›
  ∣ "?P (λx. (dist x y))" (cut) for y::"'a::metric_space" ==> ‹elim_exists y›
  ∣ "?P (λy. (x = y))" (cut) for x::"'a::metric_space" ==> ‹elim_exists x›
  ∣ "?P (λx. (x = y))" (cut) for y::"'a::metric_space" ==> ‹elim_exists y›
  ∣ _ ==> ‹
  rule exI;
  find_type›

method metric_eisbach =
  (simp only: metric_unfold)?;
  (atomize (full))?;
  (simp only: metric_prenex)?;
  (simp only: metric_nnf)?;
  ((rule allI)+)?;
  match conclusion in _ ==> find_type

subsection ‹examples›

lemma "∃x::'a::metric_space. x=x"
  by metric_eisbach

lemma "∀(x::'a::metric_space). ∃y. x = y"
  by metric_eisbach

lemma "∃x y. dist x y = 0"
  by metric_eisbach

lemma "∃y. dist x y = 0"
  by metric_eisbach

lemma "0 = dist x y ==> x = y"
  by metric_eisbach

lemma "x ≠ y ==> dist x y ≠ 0"
  by metric_eisbach

lemma "∃y. dist x y ≠ 1"
  by metric_eisbach

lemma "x = y ⟷ dist x x = dist y x ∧ dist x y = dist y y"
  by metric_eisbach

lemma "dist a b ≠ dist a c ==> b ≠ c"
  by metric_eisbach

lemma "dist y x + c ≥ c"
  by metric_eisbach

lemma "dist x y + dist x z ≥ 0"
  by metric_eisbach

lemma "dist x y ≥ v ==> dist x y + dist (a::'a) b ≥ v" for x::"('a::metric_space)"
  by metric_eisbach

lemma "dist x y < 0 ⟶ P"
  by metric_eisbach

text ‹reasoning with the triangle inequality›

lemma "dist a d ≤ dist a b + dist b c + dist c d"
  by metric_eisbach

lemma "dist a e ≤ dist a b + dist b c + dist c d + dist d e"
  by metric_eisbach

lemma "max (dist x y) ∣dist x z - dist z y∣ = dist x y"
  by metric_eisbach

lemma
  "dist w x < e/3 ==> dist x y < e/3 ==> dist y z < e/3 ==> dist w x < e"
  by metric_eisbach

lemma "dist w x < e/4 ==> dist x y < e/4 ==> dist y z < e/2 ==> dist w z < e"
  by metric_eisbach

lemma "dist x y = r / 2 ==> (∀z. dist x z < r / 4 ⟶ dist y z ≤ 3 * r / 4)"
  by metric_eisbach

lemma "∃x. ∀r≤0. ∃z. dist x z ≥ r"
  by metric_eisbach

lemma "∧a r x y. dist x a + dist a y = r ==> ∀z. r ≤ dist x z + dist z y ==> dist x y = r"
  by metric_eisbach

end