author | wenzelm |
Thu, 09 Sep 2021 14:50:26 +0200 | |
changeset 74269 | f084d599bb44 |
parent 74249 | 9d9e7ed01dbb |
child 74274 | 36f2c4a5c21b |
permissions | -rw-r--r-- |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
1 |
signature METRIC_ARITH = sig |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
2 |
val metric_arith_tac : Proof.context -> int -> tactic |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
3 |
val trace: bool Config.T |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
4 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
5 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
6 |
structure MetricArith : METRIC_ARITH = struct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
7 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
8 |
fun default d x = case x of SOME y => SOME y | NONE => d |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
9 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
10 |
(* 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
|
11 |
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
|
12 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
13 |
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
|
14 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
15 |
fun trace_tac ctxt msg = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
16 |
if Config.get ctxt trace then print_tac ctxt msg |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
17 |
else all_tac |
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 |
fun argo_trace_ctxt ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
20 |
if Config.get ctxt trace |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
21 |
then Config.map (Argo_Tactic.trace) (K "basic") ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
22 |
else ctxt |
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 IF_UNSOLVED' tac i = IF_UNSOLVED (tac i) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
25 |
fun REPEAT' tac i = REPEAT (tac i) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
26 |
|
74269 | 27 |
fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
28 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
29 |
(* 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
|
30 |
fun mk_ct_set ctxt ty = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
31 |
map Thm.term_of #> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
32 |
HOLogic.mk_set ty #> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
33 |
Thm.cterm_of ctxt |
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 |
fun prenex_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
36 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
37 |
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
|
38 |
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
|
39 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
40 |
simp_tac prenex_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
41 |
K (trace_tac ctxt "Prenex form") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
42 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
43 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
44 |
fun nnf_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
45 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
49 |
simp_tac nnf_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
50 |
K (trace_tac ctxt "NNF form") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
51 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
52 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
53 |
fun unfold_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
54 |
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
|
55 |
Proof_Context.get_thms ctxt @{named_theorems metric_unfold})) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
56 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
57 |
fun pre_arith_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
58 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
59 |
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
|
60 |
K (trace_tac ctxt "Prepared for decision procedure") |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
61 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
62 |
fun dist_refl_sym_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
63 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
67 |
simp_tac refl_sym_ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
68 |
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
|
69 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
70 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
71 |
fun is_exists ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
72 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
73 |
Const (\<^const_name>\<open>HOL.Ex\<close>,_)$_ => true |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
74 |
| Const (\<^const_name>\<open>Trueprop\<close>,_)$_ => is_exists (Thm.dest_arg ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
75 |
| _ => false |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
76 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
77 |
fun is_forall ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
78 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
79 |
Const (\<^const_name>\<open>HOL.All\<close>,_)$_ => true |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
80 |
| Const (\<^const_name>\<open>Trueprop\<close>,_)$_ => is_forall (Thm.dest_arg ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
81 |
| _ => false |
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 |
fun dist_ty mty = mty --> mty --> \<^typ>\<open>real\<close> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
84 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
85 |
(* 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
|
86 |
fun find_points ctxt metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
87 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
88 |
fun find ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
89 |
(if Thm.typ_of_cterm ct = metric_ty then [ct] else []) @ ( |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
90 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
91 |
_ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
92 |
app_union_ct_pair find (Thm.dest_comb ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
93 |
| Abs (_, _, _) => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
94 |
(* ensure the point doesn't contain the bound variable *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
95 |
let val (var, bod) = Thm.dest_abs NONE ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
96 |
filter (free_in var #> not) (find bod) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
97 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
98 |
| _ => []) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
99 |
val points = find ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
100 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
101 |
case points of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
102 |
[] => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
103 |
(* if no point can be found, invent one *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
104 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
105 |
val free_name = Term.variant_frees (Thm.term_of ct) [("x", metric_ty)] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
106 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
107 |
map (Free #> Thm.cterm_of ctxt) free_name |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
108 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
109 |
| _ => points |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
110 |
end |
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 |
(* find all cterms "dist x y" in ct, where x and y have type metric_ty *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
113 |
fun find_dist metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
114 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
115 |
val dty = dist_ty metric_ty |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
116 |
fun find ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
117 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
118 |
Const (\<^const_name>\<open>dist\<close>, ty) $ _ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
119 |
if ty = dty then [ct] else [] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
120 |
| _ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
121 |
app_union_ct_pair find (Thm.dest_comb ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
122 |
| Abs (_, _, _) => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
123 |
let val (var, bod) = Thm.dest_abs NONE ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
124 |
filter (free_in var #> not) (find bod) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
125 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
126 |
| _ => [] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
127 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
128 |
find ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
129 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
130 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
131 |
(* find all "x=y", where x has type metric_ty *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
132 |
fun find_eq metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
133 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
134 |
fun find ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
135 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
136 |
Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ _ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
137 |
if fst (dest_funT ty) = metric_ty |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
138 |
then [ct] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
139 |
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
|
140 |
| _ $ _ => app_union_ct_pair find (Thm.dest_comb ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
141 |
| Abs (_, _, _) => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
142 |
let val (var, bod) = Thm.dest_abs NONE ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
143 |
filter (free_in var #> not) (find bod) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
144 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
145 |
| _ => [] |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
146 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
147 |
find ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
148 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
149 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
150 |
(* 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
|
151 |
fun maxdist_conv ctxt fset_ct ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
152 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
153 |
val (xct, yct) = Thm.dest_binop ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
154 |
val solve_prems = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
val image_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
158 |
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
|
159 |
val dist_refl_sym_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
160 |
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
|
161 |
val algebra_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
162 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
163 |
@{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
|
164 |
val insert_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
165 |
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
|
166 |
val sup_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
167 |
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
|
168 |
val real_abs_dist_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
169 |
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
|
170 |
val maxdist_thm = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
171 |
@{thm maxdist_thm} |> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
172 |
infer_instantiate' ctxt [SOME fset_ct, SOME xct, SOME yct] |> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
173 |
solve_prems |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
174 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
175 |
((Conv.rewr_conv maxdist_thm) then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
176 |
(* SUP to Sup *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
177 |
image_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
178 |
dist_refl_sym_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
179 |
algebra_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
180 |
(* eliminate duplicate terms in set *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
181 |
insert_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
182 |
(* Sup to max *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
183 |
sup_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
184 |
real_abs_dist_simp) ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
185 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
186 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
187 |
(* 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
|
188 |
fun metric_eq_conv ctxt fset_ct ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
189 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
190 |
val (xct, yct) = Thm.dest_binop ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
191 |
val solve_prems = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
192 |
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
|
193 |
addsimps @{thms empty_iff insert_iff}))) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
194 |
val ball_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
195 |
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps |
70954 | 196 |
@{thms Set.ball_empty ball_insert}) |
70951
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
197 |
val dist_refl_sym_simp = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
198 |
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
|
199 |
val metric_eq_thm = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
200 |
@{thm metric_eq_thm} |> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
201 |
infer_instantiate' ctxt [SOME xct, SOME fset_ct, SOME yct] |> |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
202 |
solve_prems |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
203 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
204 |
((Conv.rewr_conv metric_eq_thm) then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
205 |
(* convert \<forall>x\<in>{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \<and> ... \<and> P x\<^sub>n *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
206 |
ball_simp then_conv |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
207 |
dist_refl_sym_simp) ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
208 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
209 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
210 |
(* 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
|
211 |
fun augment_dist_pos ctxt metric_ty ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
212 |
let fun inst dist_ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
213 |
let val (xct, yct) = Thm.dest_binop dist_ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
214 |
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
|
215 |
in map inst (find_dist metric_ty ct) end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
216 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
217 |
fun top_sweep_rewrs_tac ctxt thms = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
218 |
CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt) |
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 |
(* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
221 |
fun embedding_tac ctxt metric_ty i goal = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
222 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
223 |
val ct = (Thm.cprem_of goal 1) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
224 |
val points = find_points ctxt metric_ty ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
225 |
val fset_ct = mk_ct_set ctxt metric_ty points |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
226 |
(* embed all subterms of the form "dist x y" in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
227 |
val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
228 |
(* replace point equality by equality of components in \<real>\<^sup>n *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
229 |
val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
230 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
231 |
( K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
232 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
233 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
234 |
(* decision procedure for linear real arithmetic *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
235 |
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
|
236 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
237 |
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
|
238 |
val ctxt' = argo_trace_ctxt ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
239 |
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
|
240 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
241 |
fun basic_metric_arith_tac ctxt metric_ty = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
242 |
HEADGOAL (dist_refl_sym_tac ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
243 |
IF_UNSOLVED' (embedding_tac ctxt metric_ty) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
244 |
IF_UNSOLVED' (pre_arith_tac ctxt) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
245 |
IF_UNSOLVED' (lin_real_arith_tac ctxt metric_ty)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
246 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
247 |
(* 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
|
248 |
if no dist terms are present, equality terms will be used *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
249 |
fun guess_metric ctxt ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
250 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
251 |
fun find_dist ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
252 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
253 |
Const (\<^const_name>\<open>dist\<close>, ty) $ _ $ _ => SOME (fst (dest_funT ty)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
254 |
| _ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
255 |
let val (s, t) = Thm.dest_comb ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
256 |
default (find_dist t) (find_dist s) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
257 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
258 |
| Abs (_, _, _) => find_dist (snd (Thm.dest_abs NONE ct)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
259 |
| _ => NONE |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
260 |
fun find_eq ct = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
261 |
case Thm.term_of ct of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
262 |
Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ x $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
263 |
let val (l, r) = Thm.dest_binop ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
264 |
if Sign.of_sort (Proof_Context.theory_of ctxt) (type_of x, \<^sort>\<open>metric_space\<close>) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
265 |
then SOME (fst (dest_funT ty)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
266 |
else default (find_dist r) (find_eq l) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
267 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
268 |
| _ $ _ => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
269 |
let val (s, t) = Thm.dest_comb ct in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
270 |
default (find_eq t) (find_eq s) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
271 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
272 |
| Abs (_, _, _) => find_eq (snd (Thm.dest_abs NONE ct)) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
273 |
| _ => NONE |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
274 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
275 |
case default (find_eq ct) (find_dist ct) of |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
276 |
SOME ty => ty |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
277 |
| NONE => error "No Metric Space was found" |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
278 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
279 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
280 |
(* eliminate \<exists> by proving the goal for a single witness from the metric space *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
281 |
fun elim_exists ctxt goal = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
282 |
let |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
283 |
val ct = Thm.cprem_of goal 1 |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
284 |
val metric_ty = guess_metric ctxt ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
285 |
val points = find_points ctxt metric_ty ct |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
286 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
287 |
fun try_point ctxt pt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
288 |
let val ex_rule = infer_instantiate' ctxt [NONE, SOME pt] @{thm exI} |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
289 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
290 |
HEADGOAL (resolve_tac ctxt [ex_rule] ORELSE' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
291 |
(* variable doesn't occur in body *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
292 |
resolve_tac ctxt @{thms exI}) THEN |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
293 |
trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
294 |
try_points ctxt |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
295 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
296 |
and try_points ctxt goal = ( |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
297 |
if is_exists (Thm.cprem_of goal 1) then |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
298 |
FIRST (map (try_point ctxt) points) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
299 |
else if is_forall (Thm.cprem_of goal 1) then |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
300 |
HEADGOAL (resolve_tac ctxt @{thms HOL.allI} THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
301 |
Subgoal.FOCUS (fn {context = ctxt', ...} => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
302 |
trace_tac ctxt "Removed universal quantifier" THEN |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
303 |
try_points ctxt') ctxt) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
304 |
else basic_metric_arith_tac ctxt metric_ty) goal |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
305 |
in |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
306 |
try_points ctxt goal |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
307 |
end |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
308 |
|
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
309 |
fun metric_arith_tac ctxt = |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
310 |
(* unfold common definitions to get rid of sets *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
311 |
unfold_tac ctxt THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
312 |
(* remove all meta-level connectives *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
313 |
IF_UNSOLVED' (Object_Logic.full_atomize_tac ctxt) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
314 |
(* convert goal to prenex form *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
315 |
IF_UNSOLVED' (prenex_tac ctxt) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
316 |
(* and NNF to ? *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
317 |
IF_UNSOLVED' (nnf_tac ctxt) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
318 |
(* turn all universally quantified variables into free variables, by focusing the subgoal *) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
319 |
REPEAT' (resolve_tac ctxt @{thms HOL.allI}) THEN' |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
320 |
IF_UNSOLVED' (SUBPROOF (fn {context=ctxt', ...} => |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
321 |
trace_tac ctxt' "Focused on subgoal" THEN |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
322 |
elim_exists ctxt') ctxt) |
678b2abe9f7d
decision procedure for metric spaces, implemented by Maximilian Schäffeler
immler
parents:
diff
changeset
|
323 |
end |