# HG changeset patch # User Christian Urban # Date 1274116848 -3600 # Node ID 5e0a2b50707ea47a3082a89b193b784cd28feab9 # Parent 0a25b35178c33af23f3e616a2628838d6fbdbcf5 updated to new Isabelle diff -r 0a25b35178c3 -r 5e0a2b50707e ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Mon May 17 17:27:21 2010 +0100 +++ b/ProgTutorial/Parsing.thy Mon May 17 18:20:48 2010 +0100 @@ -41,8 +41,8 @@ "Pure/General/scan.ML"}. The second part of the library consists of combinators for dealing with specific token types, which are defined in the structure @{ML_struct OuterParse} in the file @{ML_file - "Pure/Isar/outer_parse.ML"}. In addition specific parsers for packages are - defined in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments + "Pure/Isar/parse.ML"}. In addition specific parsers for packages are + defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments are defined in @{ML_file "Pure/Isar/args.ML"}. \end{readmore} @@ -480,7 +480,7 @@ \begin{readmore} The parser functions for the theory syntax are contained in the structure - @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. + @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/parse.ML"}. The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}. \end{readmore} @@ -910,7 +910,7 @@ text_raw {* \begin{exercise} Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented - in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds + in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds to the ``where-part'' of the introduction rules given above. Below we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our purposes. diff -r 0a25b35178c3 -r 5e0a2b50707e ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Mon May 17 17:27:21 2010 +0100 +++ b/ProgTutorial/Solutions.thy Mon May 17 18:20:48 2010 +0100 @@ -254,7 +254,7 @@ | _ => Conv.all_conv ctrm end -val add_conv = More_Conv.bottom_conv add_simple_conv +val add_conv = Conv.bottom_conv add_simple_conv fun add_tac ctxt = CONVERSION (add_conv ctxt)*} diff -r 0a25b35178c3 -r 5e0a2b50707e ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Mon May 17 17:27:21 2010 +0100 +++ b/ProgTutorial/Tactical.thy Mon May 17 18:20:48 2010 +0100 @@ -2262,7 +2262,7 @@ "True \ P \ True \ P"} Rewriting with more than one theorem can be done using the function - @{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}. + @{ML_ind rewrs_conv in Conv} from the structure @{ML_struct Conv}. Apart from the function @{ML beta_conversion in Thm}, which is able to fully @@ -2345,21 +2345,21 @@ text {* Conversions that traverse terms, like @{ML true_conj1_conv} above, can be implemented more succinctly with the combinators @{ML_ind bottom_conv in - More_Conv} and @{ML_ind top_conv in More_Conv}. For example: + Conv} and @{ML_ind top_conv in Conv}. For example: *} ML{*fun true_conj1_conv ctxt = let val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) in - More_Conv.bottom_conv (K conv) ctxt + Conv.bottom_conv (K conv) ctxt end*} text {* If we regard terms as trees with variables and constants on the top, then - @{ML bottom_conv in More_Conv} traverses first the the term and + @{ML bottom_conv in Conv} traverses first the the term and on the ``way down'' applies the conversion, whereas @{ML top_conv in - More_Conv} applies the conversion on the ``way up''. To see the difference, + Conv} applies the conversion on the ``way up''. To see the difference, assume the following two meta-equations *} @@ -2378,9 +2378,9 @@ @{ML_response_fake [display, gray] "let val ctxt = @{context} - val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc}) - val conv_top = More_Conv.top_conv (K conv) ctxt - val conv_bot = More_Conv.bottom_conv (K conv) ctxt + val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc}) + val conv_top = Conv.top_conv (K conv) ctxt + val conv_bot = Conv.bottom_conv (K conv) ctxt val ctrm = @{cterm \"(a \ (b \ c)) \ d\"} in (conv_top ctrm, conv_bot ctrm) @@ -2400,13 +2400,13 @@ Conv.arg_conv (true_conj1_conv ctxt) ctrm | _ => Conv.no_conv ctrm -val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*} +val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv*} text {* In the first function we only treat the top-most redex and also only the success case. As default we return @{ML no_conv in Conv}. To apply this ``simple'' conversion inside a term, we use in the last line the combinator @{ML_ind - top_sweep_conv in More_Conv}, which traverses the term starting from the + top_sweep_conv in Conv}, which traverses the term starting from the root and applies it to all the redexes on the way, but stops in each branch as soon as it found one redex. Here is an example for this conversion: @@ -2496,7 +2496,7 @@ As you can see, the premises are rewritten according to @{ML if_true1_conv}, while the conclusion according to @{ML true_conj1_conv}. If we only have one conversion that should be uniformly applied to the whole goal state, we - can simplify @{ML true1_tac} using @{ML_ind top_conv in More_Conv}. + can simplify @{ML true1_tac} using @{ML_ind top_conv in Conv}. Conversions are also be helpful for constructing meta-equality theorems. Such theorems are often definitions. As an example consider the following @@ -2592,7 +2592,7 @@ \end{exercise} \begin{readmore} - See @{ML_file "Pure/conv.ML"} and @{ML_file "Tools/more_conv.ML"} + 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"}. diff -r 0a25b35178c3 -r 5e0a2b50707e progtutorial.pdf Binary file progtutorial.pdf has changed