isabelle-cookbook: ProgTutorial/Base.thy@77ea2de0ca62 (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"
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	4	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	5
394 0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	6	notation (latex output)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	7	Cons ("_ # _" [66,65] 65)
0019ebf76e10 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	8
396 a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	9	ML {*
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	10	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	11
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	12	fun rhs 1 = P 1
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	13	\| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	14
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	15	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	16	\| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	17	(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	18
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	19	fun de_bruijn n =
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	20	HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
a2e49e0771b3 tuned Christian Urban <urbanc@in.tum.de> parents: 394 diff changeset	21	*}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	22
538 e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	23	ML_file "output_tutorial.ML"
e9fd5eff62c1 removed "use" for "ML_file" Christian Urban <urbanc@in.tum.de> parents: 535 diff changeset	24	ML_file "antiquote_setup.ML"
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	25
471 f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	26	setup {* OutputTutorial.setup *}
f65b9f14d5de updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 462 diff changeset	27	setup {* AntiquoteSetup.setup *}
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 328 diff changeset	28
239 b63c72776f03 replaced "warning" with "writeln" Christian Urban <urbanc@in.tum.de> parents: 224 diff changeset	29	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 08 Jul 2014 11:34:10 +0100
changeset 557	77ea2de0ca62
parent 538	e9fd5eff62c1
child 562	daf404920ab9
permissions	-rw-r--r--