theory Solutionsimports First_Steps "Recipes/Timing"begin(*<*)setup{*open_file_with_prelude "Solutions_Code.thy" ["theory Solutions", "imports First_Steps", "begin"]*}(*>*)chapter {* Solutions to Most Exercises\label{ch:solutions} *}text {* \solution{fun:revsum} *}ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t | rev_sum t = t *}text {* An alternative solution using the function @{ML_ind mk_binop in HOLogic} is: *}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{fun:killqnt} *}ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]fun kill_trivial_quantifiers trm =let fun aux t = case t of Const (s1, T1) $ Abs (x, T2, t2) => if member (op =) quantifiers s1 andalso not (loose_bvar1 (t2, 0)) then incr_boundvars ~1 (aux t2) else Const (s1, T1) $ Abs (x, T2, aux t2) | t1 $ t2 => aux t1 $ aux t2 | Abs (s, T, t') => Abs (s, T, aux t') | _ => tin aux trmend*}text {* 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 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"}*}text {* \solution{fun:makelist} *}ML{*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"}*}text {* \solution{ex:debruijn} *}ML{*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))*}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 = (Symbol.explode \"foo bar\") val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")in (scan_all input1, scan_all input2)end""(\"foo bar\", \"foo (**test**) bar (**test**)\")"}*}text {* \solution{ex:contextfree} *}ML{*datatype expr = Number of int | Mult of expr * expr | Add of expr * exprfun parse_basic xs = (Parse.nat >> Number || Parse.$$$ "(" |-- parse_expr --| Parse.$$$ ")") xsand parse_factor xs = (parse_basic --| Parse.$$$ "*" -- parse_factor >> Mult || parse_basic) xsand parse_expr xs = (parse_factor --| Parse.$$$ "+" -- parse_expr >> Add || parse_factor) xs*}text {* \solution{ex:dyckhoff} *}text {* The axiom rule can be implemented with the function @{ML atac}. The other rules correspond to the theorems: \begin{center} \begin{tabular}{cc} \begin{tabular}{rl} $\wedge_R$ & @{thm [source] conjI}\\ $\vee_{R_1}$ & @{thm [source] disjI1}\\ $\vee_{R_2}$ & @{thm [source] disjI2}\\ $\longrightarrow_R$ & @{thm [source] impI}\\ $=_R$ & @{thm [source] iffI}\\ \end{tabular} & \begin{tabular}{rl} $False$ & @{thm [source] FalseE}\\ $\wedge_L$ & @{thm [source] conjE}\\ $\vee_L$ & @{thm [source] disjE}\\ $=_L$ & @{thm [source] iffE} \end{tabular} \end{tabular} \end{center} For the other rules we need to prove the following lemmas.*}lemma impE1: shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by iproverlemma impE2: shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 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 {* Now the tactic which applies a single rule can be implemented as follows.*}ML %linenosgray{*val apply_tac =let val intros = @{thms conjI disjI1 disjI2 impI iffI} val elims = @{thms FalseE conjE disjE iffE impE2}in atac ORELSE' resolve_tac intros ORELSE' eresolve_tac elims ORELSE' (etac @{thm impE1} THEN' atac)end*}text {* In Line 11 we apply the rule @{thm [source] impE1} in concjunction with @{ML atac} in order to reduce the number of possibilities that need to be explored. You can use the tactic as follows.*}lemma shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})donetext {* We can use the tactic to prove or disprove automatically the de Bruijn formulae from Exercise \ref{ex:debruijn}.*}ML{*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) 1)end*}text {* You can use this function to prove de Bruijn formulae.*}ML{*de_bruijn_prove @{context} 3 *}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_Data.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 %gray 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)::nat)" apply(tactic {* simp_tac (HOL_basic_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 {* The following code assumes the function @{ML dest_sum} from the previous exercise.*}ML{*fun add_simple_conv ctxt ctrm =let val trm = Thm.term_of ctrmin case trm of @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => get_sum_thm ctxt trm (dest_sum trm) | _ => Conv.all_conv ctrmendval add_conv = Conv.bottom_conv add_simple_convfun add_tac ctxt = CONVERSION (add_conv ctxt)*}text {* A test case for this conversion is as follows*}lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)" apply(tactic {* add_tac @{context} 1 *})?txt {* where it produces the goal state \begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage}\bigskip*}(*<*)oops(*>*)text {* \solution{ex:compare} *}text {* 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 unprovable goal which, after simplification, we are going to ``prove'' with 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.*}ML{*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 nend*}text {* 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 produced by @{ML term_tree} filled in.*}ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}text {* 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, respectively. The idea is to first apply the conversion (respectively simproc) and then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.*}ML{*local fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])in val c_tac = mk_tac (add_tac @{context}) val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))end*}text {* This is all we need to let the conversion run against the simproc:*}ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}text {* 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.*}end