Quelle  Suc_Notation.thy

(*  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) (🍋‹Suc› $ t)
  fun mk_sucs n = Abs("n", 🍋‹nat›, mk_sucs_aux n (Bound 0))
 
  fun Suc_tr [Free (str, _)] = mk_sucs (the (Int.fromString str))
 
  in [(🍋‹_Suc_tower›, K Suc_tr)] end
 ›

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

(* Tests
 
 ML ‹
 local
  fun mk 0 = 🍋‹x :: nat›
  | mk n = 🍋‹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