isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:8057d65607eb
+:d0b81d6e1b28
 definition and many useful operations are implemented
 in @{ML_file "Pure/type.ML"}.
 \end{readmore}
 *}
-section {* Constructing Terms Manually\label{sec:terms_types_manually} *}
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
 text {*
 While antiquotations are very convenient for constructing terms, they can
 only construct fixed terms (remember they are ``linked'' at compile-time).
 However, you often need to construct terms dynamically. For example, a
 and a list of terms as arguments, and produces as output the term
 list applied to the term. For example
 @{ML_response_fake [display,gray]
 "let
-val t = @{term \"P::nat\"}
+val trm = @{term \"P::nat\"}
 val args = [@{term \"True\"}, @{term \"False\"}]
 in
-list_comb (t, args)
+list_comb (trm, args)
 end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 Another handy function is @{ML [index] lambda}, which abstracts a variable
 in a term. For example
 @{ML_response_fake [display,gray]
-"lambda @{term \"x::nat\"} @{term \"(P::nat \<Rightarrow> bool) x\"}"
+"let
+val x_nat = @{term \"x::nat\"}
+val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+in
+lambda x_nat trm
+end"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
 and an abstraction. It also records the type of the abstracted
 variable and for printing purposes also its name.  Note that because of the
 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
 is of the same type as the abstracted variable. If it is of different type,
 as in
 @{ML_response_fake [display,gray]
-"lambda @{term \"x::nat\"} @{term \"(P::bool \<Rightarrow> bool) x\"}"
+"let
-"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
+val x_int = @{term \"x::int\"}
+val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
-then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted.
+in
+lambda x_int trm
+end"
+"Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted.
 This is a fundamental principle
 of Church-style typing, where variables with the same name still differ, if they
 have different type.
 There is also the function @{ML [index] subst_free} with which terms can
 @{ML_response_fake [display,gray]
 "let
 val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
 val s2 = (@{term \"x::nat\"}, @{term \"True\"})
-val trm =  @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
 in
 subst_free [s1, s2] trm
 end"
 "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
 example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
 The types needed in this equality are calculated from the type of the
 arguments. For example
 @{ML_response_fake [gray,display]
-"writeln (Syntax.string_of_term @{context}
+"let
-(HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
+val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
+in
+writeln (Syntax.string_of_term @{context} eq)
+end"
 "True = False"}
 *}
 text {*
 \begin{readmore}
 Most of the HOL-specific operations on terms and types are defined
 in @{ML_file "HOL/Tools/hologic.ML"}.
 \end{readmore}
-*}
+When constructing terms manually, there are a few subtle issues with
-section {* Constants *}
+constants. They usually crop up when pattern matching terms or types, or
+when constructing them. While it is perfectly ok to write the function
-text {*
+@{text is_true} as follows
-There are a few subtle issues with constants. They usually crop up when
-pattern matching terms or types, or when constructing them. While it is perfectly ok
-to write the function @{text is_true} as follows
 *}
 ML{*fun is_true @{term True} = true
 | is_true _ = false*}
 \begin{readmore}
 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
 functions about signatures in @{ML_file "Pure/sign.ML"}.
 \end{readmore}
-*}
-section {* Constructing Types Manually *}
-text {*
 Although types of terms can often be inferred, there are many
 situations where you need to construct types manually, especially
 when defining constants. For example the function returning a function
 type is as follows:
 that is they take, besides a term, also a list of type-variables as input.
 So in order to obtain the list of type-variables of a term you have to
 call them as follows
 @{ML_response [gray,display]
-"Term.add_tfrees @{term \"(a,b)\"} []"
+"Term.add_tfrees @{term \"(a, b)\"} []"
 "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 The reason for this definition is that @{ML add_tfrees in Term} can
 be easily folded over a list of terms. Similarly for all functions
-named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
+named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
 *}
 section {* Type-Checking\label{sec:typechecking} *}
 section {* Misc (TBD) *}
 ML {*Datatype.get_info @{theory} "List.list"*}
+section {* Name Space(TBD) *}
 end

changeset 299	d0b81d6e1b28
parent 298	8057d65607eb
child 301	2728e8daebc0