Quelle Suc_Notation.thy Sprache: Isabelle

(*  Title:      HOL/Library/Suc_Notation.thy
    Author:     Manuel Eberl and Tobias Nipkow

Compact notation for nested \<open>Suc\<close> terms. Just notation. Use standard numerals for large numbers.
*)

theory Suc_Notation
imports Main
begin

text \<open>Nested \<open>Suc\<close> terms of depth \<open>2 \<le> n \<le> 9\<close> are abbreviated with new notations \<open>Suc\<^sup>n\<close>:\<close>

abbreviation (input) Suc2 where "Suc2 n \ Suc (Suc n)"
abbreviation (input) Suc3 where "Suc3 n \ Suc (Suc2 n)"
abbreviation (input) Suc4 where "Suc4 n \ Suc (Suc3 n)"
abbreviation (input) Suc5 where "Suc5 n \ Suc (Suc4 n)"
abbreviation (input) Suc6 where "Suc6 n \ Suc (Suc5 n)"
abbreviation (input) Suc7 where "Suc7 n \ Suc (Suc6 n)"
abbreviation (input) Suc8 where "Suc8 n \ Suc (Suc7 n)"
abbreviation (input) Suc9 where "Suc9 n \ Suc (Suc8 n)"

notation Suc2 ("Suc\<^sup>2")
notation Suc3 ("Suc\<^sup>3")
notation Suc4 ("Suc\<^sup>4")
notation Suc5 ("Suc\<^sup>5")
notation Suc6 ("Suc\<^sup>6")
notation Suc7 ("Suc\<^sup>7")
notation Suc8 ("Suc\<^sup>8")
notation Suc9 ("Suc\<^sup>9")

text \<open>Beyond 9, the syntax \<open>Suc\<^bsup>n\<^esup>\<close> kicks in:\<close>

syntax
  "_Suc_tower" :: "num_token \ nat \ nat" ("Suc\<^bsup>_\<^esup>")

parse_translation \<open>
  let
    fun mk_sucs_aux 0 t = t
      | mk_sucs_aux n t = mk_sucs_aux (n - 1) (\<^const>\<open>Suc\<close> $ t)
    fun mk_sucs n = Abs("n", \<^typ>\<open>nat\<close>, mk_sucs_aux n (Bound 0))

    fun Suc_tr [Free (str, _)] = mk_sucs (the (Int.fromString str))

  in [(\<^syntax_const>\<open>_Suc_tower\<close>, K Suc_tr)] end
\<close>

print_translation \<open>
  let
    val digit_consts =
        [\<^const_syntax>\<open>Suc2\<close>, \<^const_syntax>\<open>Suc3\<close>, \<^const_syntax>\<open>Suc4\<close>, \<^const_syntax>\<open>Suc5\<close>,
         \<^const_syntax>\<open>Suc6\<close>, \<^const_syntax>\<open>Suc7\<close>, \<^const_syntax>\<open>Suc8\<close>, \<^const_syntax>\<open>Suc9\<close>]
    val num_token_T = Simple_Syntax.read_typ "num_token"
    val T = num_token_T --> HOLogic.natT --> HOLogic.natT
    fun mk_num_token n = Free (Int.toString n, num_token_T)
    fun dest_Suc_tower (Const (\<^const_syntax>\<open>Suc\<close>, _) $ t) acc =
          dest_Suc_tower t (acc + 1)
      | dest_Suc_tower t acc = (t, acc)

    fun Suc_tr' [t] =
      let
        val (t', n) = dest_Suc_tower t 1
      in
        if n > 9 then
          Const (\<^syntax_const>\<open>_Suc_tower\<close>, T) $ mk_num_token n $ t'
        else if n > 1 then
          Const (List.nth (digit_consts, n - 2), T) $ t'
        else
          raise Match
      end

  in [(\<^const_syntax>\<open>Suc\<close>, K Suc_tr')]
end
\<close>

(* Tests

ML \<open>
local
  fun mk 0 = \<^term>\<open>x :: nat\<close>
    | mk n = \<^const>\<open>Suc\<close> $ mk (n - 1)
  val ctxt' = Variable.add_fixes_implicit @{term "x :: nat"} @{context}
in
  val _ =
    map_range (fn n => (n + 1, mk (n + 1))) 20
    |> map (fn (n, t) =>
         Pretty.block [Pretty.str (Int.toString n ^ ": "),
           Syntax.pretty_term ctxt' t] |> Pretty.writeln)
end
\<close>

(* test parsing *)
term "Suc x"
term "Suc\<^sup>2 x"
term "Suc\<^sup>3 x"
term "Suc\<^sup>4 x"
term "Suc\<^sup>5 x"
term "Suc\<^sup>6 x"
term "Suc\<^sup>7 x"
term "Suc\<^sup>8 x"
term "Suc\<^sup>9 x"

term "Suc\<^bsup>2\<^esup> x"
term "Suc\<^bsup>3\<^esup> x"
term "Suc\<^bsup>4\<^esup> x"
term "Suc\<^bsup>5\<^esup> x"
term "Suc\<^bsup>6\<^esup> x"
term "Suc\<^bsup>7\<^esup> x"
term "Suc\<^bsup>8\<^esup> x"
term "Suc\<^bsup>9\<^esup> x"
term "Suc\<^bsup>10\<^esup> x"
term "Suc\<^bsup>11\<^esup> x"
term "Suc\<^bsup>12\<^esup> x"
term "Suc\<^bsup>13\<^esup> x"
term "Suc\<^bsup>14\<^esup> x"
term "Suc\<^bsup>15\<^esup> x"
term "Suc\<^bsup>16\<^esup> x"
term "Suc\<^bsup>17\<^esup> x"
term "Suc\<^bsup>18\<^esup> x"
term "Suc\<^bsup>19\<^esup> x"
term "Suc\<^bsup>20\<^esup> x"

(* check that the notation really means the right thing *)
lemma "Suc\<^sup>2 n = n+2 \ Suc\<^sup>3 n = n+3 \ Suc\<^sup>4 n = n+4 \ Suc\<^sup>5 n = n+5
  \<and> Suc\<^sup>6 n = n+6 \<and> Suc\<^sup>7 n = n+7 \<and> Suc\<^sup>8 n = n+8 \<and> Suc\<^sup>9 n = n+9"
by simp

lemma "Suc\<^bsup>10\<^esup> n = n+10 \ Suc\<^bsup>11\<^esup> n = n+11 \ Suc\<^bsup>12\<^esup> n = n+12 \ Suc\<^bsup>13\<^esup> n = n+13
  \<and> Suc\<^bsup>14\<^esup> n = n+14 \<and> Suc\<^bsup>15\<^esup> n = n+15 \<and> Suc\<^bsup>16\<^esup> n = n+16 \<and> Suc\<^bsup>17\<^esup> n = n+17
  \<and> Suc\<^bsup>18\<^esup> n = n+18 \<and> Suc\<^bsup>19\<^esup> n = n+19 \<and> Suc\<^bsup>20\<^esup> n = n+20"
by simp

*)

end

quality98%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.