Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Solutions.thy
changeset 517 d8c376662bb4
parent 469 7a558c5119b2
child 544 501491d56798
equal deleted inserted replaced
516:fb6c29a90003 517:d8c376662bb4 
     1 theory Solutions
 
     1 theory Solutions
 
     2 imports First_Steps "Recipes/Timing"
 
     2 imports First_Steps "Recipes/Timing"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 (*<*)
 
       
     6 setup{*
 
       
     7 open_file_with_prelude 
       
     8   "Solutions_Code.thy"
 
       
     9   ["theory Solutions", "imports First_Steps", "begin"]
 
       
    10 *}
 
       
    11 (*>*)
 
       
    12 
       
    13 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
     5 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
    14 
     6 
    15 text {* \solution{fun:revsum} *}
 
     7 text {* \solution{fun:revsum} *}
 
    16 
     8 
    17 ML{*fun rev_sum 
     9 ML %grayML{*fun rev_sum 
    18   ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t
 
    10   ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t
 
    19   | rev_sum t = t *}
 
    11   | rev_sum t = t *}
 
    20 
    12 
    21 text {* 
    13 text {* 
    22   An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
 
    14   An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
 
    23  *}
 
    15  *}
 
    24 
    16 
    25 ML{*fun rev_sum t =
 
    17 ML %grayML{*fun rev_sum t =
 
    26 let
 
    18 let
 
    27   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
 
    19   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
 
    28     | dest_sum u = [u]
 
    20     | dest_sum u = [u]
 
    29 in
 
    21 in
 
    30   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 
    22   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 
    31 end *}
 
    23 end *}
 
    32 
    24 
    33 text {* \solution{fun:makesum} *}
 
    25 text {* \solution{fun:makesum} *}
 
    34 
    26 
    35 ML{*fun make_sum t1 t2 =
 
    27 ML %grayML{*fun make_sum t1 t2 =
 
    36   HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
    28   HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
    37 
    29 
    38 text {* \solution{fun:killqnt} *}
 
    30 text {* \solution{fun:killqnt} *}
 
    39 
    31 
    40 ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]
 
    32 ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]
 
    73 
    65 
    74 
    66 
    75 
    67 
    76 text {* \solution{fun:makelist} *}
 
    68 text {* \solution{fun:makelist} *}
 
    77 
    69 
    78 ML{*fun mk_rev_upto i = 
    70 ML %grayML{*fun mk_rev_upto i = 
    79   1 upto i
 
    71   1 upto i
 
    80   |> map (HOLogic.mk_number @{typ int})
 
    72   |> map (HOLogic.mk_number @{typ int})
 
    81   |> HOLogic.mk_list @{typ int}
 
    73   |> HOLogic.mk_list @{typ int}
 
    82   |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
 
    74   |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
 
    83 
    75 
    84 text {* \solution{ex:debruijn} *}
 
    76 text {* \solution{ex:debruijn} *}
 
    85 
    77 
    86 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
    78 ML %grayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
    87 
    79 
    88 fun rhs 1 = P 1
 
    80 fun rhs 1 = P 1
 
    89   | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
 
    81   | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
 
    90 
    82 
    91 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
 
    83 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
 
    95 fun de_bruijn n =
 
    87 fun de_bruijn n =
 
    96   HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
 
    88   HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
 
    97 
    89 
    98 text {* \solution{ex:scancmts} *}
 
    90 text {* \solution{ex:scancmts} *}
 
    99 
    91 
   100 ML{*val any = Scan.one (Symbol.not_eof)
 
    92 ML %grayML{*val any = Scan.one (Symbol.not_eof)
 
   101 
    93 
   102 val scan_cmt =
 
    94 val scan_cmt =
 
   103 let
 
    95 let
 
   104   val begin_cmt = Scan.this_string "(*" 
    96   val begin_cmt = Scan.this_string "(*" 
   105   val end_cmt = Scan.this_string "*)"
 
    97   val end_cmt = Scan.this_string "*)"
 
   128 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 
   120 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 
   129 *}
 
   121 *}
 
   130 
   122 
   131 text {* \solution{ex:contextfree} *}
 
   123 text {* \solution{ex:contextfree} *}
 
   132 
   124 
   133 ML{*datatype expr = 
   125 ML %grayML{*datatype expr = 
   134    Number of int
 
   126    Number of int
 
   135  | Mult of expr * expr 
   127  | Mult of expr * expr 
   136  | Add of expr * expr
 
   128  | Add of expr * expr
 
   137 
   129 
   138 fun parse_basic xs =
 
   130 fun parse_basic xs =
 
   215 text {*
 
   207 text {*
 
   216   We can use the tactic to prove or disprove automatically the
 
   208   We can use the tactic to prove or disprove automatically the
 
   217   de Bruijn formulae from Exercise \ref{ex:debruijn}.
 
   209   de Bruijn formulae from Exercise \ref{ex:debruijn}.
 
   218 *}
 
   210 *}
 
   219 
   211 
   220 ML{*fun de_bruijn_prove ctxt n =
 
   212 ML %grayML{*fun de_bruijn_prove ctxt n =
 
   221 let 
   213 let 
   222   val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 
   214   val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 
   223 in
 
   215 in
 
   224   Goal.prove ctxt ["P"] [] goal
 
   216   Goal.prove ctxt ["P"] [] goal
 
   225    (fn _ => (DEPTH_SOLVE o apply_tac) 1)
 
   217    (fn _ => (DEPTH_SOLVE o apply_tac) 1)
 
   227 
   219 
   228 text {* 
   220 text {* 
   229   You can use this function to prove de Bruijn formulae.
 
   221   You can use this function to prove de Bruijn formulae.
 
   230 *}
 
   222 *}
 
   231 
   223 
   232 ML{*de_bruijn_prove @{context} 3 *}
 
   224 ML %grayML{*de_bruijn_prove @{context} 3 *}
 
   233 
   225 
   234 text {* \solution{ex:addsimproc} *}
 
   226 text {* \solution{ex:addsimproc} *}
 
   235 
   227 
   236 ML{*fun dest_sum term =
 
   228 ML %grayML{*fun dest_sum term =
 
   237   case term of 
   229   case term of 
   238     (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
 
   230     (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
 
   239         (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
 
   231         (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
 
   240   | _ => raise TERM ("dest_sum", [term])
 
   232   | _ => raise TERM ("dest_sum", [term])
 
   241 
   233 
   277 text {*
 
   269 text {*
 
   278   The following code assumes the function @{ML dest_sum} from the previous
 
   270   The following code assumes the function @{ML dest_sum} from the previous
 
   279   exercise.
 
   271   exercise.
 
   280 *}
 
   272 *}
 
   281 
   273 
   282 ML{*fun add_simple_conv ctxt ctrm =
 
   274 ML %grayML{*fun add_simple_conv ctxt ctrm =
 
   283 let
 
   275 let
 
   284   val trm = Thm.term_of ctrm
 
   276   val trm = Thm.term_of ctrm
 
   285 in
 
   277 in
 
   286   case trm of
 
   278   case trm of
 
   287      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
   279      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
   321   For constructing test cases, we first define a function that returns a 
   313   For constructing test cases, we first define a function that returns a 
   322   complete binary tree whose leaves are numbers and the nodes are 
   314   complete binary tree whose leaves are numbers and the nodes are 
   323   additions.
 
   315   additions.
 
   324 *}
 
   316 *}
 
   325 
   317 
   326 ML{*fun term_tree n =
 
   318 ML %grayML{*fun term_tree n =
 
   327 let
 
   319 let
 
   328   val count = Unsynchronized.ref 0; 
   320   val count = Unsynchronized.ref 0; 
   329 
   321 
   330   fun term_tree_aux n =
 
   322   fun term_tree_aux n =
 
   331     case n of
 
   323     case n of
 
   345 
   337 
   346   The next function constructs a goal of the form @{text "P \<dots>"} with a term 
   338   The next function constructs a goal of the form @{text "P \<dots>"} with a term 
   347   produced by @{ML term_tree} filled in.
 
   339   produced by @{ML term_tree} filled in.
 
   348 *}
 
   340 *}
 
   349 
   341 
   350 ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
 
   342 ML %grayML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
 
   351 
   343 
   352 text {*
 
   344 text {*
 
   353   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
 
   345   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
 
   354   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
 
   346   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
 
   355   respectively. The idea is to first apply the conversion (respectively simproc) and 
   347   respectively. The idea is to first apply the conversion (respectively simproc) and 
   356   then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 
   348   then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 
   357 *}
 
   349 *}
 
   358 
   350 
   359 ML{*local
 
   351 ML %grayML{*local
 
   360   fun mk_tac tac = 
   352   fun mk_tac tac = 
   361         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
 
   353         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
 
   362 in
 
   354 in
 
   363   val c_tac = mk_tac (add_tac @{context}) 
   355   val c_tac = mk_tac (add_tac @{context}) 
   364   val s_tac = mk_tac (simp_tac 
   356   val s_tac = mk_tac (simp_tac 
   367 
   359 
   368 text {*
 
   360 text {*
 
   369   This is all we need to let the conversion run against the simproc:
 
   361   This is all we need to let the conversion run against the simproc:
 
   370 *}
 
   362 *}
 
   371 
   363 
   372 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
 
   364 ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
 
   373 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
 
   365 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
 
   374 
   366 
   375 text {*
 
   367 text {*
 
   376   If you do the exercise, you can see that both ways of simplifying additions
 
   368   If you do the exercise, you can see that both ways of simplifying additions
 
   377   perform relatively similar with perhaps some advantages for the
 
   369   perform relatively similar with perhaps some advantages for the
isabelle-cookbook