# HG changeset patch # User Christian Urban # Date 1256169794 -7200 # Node ID 43df2d59fb98e73b8856152ecb0993bbe8957553 # Parent 42a1c230daff04e089ba689334f018c1a6ba6420 updated to new Isabelle diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/Appendix.thy --- a/ProgTutorial/Appendix.thy Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/Appendix.thy Thu Oct 22 02:03:14 2009 +0200 @@ -29,6 +29,8 @@ (@{ML_file "Pure/pattern.ML"} implements HOPU) \item useful datastructures: discrimination nets, association lists + + \item Brief history of Isabelle \end{itemize} *} diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/General.thy Thu Oct 22 02:03:14 2009 +0200 @@ -714,10 +714,11 @@ "let val natT = @{typ \"nat\"} val zero = @{term \"0::nat\"} + val plus = Const (@{const_name plus}, [natT, natT] ---> natT) in - cterm_of @{theory} - (Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero) -end" "0 + 0"} + cterm_of @{theory} (plus $ zero $ zero) +end" + "0 + 0"} In Isabelle not just terms need to be certified, but also types. For example, you obtain the certified type for the Isabelle type @{typ "nat \ bool"} on @@ -899,8 +900,7 @@ (type T = thm list val empty = [] val extend = I - val merge = K (op @) -) + val merge = K (op @)) fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*} @@ -1254,8 +1254,7 @@ We can now install a the modified theorem style as follows *} -setup %gray {* -let +setup %gray {* let val parser = Scan.repeat Args.name fun action xs = K (rename_allq xs #> strip_allq) in @@ -1288,8 +1287,8 @@ text {* Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \]"}, @{text "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags - annotated to theorems, but functions that do further processing once a - theorem is proved. In particular, it is not possible to find out + annotated to theorems, but functions that do further processing of + theorems. In particular, it is not possible to find out what are all theorems that have a given attribute in common, unless of course the function behind the attribute stores the theorems in a retrievable data structure. @@ -1306,9 +1305,9 @@ \end{isabelle} The theorem attributes fall roughly into two categories: the first category manipulates - the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \]"}), and the second - stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds - the theorem to the current simpset). + theorems (for example @{text "[symmetric]"} and @{text "[THEN \]"}), and the second + stores theorems somewhere as data (for example @{text "[simp]"}, which adds + theorems to the current simpset). To explain how to write your own attribute, let us start with an extremely simple version of the attribute @{text "[symmetric]"}. The purpose of this attribute is @@ -1330,15 +1329,14 @@ using the Isabelle command \isacommand{attribute\_setup} as follows: *} -attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *} - "applying the sym rule" +attribute_setup %gray my_sym = + {* Scan.succeed my_symmetric *} "applying the sym rule" text {* Inside the @{text "\ \ \"}, we have to specify a parser for the theorem attribute. Since the attribute does not expect any further - arguments (unlike @{text "[THEN \]"}, for example), we use the parser @{ML - Scan.succeed}. Later on we will also consider attributes taking further - arguments. An example for the attribute @{text "[my_sym]"} is the proof + arguments (unlike @{text "[THEN \]"}, for instance), we use the parser @{ML + Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof *} lemma test[my_sym]: "2 = Suc (Suc 0)" by simp @@ -1368,17 +1366,17 @@ "applying the sym rule" *} text {* - This gives a function from @{ML_type "Context.theory -> Context.theory"}, which + This gives a function from @{ML_type "theory -> theory"}, which can be used for example with \isacommand{setup}. As an example of a slightly more complicated theorem attribute, we implement our own version of @{text "[THEN \]"}. This attribute will take a list of theorems - as argument and resolve the proved theorem with this list (one theorem + 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 (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*} + Thm.rule_attribute (fn _ => fn thm => List.foldl ((op RS) o swap) thm thms)*} text {* where @{ML swap} swaps the components of a pair. The setup of this theorem @@ -1387,7 +1385,7 @@ *} attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} - "resolving the list of theorems with the proved theorem" + "resolving the list of theorems with the theorem" text {* You can, for example, use this theorem attribute to turn an equation into a @@ -1863,7 +1861,7 @@ a b"} - \footnote{\bf What happens with printing big formulae?} + \footnote{\bf FIXME: What happens with printing big formulae?} diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/Intro.thy Thu Oct 22 02:03:14 2009 +0200 @@ -26,14 +26,20 @@ If your next project requires you to program on the ML-level of Isabelle, then this tutorial is for you. It will guide you through the first steps of Isabelle programming, and also explain tricks of the trade. We also hope - the tutorial will encourage researchers to play with Isabelle. The best way to - get to know the ML-level of Isabelle is by experimenting with the many code - examples included in the tutorial. The code is as far as possible checked - against the Isabelle distribution.\footnote{\input{version}} If something does not work, - then please let us know. It is impossible for us to know every environment, - operating system or editor in which Isabelle is used. If you have comments, - criticism or like to add to the tutorial, please feel free---you are most - welcome! The tutorial is meant to be gentle and comprehensive. To achieve + the tutorial will encourage researchers to play with Isabelle and implement + new ideas. The sources of Isabelle can look intimidating, but beginners + can get by with knowledge of only a small number functions and a few basic + coding conventions. + + + The best way to get to know the ML-level of Isabelle is by experimenting + with the many code examples included in the tutorial. The code is as far as + possible checked against the Isabelle + distribution.\footnote{\input{version}} If something does not work, then + please let us know. It is impossible for us to know every environment, + operating system or editor in which Isabelle is used. If you have comments, + criticism or like to add to the tutorial, please feel free---you are most + welcome! The tutorial is meant to be gentle and comprehensive. To achieve this we need your feedback. *} diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/antiquote_setup.ML Thu Oct 22 02:03:14 2009 +0200 @@ -81,13 +81,13 @@ (* checks and expression agains a result pattern *) fun output_response {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_pat (lhs, pat)); - write_file_ml_blk lhs (Context.theory_of_proof ctxt); + write_file_ml_blk lhs (ProofContext.theory_of ctxt); output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_val [] NONE lhs); - write_file_ml_blk lhs (Context.theory_of_proof ctxt); + write_file_ml_blk lhs (ProofContext.theory_of ctxt); output ((split_lines lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) diff -r 42a1c230daff -r 43df2d59fb98 progtutorial.pdf Binary file progtutorial.pdf has changed