isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:5dcee4d751ad
+:0b337dedc306
 We can install this pretty printer with the function
 @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
+(*
+classes s
+ML {* @{typ "bool \<Rightarrow> ('a::s)"} *}
+ML {*
+fun test ty =
+case ty of
+TVar ((v, n), s) => Pretty.block [Pretty.str "TVar "]
+| TFree (x, s) => Pretty.block [Pretty.str "TFree "]
+| Type (s, tys) => Pretty.block [Pretty.str "Type "]
+*}
+ML {* toplevel_pp ["typ"] "test" *}
+*)
 text {*
 Now the type bool is printed out in full detail.
 @{ML_response [display,gray]
 section {* Theorems *}
 text {*
 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
 that can only be built by going through interfaces. As a consequence, every proof
-in Isabelle is correct by construction. This follows the tradition of the LCF approach.
+in Isabelle is correct by construction. This follows the tradition of the LCF-approach.
 To see theorems in ``action'', let us give a proof on the ML-level for the following
 statement:
 *}
 \begin{readmore}
 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
+Although we will explain the simplifier in more detail as tactic in
+Section~\ref{sec:simplifier}, the simplifier
+can be used to work directly over theorems, for example to unfold definitions. To show
 this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then
 unfold the constant @{term "True"} according to its definition (Line 2).
 @{ML_response_fake [display,gray,linenos]
 "Thm.reflexive @{cterm \"True\"}
 @{ML_response_fake [display, gray]
 "atomize_thm @{thm list.induct}"
 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
+\footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.}
 Theorems can also be produced from terms by giving an explicit proof.
 One way to achieve this is by using the function @{ML_ind prove in Goal}
 in the structure @{ML_struct Goal}. For example below we use this function
 to prove the term @{term "P \<Longrightarrow> P"}.
 is proved.  The fourth argument is the term to be proved. The fifth is a
 corresponding proof given in form of a tactic (we explain tactics in
 Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem
 by assumption. As before this code will produce a theorem, but the theorem
 is not yet stored in the theorem database.
+While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
+is the function @{ML_ind make_thm in Skip_Proof} in the structure
+@{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
+Potentially making the system unsound.  This is sometimes useful for developing
+purposes, or when explicit proof construction should be omitted due to performace
+reasons. An example of this function is as follows:
+@{ML_response_fake [display, gray]
+"Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
+"True = False"}
+The function @{ML make_thm in Skip_Proof} however only works if
+the ``quick-and-dirty'' mode is switched on.
 Theorems also contain auxiliary data, such as the name of the theorem, its
 kind, the names for cases and so on. This data is stored in a string-string
 list and can be retrieved with the function @{ML_ind get_tags in
 Thm}. Assume you prove the following lemma.
 text {*
 @{ML_ind "Binding.str_of"} returns the string with markup;
 @{ML_ind "Binding.name_of"} returns the string without markup
 *}
+section {* Concurrency (TBD) *}
+text {*
+@{ML_ind prove_future in Goal}
+@{ML_ind future_result in Goal}
+@{ML_ind fork_pri in Future}
+*}
 section {* Summary *}
 text {*
 \begin{conventions}

changeset 388	0b337dedc306
parent 387	5dcee4d751ad
child 389	4cc6df387ce9