Theory Suc_Notation

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

Compact notation for nested ‹Suc› terms. Just notation. Use standard numerals for large numbers.
*)

theory Suc_Notation
imports Main
begin

text ‹Nested ‹Suc› terms of depth ‹2 ≤ n ≤ 9› are abbreviated with new notations ‹Suc⇧n›:›

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⇧2")
notation Suc3 ("Suc⇧3")
notation Suc4 ("Suc⇧4")
notation Suc5 ("Suc⇧5")
notation Suc6 ("Suc⇧6")
notation Suc7 ("Suc⇧7")
notation Suc8 ("Suc⇧8")
notation Suc9 ("Suc⇧9")

text ‹Beyond 9, the syntax ‹Suc⇗n⇖› kicks in:›

syntax
  "_Suc_tower" :: "num_token ⇒ nat ⇒ nat"  ("Suc⇗_⇖")

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

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

  in [(\<^syntax_const>‹_Suc_tower›, K Suc_tr)] end
›

print_translation ‹
  let
    val digit_consts =
        [\<^const_syntax>‹Suc2›, \<^const_syntax>‹Suc3›, \<^const_syntax>‹Suc4›, \<^const_syntax>‹Suc5›,
         \<^const_syntax>‹Suc6›, \<^const_syntax>‹Suc7›, \<^const_syntax>‹Suc8›, \<^const_syntax>‹Suc9›]
    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>‹Suc›, _) $ 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>‹_Suc_tower›, 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>‹Suc›, K Suc_tr')]
 end
›

(* Tests

ML ‹
local
  fun mk 0 = \<^term>‹x :: nat›
    | mk n = \<^const>‹Suc› $ 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
›

(* test parsing *)
term "Suc x"
term "Suc⇧2 x"
term "Suc⇧3 x"
term "Suc⇧4 x"
term "Suc⇧5 x"
term "Suc⇧6 x"
term "Suc⇧7 x"
term "Suc⇧8 x"
term "Suc⇧9 x"

term "Suc⇗2⇖ x"
term "Suc⇗3⇖ x"
term "Suc⇗4⇖ x"
term "Suc⇗5⇖ x"
term "Suc⇗6⇖ x"
term "Suc⇗7⇖ x"
term "Suc⇗8⇖ x"
term "Suc⇗9⇖ x"
term "Suc⇗10⇖ x"
term "Suc⇗11⇖ x"
term "Suc⇗12⇖ x"
term "Suc⇗13⇖ x"
term "Suc⇗14⇖ x"
term "Suc⇗15⇖ x"
term "Suc⇗16⇖ x"
term "Suc⇗17⇖ x"
term "Suc⇗18⇖ x"
term "Suc⇗19⇖ x"
term "Suc⇗20⇖ x"

(* check that the notation really means the right thing *)
lemma "Suc⇧2 n = n+2 ∧ Suc⇧3 n = n+3 ∧ Suc⇧4 n = n+4 ∧ Suc⇧5 n = n+5
  ∧ Suc⇧6 n = n+6 ∧ Suc⇧7 n = n+7 ∧ Suc⇧8 n = n+8 ∧ Suc⇧9 n = n+9"
by simp

lemma "Suc⇗10⇖ n = n+10 ∧ Suc⇗11⇖ n = n+11 ∧ Suc⇗12⇖ n = n+12 ∧ Suc⇗13⇖ n = n+13
  ∧ Suc⇗14⇖ n = n+14 ∧ Suc⇗15⇖ n = n+15 ∧ Suc⇗16⇖ n = n+16 ∧ Suc⇗17⇖ n = n+17
  ∧ Suc⇗18⇖ n = n+18 ∧ Suc⇗19⇖ n = n+19 ∧ Suc⇗20⇖ n = n+20"
by simp

*)

end