author | immler |
Sun, 27 Oct 2019 20:55:58 -0400 | |
changeset 70959 | ba0b65d45aec |
parent 70958 | e8fc52f3f175 |
child 74739 | a06652d397a7 |
permissions | -rw-r--r-- |
70959
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
1 |
(* Title: Example_Metric.thy |
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
2 |
Author: Maximilian Schäffeler |
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
3 |
*) |
70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
4 |
theory Example_Metric |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
5 |
imports "HOL-Analysis.Metric_Arith" "HOL-Eisbach.Eisbach_Tools" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
6 |
begin |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
7 |
|
70959
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
8 |
text \<open>An Eisbach implementation of the method @{method metric}. |
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
9 |
Slower than the Isabelle/ML implementation but arguably more readable.\<close> |
ba0b65d45aec
header with Title/Author; added note on motivation of this example
immler
parents:
70958
diff
changeset
|
10 |
|
70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
11 |
method dist_refl_sym = simp only: simp_thms dist_commute dist_self |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
12 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
13 |
method lin_real_arith uses thms = argo thms |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
14 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
15 |
method pre_arith uses argo_thms = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
16 |
(simp only: metric_pre_arith)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
17 |
lin_real_arith thms: argo_thms |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
18 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
19 |
method elim_sup = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
20 |
(simp only: image_insert image_empty)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
21 |
dist_refl_sym?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
22 |
(simp only: algebra_simps simp_thms)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
23 |
(simp only: simp_thms Sup_insert_insert cSup_singleton)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
24 |
(simp only: simp_thms real_abs_dist)? |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
25 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
26 |
method ball_simp = simp only: Set.ball_simps(5,7) |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
27 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
28 |
lemmas maxdist_thm = maxdist_thm\<comment> \<open>normalizes indexnames\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
29 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
30 |
method rewr_maxdist for ps::"'a::metric_space set" uses pos_thms = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
31 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
32 |
"?P (dist x y)" (cut) for x y::'a \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
33 |
simp only: maxdist_thm[where s=ps and x=x and y=y] |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
34 |
simp_thms finite.emptyI finite_insert empty_iff insert_iff; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
35 |
rewr_maxdist ps pos_thms: pos_thms zero_le_dist[of x y]\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
36 |
\<bar> _ \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
37 |
ball_simp?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
38 |
dist_refl_sym?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
39 |
elim_sup?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
40 |
pre_arith argo_thms: pos_thms\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
41 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
42 |
lemmas metric_eq_thm = metric_eq_thm\<comment> \<open>normalizes indexnames\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
43 |
method rewr_metric_eq for ps::"'a::metric_space set" = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
44 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
45 |
"?P (x = y)" (cut) for x y::'a \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
46 |
simp only: metric_eq_thm[where s=ps and x=x and y=y] simp_thms empty_iff insert_iff; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
47 |
rewr_metric_eq ps\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
48 |
\<bar> _ \<Rightarrow> \<open>-\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
49 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
50 |
method find_points for ps::"'a::metric_space set" and t::bool = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
51 |
match (t) in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
52 |
"Q p" (cut) for p::'a and Q::"'a\<Rightarrow>bool" \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
53 |
find_points \<open>insert p ps\<close> \<open>\<forall>p. Q p\<close>\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
54 |
\<bar> _ \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
55 |
rewr_metric_eq ps; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
56 |
rewr_maxdist ps\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
57 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
58 |
method basic_metric_arith for p::"'a::metric_space" = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
59 |
dist_refl_sym?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
60 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
61 |
"Q q" (cut) for q::'a and Q \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
62 |
find_points \<open>{q}\<close> \<open>\<forall>p. Q p\<close>\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
63 |
\<bar> _ \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
64 |
rewr_metric_eq \<open>{}::'a set\<close>; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
65 |
rewr_maxdist \<open>{}::'a set\<close>\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
66 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
67 |
method elim_exists_loop for p::"'a::metric_space" = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
68 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
69 |
"\<exists>q::'a. ?P q r" for r::'a \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
70 |
print_term r; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
71 |
rule exI[of _ r]; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
72 |
elim_exists_loop p\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
73 |
\<bar> "\<forall>x. ?P x" (cut) \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
74 |
rule allI; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
75 |
elim_exists_loop p\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
76 |
\<bar> _ \<Rightarrow> \<open>-\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
77 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
78 |
method elim_exists for p::"'a::metric_space" = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
79 |
elim_exists_loop p; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
80 |
basic_metric_arith p |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
81 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
82 |
method find_type = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
83 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
84 |
(* exists in front *) |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
85 |
"\<exists>x::'a::metric_space. ?P x" \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
86 |
match conclusion in |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
87 |
"?Q x" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
88 |
\<bar> _ \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
89 |
rule exI; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
90 |
match conclusion in "?Q x" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close>\<close>\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
91 |
(* no exists *) |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
92 |
\<bar> "?P (\<lambda>y. (dist x y))" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
93 |
\<bar> "?P (\<lambda>x. (dist x y))" (cut) for y::"'a::metric_space" \<Rightarrow> \<open>elim_exists y\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
94 |
\<bar> "?P (\<lambda>y. (x = y))" (cut) for x::"'a::metric_space" \<Rightarrow> \<open>elim_exists x\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
95 |
\<bar> "?P (\<lambda>x. (x = y))" (cut) for y::"'a::metric_space" \<Rightarrow> \<open>elim_exists y\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
96 |
\<bar> _ \<Rightarrow> \<open> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
97 |
rule exI; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
98 |
find_type\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
99 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
100 |
method metric_eisbach = |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
101 |
(simp only: metric_unfold)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
102 |
(atomize (full))?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
103 |
(simp only: metric_prenex)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
104 |
(simp only: metric_nnf)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
105 |
((rule allI)+)?; |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
106 |
match conclusion in _ \<Rightarrow> find_type |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
107 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
108 |
subsection \<open>examples\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
109 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
110 |
lemma "\<exists>x::'a::metric_space. x=x" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
111 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
112 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
113 |
lemma "\<forall>(x::'a::metric_space). \<exists>y. x = y" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
114 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
115 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
116 |
lemma "\<exists>x y. dist x y = 0" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
117 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
118 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
119 |
lemma "\<exists>y. dist x y = 0" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
120 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
121 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
122 |
lemma "0 = dist x y \<Longrightarrow> x = y" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
123 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
124 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
125 |
lemma "x \<noteq> y \<Longrightarrow> dist x y \<noteq> 0" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
126 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
127 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
128 |
lemma "\<exists>y. dist x y \<noteq> 1" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
129 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
130 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
131 |
lemma "x = y \<longleftrightarrow> dist x x = dist y x \<and> dist x y = dist y y" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
132 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
133 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
134 |
lemma "dist a b \<noteq> dist a c \<Longrightarrow> b \<noteq> c" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
135 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
136 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
137 |
lemma "dist y x + c \<ge> c" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
138 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
139 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
140 |
lemma "dist x y + dist x z \<ge> 0" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
141 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
142 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
143 |
lemma "dist x y \<ge> v \<Longrightarrow> dist x y + dist (a::'a) b \<ge> v" for x::"('a::metric_space)" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
144 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
145 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
146 |
lemma "dist x y < 0 \<longrightarrow> P" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
147 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
148 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
149 |
text \<open>reasoning with the triangle inequality\<close> |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
150 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
151 |
lemma "dist a d \<le> dist a b + dist b c + dist c d" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
152 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
153 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
154 |
lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
155 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
156 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
157 |
lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
158 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
159 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
160 |
lemma |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
161 |
"dist w x < e/3 \<Longrightarrow> dist x y < e/3 \<Longrightarrow> dist y z < e/3 \<Longrightarrow> dist w x < e" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
162 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
163 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
164 |
lemma "dist w x < e/4 \<Longrightarrow> dist x y < e/4 \<Longrightarrow> dist y z < e/2 \<Longrightarrow> dist w z < e" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
165 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
166 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
167 |
lemma "dist x y = r / 2 \<Longrightarrow> (\<forall>z. dist x z < r / 4 \<longrightarrow> dist y z \<le> 3 * r / 4)" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
168 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
169 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
170 |
lemma "\<exists>x. \<forall>r\<le>0. \<exists>z. dist x z \<ge> r" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
171 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
172 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
173 |
lemma "\<And>a r x y. dist x a + dist a y = r \<Longrightarrow> \<forall>z. r \<le> dist x z + dist z y \<Longrightarrow> dist x y = r" |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
174 |
by metric_eisbach |
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
175 |
|
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
diff
changeset
|
176 |
end |