# HG changeset patch # User haftmann # Date 1233675610 -3600 # Node ID dce05b909056f776d78197258f25dd7de5e37b52 # Parent 1e3afd4fe3a32b7b403bdf0843e7701fd7adfc31# Parent 02e76245e5af353c32f60e8a4692e6116659c7e3 merged diff -r 02e76245e5af -r dce05b909056 doc-src/IsarAdvanced/Functions/Thy/Functions.thy --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Tue Feb 03 16:39:52 2009 +0100 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Tue Feb 03 16:40:10 2009 +0100 @@ -1,5 +1,4 @@ -(* Title: Doc/IsarAdvanced/Functions/Thy/Fundefs.thy - ID: $Id$ +(* Title: doc-src/IsarAdvanced/Functions/Thy/Fundefs.thy Author: Alexander Krauss, TU Muenchen Tutorial for function definitions with the new "function" package. @@ -712,7 +711,7 @@ text {* \noindent Clearly, any attempt of a termination proof must fail. And without - that, we do not get the usual rules @{text "findzero.simp"} and + that, we do not get the usual rules @{text "findzero.simps"} and @{text "findzero.induct"}. So what was the definition good for at all? *} @@ -953,7 +952,7 @@ The predicate @{term "accp findzero_rel"} is the accessible part of that relation. An argument belongs to the accessible part, if it can be reached in a finite number of steps (cf.~its definition in @{text - "Accessible_Part.thy"}). + "Wellfounded.thy"}). Since the domain predicate is just an abbreviation, you can use lemmas for @{const accp} and @{const findzero_rel} directly. Some @@ -1136,7 +1135,7 @@ text {* Higher-order recursion occurs when recursive calls - are passed as arguments to higher-order combinators such as @{term + are passed as arguments to higher-order combinators such as @{const map}, @{term filter} etc. As an example, imagine a datatype of n-ary trees: *} @@ -1164,7 +1163,7 @@ As usual, we have to give a wellfounded relation, such that the arguments of the recursive calls get smaller. But what exactly are the arguments of the recursive calls when mirror is given as an - argument to map? Isabelle gives us the + argument to @{const map}? Isabelle gives us the subgoals @{subgoals[display,indent=0]} @@ -1173,9 +1172,9 @@ applies the recursive call @{term "mirror"} to elements of @{term "l"}, which is essential for the termination proof. - This knowledge about map is encoded in so-called congruence rules, + This knowledge about @{const map} is encoded in so-called congruence rules, which are special theorems known to the \cmd{function} command. The - rule for map is + rule for @{const map} is @{thm[display] map_cong} diff -r 02e76245e5af -r dce05b909056 src/HOL/Int.thy --- a/src/HOL/Int.thy Tue Feb 03 16:39:52 2009 +0100 +++ b/src/HOL/Int.thy Tue Feb 03 16:40:10 2009 +0100 @@ -478,6 +478,9 @@ end +text {* For termination proofs: *} +lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. + subsection{*Lemmas about the Function @{term of_nat} and Orderings*} diff -r 02e76245e5af -r dce05b909056 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Tue Feb 03 16:39:52 2009 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Tue Feb 03 16:40:10 2009 +0100 @@ -8,8 +8,8 @@ signature LEXICOGRAPHIC_ORDER = sig val lexicographic_order : thm list -> Proof.context -> Method.method + val lexicographic_order_tac : Proof.context -> tactic -> tactic - (* exported for debugging *) val setup: theory -> theory end diff -r 02e76245e5af -r dce05b909056 src/HOL/Tools/function_package/scnp_solve.ML --- a/src/HOL/Tools/function_package/scnp_solve.ML Tue Feb 03 16:39:52 2009 +0100 +++ b/src/HOL/Tools/function_package/scnp_solve.ML Tue Feb 03 16:40:10 2009 +0100 @@ -151,33 +151,33 @@ val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp fun encode_graph MAX (g, p, q, n, m, _) = - all [ + And ( Equiv (WEAK g, iforall m (fn j => Implies (P (q, j), iexists n (fn i => And (P (p, i), EW (g, i, j)))))), Equiv (STRICT g, - iforall m (fn j => - Implies (P (q, j), - iexists n (fn i => - And (P (p, i), ES (g, i, j)))))), - iexists n (fn i => P (p, i)) - ] + And ( + iforall m (fn j => + Implies (P (q, j), + iexists n (fn i => + And (P (p, i), ES (g, i, j))))), + iexists n (fn i => P (p, i))))) | encode_graph MIN (g, p, q, n, m, _) = - all [ + And ( Equiv (WEAK g, iforall n (fn i => Implies (P (p, i), iexists m (fn j => And (P (q, j), EW (g, i, j)))))), Equiv (STRICT g, - iforall n (fn i => - Implies (P (p, i), - iexists m (fn j => - And (P (q, j), ES (g, i, j)))))), - iexists m (fn j => P (q, j)) - ] + And ( + iforall n (fn i => + Implies (P (p, i), + iexists m (fn j => + And (P (q, j), ES (g, i, j))))), + iexists m (fn j => P (q, j))))) | encode_graph MS (g, p, q, n, m, _) = all [ Equiv (WEAK g, diff -r 02e76245e5af -r dce05b909056 src/HOL/ex/MergeSort.thy --- a/src/HOL/ex/MergeSort.thy Tue Feb 03 16:39:52 2009 +0100 +++ b/src/HOL/ex/MergeSort.thy Tue Feb 03 16:40:10 2009 +0100 @@ -10,40 +10,40 @@ imports Sorting begin -consts merge :: "('a::linorder)list * 'a list \ 'a list" +context linorder +begin -recdef merge "measure(%(xs,ys). size xs + size ys)" - "merge(x#xs, y#ys) = - (if x \ y then x # merge(xs, y#ys) else y # merge(x#xs, ys))" - - "merge(xs,[]) = xs" - - "merge([],ys) = ys" +fun merge :: "'a list \ 'a list \ 'a list" +where + "merge (x#xs) (y#ys) = + (if x \ y then x # merge xs (y#ys) else y # merge (x#xs) ys)" +| "merge xs [] = xs" +| "merge [] ys = ys" lemma multiset_of_merge[simp]: - "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys" + "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys" apply(induct xs ys rule: merge.induct) apply (auto simp: union_ac) done -lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \ set ys" +lemma set_merge[simp]: "set (merge xs ys) = set xs \ set ys" apply(induct xs ys rule: merge.induct) apply auto done lemma sorted_merge[simp]: - "sorted (op \) (merge(xs,ys)) = (sorted (op \) xs & sorted (op \) ys)" + "sorted (op \) (merge xs ys) = (sorted (op \) xs & sorted (op \) ys)" apply(induct xs ys rule: merge.induct) -apply(simp_all add: ball_Un linorder_not_le order_less_le) +apply(simp_all add: ball_Un not_le less_le) apply(blast intro: order_trans) done -consts msort :: "('a::linorder) list \ 'a list" -recdef msort "measure size" - "msort [] = []" - "msort [x] = [x]" - "msort xs = merge(msort(take (size xs div 2) xs), - msort(drop (size xs div 2) xs))" +fun msort :: "'a list \ 'a list" +where + "msort [] = []" +| "msort [x] = [x]" +| "msort xs = merge (msort (take (size xs div 2) xs)) + (msort (drop (size xs div 2) xs))" theorem sorted_msort: "sorted (op \) (msort xs)" by (induct xs rule: msort.induct) simp_all @@ -57,3 +57,6 @@ done end + + +end diff -r 02e76245e5af -r dce05b909056 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Feb 03 16:39:52 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Tue Feb 03 16:40:10 2009 +0100 @@ -3,8 +3,6 @@ Miscellaneous examples for Higher-Order Logic. *) -set Toplevel.timing; - no_document use_thys [ "State_Monad", "Efficient_Nat_examples", diff -r 02e76245e5af -r dce05b909056 src/Pure/ML-Systems/polyml-experimental.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Tue Feb 03 16:40:10 2009 +0100 @@ -0,0 +1,76 @@ +(* Title: Pure/ML-Systems/polyml.ML + +Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. +*) + +open Thread; +use "ML-Systems/polyml_common.ML"; +use "ML-Systems/multithreading_polyml.ML"; + +val pointer_eq = PolyML.pointerEq; + +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; + + +(* toplevel pretty printers *) + +(*dummy version*) +fun make_pp path pprint = (); +fun install_pp _ = (); + + +(* runtime compilation *) + +structure ML_NameSpace = +struct + open PolyML.NameSpace; + val global = PolyML.globalNameSpace; +end; + +local + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +in + +fun use_text (tune: string -> string) str_of_pos + name_space (start_line, name) (print, err) verbose txt = + let + val current_line = ref start_line; + val in_buffer = ref (String.explode (tune txt)); + val out_buffer = ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => + (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun put_message (prt, is_err, {file, line, offset}) = + (put (if is_err then "Error: " else "Warning: "); + PolyML.prettyPrint (put, 76) prt; + put (str_of_pos line name ^ "\n")); + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPErrorMessageProc put_message, + PolyML.Compiler.CPNameSpace name_space]; + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + err (output ()); raise exn); + in if verbose then print (output ()) else () end; + +fun use_file tune str_of_pos name_space output verbose name = + let + val instream = TextIO.openIn name; + val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); + in use_text tune str_of_pos name_space (1, name) output verbose txt end; + +end;