# HG changeset patch # User Christian Urban # Date 1298505337 0 # Node ID 242e81f4d461c8685b2e1a8a922ea98b26f0acae # Parent aedfdcae39a9520d3172650f6445a147403d574a updated to post-2011 Isabelle diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/Essential.thy Wed Feb 23 23:55:37 2011 +0000 @@ -1704,7 +1704,7 @@ val thm = @{thm foo_test1} val meta_eq = Object_Logic.atomize (cprop_of thm) in - MetaSimplifier.rewrite_rule [meta_eq] thm + Raw_Simplifier.rewrite_rule [meta_eq] thm end" "?A \ ?B \ ?C"} @@ -1728,7 +1728,7 @@ val thm' = forall_intr_vars thm val thm'' = Object_Logic.atomize (cprop_of thm') in - MetaSimplifier.rewrite_rule [thm''] thm' + Raw_Simplifier.rewrite_rule [thm''] thm' end*} text {* diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/First_Steps.thy Wed Feb 23 23:55:37 2011 +0000 @@ -158,34 +158,6 @@ @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} - It is also possible to redirect the ``channel'' where the string @{text - "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from - choking on massive amounts of trace output. This redirection can be achieved - with the code: -*} - -ML{*val strip_specials = -let - fun strip ("\^A" :: _ :: cs) = strip cs - | strip (c :: cs) = c :: strip cs - | strip [] = []; -in - implode o strip o explode -end - -fun redirect_tracing stream = - Output.Private_Hooks.tracing_fn := (fn s => - (TextIO.output (stream, (strip_specials s)); - TextIO.output (stream, "\n"); - TextIO.flushOut stream)) *} - -text {* - Calling now - - @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"} - - will cause that all tracing information is printed into the file @{text "foo.bar"}. - You can print out error messages with the function @{ML_ind error in Library}; for example: @@ -900,13 +872,13 @@ ML{*fun get_thm_names_from_ss simpset = let - val {simps,...} = MetaSimplifier.dest_ss simpset + val {simps,...} = Raw_Simplifier.dest_ss simpset in map #1 simps end*} text {* - The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all + The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all information stored in the simpset, but here we are only interested in the names of the simp-rules. Now you can feed in the current simpset into this function. The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/Parsing.thy Wed Feb 23 23:55:37 2011 +0000 @@ -90,7 +90,7 @@ In the examples above we use the function @{ML_ind explode in Symbol} from the structure @{ML_struct Symbol}, instead of the more standard library function @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is - that @{ML explode} in @{ML_struct Symbol} is aware of character + that @{ML explode in Symbol} is aware of character sequences, for example @{text "\"}, that have a special meaning in Isabelle. To see the difference consider @@ -98,7 +98,7 @@ "let val input = \"\ bar\" in - (explode input, Symbol.explode input) + (String.explode input, Symbol.explode input) end" "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"], [\"\\", \" \", \"b\", \"a\", \"r\"])"} diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Recipes/Sat.thy --- a/ProgTutorial/Recipes/Sat.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/Recipes/Sat.thy Wed Feb 23 23:55:37 2011 +0000 @@ -18,22 +18,22 @@ The SAT solvers expect a propositional formula as input and produce a result indicating that the formula is either satisfiable, unsatisfiable or unknown. The type of the propositional formula is - @{ML_type "PropLogic.prop_formula"} with the usual constructors such - as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on. + @{ML_type "Prop_Logic.prop_formula"} with the usual constructors such + as @{ML And in Prop_Logic}, @{ML Or in Prop_Logic} and so on. - The function @{ML PropLogic.prop_formula_of_term} translates an Isabelle + The function @{ML Prop_Logic.prop_formula_of_term} translates an Isabelle term into a propositional formula. Let us illustrate this function by translating @{term "A \ \A \ B"}. The function will return a propositional formula and a table. Suppose *} ML{*val (pform, table) = - PropLogic.prop_formula_of_term @{term "A \ \A \ B"} Termtab.empty*} + Prop_Logic.prop_formula_of_term @{term "A \ \A \ B"} Termtab.empty*} text {* then the resulting propositional formula @{ML pform} is - @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} + @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} where indices are assigned for the variables @@ -52,10 +52,10 @@ *} ML{*val (pform', table') = - PropLogic.prop_formula_of_term @{term "\x::nat. P x"} Termtab.empty*} + Prop_Logic.prop_formula_of_term @{term "\x::nat. P x"} Termtab.empty*} text {* - returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table + returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table @{ML table'} is: @{ML_response_fake [display,gray] diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/Solutions.thy Wed Feb 23 23:55:37 2011 +0000 @@ -83,8 +83,8 @@ @{ML_response [display,gray] "let - val input1 = (explode \"foo bar\") - val input2 = (explode \"foo (*test*) bar (*test*)\") + val input1 = (Symbol.explode \"foo bar\") + val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\") in (scan_all input1, scan_all input2) end" diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/Tactical.thy Wed Feb 23 23:55:37 2011 +0000 @@ -1400,7 +1400,7 @@ corresponding preconditions. \begin{readmore} - For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"} + For more information about the simplifier see @{ML_file "Pure/raw_simplifier.ML"} and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in @{ML_file "Provers/splitter.ML"}. \end{readmore} @@ -1413,9 +1413,9 @@ \begin{isabelle} \begin{tabular}{l@ {\hspace{10mm}}l} - @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\ - @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\ - @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\ + @{ML_ind addsimps in Raw_Simplifier} & @{ML_ind delsimps in Raw_Simplifier}\\ + @{ML_ind addcongs in Raw_Simplifier} & @{ML_ind delcongs in Raw_Simplifier}\\ + @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\ \end{tabular} \end{isabelle} @@ -1428,7 +1428,7 @@ \begin{isabelle}*} ML{*fun print_ss ctxt ss = let - val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss + val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss fun name_thm (nm, thm) = Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm] @@ -1445,7 +1445,7 @@ text_raw {* \end{isabelle} \end{minipage} -\caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing +\caption{The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all printable information stored in a simpset. We are here only interested in the simplification rules, congruence rules and simprocs.\label{fig:printss}} \end{figure} *} @@ -1454,7 +1454,7 @@ text {* To see how they work, consider the function in Figure~\ref{fig:printss}, which prints out some parts of a simpset. If you use it to print out the components of the - empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier} + empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier} @{ML_response_fake [display,gray] "print_ss @{context} empty_ss" @@ -1559,7 +1559,7 @@ \end{readmore} The simplifier is often used to unfold definitions in a proof. For this the - simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME: + simplifier implements the tactic @{ML_ind rewrite_goal_tac in Raw_Simplifier}.\footnote{\bf FIXME: see LocalDefs infrastructure.} Suppose for example the definition *} @@ -1581,7 +1581,7 @@ text {* If you want to unfold definitions in \emph{all} subgoals, not just one, - then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}. + then use the the tactic @{ML_ind rewrite_goals_tac in Raw_Simplifier}. *} @@ -1871,7 +1871,7 @@ Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). The function also takes a list of patterns that can trigger the simproc. Now the simproc is set up and can be explicitly added using - @{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever + @{ML_ind addsimprocs in Raw_Simplifier} to a simpset whenever needed. Simprocs are applied from inside to outside and from left to right. You can @@ -2539,7 +2539,7 @@ See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. Some basic conversions are defined in @{ML_file "Pure/thm.ML"}, - @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. + @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/raw_simplifier.ML"}. \end{readmore} *} diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Fri Oct 29 13:46:37 2010 +0200 +++ b/ProgTutorial/document/root.tex Wed Feb 23 23:55:37 2011 +0000 @@ -153,7 +153,7 @@ \title{\mbox{}\\[-10ex] \includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex] {\huge\bf The Isabelle Cookbook}\\ - \mbox{A Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} + \mbox{A Gentle Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)} \author{by Christian Urban with contributions from:\\[2ex] \begin{tabular}{r@{\hspace{1.8mm}}l} diff -r aedfdcae39a9 -r 242e81f4d461 progtutorial.pdf Binary file progtutorial.pdf has changed