author | haftmann |
Sun, 08 Oct 2017 22:28:21 +0200 | |
changeset 66812 | 7163b780549d |
parent 61841 | 4d3527b94f2a |
child 67149 | e61557884799 |
permissions | -rw-r--r-- |
30878 | 1 |
(* Title: HOL/Tools/arith_data.ML |
24095 | 2 |
Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
3 |
|
33359 | 4 |
Common arithmetic proof auxiliary and legacy. |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
6 |
|
26101 | 7 |
signature ARITH_DATA = |
8 |
sig |
|
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
9 |
val arith_tac: Proof.context -> int -> tactic |
59657
2441a80fb6c1
eliminated unused arith "verbose" flag -- tools that need options can use the context;
wenzelm
parents:
58820
diff
changeset
|
10 |
val add_tactic: string -> (Proof.context -> int -> tactic) -> theory -> theory |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
11 |
|
33359 | 12 |
val mk_number: typ -> int -> term |
13 |
val mk_sum: typ -> term list -> term |
|
14 |
val long_mk_sum: typ -> term list -> term |
|
15 |
val dest_sum: term -> term list |
|
16 |
||
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
17 |
val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option |
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
18 |
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
19 |
val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
20 |
val simp_all_tac: thm list -> Proof.context -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
21 |
val simplify_meta_eq: thm list -> Proof.context -> thm -> thm |
26101 | 22 |
end; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
23 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
24 |
structure Arith_Data: ARITH_DATA = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
25 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
26 |
|
57952 | 27 |
(* slot for plugging in tactics *) |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
28 |
|
33522 | 29 |
structure Arith_Tactics = Theory_Data |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
30 |
( |
59657
2441a80fb6c1
eliminated unused arith "verbose" flag -- tools that need options can use the context;
wenzelm
parents:
58820
diff
changeset
|
31 |
type T = (serial * (string * (Proof.context -> int -> tactic))) list; |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
32 |
val empty = []; |
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
33 |
val extend = I; |
33522 | 34 |
fun merge data : T = AList.merge (op =) (K true) data; |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
35 |
); |
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
36 |
|
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
37 |
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac))); |
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
38 |
|
59657
2441a80fb6c1
eliminated unused arith "verbose" flag -- tools that need options can use the context;
wenzelm
parents:
58820
diff
changeset
|
39 |
fun arith_tac ctxt = |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
40 |
let |
42361 | 41 |
val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt); |
59657
2441a80fb6c1
eliminated unused arith "verbose" flag -- tools that need options can use the context;
wenzelm
parents:
58820
diff
changeset
|
42 |
fun invoke (_, (_, tac)) k st = tac ctxt k st; |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
43 |
in FIRST' (map invoke (rev tactics)) end; |
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
44 |
|
58820 | 45 |
val _ = |
46 |
Theory.setup |
|
47 |
(Method.setup @{binding arith} |
|
48 |
(Scan.succeed (fn ctxt => |
|
49 |
METHOD (fn facts => |
|
50 |
HEADGOAL |
|
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
59657
diff
changeset
|
51 |
(Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts) |
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
59657
diff
changeset
|
52 |
THEN' arith_tac ctxt)))) |
58820 | 53 |
"various arithmetic decision procedures"); |
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
54 |
|
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
55 |
|
33359 | 56 |
(* some specialized syntactic operations *) |
57 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45620
diff
changeset
|
58 |
fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45620
diff
changeset
|
59 |
| mk_number T n = HOLogic.mk_number T n; |
33359 | 60 |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset
|
61 |
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
33359 | 62 |
|
50107 | 63 |
fun mk_minus t = |
33359 | 64 |
let val T = Term.fastype_of t |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset
|
65 |
in Const (@{const_name Groups.uminus}, T --> T) $ t end; |
33359 | 66 |
|
67 |
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
44945 | 68 |
fun mk_sum T [] = mk_number T 0 |
69 |
| mk_sum T [t, u] = mk_plus (t, u) |
|
33359 | 70 |
| mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
71 |
||
72 |
(*this version ALWAYS includes a trailing zero*) |
|
44945 | 73 |
fun long_mk_sum T [] = mk_number T 0 |
66812 | 74 |
| long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts); |
33359 | 75 |
|
76 |
(*decompose additions AND subtractions as a sum*) |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset
|
77 |
fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) = |
44945 | 78 |
dest_summing (pos, t, dest_summing (pos, u, ts)) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset
|
79 |
| dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) = |
44945 | 80 |
dest_summing (pos, t, dest_summing (not pos, u, ts)) |
81 |
| dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts; |
|
33359 | 82 |
|
83 |
fun dest_sum t = dest_summing (true, t, []); |
|
84 |
||
85 |
||
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
86 |
(* various auxiliary and legacy *) |
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset
|
87 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
88 |
fun prove_conv_nohyps tacs ctxt (t, u) = |
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
89 |
if t aconv u then NONE |
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
90 |
else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
91 |
in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end; |
26101 | 92 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
93 |
fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt; |
26101 | 94 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
95 |
fun prove_conv2 expand_tac norm_tac ctxt tu = (* FIXME avoid Drule.export_without_context *) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
96 |
mk_meta_eq (Drule.export_without_context (Goal.prove ctxt [] [] |
26101 | 97 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
98 |
(K (EVERY [expand_tac, norm_tac ctxt])))); |
26101 | 99 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
100 |
fun simp_all_tac rules ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
101 |
ALLGOALS (safe_simp_tac (put_simpset HOL_ss ctxt addsimps rules)); |
26101 | 102 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
103 |
fun simplify_meta_eq rules ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
104 |
simplify (put_simpset HOL_basic_ss ctxt addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50107
diff
changeset
|
105 |
o mk_meta_eq; |
30518 | 106 |
|
24095 | 107 |
end; |