Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/First_Steps.thy
changeset 481 32323727af96
parent 480 ae49c5e8868e
parent 479 7a84649d8839
child 482 9699ad581dc2
equal deleted inserted replaced
480:ae49c5e8868e 481:32323727af96 
   642   
   642   
   643   @{ML_response [display,gray]
 
   643   @{ML_response [display,gray]
 
   644   "acc_incs 1 ||>> (fn x => (x, x + 2))"
 
   644   "acc_incs 1 ||>> (fn x => (x, x + 2))"
 
   645   "(((((\"\", 1), 2), 3), 4), 6)"}
 
   645   "(((((\"\", 1), 2), 3), 4), 6)"}
 
   646 
   646 
   647   An example for this combinator is for example the following code
 
   647   A more realistic example for this combinator is the following code
 
   648 *}
 
   648 *}
 
   649 
   649 
   650 ML {*
 
   650 ML{*val (((one_def, two_def), three_def), ctxt') = 
   651 val (((one_def, two_def), three_def), ctxt') = 
       
   652   @{context}
 
   651   @{context}
 
   653   |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
   652   |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
   654   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
 
   653   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
 
   655   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
 
   654   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
 
   656 *}
 
   655 
   657 
   656 text {*
 
   658 ML {*
 
   657   where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
 
   659   @{context}
 
   658   and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
 
   660   |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
   659   context with the definitions. The result we are interested in is the
 
   661   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
 
   660   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 
   662   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
 
   661   information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
 
   663 *}
 
   662   both as pairs. We can use this information for example to print out the definiens and 
   664 
   663   the theorem corresponding to the definitions. For example for the first definition:
 
   665 
   664 
   666 text {*
 
   665   @{ML_response_fake [display, gray]
 
       
   666   "let 
       
   667   val (one_trm, one_thm) = one_def
 
       
   668 in
 
       
   669   pwriteln (pretty_term ctxt' one_trm);
 
       
   670   pwriteln (pretty_thm ctxt' one_thm)
 
       
   671 end"
 
       
   672   "one
 
       
   673 one \<equiv> 1"}
 
       
   674 
   667   Recall that @{ML "|>"} is the reverse function application. Recall also that
 
   675   Recall that @{ML "|>"} is the reverse function application. Recall also that
 
   668   the related reverse function composition is @{ML "#>"}. In fact all the
 
   676   the related reverse function composition is @{ML "#>"}. In fact all the
 
   669   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
 
   677   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
 
   670   described above have related combinators for function composition, namely
 
   678   described above have related combinators for function composition, namely
 
   671   @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
 
   679   @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
 
   729   "Pure/library.ML"}
 
   737   "Pure/library.ML"}
 
   730   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
   738   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
   731   contains further information about combinators.
 
   739   contains further information about combinators.
 
   732   \end{readmore}
 
   740   \end{readmore}
 
   733 
   741 
   734   \footnote{\bf FIXME: find a good exercise for combinators}
 
       
   735   \begin{exercise}
 
   742   \begin{exercise}
 
   736   Find out what the combinator @{ML "K I"} does.
 
   743   Find out what the combinator @{ML "K I"} does.
 
   737   \end{exercise}
 
   744   \end{exercise}
 
   738 
       
   739 
       
   740   \footnote{\bf FIXME: say something about calling conventions} 
       
   741 *}
 
   745 *}
 
   742 
   746 
   743 
   747 
   744 section {* ML-Antiquotations\label{sec:antiquote} *}
 
   748 section {* ML-Antiquotations\label{sec:antiquote} *}
 
   745 
   749 
   891 
   895 
   892 text {*
 
   896 text {*
 
   893   To use it you also have to install it using \isacommand{setup} like so
 
   897   To use it you also have to install it using \isacommand{setup} like so
 
   894 *}
 
   898 *}
 
   895 
   899 
   896 setup{* term_pat_setup *}
 
   900 setup %gray {* term_pat_setup *}
 
   897 
   901 
   898 text {*
 
   902 text {*
 
   899   The parser in Line 2 provides us with a context and a string; this string is
 
   903   The parser in Line 2 provides us with a context and a string; this string is
 
   900   transformed into a term using the function @{ML_ind read_term_pattern in
 
   904   transformed into a term using the function @{ML_ind read_term_pattern in
 
   901   Proof_Context} (Line 5); the next two lines transform the term into a string
 
   905   Proof_Context} (Line 5); the next two lines transform the term into a string
 
   924 
   928 
   925 text {*
 
   929 text {*
 
   926   which can be installed with
 
   930   which can be installed with
 
   927 *}
 
   931 *}
 
   928 
   932 
   929 setup{* type_pat_setup *}
 
   933 setup %gray {* type_pat_setup *}
 
   930 
   934 
   931 text {*
 
   935 text {*
 
   932   However, a word of warning is in order: Introducing new antiquotations
 
   936   However, a word of warning is in order: Introducing new antiquotations
 
   933   should be done only after careful deliberations. They can make your 
   937   should be done only after careful deliberations. They can make your 
   934   code harder to read, than making it easier. 
   938   code harder to read, than making it easier. 
  1239   @{ML_funct_ind Named_Thms}. This is because storing theorems in a list 
  1243   @{ML_funct_ind Named_Thms}. This is because storing theorems in a list 
  1240   is such a common task.  To obtain a named theorem list, you just declare
 
  1244   is such a common task.  To obtain a named theorem list, you just declare
 
  1241 *}
 
  1245 *}
 
  1242 
  1246 
  1243 ML{*structure FooRules = Named_Thms
 
  1247 ML{*structure FooRules = Named_Thms
 
  1244   (val name = "foo" 
  1248   (val name = @{binding "foo"} 
  1245    val description = "Theorems for foo") *}
 
  1249    val description = "Theorems for foo") *}
 
  1246 
  1250 
  1247 text {*
 
  1251 text {*
 
  1248   and set up the @{ML_struct FooRules} with the command
 
  1252   and set up the @{ML_struct FooRules} with the command
 
  1249 *}
 
  1253 *}
 
  1388   \item Do not use references in Isabelle code.
 
  1392   \item Do not use references in Isabelle code.
 
  1389   \end{itemize}
 
  1393   \end{itemize}
 
  1390   \end{conventions}
 
  1394   \end{conventions}
 
  1391 
  1395 
  1392 *}
 
  1396 *}
 
  1393 
       
  1394 
       
  1395 (**************************************************)
 
       
  1396 (* bak                                            *)
 
       
  1397 (**************************************************)
 
       
  1398 
       
  1399 (*
 
       
  1400 section {* Do Not Try This At Home! *}
 
       
  1401 
       
  1402 ML {* val my_thms = ref ([]: thm list) *}
 
       
  1403 
       
  1404 attribute_setup my_thm_bad =
 
       
  1405   {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
 
       
  1406       (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"
 
       
  1407 
       
  1408 declare sym [my_thm_bad]
 
       
  1409 declare refl [my_thm_bad]
 
       
  1410 
       
  1411 ML "!my_thms"
 
       
  1412 *)
 
       
  1413 end
 
  1397 end
isabelle-cookbook