author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 35761  c4a698ee83b4 
child 38715  6513ea67d95d 
permissions  rwrr 
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_arithtac 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_arithtac 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_arithtac 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_arithtac 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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

13 

33359  14 
val mk_number: typ > int > term 
15 
val mk_sum: typ > term list > term 

16 
val long_mk_sum: typ > term list > term 

17 
val dest_sum: term > term list 

18 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

19 
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

20 
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

21 
val prove_conv2: tactic > (simpset > tactic) > simpset > term * term > thm 
29302  22 
val simp_all_tac: thm list > simpset > tactic 
30518  23 
val simplify_meta_eq: thm list > simpset > thm > thm 
24 
val trans_tac: thm option > tactic 

32155  25 
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

26 
> simproc 
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

27 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

28 
val setup: theory > theory 
26101  29 
end; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

30 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

31 
structure Arith_Data: ARITH_DATA = 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

32 
struct 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

33 

30878  34 
(* 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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

35 

31902  36 
structure Arith_Facts = Named_Thms 
37 
( 

30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

38 
val name = "arith" 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

39 
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_arithtac 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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

41 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

42 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

43 

33522  44 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

45 
( 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

46 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

47 
val empty = []; 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

48 
val extend = I; 
33522  49 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

50 
); 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

51 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

52 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

53 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

54 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

55 
let 
35761
c4a698ee83b4
reverted fe9b43a08187  "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents:
35636
diff
changeset

56 
val tactics = Arith_Tactics.get (ProofContext.theory_of ctxt); 
c4a698ee83b4
reverted fe9b43a08187  "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents:
35636
diff
changeset

57 
fun invoke (_, (name, tac)) k st = 
c4a698ee83b4
reverted fe9b43a08187  "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents:
35636
diff
changeset

58 
(if verbose then warning ("Trying " ^ name ^ "...") else (); 
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

59 
tac verbose ctxt k st); 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

60 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

61 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

62 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

63 
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_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

64 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset

65 
val setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset

66 
Arith_Facts.setup #> 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset

67 
Method.setup @{binding arith} 
33554  68 
(Scan.succeed (fn ctxt => 
69 
METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts) 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset

70 
THEN' verbose_arith_tac ctxt)))) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30686
diff
changeset

71 
"various arithmetic decision procedures"; 
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

72 

47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

73 

33359  74 
(* some specialized syntactic operations *) 
75 

76 
fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; 

77 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset

78 
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; 
33359  79 

80 
fun mk_minus t = 

81 
let val T = Term.fastype_of t 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset

82 
in Const (@{const_name Groups.uminus}, T > T) $ t end; 
33359  83 

84 
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) 

85 
fun mk_sum T [] = mk_number T 0 

86 
 mk_sum T [t,u] = mk_plus (t, u) 

87 
 mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); 

88 

89 
(*this version ALWAYS includes a trailing zero*) 

90 
fun long_mk_sum T [] = mk_number T 0 

91 
 long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); 

92 

93 
(*decompose additions AND subtractions as a sum*) 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35021
diff
changeset

94 
fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) = 
33359  95 
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

96 
 dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) = 
33359  97 
dest_summing (pos, t, dest_summing (not pos, u, ts)) 
98 
 dest_summing (pos, t, ts) = 

99 
if pos then t::ts else mk_minus t :: ts; 

100 

101 
fun dest_sum t = dest_summing (true, t, []); 

102 

103 

30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

104 
(* various auxiliary and legacy *) 
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arithtac now named linear_arith_tac
haftmann
parents:
30518
diff
changeset

105 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

106 
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

107 
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

108 
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

109 
in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end; 
26101  110 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset

111 
fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt; 
26101  112 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34974
diff
changeset

113 
fun prove_conv2 expand_tac norm_tac ss tu = (* FIXME avoid Drule.export_without_context *) 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34974
diff
changeset

114 
mk_meta_eq (Drule.export_without_context (Goal.prove (Simplifier.the_context ss) [] [] 
26101  115 
(HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) 
116 
(K (EVERY [expand_tac, norm_tac ss])))); 

117 

118 
fun simp_all_tac rules = 

119 
let val ss0 = HOL_ss addsimps rules 

120 
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; 

121 

30518  122 
fun simplify_meta_eq rules = 
35410  123 
let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules 
30518  124 
in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end 
125 

126 
fun trans_tac NONE = all_tac 

127 
 trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); 

128 

32155  129 
fun prep_simproc thy (name, pats, proc) = 
130 
Simplifier.simproc thy name pats proc; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

131 

24095  132 
end; 