isabelle-cookbook: CookBook/Solutions.thy@126646f2aa88 (annotated)

15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Solutions
25 e2f9f94b26d4 Antiquotation setup is now contained in theory Base. berghofe parents: 15 diff changeset	2	imports Base
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	chapter {* Solutions to Most Exercises *}
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	text {* \solution{fun:revsum} *}
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	ML {*
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	10	fun rev_sum t =
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	11	let
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	12	fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	13	\| dest_sum u = [u]
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	14	in
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	15	foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	16	end;
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	*}
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	text {* \solution{fun:makesum} *}
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	ML {*
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	22	fun make_sum t1 t2 =
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 35 diff changeset	23	HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	*}
9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
56 126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	26	text {* \solution{ex:scancmts} *}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	27
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	28	ML {*
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	29	val any = Scan.one (Symbol.not_eof);
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	30
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	31	val scan_cmt =
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	32	let
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	33	val begin_cmt = Scan.this_string "(*"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	34	val end_cmt = Scan.this_string "*)"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	35	in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	36	begin_cmt \|-- Scan.repeat (Scan.unless end_cmt any) --\| end_cmt
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	37	>> (enclose "(" ")" o implode)
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	38	end
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	39
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	40	val scan_all =
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	41	Scan.finite Symbol.stopper (Scan.repeat (scan_cmt \|\| any))
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	42	>> implode #> fst
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	43	*}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	44
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	45	text {*
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	46	By using @{ML_text "#> fst"} in the last line, the function
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	47	@{ML scan_all} retruns a string instead of a pair. For example:
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	48
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	49	@{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	50
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	51	@{ML_response [display] "scan_all (explode \"foo (test) bar (test)\")"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	52	"\"foo (test) bar (test)\""}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	53
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	54	*}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	55
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 16 Dec 2008 08:08:44 +0000 (2008-12-16)
changeset 56	126646f2aa88
parent 47	4daf913fdbe1
child 58	f3794c231898
permissions	-rw-r--r--