equal
deleted
inserted
replaced
7 signature ARITH_DATA = |
7 signature ARITH_DATA = |
8 sig |
8 sig |
9 val arith_tac: Proof.context -> int -> tactic |
9 val arith_tac: Proof.context -> int -> tactic |
10 val verbose_arith_tac: Proof.context -> int -> tactic |
10 val verbose_arith_tac: Proof.context -> int -> tactic |
11 val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory |
11 val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory |
12 val get_arith_facts: Proof.context -> thm list |
|
13 |
12 |
14 val mk_number: typ -> int -> term |
13 val mk_number: typ -> int -> term |
15 val mk_sum: typ -> term list -> term |
14 val mk_sum: typ -> term list -> term |
16 val long_mk_sum: typ -> term list -> term |
15 val long_mk_sum: typ -> term list -> term |
17 val dest_sum: term -> term list |
16 val dest_sum: term -> term list |
26 end; |
25 end; |
27 |
26 |
28 structure Arith_Data: ARITH_DATA = |
27 structure Arith_Data: ARITH_DATA = |
29 struct |
28 struct |
30 |
29 |
31 (* slots for plugging in arithmetic facts and tactics *) |
30 (* slot for plugging in tactics *) |
32 |
|
33 structure Arith_Facts = Named_Thms |
|
34 ( |
|
35 val name = @{binding arith} |
|
36 val description = "arith facts -- only ground formulas" |
|
37 ); |
|
38 |
|
39 val get_arith_facts = Arith_Facts.get; |
|
40 |
31 |
41 structure Arith_Tactics = Theory_Data |
32 structure Arith_Tactics = Theory_Data |
42 ( |
33 ( |
43 type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; |
34 type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; |
44 val empty = []; |
35 val empty = []; |
56 |
47 |
57 val arith_tac = gen_arith_tac false; |
48 val arith_tac = gen_arith_tac false; |
58 val verbose_arith_tac = gen_arith_tac true; |
49 val verbose_arith_tac = gen_arith_tac true; |
59 |
50 |
60 val setup = |
51 val setup = |
61 Arith_Facts.setup #> |
|
62 Method.setup @{binding arith} |
52 Method.setup @{binding arith} |
63 (Scan.succeed (fn ctxt => |
53 (Scan.succeed (fn ctxt => |
64 METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts) |
54 METHOD (fn facts => |
65 THEN' verbose_arith_tac ctxt)))) |
55 HEADGOAL |
|
56 (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts) |
|
57 THEN' verbose_arith_tac ctxt)))) |
66 "various arithmetic decision procedures"; |
58 "various arithmetic decision procedures"; |
67 |
59 |
68 |
60 |
69 (* some specialized syntactic operations *) |
61 (* some specialized syntactic operations *) |
70 |
62 |