theory Solutions
imports FirstSteps "Recipes/Timing"
begin

(*<*)
setup{*
open_file_with_prelude 
  "Solutions_Code.thy"
  ["theory Solutions", "imports FirstSteps", "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{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)
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 = (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:contextfree} *}

ML{*datatype expr = 
   Number of int
 | Mult of expr * expr 
 | Add of expr * expr

fun parse_basic xs =
  (OuterParse.nat >> Number 
   || OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs
and parse_factor xs =
  (parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult 
   || parse_basic) xs
and parse_expr xs =
  (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 
   || parse_factor) xs*}


text {* \solution{ex:dyckhoff} 
  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"
  by iprover

lemma impE3:
  shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  by iprover

lemma impE4:
  shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  by iprover

lemma impE5:
  shows "\<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 = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, 
                @{thm impI}, @{thm iffI}]
  val elims  = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE},
                @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}]
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{*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))
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)"
  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 ctrm
in 
  get_sum_thm ctxt trm (dest_sum trm)
end

fun add_conv ctxt ctrm =
  (case Thm.term_of ctrm of
     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
         (Conv.binop_conv (add_conv ctxt)
          then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         
    | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm
    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
    | _ => Conv.all_conv ctrm)

fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
  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)*}

text {*
  A test case for this conversion is as follows
*}

lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
  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:addconversion} *}

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 n
end*}

text {*
  This function generates for example:

  @{ML_response_fake [display,gray] 
  "writeln (string_of_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