isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:80b56d9b322f
+:9cf3bc448210
 ["theory General", "imports Base FirstSteps", "begin"]
 *}
 (*>*)
-chapter {* Isabelle in More Detail *}
+chapter {* Isabelle Essentials *}
 text {*
 Isabelle is build around a few central ideas. One central idea is the
 LCF-approach to theorem proving where there is a small trusted core and
 everything else is build on top of this trusted core
 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the
 user has no access to these theorems.
 Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
 with the same theorem name. In effect, once a theorem is stored under a name,
-this association will be fixed. While this is a ``safety-net'' to make sure a
+this association is fixed. While this is a ``safety-net'' to make sure a
 theorem name refers to a particular theorem or collection of theorems, it is
 also a bit too restrictive in cases where a theorem name should refer to a
 dynamically expanding list of theorems (like a simpset). Therefore Isabelle
 also implements a mechanism where a theorem name can refer to a custom theorem
 list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}.
-To see how it works let us assume we defined our own theorem list maintained
+To see how it works let us assume we defined our own theorem list @{text MyThmList}.
-in the data storage @{text MyThmList}.
 *}
 ML{*structure MyThmList = GenericDataFun
 (type T = thm list
 val empty = []
 \isacommand{thm}~@{text "mythmlist"}\\
 @{text "> False \<Longrightarrow> ?P"}\\
 @{text "> True"}
 \end{isabelle}
-There is a multitude of functions that manage or manipulate theorems in the
+There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule}
-structures @{ML_struct Thm} and @{ML_struct Drule}. For example
+for managing or manipulating theorems. For example
 we can test theorems for alpha equality. Suppose you proved the following three
 theorems.
 *}
 lemma
 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 Note that in the second case, there is no premise.
 \begin{readmore}
-For the functions @{text "assume"}, @{text "forall_elim"} etc
+The basic functions for theorems are defined in
-see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
 \end{readmore}
 The simplifier can be used to unfold definition in theorems. To show
 this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
 readers. For such situations Isabelle allows the installation of \emph{\index*{theorem
 styles}}. These are, roughly speaking, functions from terms to terms. The input
 term stands for the theorem to be presented; the output can be constructed to
 ones wishes.  Let us, for example, assume we want to quote theorems without
 leading @{text \<forall>}-quantifiers. For this we can implement the following function
-that strips off meta-quantifiers.
+that strips off @{text "\<forall>"}s.
 *}
-ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) =
+ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) =
 Term.dest_abs body |> snd |> strip_allq
 | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) =
 strip_allq t
 | strip_allq t = t*}
 giving a list of strings that should be used for the replacement of the
 variables. For this we implement the function which takes a list of strings
 and uses them as name in the outermost abstractions.
 *}
-ML {*fun rename_allq [] t = t
+ML{*fun rename_allq [] t = t
 | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) =
 Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
 | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
 rename_allq xs t
 | rename_allq _ t = t*}
 @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
 parsing.
 \end{readmore}
 *}
