1 theory Solutions

     2 imports Base "Recipes/Timing"

     3 begin

     4 

     5 chapter {* Solutions to Most Exercises\label{ch:solutions} *}

     6 

     7 text {* \solution{fun:revsum} *}

     8 

     9 ML{*fun rev_sum t =

    10 let

    11   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u

    12     | dest_sum u = [u]

    13 in

    14    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)

    15 end *}

    16 

    17 text {* \solution{fun:makesum} *}

    18 

    19 ML{*fun make_sum t1 t2 =

    20       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}

    21 

    22 text {* \solution{ex:scancmts} *}

    23 

    24 ML{*val any = Scan.one (Symbol.not_eof)

    25 

    26 val scan_cmt =

    27 let

    28   val begin_cmt = Scan.this_string "(*" 

    29   val end_cmt = Scan.this_string "*)"

    30 in

    31   begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 

    32   >> (enclose "(**" "**)" o implode)

    33 end

    34 

    35 val parser = Scan.repeat (scan_cmt || any)

    36 

    37 val scan_all =

    38       Scan.finite Symbol.stopper parser >> implode #> fst *}

    39 

    40 text {*

    41   By using @{text "#> fst"} in the last line, the function 

    42   @{ML scan_all} retruns a string, instead of the pair a parser would

    43   normally return. For example:

    44 

    45   @{ML_response [display,gray]

    46 "let

    47   val input1 = (explode \"foo bar\")

    48   val input2 = (explode \"foo (*test*) bar (*test*)\")

    49 in

    50   (scan_all input1, scan_all input2)

    51 end"

    52 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}

    53 *}

    54 

    55 text {* \solution{ex:addsimproc} *}

    56 

    57 ML{*fun dest_sum term =

    58   case term of 

    59     (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>

    60         (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))

    61   | _ => raise TERM ("dest_sum", [term])

    62 

    63 fun get_sum_thm ctxt t (n1, n2) =  

    64 let 

    65   val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)

    66   val goal = Logic.mk_equals (t, sum)

    67 in

    68   Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))

    69 end

    70 

    71 fun add_sp_aux ss t =

    72 let 

    73   val ctxt = Simplifier.the_context ss

    74   val t' = term_of t

    75 in

    76   SOME (get_sum_thm ctxt t' (dest_sum t'))

    77   handle TERM _ => NONE

    78 end*}

    79 

    80 text {* The setup for the simproc is *}

    81 

    82 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *}

    83  

    84 text {* and a test case is the lemma *}

    85 

    86 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"

    87   apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})

    88 txt {* 

    89   where the simproc produces the goal state

    90   

    91   \begin{minipage}{\textwidth}

    92   @{subgoals [display]}

    93   \end{minipage}\bigskip

    94 *}(*<*)oops(*>*)

    95 

    96 text {* \solution{ex:addconversion} *}

    97 

    98 text {*

    99   The following code assumes the function @{ML dest_sum} from the previous

   100   exercise.

   101 *}

   102 

   103 ML{*fun add_simple_conv ctxt ctrm =

   104 let

   105   val trm =  Thm.term_of ctrm

   106 in 

   107   get_sum_thm ctxt trm (dest_sum trm)

   108 end

   109 

   110 fun add_conv ctxt ctrm =

   111   (case Thm.term_of ctrm of

   112      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 

   113          (Conv.binop_conv (add_conv ctxt)

   114           then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         

   115     | _ $ _ => Conv.combination_conv 

   116                  (add_conv ctxt) (add_conv ctxt) ctrm

   117     | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm

   118     | _ => Conv.all_conv ctrm)

   119 

   120 fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>

   121   CONVERSION

   122     (Conv.params_conv ~1 (fn ctxt =>

   123        (Conv.prems_conv ~1 (add_conv ctxt) then_conv

   124           Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*}

   125 

   126 text {*

   127   A test case for this conversion is as follows

   128 *}

   129 

   130 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"

   131   apply(tactic {* add_tac @{context} 1 *})?

   132 txt {* 

   133   where it produces the goal state

   134   

   135   \begin{minipage}{\textwidth}

   136   @{subgoals [display]}

   137   \end{minipage}\bigskip

   138 *}(*<*)oops(*>*)

   139 

   140 text {* \solution{ex:addconversion} *}

   141 

   142 text {* 

   143   We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.

   144   To measure any difference between the simproc and conversion, we will create 

   145   mechanically terms involving additions and then set up a goal to be 

   146   simplified. We have to be careful to set up the goal so that

   147   other parts of the simplifier do not interfere. For this we construct an

   148   unprovable goal which, after simplification, we are going to ``prove'' with

   149   the help of the lemma:

   150 *}

   151 

   152 lemma cheat: "A" sorry

   153 

   154 text {*

   155   For constructing test cases, we first define a function that returns a 

   156   complete binary tree whose leaves are numbers and the nodes are 

   157   additions.

   158 *}

   159 

   160 ML{*fun term_tree n =

   161 let

   162   val count = ref 0; 

   163 

   164   fun term_tree_aux n =

   165     case n of

   166       0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))

   167     | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 

   168              $ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))

   169 in

   170   term_tree_aux n

   171 end*}

   172 

   173 text {*

   174   This function generates for example:

   175 

   176   @{ML_response_fake [display,gray] 

   177   "warning (Syntax.string_of_term @{context} (term_tree 2))" 

   178   "(1 + 2) + (3 + 4)"} 

   179 

   180   The next function constructs a goal of the form @{text "P \<dots>"} with a term 

   181   produced by @{ML term_tree} filled in.

   182 *}

   183 

   184 ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}

   185 

   186 text {*

   187   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define

   188   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,

   189   respectively. The idea is to first apply the conversion (respectively simproc) and 

   190   then prove the remaining goal using the @{thm [source] cheat}-lemma.

   191 *}

   192 

   193 ML{*local

   194   fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])

   195 in

   196 val c_tac = mk_tac (add_tac @{context}) 

   197 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))

   198 end*}

   199 

   200 text {*

   201   This is all we need to let the conversion run against the simproc:

   202 *}

   203 

   204 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)

   205 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}

   206 

   207 text {*

   208   If you do the exercise, you can see that both ways of simplifying additions

   209   perform relatively similar with perhaps some advantages for the

   210   simproc. That means the simplifier, even if much more complicated than

   211   conversions, is quite efficient for tasks it is designed for. It usually does not

   212   make sense to implement general-purpose rewriting using

   213   conversions. Conversions only have clear advantages in special situations:

   214   for example if you need to have control over innermost or outermost

   215   rewriting, or when rewriting rules are lead to non-termination.

   216 *}

   217 

   218 end