author | wenzelm |
Fri, 29 Oct 2021 19:49:11 +0200 | |
changeset 74628 | cd030003efa8 |
parent 74627 | c690435c47ee |
child 74629 | 9264ef3a2ba3 |
permissions | -rw-r--r-- |
74546 | 1 |
(* Title: HOL/Analysis/metric_arith.ML |
2 |
Author: Maximilian Schäffeler (port from HOL Light) |
|
3 |
||
4 |
A decision procedure for metric spaces. |
|
5 |
*) |
|
6 |
||
7 |
signature METRIC_ARITH = |
|
8 |
sig |
|
9 |
val trace: bool Config.T |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
10 |
val metric_arith_tac : Proof.context -> int -> tactic |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
11 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
12 |
|
74546 | 13 |
structure Metric_Arith : METRIC_ARITH = |
14 |
struct |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
15 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
16 |
(* apply f to both cterms in ct_pair, merge results *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
17 |
fun app_union_ct_pair f ct_pair = uncurry (union (op aconvc)) (apply2 f ct_pair) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
18 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
19 |
val trace = Attrib.setup_config_bool \<^binding>\<open>metric_trace\<close> (K false) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
20 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
21 |
fun trace_tac ctxt msg = |
74627 | 22 |
if Config.get ctxt trace then print_tac ctxt msg else all_tac |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
23 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
24 |
fun argo_trace_ctxt ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
25 |
if Config.get ctxt trace |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
26 |
then Config.map (Argo_Tactic.trace) (K "basic") ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
27 |
else ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
28 |
|
74627 | 29 |
fun free_in v t = |
30 |
Term.exists_subterm (fn u => u aconv Thm.term_of v) (Thm.term_of t); |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
31 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
32 |
(* build a cterm set with elements cts of type ty *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
33 |
fun mk_ct_set ctxt ty = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
34 |
map Thm.term_of #> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
35 |
HOLogic.mk_set ty #> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
36 |
Thm.cterm_of ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
37 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
38 |
fun prenex_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
39 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
40 |
val prenex_simps = Proof_Context.get_thms ctxt @{named_theorems metric_prenex} |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
41 |
val prenex_ctxt = put_simpset HOL_basic_ss ctxt addsimps prenex_simps |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
42 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
43 |
simp_tac prenex_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
44 |
K (trace_tac ctxt "Prenex form") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
45 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
46 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
47 |
fun nnf_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
48 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
49 |
val nnf_simps = Proof_Context.get_thms ctxt @{named_theorems metric_nnf} |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
50 |
val nnf_ctxt = put_simpset HOL_basic_ss ctxt addsimps nnf_simps |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
51 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
52 |
simp_tac nnf_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
53 |
K (trace_tac ctxt "NNF form") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
54 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
55 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
56 |
fun unfold_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
57 |
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
58 |
Proof_Context.get_thms ctxt @{named_theorems metric_unfold})) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
59 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
60 |
fun pre_arith_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
61 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
62 |
Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
63 |
K (trace_tac ctxt "Prepared for decision procedure") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
64 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
65 |
fun dist_refl_sym_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
66 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
67 |
val refl_sym_simps = @{thms dist_self dist_commute add_0_right add_0_left simp_thms} |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
68 |
val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt addsimps refl_sym_simps |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
69 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
70 |
simp_tac refl_sym_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
71 |
K (trace_tac ctxt ("Simplified using " ^ @{make_string} refl_sym_simps)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
72 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
73 |
|
74627 | 74 |
fun is_exists \<^Const_>\<open>Ex _ for _\<close> = true |
75 |
| is_exists \<^Const_>\<open>Trueprop for t\<close> = is_exists t |
|
76 |
| is_exists _ = false |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
77 |
|
74627 | 78 |
fun is_forall \<^Const_>\<open>All _ for _\<close> = true |
79 |
| is_forall \<^Const_>\<open>Trueprop for t\<close> = is_forall t |
|
80 |
| is_forall _ = false |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
81 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
82 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
83 |
(* find all free points in ct of type metric_ty *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
84 |
fun find_points ctxt metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
85 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
86 |
fun find ct = |
74627 | 87 |
(if Thm.typ_of_cterm ct = metric_ty then [ct] else []) @ |
88 |
(case Thm.term_of ct of |
|
89 |
_ $ _ => app_union_ct_pair find (Thm.dest_comb ct) |
|
90 |
| Abs _ => |
|
91 |
(*ensure the point doesn't contain the bound variable*) |
|
92 |
let val (x, body) = Thm.dest_abs_global ct |
|
93 |
in filter_out (free_in x) (find body) end |
|
94 |
| _ => []) |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
95 |
in |
74627 | 96 |
(case find ct of |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
97 |
[] => |
74627 | 98 |
(*if no point can be found, invent one*) |
99 |
let val x = singleton (Term.variant_frees (Thm.term_of ct)) ("x", metric_ty) |
|
100 |
in [Thm.cterm_of ctxt (Free x)] end |
|
101 |
| points => points) |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
102 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
103 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
104 |
(* find all cterms "dist x y" in ct, where x and y have type metric_ty *) |
74627 | 105 |
fun find_dist metric_ty = |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
106 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
107 |
fun find ct = |
74627 | 108 |
(case Thm.term_of ct of |
109 |
\<^Const_>\<open>dist T for _ _\<close> => if T = metric_ty then [ct] else [] |
|
110 |
| _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) |
|
111 |
| Abs _ => |
|
112 |
let val (x, body) = Thm.dest_abs_global ct |
|
113 |
in filter_out (free_in x) (find body) end |
|
114 |
| _ => []) |
|
115 |
in find end |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
116 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
117 |
(* find all "x=y", where x has type metric_ty *) |
74627 | 118 |
fun find_eq metric_ty = |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
119 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
120 |
fun find ct = |
74627 | 121 |
(case Thm.term_of ct of |
122 |
\<^Const_>\<open>HOL.eq T for _ _\<close> => |
|
123 |
if T = metric_ty then [ct] |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
124 |
else app_union_ct_pair find (Thm.dest_binop ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
125 |
| _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) |
74627 | 126 |
| Abs _ => |
127 |
let val (x, body) = Thm.dest_abs_global ct |
|
128 |
in filter_out (free_in x) (find body) end |
|
129 |
| _ => []) |
|
130 |
in find end |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
131 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
132 |
(* rewrite ct of the form "dist x y" using maxdist_thm *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
133 |
fun maxdist_conv ctxt fset_ct ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
134 |
let |
74627 | 135 |
val (x, y) = Thm.dest_binop ct |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
136 |
val solve_prems = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
137 |
rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
138 |
addsimps @{thms finite.emptyI finite_insert empty_iff insert_iff}))) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
139 |
val image_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
140 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms image_empty image_insert}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
141 |
val dist_refl_sym_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
142 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
143 |
val algebra_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
144 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
145 |
@{thms diff_self diff_0_right diff_0 abs_zero abs_minus_cancel abs_minus_commute}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
146 |
val insert_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
147 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms insert_absorb2 insert_commute}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
148 |
val sup_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
149 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms cSup_singleton Sup_insert_insert}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
150 |
val real_abs_dist_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
151 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
152 |
val maxdist_thm = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
153 |
@{thm maxdist_thm} |> |
74627 | 154 |
infer_instantiate' ctxt [SOME fset_ct, SOME x, SOME y] |> |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
155 |
solve_prems |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
156 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
157 |
((Conv.rewr_conv maxdist_thm) then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
158 |
(* SUP to Sup *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
159 |
image_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
160 |
dist_refl_sym_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
161 |
algebra_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
162 |
(* eliminate duplicate terms in set *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
163 |
insert_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
164 |
(* Sup to max *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
165 |
sup_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
166 |
real_abs_dist_simp) ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
167 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
168 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
169 |
(* rewrite ct of the form "x=y" using metric_eq_thm *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
170 |
fun metric_eq_conv ctxt fset_ct ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
171 |
let |
74627 | 172 |
val (x, y) = Thm.dest_binop ct |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
173 |
val solve_prems = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
174 |
rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
175 |
addsimps @{thms empty_iff insert_iff}))) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
176 |
val ball_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
177 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps |
70954 | 178 |
@{thms Set.ball_empty ball_insert}) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
179 |
val dist_refl_sym_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
180 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
181 |
val metric_eq_thm = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
182 |
@{thm metric_eq_thm} |> |
74627 | 183 |
infer_instantiate' ctxt [SOME x, SOME fset_ct, SOME y] |> |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
184 |
solve_prems |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
185 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
186 |
((Conv.rewr_conv metric_eq_thm) then_conv |
74627 | 187 |
(*convert \<forall>x\<in>{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \<and> ... \<and> P x\<^sub>n*) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
188 |
ball_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
189 |
dist_refl_sym_simp) ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
190 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
191 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
192 |
(* build list of theorems "0 \<le> dist x y" for all dist terms in ct *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
193 |
fun augment_dist_pos ctxt metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
194 |
let fun inst dist_ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
195 |
let val (xct, yct) = Thm.dest_binop dist_ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
196 |
in infer_instantiate' ctxt [SOME xct, SOME yct] @{thm zero_le_dist} end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
197 |
in map inst (find_dist metric_ty ct) end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
198 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
199 |
(* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *) |
74547 | 200 |
fun embedding_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) => |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
201 |
let |
74547 | 202 |
val points = find_points ctxt metric_ty goal |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
203 |
val fset_ct = mk_ct_set ctxt metric_ty points |
74627 | 204 |
(*embed all subterms of the form "dist x y" in (\<real>\<^sup>n,dist\<^sub>\<infinity>)*) |
74547 | 205 |
val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty goal) |
74627 | 206 |
(*replace point equality by equality of components in \<real>\<^sup>n*) |
74547 | 207 |
val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty goal) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
208 |
in |
74545 | 209 |
(K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN' |
74547 | 210 |
CONVERSION (Conv.top_sweep_rewrs_conv (eq1 @ eq2) ctxt)) i |
211 |
end) |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
212 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
213 |
(* decision procedure for linear real arithmetic *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
214 |
fun lin_real_arith_tac ctxt metric_ty i goal = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
215 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
216 |
val dist_thms = augment_dist_pos ctxt metric_ty (Thm.cprem_of goal 1) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
217 |
val ctxt' = argo_trace_ctxt ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
218 |
in (Argo_Tactic.argo_tac ctxt' dist_thms) i goal end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
219 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
220 |
fun basic_metric_arith_tac ctxt metric_ty = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
221 |
HEADGOAL (dist_refl_sym_tac ctxt THEN' |
74627 | 222 |
IF_UNSOLVED o (embedding_tac ctxt metric_ty) THEN' |
223 |
IF_UNSOLVED o (pre_arith_tac ctxt) THEN' |
|
224 |
IF_UNSOLVED o (lin_real_arith_tac ctxt metric_ty)) |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
225 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
226 |
(* tries to infer the metric space from ct from dist terms, |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
227 |
if no dist terms are present, equality terms will be used *) |
74627 | 228 |
fun guess_metric ctxt tm = |
229 |
let |
|
230 |
val thy = Proof_Context.theory_of ctxt |
|
231 |
fun find_dist t = |
|
232 |
(case t of |
|
233 |
\<^Const_>\<open>dist T for _ _\<close> => SOME T |
|
234 |
| t1 $ t2 => (case find_dist t1 of NONE => find_dist t2 | some => some) |
|
235 |
| Abs _ => find_dist (#2 (Term.dest_abs_global t)) |
|
236 |
| _ => NONE) |
|
237 |
fun find_eq t = |
|
238 |
(case t of |
|
239 |
\<^Const_>\<open>HOL.eq T for l r\<close> => |
|
240 |
if Sign.of_sort thy (T, \<^sort>\<open>metric_space\<close>) then SOME T |
|
74628 | 241 |
else (case find_eq l of NONE => find_eq r | some => some) |
74627 | 242 |
| t1 $ t2 => (case find_eq t1 of NONE => find_eq t2 | some => some) |
243 |
| Abs _ => find_eq (#2 (Term.dest_abs_global t)) |
|
244 |
| _ => NONE) |
|
245 |
in |
|
246 |
(case find_dist tm of |
|
247 |
SOME ty => ty |
|
248 |
| NONE => |
|
249 |
case find_eq tm of |
|
250 |
SOME ty => ty |
|
251 |
| NONE => error "No Metric Space was found") |
|
252 |
end |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
253 |
|
74627 | 254 |
(* solve \<exists> by proving the goal for a single witness from the metric space *) |
255 |
fun exists_tac ctxt st = |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
256 |
let |
74627 | 257 |
val goal = Thm.cprem_of st 1 |
258 |
val metric_ty = guess_metric ctxt (Thm.term_of goal) |
|
259 |
val points = find_points ctxt metric_ty goal |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
260 |
|
74627 | 261 |
fun try_point_tac ctxt pt = |
262 |
let |
|
263 |
val ex_rule = |
|
264 |
\<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm pt\<close> and x = pt in |
|
265 |
lemma (schematic) \<open>P x \<Longrightarrow> \<exists>x::'a. P x\<close> by (rule exI)\<close> |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
266 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
267 |
HEADGOAL (resolve_tac ctxt [ex_rule] ORELSE' |
74627 | 268 |
(*variable doesn't occur in body*) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
269 |
resolve_tac ctxt @{thms exI}) THEN |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
270 |
trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN |
74627 | 271 |
try_points_tac ctxt |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
272 |
end |
74627 | 273 |
and try_points_tac ctxt st = ( |
274 |
if is_exists (Thm.major_prem_of st) then |
|
275 |
FIRST (map (try_point_tac ctxt) points) |
|
276 |
else if is_forall (Thm.major_prem_of st) then |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
277 |
HEADGOAL (resolve_tac ctxt @{thms HOL.allI} THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
278 |
Subgoal.FOCUS (fn {context = ctxt', ...} => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
279 |
trace_tac ctxt "Removed universal quantifier" THEN |
74627 | 280 |
try_points_tac ctxt') ctxt) |
281 |
else basic_metric_arith_tac ctxt metric_ty) st |
|
282 |
in try_points_tac ctxt st end |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
283 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
284 |
fun metric_arith_tac ctxt = |
74627 | 285 |
(*unfold common definitions to get rid of sets*) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
286 |
unfold_tac ctxt THEN' |
74627 | 287 |
(*remove all meta-level connectives*) |
288 |
IF_UNSOLVED o (Object_Logic.full_atomize_tac ctxt) THEN' |
|
289 |
(*convert goal to prenex form*) |
|
290 |
IF_UNSOLVED o (prenex_tac ctxt) THEN' |
|
291 |
(*and NNF to ?*) |
|
292 |
IF_UNSOLVED o (nnf_tac ctxt) THEN' |
|
293 |
(*turn all universally quantified variables into free variables, by focusing the subgoal*) |
|
294 |
REPEAT o (resolve_tac ctxt @{thms HOL.allI}) THEN' |
|
295 |
IF_UNSOLVED o SUBPROOF (fn {context = ctxt', ...} => |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
296 |
trace_tac ctxt' "Focused on subgoal" THEN |
74627 | 297 |
exists_tac ctxt') ctxt |
74546 | 298 |
|
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
299 |
end |