added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
theory Solutionsimports Baseuses "infix_conv.ML"beginchapter {* Solutions to Most Exercises *}text {* \solution{fun:revsum} *}ML{*fun rev_sum t =let fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u | dest_sum u = [u]in foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)end *}text {* \solution{fun:makesum} *}ML{*fun make_sum t1 t2 = HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}text {* \solution{ex:scancmts} *}ML{*val any = Scan.one (Symbol.not_eof)val scan_cmt = let val begin_cmt = Scan.this_string "(*" val end_cmt = Scan.this_string "*)" in begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt >> (enclose "(**" "**)" o implode) endval parser = Scan.repeat (scan_cmt || any)val scan_all = Scan.finite Symbol.stopper parser >> implode #> fst *}text {* By using @{text "#> fst"} in the last line, the function @{ML scan_all} retruns a string, instead of the pair a parser would normally return. For example: @{ML_response [display,gray]"let val input1 = (explode \"foo bar\") val input2 = (explode \"foo (*test*) bar (*test*)\")in (scan_all input1, scan_all input2)end""(\"foo bar\", \"foo (**test**) bar (**test**)\")"}*}text {* \solution{ex:addsimproc} *}ML{*fun dest_sum term = case term of (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) => (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) | _ => raise TERM ("dest_sum", [term])fun get_sum_thm ctxt t (n1, n2) = let val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2) val goal = Logic.mk_equals (t, sum)in Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))endfun add_sp_aux ss t =let val ctxt = Simplifier.the_context ss val t' = term_of tin SOME (get_sum_thm ctxt t' (dest_sum t')) handle TERM _ => NONEend*}text {* The setup for the simproc is *}simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}text {* and a test case is the lemma *}lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})txt {* where the simproc produces the goal state \begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage}\bigskip*}(*<*)oops(*>*)text {* \solution{ex:addconversion} *}text {* (FIXME This solution works but is awkward.)*}ML{*fun add_conv ctxt ctrm = (case Thm.term_of ctrm of @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => (let val eq1 = Conv.binop_conv (add_conv ctxt) ctrm; val ctrm' = Thm.rhs_of eq1; val trm' = Thm.term_of ctrm'; val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm' in Thm.transitive eq1 eq2 end) | _ $ _ => Conv.combination_conv (add_conv ctxt) (add_conv ctxt) ctrm | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm | _ => Conv.all_conv ctrm)val add_tac = CSUBGOAL (fn (goal, i) => let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) in CONVERSION (Conv.params_conv ~1 (fn ctxt => (Conv.prems_conv ~1 (add_conv ctxt) then_conv Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i end)*}lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" apply(tactic {* add_tac 1 *})?txt {* where the simproc produces the goal state \begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage}\bigskip*}(*<*)oops(*>*)end