theory Solutions+ −
imports First_Steps "Recipes/Timing"+ −
begin+ −
+ −
chapter {* Solutions to Most Exercises\label{ch:solutions} *}+ −
+ −
text {* \solution{fun:revsum} *}+ −
+ −
ML %grayML{*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 %grayML{*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 %grayML{*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')+ −
| _ => t+ −
in + −
aux trm+ −
end*}+ −
+ −
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 %grayML{*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 %grayML{*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 %grayML{*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)+ −
end+ −
+ −
val 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 %grayML{*datatype expr = + −
Number of int+ −
| Mult of expr * expr + −
| Add of expr * expr+ −
+ −
fun parse_basic xs =+ −
(Parse.nat >> Number + −
|| Parse.$$$ "(" |-- parse_expr --| Parse.$$$ ")") 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*}+ −
+ −
+ −
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 iprover+ −
+ −
lemma 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 *})+ −
done+ −
+ −
text {*+ −
We can use the tactic to prove or disprove automatically the+ −
de Bruijn formulae from Exercise \ref{ex:debruijn}.+ −
*}+ −
+ −
ML %grayML{*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 %grayML{*de_bruijn_prove @{context} 3 *}+ −
+ −
text {* \solution{ex:addsimproc} *}+ −
+ −
ML %grayML{*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))+ −
end+ −
+ −
fun add_sp_aux ss t =+ −
let + −
val ctxt = Simplifier.the_context ss+ −
val t' = term_of t+ −
in+ −
SOME (get_sum_thm ctxt t' (dest_sum t'))+ −
handle TERM _ => NONE+ −
end*}+ −
+ −
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 %grayML{*fun add_simple_conv ctxt ctrm =+ −
let+ −
val trm = Thm.term_of ctrm+ −
in+ −
case trm of+ −
@{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => + −
get_sum_thm ctxt trm (dest_sum trm)+ −
| _ => Conv.all_conv ctrm+ −
end+ −
+ −
val add_conv = Conv.bottom_conv add_simple_conv+ −
+ −
fun 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 %grayML{*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*}+ −
+ −
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 %grayML{*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 %grayML{*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 %grayML{*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+ −