(* Title: Example_Metric.thy
Author: Maximilian Schäffeler
*)
theory Example_Metric
imports "HOL-Analysis.Metric_Arith" "HOL-Eisbach.Eisbach_Tools"
begin
text \<open>An Eisbach implementation of the method @{method metric}.
Slower than the Isabelle/ML implementation but arguably more readable.\<close>
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\<comment> \<open>normalizes indexnames\<close>
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]\<close>
\<bar> _ \<Rightarrow> \<open>
ball_simp?;
dist_refl_sym?;
elim_sup?;
pre_arith argo_thms: pos_thms\<close>
lemmas metric_eq_thm = metric_eq_thm\<comment> \<open>normalizes indexnames\<close>
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\<close>
\<bar> _ \<Rightarrow> \<open>-\<close>
method find_points for ps::"'a::metric_space set" and t::bool =
match (t) in
"Q p" (cut) for p::'a and Q::"'a\<Rightarrow>bool" \<Rightarrow> \<open>
find_points \<open>insert p ps\<close> \<open>\<forall>p. Q p\<close>\<close>
\<bar> _ \<Rightarrow> \<open>
rewr_metric_eq ps;
rewr_maxdist ps\<close>
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 \<open>{q}\<close> \<open>\<forall>p. Q p\<close>\<close>
\<bar> _ \<Rightarrow> \<open>
rewr_metric_eq \<open>{}::'a set\<close>;
rewr_maxdist \<open>{}::'a set\<close>\<close>
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\<close>
\<bar> "\<forall>x. ?P x" (cut) \<Rightarrow> \<open>
rule allI;
elim_exists_loop p\<close>
\<bar> _ \<Rightarrow> \<open>-\<close>
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" \<Rightarrow> \<open>elim_exists x\<close>
\<bar> _ \<Rightarrow> \<open>
rule exI;
match conclusion in "?Q x" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close>\<close>\<close>
(* no exists *)
\<bar> "?P (\<lambda>y. (dist x y))" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close>
\<bar> "?P (\<lambda>x. (dist x y))" (cut) for y::"'a::metric_space" \<Rightarrow> \<open>elim_exists y\<close>
\<bar> "?P (\<lambda>y. (x = y))" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close>
\<bar> "?P (\<lambda>x. (x = y))" (cut) for y::"'a::metric_space" \<Rightarrow> \<open>elim_exists y\<close>
\<bar> _ \<Rightarrow> \<open>
rule exI;
find_type\<close>
method metric_eisbach =
(simp only: metric_unfold)?;
(atomize (full))?;
(simp only: metric_prenex)?;
(simp only: metric_nnf)?;
((rule allI)+)?;
match conclusion in _ \<Rightarrow> find_type
subsection \<open>examples\<close>
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 \<open>reasoning with the triangle inequality\<close>
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
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
