summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Arith_Examples.thy

changeset 23218 | 01c4d19f597e |

parent 23211 | 4d56ad10b5e8 |

child 24075 | 366d4d234814 |

1.1 --- a/src/HOL/ex/Arith_Examples.thy Sun Jun 03 23:16:45 2007 +0200 1.2 +++ b/src/HOL/ex/Arith_Examples.thy Sun Jun 03 23:16:46 2007 +0200 1.3 @@ -3,35 +3,35 @@ 1.4 Author: Tjark Weber 1.5 *) 1.6 1.7 -header {* {\tt arith} *} 1.8 +header {* Arithmetic *} 1.9 1.10 theory Arith_Examples imports Main begin 1.11 1.12 text {* 1.13 - The {\tt arith} tactic is used frequently throughout the Isabelle 1.14 + The @{text arith} method is used frequently throughout the Isabelle 1.15 distribution. This file merely contains some additional tests and special 1.16 corner cases. Some rather technical remarks: 1.17 1.18 - \verb!fast_arith_tac! is a very basic version of the tactic. It performs no 1.19 + @{ML fast_arith_tac} is a very basic version of the tactic. It performs no 1.20 meta-to-object-logic conversion, and only some splitting of operators. 1.21 - \verb!simple_arith_tac! performs meta-to-object-logic conversion, full 1.22 - splitting of operators, and NNF normalization of the goal. The {\tt arith} 1.23 - tactic combines them both, and tries other tactics (e.g.~{\tt presburger}) 1.24 + @{ML simple_arith_tac} performs meta-to-object-logic conversion, full 1.25 + splitting of operators, and NNF normalization of the goal. The @{text arith} 1.26 + method combines them both, and tries other methods (e.g.~@{text presburger}) 1.27 as well. This is the one that you should use in your proofs! 1.28 1.29 - An {\tt arith}-based simproc is available as well 1.30 - (see \verb!Fast_Arith.lin_arith_prover!), 1.31 + An @{text arith}-based simproc is available as well 1.32 + (see @{ML Fast_Arith.lin_arith_prover}), 1.33 which---for performance reasons---however 1.34 - does even less splitting than \verb!fast_arith_tac! at the moment (namely 1.35 + does even less splitting than @{ML fast_arith_tac} at the moment (namely 1.36 inequalities only). (On the other hand, it does take apart conjunctions, 1.37 - which \verb!fast_arith_tac! currently does not do.) 1.38 + which @{ML fast_arith_tac} currently does not do.) 1.39 *} 1.40 1.41 (* 1.42 ML {* set trace_arith; *} 1.43 *) 1.44 1.45 -section {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, 1.46 +subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, 1.47 @{term HOL.minus}, @{term nat}, @{term Divides.mod}, 1.48 @{term Divides.div} *} 1.49 1.50 @@ -130,7 +130,8 @@ 1.51 apply (tactic {* LA_Data_Ref.pre_tac 1 *}) 1.52 oops 1.53 1.54 -section {* Meta-Logic *} 1.55 + 1.56 +subsection {* Meta-Logic *} 1.57 1.58 lemma "x < Suc y == x <= y" 1.59 by (tactic {* simple_arith_tac 1 *}) 1.60 @@ -138,7 +139,8 @@ 1.61 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y" 1.62 by (tactic {* simple_arith_tac 1 *}) 1.63 1.64 -section {* Various Other Examples *} 1.65 + 1.66 +subsection {* Various Other Examples *} 1.67 1.68 lemma "(x < Suc y) = (x <= y)" 1.69 by (tactic {* simple_arith_tac 1 *})