isabelle-cookbook: comparison ProgTutorial/Solutions.thy

equal deleted inserted replaced

-:6e2479089226
+:cecd7a941885
 theory Solutions
 imports First_Steps "Recipes/Timing"
 begin
-chapter {* Solutions to Most Exercises\label{ch:solutions} *}
+chapter \<open>Solutions to Most Exercises\label{ch:solutions}\<close>
-text {* \solution{fun:revsum} *}
+text \<open>\solution{fun:revsum}\<close>
-ML %grayML{*fun rev_sum
+ML %grayML\<open>fun rev_sum
 ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t
-| rev_sum t = t *}
+| rev_sum t = t\<close>
-text {*
+text \<open>
 An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
-*}
+\<close>
-ML %grayML{*fun rev_sum t =
+ML %grayML\<open>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 *}
+end\<close>
-text {* \solution{fun:makesum} *}
+text \<open>\solution{fun:makesum}\<close>
-ML %grayML{*fun make_sum t1 t2 =
+ML %grayML\<open>fun make_sum t1 t2 =
-HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
+HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)\<close>
-text {* \solution{fun:killqnt} *}
+text \<open>\solution{fun:killqnt}\<close>
-ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]
+ML %linenosgray\<open>val quantifiers = [@{const_name All}, @{const_name Ex}]
 fun kill_trivial_quantifiers trm =
 let
 fun aux t =
 case t of
 | t1 $ t2 => aux t1 $ aux t2
 | Abs (s, T, t') => Abs (s, T, aux t')
 | _ => t
 in
 aux trm
-end*}
+end\<close>
-text {*
+text \<open>
 In line 7 we traverse the term, by first checking whether a term is an
 application of a constant with an abstraction. If the constant stands for
 a listed quantifier (see Line 1) and the bound variable does not occur
 as a loose bound variable in the body, then we delete the quantifier.
 For this we have to increase all other dangling de Bruijn indices by
-@{text "-1"} to account for the deleted quantifier. An example is
+\<open>-1\<close> to account for the deleted quantifier. An example is
 as follows:
 @{ML_response_fake [display,gray]
 "@{prop \"\<forall>x y z. P x = P z\"}
 |> kill_trivial_quantifiers
 |> pretty_term @{context}
 |> pwriteln"
 "\<forall>x z. P x = P z"}
-*}
+\<close>
-text {* \solution{fun:makelist} *}
+text \<open>\solution{fun:makelist}\<close>
-ML %grayML{*fun mk_rev_upto i =
+ML %grayML\<open>fun mk_rev_upto i =
 1 upto i
 |> map (HOLogic.mk_number @{typ int})
 |> HOLogic.mk_list @{typ int}
-|> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
+|> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}\<close>
-text {* \solution{ex:debruijn} *}
+text \<open>\solution{ex:debruijn}\<close>
-ML %grayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
+ML %grayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
 fun rhs 1 = P 1
 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
 fun de_bruijn n =
-HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
+HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close>
-text {* \solution{ex:scancmts} *}
+text \<open>\solution{ex:scancmts}\<close>
-ML %grayML{*val any = Scan.one (Symbol.not_eof)
+ML %grayML\<open>val any = Scan.one (Symbol.not_eof)
 val scan_cmt =
 let
 val begin_cmt = Scan.this_string "(*"
 val end_cmt = Scan.this_string "*)"
 end
 val parser = Scan.repeat (scan_cmt || any)
 val scan_all =
-Scan.finite Symbol.stopper parser >> implode #> fst *}
+Scan.finite Symbol.stopper parser >> implode #> fst\<close>
-text {*
+text \<open>
-By using @{text "#> fst"} in the last line, the function
+By using \<open>#> fst\<close> 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 input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
 in
 (scan_all input1, scan_all input2)
 end"
 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
-*}
+\<close>
-text {* \solution{ex:contextfree} *}
+text \<open>\solution{ex:contextfree}\<close>
-ML %grayML{*datatype expr =
+ML %grayML\<open>datatype expr =
 Number of int
 | Mult of expr * expr
 | Add of expr * expr
 fun parse_basic xs =
 and parse_factor xs =
 (parse_basic --| Parse.$$$ "*" -- parse_factor >> Mult
 || parse_basic) xs
 and parse_expr xs =
 (parse_factor --| Parse.$$$ "+" -- parse_expr >> Add
-|| parse_factor) xs*}
+|| parse_factor) xs\<close>
-text {* \solution{ex:dyckhoff} *}
+text \<open>\solution{ex:dyckhoff}\<close>
-text {*
+text \<open>
 The axiom rule can be implemented with the function @{ML assume_tac}. The other
 rules correspond to the theorems:
 \begin{center}
 \begin{tabular}{cc}
 \end{tabular}
 \end{tabular}
 \end{center}
 For the other rules we need to prove the following lemmas.
-*}
+\<close>
 lemma impE1:
 shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by iprover
 and   "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 and   "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 and   "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by iprover+
-text {*
+text \<open>
 Now the tactic which applies a single rule can be implemented
 as follows.
-*}
+\<close>
-ML %linenosgray{*fun apply_tac ctxt =
+ML %linenosgray\<open>fun apply_tac ctxt =
 let
 val intros = @{thms conjI disjI1 disjI2 impI iffI}
 val elims = @{thms FalseE conjE disjE iffE impE2}
 in
 assume_tac ctxt
 ORELSE' resolve_tac ctxt intros
 ORELSE' eresolve_tac ctxt elims
 ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt)
-end*}
+end\<close>
-text {*
+text \<open>
 In Line 11 we apply the rule @{thm [source] impE1} in concjunction
 with @{ML assume_tac} in order to reduce the number of possibilities that
 need to be explored. You can use the tactic as follows.
-*}
+\<close>
 lemma
 shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
-apply(tactic {* (DEPTH_SOLVE o apply_tac @{context}) 1 *})
+apply(tactic \<open>(DEPTH_SOLVE o apply_tac @{context}) 1\<close>)
 done
-text {*
+text \<open>
 We can use the tactic to prove or disprove automatically the
 de Bruijn formulae from Exercise \ref{ex:debruijn}.
-*}
+\<close>
-ML %grayML{*fun de_bruijn_prove ctxt n =
+ML %grayML\<open>fun de_bruijn_prove ctxt n =
 let
 val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 in
 Goal.prove ctxt ["P"] [] goal
 (fn _ => (DEPTH_SOLVE o apply_tac ctxt) 1)
-end*}
+end\<close>
-text {*
+text \<open>
 You can use this function to prove de Bruijn formulae.
-*}
+\<close>
-ML %grayML{*de_bruijn_prove @{context} 3 *}
+ML %grayML\<open>de_bruijn_prove @{context} 3\<close>
-text {* \solution{ex:addsimproc} *}
+text \<open>\solution{ex:addsimproc}\<close>
-ML %grayML{*fun dest_sum term =
+ML %grayML\<open>fun dest_sum term =
 case term of
 (@{term "(+):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
 (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
 | _ => raise TERM ("dest_sum", [term])
 let
 val t' = Thm.term_of t
 in
 SOME (get_sum_thm ctxt t' (dest_sum t'))
 handle TERM _ => NONE
-end*}
+end\<close>
-text {* The setup for the simproc is *}
+text \<open>The setup for the simproc is\<close>
-simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *}
+simproc_setup %gray add_sp ("t1 + t2") = \<open>K add_sp_aux\<close>
-text {* and a test case is the lemma *}
+text \<open>and a test case is the lemma\<close>
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
-apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc add_sp}]) 1 *})
+apply(tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc add_sp}]) 1\<close>)
-txt {*
+txt \<open>
 where the simproc produces the goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}\bigskip
