author | haftmann |
Wed, 07 Oct 2009 14:01:26 +0200 | |
changeset 32887 | 85e7ab9020ba |
parent 32155 | e2bf2f73b0c8 |
child 32957 | 675c0c7e6a37 |
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 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
4 |
Common arithmetic proof auxiliary. |
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 |
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
|
10 |
val verbose_arith_tac: Proof.context -> int -> tactic |
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 |
val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory |
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
|
12 |
val get_arith_facts: Proof.context -> thm list |
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
|
13 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
14 |
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
|
15 |
val prove_conv: tactic list -> Proof.context -> thm list -> 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
|
16 |
val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm |
29302 | 17 |
val simp_all_tac: thm list -> simpset -> tactic |
30518 | 18 |
val simplify_meta_eq: thm list -> simpset -> thm -> thm |
19 |
val trans_tac: thm option -> tactic |
|
32155 | 20 |
val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option) |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
21 |
-> simproc |
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
|
22 |
|
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
|
23 |
val setup: theory -> theory |
26101 | 24 |
end; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
25 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
26 |
structure Arith_Data: ARITH_DATA = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
27 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
28 |
|
30878 | 29 |
(* slots for plugging in arithmetic facts and 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
|
30 |
|
31902 | 31 |
structure Arith_Facts = Named_Thms |
32 |
( |
|
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
|
33 |
val name = "arith" |
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
|
34 |
val description = "arith facts - only ground formulas" |
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 |
val get_arith_facts = Arith_Facts.get; |
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 |
|
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
|
39 |
structure Arith_Tactics = TheoryDataFun |
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 |
( |
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
|
41 |
type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; |
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
|
42 |
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
|
43 |
val copy = I; |
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 |
val extend = I; |
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
|
45 |
fun merge _ = AList.merge (op =) (K true); |
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
|
46 |
); |
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
|
47 |
|
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
|
48 |
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
|
49 |
|
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
|
50 |
fun gen_arith_tac verbose ctxt = |
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
|
51 |
let |
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
|
52 |
val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt |
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
|
53 |
fun invoke (_, (name, tac)) k st = (if verbose |
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 |
then warning ("Trying " ^ name ^ "...") else (); |
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 |
tac verbose ctxt k st); |
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
|
56 |
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
|
57 |
|
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
|
58 |
val arith_tac = gen_arith_tac false; |
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
|
59 |
val verbose_arith_tac = gen_arith_tac true; |
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
|
60 |
|
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
61 |
val setup = |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
62 |
Arith_Facts.setup #> |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
63 |
Method.setup @{binding arith} |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
64 |
(Args.bang_facts >> (fn prems => fn ctxt => |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
65 |
METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts) |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
66 |
THEN' verbose_arith_tac ctxt)))) |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset
|
67 |
"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
|
68 |
|
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
|
69 |
|
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
|
70 |
(* 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
|
71 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end; |
26101 | 76 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
77 |
fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt; |
26101 | 78 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
79 |
fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*) |
26101 | 80 |
mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] [] |
81 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
|
82 |
(K (EVERY [expand_tac, norm_tac ss])))); |
|
83 |
||
84 |
fun simp_all_tac rules = |
|
85 |
let val ss0 = HOL_ss addsimps rules |
|
86 |
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
87 |
||
30518 | 88 |
fun simplify_meta_eq rules = |
89 |
let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules |
|
90 |
in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end |
|
91 |
||
92 |
fun trans_tac NONE = all_tac |
|
93 |
| trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); |
|
94 |
||
32155 | 95 |
fun prep_simproc thy (name, pats, proc) = |
96 |
Simplifier.simproc thy name pats proc; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
97 |
|
24095 | 98 |
end; |