theory Base

imports Main 

        "~~/src/HOL/Library/LaTeXsugar"

keywords "ML" "setup" "local_setup" :: thy_decl and

         "ML_prf" :: prf_decl and

         "ML_val" :: diag

uses

  ("output_tutorial.ML")

  ("antiquote_setup.ML")

begin

notation (latex output)

  Cons ("_ # _" [66,65] 65)

ML {*

fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 

fun rhs 1 = P 1

  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))

fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)

  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 

                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)

fun de_bruijn n =

  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))

*}

use "output_tutorial.ML"

use "antiquote_setup.ML"

setup {* OutputTutorial.setup *}

setup {* AntiquoteSetup.setup *}

end