-*}(*<*)oops(*>*)
+\<close>(*<*)oops(*>*)
-text {* \solution{ex:addconversion} *}
+text \<open>\solution{ex:addconversion}\<close>
-text {*
+text \<open>
 The following code assumes the function @{ML dest_sum} from the previous
 exercise.
-*}
+\<close>
-ML %grayML{*fun add_simple_conv ctxt ctrm =
+ML %grayML\<open>fun add_simple_conv ctxt ctrm =
 let
 val trm = Thm.term_of ctrm
 in
 case trm of
 @{term "(+)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
 | _ => Conv.all_conv ctrm
 end
 val add_conv = Conv.bottom_conv add_simple_conv
-fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
+fun add_tac ctxt = CONVERSION (add_conv ctxt)\<close>
-text {*
+text \<open>
 A test case for this conversion is as follows
-*}
+\<close>
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
-apply(tactic {* add_tac @{context} 1 *})?
+apply(tactic \<open>add_tac @{context} 1\<close>)?
-txt {*
+txt \<open>
 where it produces the goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}\bigskip
-*}(*<*)oops(*>*)
+\<close>(*<*)oops(*>*)
-text {* \solution{ex:compare} *}
+text \<open>\solution{ex:compare}\<close>
-text {*
+text \<open>
 We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
 To measure any difference between the simproc and conversion, we will create
 mechanically terms involving additions and then set up a goal to be
 simplified. We have to be careful to set up the goal so that
 other parts of the simplifier do not interfere. For this we construct an
 the help of ``\isacommand{sorry}'', that is the method @{ML Skip_Proof.cheat_tac}
 For constructing test cases, we first define a function that returns a
 complete binary tree whose leaves are numbers and the nodes are
 additions.
-*}
+\<close>
-ML %grayML{*fun term_tree n =
+ML %grayML\<open>fun term_tree n =
 let
 val count = Unsynchronized.ref 0;
 fun term_tree_aux n =
 case n of
 0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))
 | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"})
 $ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))
 in
 term_tree_aux n
-end*}
+end\<close>
-text {*
+text \<open>
 This function generates for example:
 @{ML_response_fake [display,gray]
 "pwriteln (pretty_term @{context} (term_tree 2))"
 "(1 + 2) + (3 + 4)"}
-The next function constructs a goal of the form @{text "P \<dots>"} with a term
+The next function constructs a goal of the form \<open>P \<dots>\<close> with a term
 produced by @{ML term_tree} filled in.
-*}
+\<close>
-ML %grayML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
+ML %grayML\<open>fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))\<close>
-text {*
+text \<open>
 Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
-two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
+two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc,
 respectively. The idea is to first apply the conversion (respectively simproc) and
 then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
-*}
+\<close>
 ML Skip_Proof.cheat_tac
-ML %grayML{*local
+ML %grayML\<open>local
 fun mk_tac ctxt tac =
 timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac ctxt])
 in
 fun c_tac ctxt = mk_tac ctxt (add_tac ctxt)
 fun s_tac ctxt = mk_tac ctxt (simp_tac
 (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}]))
-end*}
+end\<close>
-text {*
+text \<open>
 This is all we need to let the conversion run against the simproc:
-*}
+\<close>
-ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
+ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
-val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)*}
+val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)\<close>
-text {*
+text \<open>
 If you do the exercise, you can see that both ways of simplifying additions
 perform relatively similar with perhaps some advantages for the
 simproc. That means the simplifier, even if much more complicated than
 conversions, is quite efficient for tasks it is designed for. It usually does not
 make sense to implement general-purpose rewriting using
 conversions. Conversions only have clear advantages in special situations:
 for example if you need to have control over innermost or outermost
 rewriting, or when rewriting rules are lead to non-termination.
-*}
+\<close>
 end

changeset 565	cecd7a941885
parent 562	daf404920ab9
child 567	f7c97e64cc2a