isabelle-cookbook: ProgTutorial/Base.thy@5734ab5dd86d (annotated)

23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	1	theory Base
459 4532577b61e0 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 441 diff changeset	2	imports Main
4532577b61e0 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 441 diff changeset	3	"~~/src/HOL/Library/LaTeXsugar"
535 5734ab5dd86d adapted to new build framework Christian Urban <urbanc@in.tum.de> parents: 517 diff changeset	4	(*keywords "ML" "setup" "local_setup" :: thy_decl and
514 7e25716c3744 updated to outer syntax / parser changes Christian Urban <urbanc@in.tum.de> parents: 488 diff changeset	5	"ML_prf" :: prf_decl and
7e25716c3744 updated to outer syntax / parser changes Christian Urban <urbanc@in.tum.de> parents: 488 diff changeset	6	"ML_val" :: diag
535 5734ab5dd86d adapted to new build framework Christian Urban <urbanc@in.tum.de> parents: 517 diff changeset	7	*)
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	8	uses
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	9	("output_tutorial.ML")
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	10	("antiquote_setup.ML")
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	11	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	12
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	13	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	14	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	15
396 a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	16	ML {*
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	17	fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	18
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	19	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	20	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	21
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	22	fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	23	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	24	(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	25
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	26	fun de_bruijn n =
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	27	HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	28	*}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	29
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	30	use "output_tutorial.ML"
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	31	use "antiquote_setup.ML"
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	32
471 f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	33	setup {* OutputTutorial.setup *}
f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	34	setup {* AntiquoteSetup.setup *}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	35
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	36	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 27 Aug 2012 10:24:10 +0100
changeset 535	5734ab5dd86d
parent 517	d8c376662bb4
child 538	e9fd5eff62c1
permissions	-rw-r--r--