isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:df09e49b19bf
+:733614e236a3
 text {*
 then Isabelle's undo operation has no effect on the definition of
 @{ML "foo"}.
-During coding you might find it necessary to quickly inspect some data
+During developments you might find it necessary to quickly inspect some data
 in your code. This can be done in a ``quick-and-dirty'' fashion using
-@{ML "warning"}. For example
+the function @{ML "warning"}. For example
 *}
 ML {*
 val _ = warning "any string"
 *}
 *}
 section {* Terms *}
 text {*
-Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"}
+One way to construct terms of Isabelle on the ML-level is by using the antiquotation
-antiquotation:
+@{text "@{term \<dots>}"}:
 *}
 ML {* @{term "(a::nat) + b = c"} *}
 text {*
 This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
-representation of this term. This internal represenation is just a
+representation of this term. This internal represenation corresponds to the
 datatype defined in @{ML_file "Pure/term.ML"}.
-The internal representation of terms uses the usual deBruin indices mechanism: bound
+The internal representation of terms uses the usual de-Bruijn indices mechanism where bound
-variables are represented by the constructor @{ML Bound} whose argument refers to
+variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
 binds the corresponding variable. However, the names of bound variables are
-kept at abstractions for printing purposes, and so should be treated just as comments.
+kept at abstractions for printing purposes, and so should be treated only as comments.
-See \ichcite{ch:logic} for more details.
-(FIXME: Alex why is the reference bolow given. It somehow does not read
-with what is written above.)
 \begin{readmore}
 Terms are described in detail in \ichcite{ch:logic}. Their
 definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
 \end{readmore}
 Hint: The third term is already quite big, and the pretty printer
 may omit parts of it by default. If you want to see all of it, you
 can use @{ML "print_depth 50"} to set the limit to a value high enough.
 \end{exercise}
-\begin{exercise}
-Write a function @{ML_text "rev_sum : term -> term"} that takes a
-term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"}
-and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.
-Note that @{text "+"} associates to the left.
-Try your function on some examples, and see if the result typechecks.
-\end{exercise}
-*}
-text {* FIXME: check possible solution *}
-ML {*
-exception FORM_ERROR
-fun rev_sum term =
-case term of
-@{term "op +"} $ (Free (x,t1)) $ (Free (y,t2)) =>
-@{term "op +"} $ (Free (y,t2)) $ (Free (x,t1))
-|  @{term "op +"} $ left $ (Free (x,t)) =>
-@{term "op +"} $ (Free (x,t)) $ (rev_sum left)
-|  _ => raise FORM_ERROR
-*}
-text {*
-\begin{exercise}
-Write a function which takes two terms representing natural numbers
-in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
-number representing their sum.
-\end{exercise}
-\begin{exercise}
-Look at the functions defined in @{ML_file "Pure/logic.ML"} and
-@{ML_file "HOL/hologic.ML"} and see if they can make your life
-easier.
-\end{exercise}
-(FIXME what is coming next should fit with the main flow)
 *}
 ML {*
 @{const_name plus}
 *}
 ML {* @{prop "True"} *}
+section {* Possible Section on Construting Explicitly Terms *}
+text {*
+There is a disadvantage of using the @{text "@{term \<dots>}"} antiquotation
+directly in order to construct terms.
+*}
+ML {*
+val nat = HOLogic.natT
+val x = Free ("x", nat)
+val t = Free ("t", nat)
+val P = Free ("P", nat --> HOLogic.boolT)
+val Q = Free ("Q", nat --> HOLogic.boolT)
+val A1 = Logic.all x
+(Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
+HOLogic.mk_Trueprop (Q $ x)))
+val A2 = HOLogic.mk_Trueprop (P $ t)
+*}
+text {*
+\begin{exercise}
+Write a function @{ML_text "rev_sum : term -> term"} that takes a
+term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
+and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
+associates to the left. Try your function on some examples, and see if
+the result typechecks. (FIXME: clash with the type-checking section later)
+\end{exercise}
+*}
+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 {*
+\begin{exercise}
+Write a function which takes two terms representing natural numbers
+in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
+number representing their sum.
+\end{exercise}
+*}
+ML {*
+fun make_sum t1 t2 =
+HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
+*}
+text {*
+\begin{exercise}
+Look at the functions defined in @{ML_file "Pure/logic.ML"} and
+@{ML_file "HOL/hologic.ML"} and see if they can make your life
+easier.
+\end{exercise}
+*}
 section {* Type checking *}
 text {*
 We can freely construct and manipulate terms, since they are just
 can be proved in ML like
 this\footnote{Note that @{text "|>"} is just reverse
 application. This combinator, and several variants are defined in
 @{ML_file "Pure/General/basics.ML"}}:
+*}
-(FIXME: Alex why did you not use antiquotations for this?)
-*}
-ML {*
-let
-val thy = @{theory}
-val nat = HOLogic.natT
-val x = Free ("x", nat)
-val t = Free ("t", nat)
-val P = Free ("P", nat --> HOLogic.boolT)
-val Q = Free ("Q", nat --> HOLogic.boolT)
-val A1 = Logic.all x
-(Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
-HOLogic.mk_Trueprop (Q $ x)))
-|> cterm_of thy
-val A2 = HOLogic.mk_Trueprop (P $ t)
-|> cterm_of thy
-val Pt_implies_Qt =
-assume A1
-|> forall_elim (cterm_of thy t)
-val Qt = implies_elim Pt_implies_Qt (assume A2)
-in
-Qt
-|> implies_intr A2
-|> implies_intr A1
-end
-*}
 ML {*
 let
 val thy = @{theory}
 end
 *}
 text {*
-FIXME Explain this program more carefully
+FIXME Explain this program more carefully (@{ML_text assume},  @{ML_text "forall_elim"} \ldots)
 *}
 section {* Tactical reasoning *}
 text {*
 Tactics that affect only a certain subgoal, take a subgoal number as
 an integer parameter. Here we always work on the first subgoal,
 following exactly the @{text "apply"} script.
+(Fixme: would it make sense to explain THEN' here)
 *}
 section {* Case Study: Relation Composition *}

changeset 11	733614e236a3
parent 10	df09e49b19bf
child 12	2f1736cb8f26