1023 section {* Simprocs *}

  1023 section {* Simprocs *}

  1024 

  1024 

  1025 text {*

  1025 text {*

  1026   In Isabelle you can also implement custom simplification procedures, called

  1026   In Isabelle you can also implement custom simplification procedures, called

  1027   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and

  1027   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and

  1029   a rewriting rule must be produced on ``demand'' or when rewriting by

  1029   a rewriting rule must be produced on ``demand'' or when rewriting by

  1030   simplification is too unpredictable and potentially loops.

  1030   simplification is too unpredictable and potentially loops.

  1031 

  1031 

  1032   To see how simprocs work, let us first write a simproc that just prints out

  1032   To see how simprocs work, let us first write a simproc that just prints out

  1033   the pattern which triggers it and otherwise does nothing. For this

  1033   the pattern which triggers it and otherwise does nothing. For this

  1230 text {*

  1230 text {*

  1231   From the integer value it generates the corresponding number term, called 

  1231   From the integer value it generates the corresponding number term, called 

  1232   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 

  1232   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 

  1233   (Line 4), which it proves by the arithmetic tactic in Line 6. 

  1233   (Line 4), which it proves by the arithmetic tactic in Line 6. 

  1234 

  1234 

  1236   fine, but there is also an alternative employing the simplifier with a very

  1236   fine, but there is also an alternative employing the simplifier with a very

  1237   restricted simpset. For the kind of lemmas we want to prove, the simpset

  1237   restricted simpset. For the kind of lemmas we want to prove, the simpset

  1238   @{text "num_ss"} in the code will suffice.

  1238   @{text "num_ss"} in the code will suffice.

  1239 *}

  1239 *}

  1240 

  1240