--- 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}
--- 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*}
--- 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
--- 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,
--- 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 \<Rightarrow> 'a list"
+context linorder
+begin
-recdef merge "measure(%(xs,ys). size xs + size ys)"
- "merge(x#xs, y#ys) =
- (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
-
- "merge(xs,[]) = xs"
-
- "merge([],ys) = ys"
+fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ "merge (x#xs) (y#ys) =
+ (if x \<le> 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 \<union> set ys"
+lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
apply(induct xs ys rule: merge.induct)
apply auto
done
lemma sorted_merge[simp]:
- "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
+ "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) 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 \<Rightarrow> '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 \<Rightarrow> '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 \<le>) (msort xs)"
by (induct xs rule: msort.induct) simp_all
@@ -57,3 +57,6 @@
done
end
+
+
+end
--- 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",
--- /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;