author | immler |
Sun, 27 Oct 2019 12:13:04 -0400 | |
changeset 70954 | 23e6eef4e6aa |
parent 70953 | 420359ba6acd |
child 70962 | e8207714d505 |
permissions | -rw-r--r-- |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
1 |
(* Title: Metric_Arith.thy |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
2 |
Author: Maximilian Schäffeler (port from HOL Light) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
3 |
*) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
4 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
5 |
section \<open>A decision procedure for metric spaces\<close> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
6 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
7 |
theory Metric_Arith |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
8 |
imports HOL.Real_Vector_Spaces |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
9 |
begin |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
10 |
|
70953 | 11 |
text \<open> |
12 |
A port of the decision procedure ``Formalization of metric spaces in HOL Light'' |
|
13 |
@{cite "DBLP:journals/jar/Maggesi18"} for the type class @{class metric_space}, |
|
14 |
with the \<open>Argo\<close> solver as backend. |
|
15 |
\<close> |
|
16 |
||
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
17 |
named_theorems metric_prenex |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
18 |
named_theorems metric_nnf |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
19 |
named_theorems metric_unfold |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
20 |
named_theorems metric_pre_arith |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
21 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
22 |
lemmas pre_arith_simps = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
23 |
max.bounded_iff max_less_iff_conj |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
24 |
le_max_iff_disj less_max_iff_disj |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
25 |
simp_thms HOL.eq_commute |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
26 |
declare pre_arith_simps [metric_pre_arith] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
27 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
28 |
lemmas unfold_simps = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
29 |
Un_iff subset_iff disjoint_iff_not_equal |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
30 |
Ball_def Bex_def |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
31 |
declare unfold_simps [metric_unfold] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
32 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
33 |
declare HOL.nnf_simps(4) [metric_prenex] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
34 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
35 |
lemma imp_prenex [metric_prenex]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
36 |
"\<And>P Q. (\<exists>x. P x) \<longrightarrow> Q \<equiv> \<forall>x. (P x \<longrightarrow> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
37 |
"\<And>P Q. P \<longrightarrow> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<longrightarrow> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
38 |
"\<And>P Q. (\<forall>x. P x) \<longrightarrow> Q \<equiv> \<exists>x. (P x \<longrightarrow> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
39 |
"\<And>P Q. P \<longrightarrow> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<longrightarrow> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
40 |
by simp_all |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
41 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
42 |
lemma ex_prenex [metric_prenex]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
43 |
"\<And>P Q. (\<exists>x. P x) \<and> Q \<equiv> \<exists>x. (P x \<and> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
44 |
"\<And>P Q. P \<and> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<and> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
45 |
"\<And>P Q. (\<exists>x. P x) \<or> Q \<equiv> \<exists>x. (P x \<or> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
46 |
"\<And>P Q. P \<or> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<or> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
47 |
"\<And>P. \<not>(\<exists>x. P x) \<equiv> \<forall>x. \<not>P x" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
48 |
by simp_all |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
49 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
50 |
lemma all_prenex [metric_prenex]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
51 |
"\<And>P Q. (\<forall>x. P x) \<and> Q \<equiv> \<forall>x. (P x \<and> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
52 |
"\<And>P Q. P \<and> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<and> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
53 |
"\<And>P Q. (\<forall>x. P x) \<or> Q \<equiv> \<forall>x. (P x \<or> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
54 |
"\<And>P Q. P \<or> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<or> Q x)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
55 |
"\<And>P. \<not>(\<forall>x. P x) \<equiv> \<exists>x. \<not>P x" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
56 |
by simp_all |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
57 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
58 |
lemma nnf_thms [metric_nnf]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
59 |
"(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
60 |
"(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
61 |
"(P \<longrightarrow> Q) = (\<not> P \<or> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
62 |
"(P = Q) \<longleftrightarrow> (P \<or> \<not> Q) \<and> (\<not> P \<or> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
63 |
"(\<not> (P = Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q) \<and> (P \<or> Q)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
64 |
"(\<not> \<not> P) = P" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
65 |
by blast+ |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
66 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
67 |
lemmas nnf_simps = nnf_thms linorder_not_less linorder_not_le |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
68 |
declare nnf_simps[metric_nnf] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
69 |
|
70954 | 70 |
lemma ball_insert: "(\<forall>x\<in>insert a B. P x) = (P a \<and> (\<forall>x\<in>B. P x))" |
71 |
by blast |
|
72 |
||
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
73 |
lemma Sup_insert_insert: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
74 |
fixes a::real |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
75 |
shows "Sup (insert a (insert b s)) = Sup (insert (max a b) s)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
76 |
by (simp add: Sup_real_def) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
77 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
78 |
lemma real_abs_dist: "\<bar>dist x y\<bar> = dist x y" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
79 |
by simp |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
80 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
81 |
lemma maxdist_thm [THEN HOL.eq_reflection]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
82 |
assumes "finite s" "x \<in> s" "y \<in> s" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
83 |
defines "\<And>a. f a \<equiv> \<bar>dist x a - dist a y\<bar>" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
84 |
shows "dist x y = Sup (f ` s)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
85 |
proof - |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
86 |
have "dist x y \<le> Sup (f ` s)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
87 |
proof - |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
88 |
have "finite (f ` s)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
89 |
by (simp add: \<open>finite s\<close>) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
90 |
moreover have "\<bar>dist x y - dist y y\<bar> \<in> f ` s" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
91 |
by (metis \<open>y \<in> s\<close> f_def imageI) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
92 |
ultimately show ?thesis |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
93 |
using le_cSup_finite by simp |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
94 |
qed |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
95 |
also have "Sup (f ` s) \<le> dist x y" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
96 |
using \<open>x \<in> s\<close> cSUP_least[of s f] abs_dist_diff_le |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
97 |
unfolding f_def |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
98 |
by blast |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
99 |
finally show ?thesis . |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
100 |
qed |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
101 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
102 |
theorem metric_eq_thm [THEN HOL.eq_reflection]: |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
103 |
"x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
104 |
by auto |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
105 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
106 |
ML_file "metricarith.ml" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
107 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
108 |
method_setup metric = \<open> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
109 |
Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
110 |
\<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
111 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
112 |
end |