isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:2c392f61f400
+:a2e49e0771b3
 local_setup %gray {*
 Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 text {*
-The fourth argument of @{ML note in Local_Theory} is the list of theorems we
+The third argument of @{ML note in Local_Theory} is the list of theorems we
 want to store under a name. We can store more than one under a single name.
-The first argument @{ML_ind theoremK in Thm} is
+The first argument of @{ML note in Local_Theory} is the name under
-a kind indicator, which classifies the theorem. There are several such kind
+which we store the theorem or theorems. The second argument can contain a
-indicators: for a theorem arising from a definition you should use @{ML_ind
-definitionK in Thm}, and for
-``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
-in Thm}.  The second argument of @{ML note in Local_Theory} is the name under
-which we store the theorem or theorems. The third argument can contain a
 list of theorem attributes, which we will explain in detail in
 Section~\ref{sec:attributes}. Below we just use one such attribute for
 adding the theorem to the simpset:
 *}
 as argument and resolve the theorem with this list (one theorem
 after another). The code for this attribute is
 *}
 ML{*fun MY_THEN thms =
-Thm.rule_attribute
+let
-(fn _ => fn thm => fold (curry ((op RS) o swap)) thms thm)*}
+fun RS_rev thm1 thm2 = thm2 RS thm1
+in
+Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
+end*}
 text {*
-where @{ML swap} swaps the components of a pair. The setup of this theorem
+where for convenience we define the reverse and curried version of @{ML RS}.
-attribute uses the parser @{ML thms in Attrib}, which parses a list of
+The setup of this theorem attribute uses the parser @{ML thms in Attrib},
-theorems.
+which parses a list of theorems.
 *}
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
 "resolving the list of theorems with the theorem"
 We used in this example two functions declared as @{ML_ind
 declaration_attribute in Thm}, but there can be any number of them. We just
 have to change the parser for reading the arguments accordingly.
 \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
+\footnote{\bf FIXME readmore}
 \begin{readmore}
 FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in
 @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
 parsing.
 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21
 and 22
 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
 28"}
-Next we like to pretty-print a term and its type. For this we use the
+Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out
-function @{text "tell_type"}.
+a list of items, but automatically inserts forced breaks between each item.
-*}
+Compare
-ML %linenosgray{*fun tell_type ctxt t =
+@{ML_response_fake [display,gray]
-let
+"let
-fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
+val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
-val ptrm = Pretty.quote (Syntax.pretty_term ctxt t)
+in
-val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t))
+pprint (Pretty.blk (0, a_and_b));
-in
+pprint (Pretty.chunks a_and_b)
-pprint (Pretty.blk (0,
+end"
-(pstr "The term " @ [ptrm] @ pstr " has type "
+"ab
-@ [pty, Pretty.str "."])))
+a
-end*}
+b"}
-text {*
-In Line 3 we define a function that inserts possible linebreaks in places
-where a space is. In Lines 4 and 5 we pretty-print the term and its type
-using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind
-pretty_typ in Syntax}. We also use the function @{ML_ind quote in
-Pretty} in order to enclose the term and type inside quotation marks. In
-Line 9 we add a period right after the type without the possibility of a
-line break, because we do not want that a line break occurs there.
-Now you can write
-@{ML_response_fake [display,gray]
-"tell_type @{context} @{term \"min (Suc 0)\"}"
-"The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
-To see the proper line breaking, you can try out the function on a bigger term
-and type. For example:
-@{ML_response_fake [display,gray]
-"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
-"The term \"op = (op = (op = (op = (op = op =))))\" has type
-\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 The function @{ML_ind big_list in Pretty} helps with printing long lists.
 It is used for example in the command \isacommand{print\_theorems}. An
 example is as follows.
 7
 8
 9
 10"}
-Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out
+The point of the pretty-printing functions is to conveninetly obtain
-a list of items, but automatically inserts forced breaks between each item.
+a lay-out of terms and types that is pleasing to the eye. If we print
-Compare
+out the the terms produced by the the function @{ML de_bruijn} from
+exercise~\ref{ex:debruijn} we obtain the following:
-@{ML_response_fake [display,gray]
-"let
+@{ML_response_fake [display,gray]
-val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+"pprint (Syntax.pretty_term  @{context} (de_bruijn 4))"
-in
+"(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
-pprint (Pretty.blk (0, a_and_b));
+(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
-pprint (Pretty.chunks a_and_b)
+(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
-end"
+(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
-"ab
+P 4 \<and> P 3 \<and> P 2 \<and> P 1"}
-a
-b"}
+We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
+terms. Next we like to pretty-print a term and its type. For this we use the
+function @{text "tell_type"}.
+*}
+ML %linenosgray{*fun tell_type ctxt trm =
+let
+fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
+val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm)
+val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm))
+in
+pprint (Pretty.blk (0,
+(pstr "The term " @ [ptrm] @ pstr " has type "
+@ [pty, Pretty.str "."])))
+end*}
+text {*
+In Line 3 we define a function that inserts possible linebreaks in places
+where a space is. In Lines 4 and 5 we pretty-print the term and its type
+using the functions @{ML pretty_term in Syntax} and @{ML_ind
+pretty_typ in Syntax}. We also use the function @{ML_ind quote in
+Pretty} in order to enclose the term and type inside quotation marks. In
+Line 9 we add a period right after the type without the possibility of a
+line break, because we do not want that a line break occurs there.
+Now you can write
+@{ML_response_fake [display,gray]
+"tell_type @{context} @{term \"min (Suc 0)\"}"
+"The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
-\footnote{\bf FIXME: What happens with printing big formulae?}
+To see the proper line breaking, you can try out the function on a bigger term
+and type. For example:
+@{ML_response_fake [display,gray]
+"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
+"The term \"op = (op = (op = (op = (op = op =))))\" has type
+\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 \begin{readmore}
 The general infrastructure for pretty-printing is implemented in the file
 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
 contains pretty-printing functions for terms, types, theorems and so on.
 @{ML_file "Pure/General/markup.ML"}
 \end{readmore}
 *}
-(*
-text {*
-printing into the goal buffer as part of the proof state
-*}
-text {* writing into the goal buffer *}
-ML {* fun my_hook interactive state =
-(interactive ? Proof.goal_message (fn () => Pretty.str
-"foo")) state
-*}
-setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
-lemma "False"
-oops
-*)
-(*
-ML {*
-fun setmp_show_all_types f =
-setmp show_all_types
-(! show_types orelse ! show_sorts orelse ! show_all_types) f;
-val ctxt = @{context};
-val t1 = @{term "undefined::nat"};
-val t2 = @{term "Suc y"};
-val pty =        Pretty.block (Pretty.breaks
-[(setmp show_question_marks false o setmp_show_all_types)
-(Syntax.pretty_term ctxt) t1,
-Pretty.str "=", Syntax.pretty_term ctxt t2]);
-pty |> Pretty.string_of
-*}
-text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-*)
 section {* Summary *}
 text {*
 \begin{conventions}
 \begin{itemize}

changeset 396	a2e49e0771b3
parent 395	2c392f61f400
child 398	7f7080ce7c2b