23
|
1 |
theory Base
|
459
|
2 |
imports Main
|
|
3 |
"~~/src/HOL/Library/LaTeXsugar"
|
535
|
4 |
(*keywords "ML" "setup" "local_setup" :: thy_decl and
|
514
|
5 |
"ML_prf" :: prf_decl and
|
|
6 |
"ML_val" :: diag
|
535
|
7 |
*)
|
23
|
8 |
begin
|
|
9 |
|
394
|
10 |
notation (latex output)
|
|
11 |
Cons ("_ # _" [66,65] 65)
|
|
12 |
|
396
|
13 |
ML {*
|
|
14 |
fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
|
|
15 |
|
|
16 |
fun rhs 1 = P 1
|
|
17 |
| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
|
|
18 |
|
|
19 |
fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
|
|
20 |
| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
|
|
21 |
(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
|
|
22 |
|
|
23 |
fun de_bruijn n =
|
|
24 |
HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
|
|
25 |
*}
|
346
|
26 |
|
538
|
27 |
ML_file "output_tutorial.ML"
|
|
28 |
ML_file "antiquote_setup.ML"
|
346
|
29 |
|
471
|
30 |
setup {* OutputTutorial.setup *}
|
|
31 |
setup {* AntiquoteSetup.setup *}
|
346
|
32 |
|
239
|
33 |
end |