-section {* Setups (TBD) *}
+section {* Theories\label{sec:theories} (TBD) *}
-text {*
-In the previous section we used \isacommand{setup} in order to make
+text {*
-a theorem attribute known to Isabelle. What happens behind the scenes
+Theories are the most fundamental building blocks in Isabelle. They
-is that \isacommand{setup} expects a function of type
+contain definitions, syntax declarations, axioms, proofs etc. If a definition
-@{ML_type "theory -> theory"}: the input theory is the current theory and the
+is stated, it must be stored in a theory in order to be usable later
-output the theory where the theory attribute has been stored.
+on. Similar with proofs: once a proof is finished, the proved theorem
+needs to be stored in the theorem database of the theory in order to
-This is a fundamental principle in Isabelle. A similar situation occurs
+be usable. All relevant data of a theort can be querried as follows.
-for example with declaring constants. The function that declares a
-constant on the ML-level is @{ML_ind  add_consts_i in Sign}.
-If you write\footnote{Recall that ML-code  needs to be
-enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
-*}
-ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
-text {*
-for declaring the constant @{text "BAR"} with type @{typ nat} and
-run the code, then you indeed obtain a theory as result. But if you
-query the constant on the Isabelle level using the command \isacommand{term}
 \begin{isabelle}
-\isacommand{term}~@{text [quotes] "BAR"}\\
+\isacommand{print\_theory}\\
-@{text "> \"BAR\" :: \"'a\""}
+@{text "> names: Pure Code_Generator HOL \<dots>"}\\
+@{text "> classes: Inf < type \<dots>"}\\
+@{text "> default sort: type"}\\
+@{text "> syntactic types: #prop \<dots>"}\\
+@{text "> logical types: 'a \<times> 'b \<dots>"}\\
+@{text "> type arities: * :: (random, random) random \<dots>"}\\
+@{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\
+@{text "> abbreviations: \<dots>"}\\
+@{text "> axioms: \<dots>"}\\
+@{text "> oracles: \<dots>"}\\
+@{text "> definitions: \<dots>"}\\
+@{text "> theorems: \<dots>"}
 \end{isabelle}
-you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+\begin{center}
-blue) of polymorphic type. The problem is that the ML-expression above did
+\begin{tikzpicture}
-not register the declaration with the current theory. This is what the command
+\node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};
-\isacommand{setup} is for. The constant is properly declared with
+\end{tikzpicture}
-*}
+\end{center}
-setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
-text {*
-Now
-\begin{isabelle}
-\isacommand{term}~@{text [quotes] "BAR"}\\
-@{text "> \"BAR\" :: \"nat\""}
-\end{isabelle}
-returns a (black) constant with the type @{typ nat}.
-A similar command is \isacommand{local\_setup}, which expects a function
-of type @{ML_type "local_theory -> local_theory"}. Later on we will also
-use the commands \isacommand{method\_setup} for installing methods in the
-current theory and \isacommand{simproc\_setup} for adding new simprocs to
-the current simpset.
-*}
-section {* Theories\label{sec:theories} (TBD) *}
-text {*
-There are theories, proof contexts and local theories (in this order, if you
-want to order them).
 In contrast to an ordinary theory, which simply consists of a type
 signature, as well as tables for constants, axioms and theorems, a local
 theory contains additional context information, such as locally fixed
 variables and local assumptions that may be used by the package. The type
 @{ML_type local_theory} is identical to the type of \emph{proof contexts}
 @{ML_type "Proof.context"}, although not every proof context constitutes a
 valid local theory.
+*}
+section {* Setups (TBD) *}
+text {*
+In the previous section we used \isacommand{setup} in order to make
+a theorem attribute known to Isabelle. What happens behind the scenes
+is that \isacommand{setup} expects a function of type
+@{ML_type "theory -> theory"}: the input theory is the current theory and the
+output the theory where the theory attribute has been stored.
+This is a fundamental principle in Isabelle. A similar situation occurs
+for example with declaring constants. The function that declares a
+constant on the ML-level is @{ML_ind  add_consts_i in Sign}.
+If you write\footnote{Recall that ML-code  needs to be
+enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
+*}
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
+text {*
+for declaring the constant @{text "BAR"} with type @{typ nat} and
+run the code, then you indeed obtain a theory as result. But if you
+query the constant on the Isabelle level using the command \isacommand{term}
+\begin{isabelle}
+\isacommand{term}~@{text [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"'a\""}
+\end{isabelle}
+you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+blue) of polymorphic type. The problem is that the ML-expression above did
+not register the declaration with the current theory. This is what the command
+\isacommand{setup} is for. The constant is properly declared with
+*}
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
+text {*
+Now
+\begin{isabelle}
+\isacommand{term}~@{text [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"nat\""}
+\end{isabelle}
+returns a (black) constant with the type @{typ nat}.
+A similar command is \isacommand{local\_setup}, which expects a function
+of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+use the commands \isacommand{method\_setup} for installing methods in the
+current theory and \isacommand{simproc\_setup} for adding new simprocs to
+the current simpset.
 *}
 section {* Contexts (TBD) *}
 section {* Local Theories (TBD) *}

changeset 358	9cf3bc448210
parent 356	43df2d59fb98
child 359	be6538c7b41d