(*  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 ‹Nested ‹Suc› terms of depth ‹2 ≤ n ≤ 9› are abbreviated with new notations ‹Sucⁿ›:›

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²")
notation Suc3 ("Suc³")
notation Suc4 ("Suc⁴")
notation Suc5 ("Suc⁵")
notation Suc6 ("Suc⁶")
notation Suc7 ("Suc⁷")
notation Suc8 ("Suc⁸")
notation Suc9 ("Suc⁹")

text ‹Beyond 9, the syntax ‹Suc› 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 \<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² x"
term "Suc³ x"
term "Suc⁴ x"
term "Suc⁵ x"
term "Suc⁶ x"
term "Suc⁷ x"
term "Suc⁸ x"
term "Suc⁹ x"

term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"
term "Suc x"

(* check that the notation really means the right thing *)
lemma "Suc² n = n+2 ∧ Suc³ n = n+3 ∧ Suc⁴ n = n+4 ∧ Suc⁵ n = n+5
  ∧ Suc⁶ n = n+6 ∧ Suc⁷ n = n+7 ∧ Suc⁸ n = n+8 ∧ Suc⁹ n = n+9"
by simp

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

*)

end