products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sos_wrapper.ML   Sprache: Isabelle

Original von: Isabelle©
theory Metric_Arith_Examples
imports "HOL-Analysis.Elementary_Metric_Spaces"
begin


text \<open>simple examples\<close>

lemma "\x::'a::metric_space. x=x"
  by metric
lemma "\(x::'a::metric_space). \y. x = y"
  by metric


text \<open>reasoning with "dist x y = 0 \<longleftrightarrow> x = y"\<close>

lemma "\x y. dist x y = 0"
  by metric

lemma "\y. dist x y = 0"
  by metric

lemma "0 = dist x y \ x = y"
  by metric

lemma "x \ y \ dist x y \ 0"
  by metric

lemma "\y. dist x y \ 1"
  by metric

lemma "x = y \ dist x x = dist y x \ dist x y = dist y y"
  by metric

lemma "dist a b \ dist a c \ b \ c"
  by metric

text \<open>reasoning with positive semidefiniteness\<close>

lemma "dist y x + c \ c"
  by metric

lemma "dist x y + dist x z \ 0"
  by metric

lemma "dist x y \ v \ dist x y + dist (a::'a) b \ v" for x::"('a::metric_space)"
  by metric

lemma "dist x y < 0 \ P"
  by metric

text \<open>reasoning with the triangle inequality\<close>

lemma "dist a d \ dist a b + dist b c + dist c d"
  by metric

lemma "dist a e \ dist a b + dist b c + dist c d + dist d e"
  by metric

lemma "max (dist x y) \dist x z - dist z y\ = dist x y"
  by metric

lemma
  "dist w x < e/3 \ dist x y < e/3 \ dist y z < e/3 \ dist w x < e"
  by metric

lemma "dist w x < e/4 \ dist x y < e/4 \ dist y z < e/2 \ dist w z < e"
  by metric


text \<open>more complex examples\<close>

lemma "dist x y \ e \ dist x z \ e \ dist y z \ e
  \<Longrightarrow> p \<in> (cball x e \<union> cball y e \<union> cball z e) \<Longrightarrow> dist p x \<le> 2*e"
  by metric

lemma hol_light_example:
  "\ disjnt (ball x r) (ball y s) \
    (\<forall>p q. p \<in> ball x r \<union> ball y s \<and> q \<in> ball x r \<union> ball y s \<longrightarrow> dist p q < 2 * (r + s))"
  unfolding disjnt_iff
  by metric

lemma "dist x y \ e \ z \ ball x f \ dist z y < e + f"
  by metric

lemma "dist x y = r / 2 \ (\z. dist x z < r / 4 \ dist y z \ 3 * r / 4)"
  by metric

lemma "s \ 0 \ t \ 0 \ z \ (ball x s) \ (ball y t) \ dist z y \ dist x y + s + t"
  by metric

lemma "0 < r \ ball x r \ ball y s \ ball x r \ ball z t \ dist y z \ s + t"
  by metric


text \<open>non-trivial quantifier structure\<close>

lemma "\x. \r\0. \z. dist x z \ r"
  by metric

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

end

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff