1.1 --- a/NEWS Sat Nov 27 19:41:28 2010 +0100
1.2 +++ b/NEWS Sat Nov 27 19:41:37 2010 +0100
1.3 @@ -521,6 +521,9 @@
1.4
1.5 *** ML ***
1.6
1.7 +* Former exception Library.UnequalLengths now coincides with
1.8 +ListPair.UnequalLengths.
1.9 +
1.10 * Renamed raw "explode" function to "raw_explode" to emphasize its
1.11 meaning. Note that internally to Isabelle, Symbol.explode is used in
1.12 almost all situations.
2.1 --- a/doc-src/LaTeXsugar/Sugar/document/root.tex Sat Nov 27 19:41:28 2010 +0100
2.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Sat Nov 27 19:41:37 2010 +0100
2.3 @@ -3,23 +3,7 @@
2.4
2.5 % further packages required for unusual symbols (see also isabellesym.sty)
2.6 % use only when needed
2.7 -\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
2.8 - % \<sqsupset>, \<mho>, \<Join>,
2.9 - % \<lhd>, \<lesssim>, \<greatersim>,
2.10 - % \<lessapprox>, \<greaterapprox>,
2.11 - % \<triangleq>, \<yen>, \<lozenge>
2.12 -%\usepackage[greek,english]{babel} % greek for \<euro>,
2.13 - % english for \<guillemotleft>,
2.14 - % \<guillemotright>
2.15 - % default language = last
2.16 -%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
2.17 - % \<twosuperior>, \<onehalf>,
2.18 - % \<threesuperior>, \<threequarters>,
2.19 - % \<degree>
2.20 -%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
2.21 -%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
2.22 - % (only needed if amssymb not used)
2.23 -%\usepackage{textcomp} % for \<cent>, \<currency>
2.24 +\usepackage{amssymb}
2.25
2.26 \usepackage{mathpartir}
2.27
3.1 --- a/doc-src/Main/main.tex Sat Nov 27 19:41:28 2010 +0100
3.2 +++ b/doc-src/Main/main.tex Sat Nov 27 19:41:37 2010 +0100
3.3 @@ -9,31 +9,8 @@
3.4 \textheight=234mm
3.5
3.6 \usepackage{../isabelle,../isabellesym}
3.7 -
3.8 -% further packages required for unusual symbols (see also
3.9 -% isabellesym.sty), use only when needed
3.10 -
3.11 \usepackage{amssymb}
3.12 - %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
3.13 - %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
3.14 - %\<triangleq>, \<yen>, \<lozenge>
3.15 -
3.16 -%\usepackage[greek,english]{babel}
3.17 - %option greek for \<euro>
3.18 - %option english (default language) for \<guillemotleft>, \<guillemotright>
3.19 -
3.20 -%\usepackage[latin1]{inputenc}
3.21 - %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
3.22 - %\<threesuperior>, \<threequarters>, \<degree>
3.23 -
3.24 \usepackage[only,bigsqcap]{stmaryrd}
3.25 - %for \<Sqinter>
3.26 -
3.27 -%\usepackage{eufrak}
3.28 - %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
3.29 -
3.30 -%\usepackage{textcomp}
3.31 - %for \<cent>, \<currency>
3.32
3.33 % this should be the last package used
3.34 \usepackage{../pdfsetup}
4.1 --- a/src/HOL/Fun.thy Sat Nov 27 19:41:28 2010 +0100
4.2 +++ b/src/HOL/Fun.thy Sat Nov 27 19:41:37 2010 +0100
4.3 @@ -155,11 +155,6 @@
4.4 shows "inj f"
4.5 using assms unfolding inj_on_def by auto
4.6
4.7 -text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
4.8 -lemma datatype_injI:
4.9 - "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
4.10 -by (simp add: inj_on_def)
4.11 -
4.12 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
4.13 by (unfold inj_on_def, blast)
4.14
5.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Nov 27 19:41:28 2010 +0100
5.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Nov 27 19:41:37 2010 +0100
5.3 @@ -103,11 +103,6 @@
5.4
5.5 fun iszero (k,r) = r =/ rat_0;
5.6
5.7 -fun fold_rev2 f l1 l2 b =
5.8 - case (l1,l2) of
5.9 - ([],[]) => b
5.10 - | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
5.11 - | _ => error "fold_rev2";
5.12
5.13 (* Vectors. Conventionally indexed 1..n. *)
5.14
6.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Nov 27 19:41:28 2010 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Nov 27 19:41:37 2010 +0100
6.3 @@ -19,7 +19,7 @@
6.4 lemma injective_scaleR:
6.5 assumes "(c :: real) ~= 0"
6.6 shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
6.7 -by (metis assms datatype_injI injI real_vector.scale_cancel_left)
6.8 + by (metis assms injI real_vector.scale_cancel_left)
6.9
6.10 lemma linear_add_cmul:
6.11 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
7.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat Nov 27 19:41:28 2010 +0100
7.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Nov 27 19:41:37 2010 +0100
7.3 @@ -117,13 +117,6 @@
7.4 [] => []
7.5 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
7.6
7.7 -
7.8 -fun forall2 p l1 l2 = case (l1,l2) of
7.9 - ([],[]) => true
7.10 - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
7.11 - | _ => false;
7.12 -
7.13 -
7.14 fun vertices vs eqs =
7.15 let
7.16 fun vertex cmb = case solve(vs,cmb) of
7.17 @@ -131,16 +124,16 @@
7.18 | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
7.19 val rawvs = map_filter vertex (combinations (length vs) eqs)
7.20 val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
7.21 - in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
7.22 + in fold_rev (insert (eq_list op =/)) unset []
7.23 end
7.24
7.25 -fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
7.26 +val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
7.27
7.28 fun subsume todo dun = case todo of
7.29 [] => dun
7.30 |v::ovs =>
7.31 - let val dun' = if exists (fn w => subsumes w v) dun then dun
7.32 - else v::(filter (fn w => not(subsumes v w)) dun)
7.33 + let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
7.34 + else v:: filter (fn w => not (subsumes (v, w))) dun
7.35 in subsume ovs dun'
7.36 end;
7.37
7.38 @@ -246,10 +239,6 @@
7.39 Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
7.40 | _ => raise CTERM ("norm_canon_conv", [ct])
7.41
7.42 -fun fold_rev2 f [] [] z = z
7.43 - | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
7.44 - | fold_rev2 f _ _ _ = raise UnequalLengths;
7.45 -
7.46 fun int_flip v eq =
7.47 if FuncUtil.Intfunc.defined eq v
7.48 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
8.1 --- a/src/HOL/Statespace/document/root.tex Sat Nov 27 19:41:28 2010 +0100
8.2 +++ b/src/HOL/Statespace/document/root.tex Sat Nov 27 19:41:37 2010 +0100
8.3 @@ -1,31 +1,5 @@
8.4 \documentclass[11pt,a4paper]{article}
8.5 \usepackage{isabelle,isabellesym}
8.6 -
8.7 -% further packages required for unusual symbols (see also
8.8 -% isabellesym.sty), use only when needed
8.9 -
8.10 -%\usepackage{amssymb}
8.11 - %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
8.12 - %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
8.13 - %\<triangleq>, \<yen>, \<lozenge>
8.14 -
8.15 -%\usepackage[greek,english]{babel}
8.16 - %option greek for \<euro>
8.17 - %option english (default language) for \<guillemotleft>, \<guillemotright>
8.18 -
8.19 -%\usepackage[latin1]{inputenc}
8.20 - %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
8.21 - %\<threesuperior>, \<threequarters>, \<degree>
8.22 -
8.23 -%\usepackage[only,bigsqcap]{stmaryrd}
8.24 - %for \<Sqinter>
8.25 -
8.26 -%\usepackage{eufrak}
8.27 - %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
8.28 -
8.29 -%\usepackage{textcomp}
8.30 - %for \<cent>, \<currency>
8.31 -
8.32 % this should be the last package used
8.33 \usepackage{pdfsetup}
8.34
9.1 --- a/src/HOL/Tools/Datatype/datatype.ML Sat Nov 27 19:41:28 2010 +0100
9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Sat Nov 27 19:41:37 2010 +0100
9.3 @@ -54,6 +54,8 @@
9.4 val Suml_inject = @{thm Suml_inject};
9.5 val Sumr_inject = @{thm Sumr_inject};
9.6
9.7 +val datatype_injI =
9.8 + @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
9.9
9.10
9.11 (** proof of characteristic theorems **)
9.12 @@ -438,8 +440,7 @@
9.13 Lim_inject :: inj_thms') @ fun_congs) 1),
9.14 atac 1]))])])])]);
9.15
9.16 - val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
9.17 - (split_conj_thm inj_thm);
9.18 + val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
9.19
9.20 val elem_thm =
9.21 Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
10.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML Sat Nov 27 19:41:28 2010 +0100
10.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sat Nov 27 19:41:37 2010 +0100
10.3 @@ -324,7 +324,7 @@
10.4 \ nested recursion")
10.5 | (SOME {index, descr, ...}) =>
10.6 let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
10.7 - val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
10.8 + val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
10.9 typ_error T ("Type constructor " ^ tname ^ " used with wrong\
10.10 \ number of arguments")
10.11 in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
11.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Nov 27 19:41:28 2010 +0100
11.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Nov 27 19:41:37 2010 +0100
11.3 @@ -48,8 +48,8 @@
11.4
11.5 fun make_tnames Ts =
11.6 let
11.7 - fun type_name (TFree (name, _)) = implode (tl (raw_explode name)) (* FIXME Symbol.explode (?) *)
11.8 - | type_name (Type (name, _)) =
11.9 + fun type_name (TFree (name, _)) = unprefix "'" name
11.10 + | type_name (Type (name, _)) =
11.11 let val name' = Long_Name.base_name name
11.12 in if Syntax.is_identifier name' then name' else "x" end;
11.13 in indexify_names (map type_name Ts) end;
12.1 --- a/src/HOL/Tools/Function/function_lib.ML Sat Nov 27 19:41:28 2010 +0100
12.2 +++ b/src/HOL/Tools/Function/function_lib.ML Sat Nov 27 19:41:37 2010 +0100
12.3 @@ -44,11 +44,11 @@
12.4
12.5 fun map4 _ [] [] [] [] = []
12.6 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
12.7 - | map4 _ _ _ _ _ = raise Library.UnequalLengths;
12.8 + | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
12.9
12.10 fun map7 _ [] [] [] [] [] [] [] = []
12.11 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
12.12 - | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
12.13 + | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
12.14
12.15
12.16
13.1 --- a/src/HOL/Tools/Function/size.ML Sat Nov 27 19:41:28 2010 +0100
13.2 +++ b/src/HOL/Tools/Function/size.ML Sat Nov 27 19:41:37 2010 +0100
13.3 @@ -71,7 +71,7 @@
13.4 val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
13.5 map (fn T as TFree (s, _) =>
13.6 let
13.7 - val name = "f" ^ implode (tl (raw_explode s)); (* FIXME Symbol.explode (?) *)
13.8 + val name = "f" ^ unprefix "'" s;
13.9 val U = T --> HOLogic.natT
13.10 in
13.11 (((s, Free (name, U)), U), name)
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Nov 27 19:41:28 2010 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Nov 27 19:41:37 2010 +0100
14.3 @@ -393,7 +393,7 @@
14.4 | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
14.5 accum =
14.6 (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
14.7 - handle Library.UnequalLengths =>
14.8 + handle ListPair.UnequalLengths =>
14.9 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
14.10 | do_mtype_comp _ _ (MType _) (MType _) accum =
14.11 accum (* no need to compare them thanks to the cache *)
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Nov 27 19:41:28 2010 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Nov 27 19:41:37 2010 +0100
15.3 @@ -527,7 +527,7 @@
15.4 | NONE =>
15.5 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
15.6 $ Abs (s, T, kill ss Ts ts))
15.7 - | kill _ _ _ = raise UnequalLengths
15.8 + | kill _ _ _ = raise ListPair.UnequalLengths
15.9 fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
15.10 gather (ss @ [s1]) (Ts @ [T1]) t1
15.11 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Nov 27 19:41:28 2010 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Nov 27 19:41:37 2010 +0100
16.3 @@ -204,7 +204,7 @@
16.4
16.5 fun map3 _ [] [] [] = []
16.6 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
16.7 - | map3 _ _ _ _ = raise UnequalLengths
16.8 + | map3 _ _ _ _ = raise ListPair.UnequalLengths
16.9
16.10 fun double_lookup eq ps key =
16.11 case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
17.1 --- a/src/HOL/Tools/groebner.ML Sat Nov 27 19:41:28 2010 +0100
17.2 +++ b/src/HOL/Tools/groebner.ML Sat Nov 27 19:41:37 2010 +0100
17.3 @@ -233,14 +233,9 @@
17.4
17.5 fun align ((p,hp),(q,hq)) =
17.6 if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
17.7 -fun forall2 p l1 l2 =
17.8 - case (l1,l2) of
17.9 - ([],[]) => true
17.10 - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
17.11 - | _ => false;
17.12
17.13 fun poly_eq p1 p2 =
17.14 - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
17.15 + eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
17.16
17.17 fun memx ((p1,h1),(p2,h2)) ppairs =
17.18 not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
18.1 --- a/src/HOL/Tools/record.ML Sat Nov 27 19:41:28 2010 +0100
18.2 +++ b/src/HOL/Tools/record.ML Sat Nov 27 19:41:37 2010 +0100
18.3 @@ -917,7 +917,7 @@
18.4 val fields' = extern f :: map Long_Name.base_name fs;
18.5 val (args', more) = split_last args;
18.6 in (fields' ~~ args') @ strip_fields more end
18.7 - handle Library.UnequalLengths => [("", t)])
18.8 + handle ListPair.UnequalLengths => [("", t)])
18.9 | NONE => [("", t)])
18.10 | NONE => [("", t)])
18.11 | _ => [("", t)]);
19.1 --- a/src/HOL/Tools/refute.ML Sat Nov 27 19:41:28 2010 +0100
19.2 +++ b/src/HOL/Tools/refute.ML Sat Nov 27 19:41:37 2010 +0100
19.3 @@ -2953,9 +2953,7 @@
19.4 fun stlc_printer ctxt model T intr assignment =
19.5 let
19.6 (* string -> string *)
19.7 - fun strip_leading_quote s =
19.8 - (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
19.9 - o raw_explode) s (* FIXME Symbol.explode (?) *)
19.10 + val strip_leading_quote = perhaps (try (unprefix "'"))
19.11 (* Term.typ -> string *)
19.12 fun string_of_typ (Type (s, _)) = s
19.13 | string_of_typ (TFree (x, _)) = strip_leading_quote x
20.1 --- a/src/HOLCF/Cont.thy Sat Nov 27 19:41:28 2010 +0100
20.2 +++ b/src/HOLCF/Cont.thy Sat Nov 27 19:41:37 2010 +0100
20.3 @@ -97,22 +97,26 @@
20.4 done
20.5
20.6 lemma contI2:
20.7 + fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
20.8 assumes mono: "monofun f"
20.9 assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
20.10 \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
20.11 shows "cont f"
20.12 -apply (rule contI)
20.13 -apply (rule thelubE)
20.14 -apply (erule ch2ch_monofun [OF mono])
20.15 -apply (rule below_antisym)
20.16 -apply (rule is_lub_thelub)
20.17 -apply (erule ch2ch_monofun [OF mono])
20.18 -apply (rule ub2ub_monofun [OF mono])
20.19 -apply (rule is_lubD1)
20.20 -apply (erule cpo_lubI)
20.21 -apply (rule below, assumption)
20.22 -apply (erule ch2ch_monofun [OF mono])
20.23 -done
20.24 +proof (rule contI)
20.25 + fix Y :: "nat \<Rightarrow> 'a"
20.26 + assume Y: "chain Y"
20.27 + with mono have fY: "chain (\<lambda>i. f (Y i))"
20.28 + by (rule ch2ch_monofun)
20.29 + have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
20.30 + apply (rule below_antisym)
20.31 + apply (rule lub_below [OF fY])
20.32 + apply (rule monofunE [OF mono])
20.33 + apply (rule is_ub_thelub [OF Y])
20.34 + apply (rule below [OF Y fY])
20.35 + done
20.36 + with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
20.37 + by (rule thelubE)
20.38 +qed
20.39
20.40 subsection {* Collection of continuity rules *}
20.41
21.1 --- a/src/HOLCF/Domain.thy Sat Nov 27 19:41:28 2010 +0100
21.2 +++ b/src/HOLCF/Domain.thy Sat Nov 27 19:41:37 2010 +0100
21.3 @@ -340,13 +340,13 @@
21.4 deflation_sprod_map deflation_cprod_map deflation_u_map
21.5
21.6 setup {*
21.7 - fold Domain_Take_Proofs.add_map_function
21.8 - [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
21.9 - (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
21.10 - (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
21.11 - (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
21.12 - (@{type_name prod}, @{const_name cprod_map}, [true, true]),
21.13 - (@{type_name "u"}, @{const_name u_map}, [true])]
21.14 + fold Domain_Take_Proofs.add_rec_type
21.15 + [(@{type_name cfun}, [true, true]),
21.16 + (@{type_name "sfun"}, [true, true]),
21.17 + (@{type_name ssum}, [true, true]),
21.18 + (@{type_name sprod}, [true, true]),
21.19 + (@{type_name prod}, [true, true]),
21.20 + (@{type_name "u"}, [true])]
21.21 *}
21.22
21.23 end
22.1 --- a/src/HOLCF/Fixrec.thy Sat Nov 27 19:41:28 2010 +0100
22.2 +++ b/src/HOLCF/Fixrec.thy Sat Nov 27 19:41:37 2010 +0100
22.3 @@ -26,10 +26,6 @@
22.4 succeed :: "'a \<rightarrow> 'a match" where
22.5 "succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))"
22.6
22.7 -definition
22.8 - match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where
22.9 - "match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))"
22.10 -
22.11 lemma matchE [case_names bottom fail succeed, cases type: match]:
22.12 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
22.13 unfolding fail_def succeed_def
22.14 @@ -52,40 +48,31 @@
22.15 "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
22.16 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
22.17
22.18 -lemma match_case_simps [simp]:
22.19 - "match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
22.20 - "match_case\<cdot>f\<cdot>r\<cdot>fail = f"
22.21 - "match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x"
22.22 -by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match
22.23 - cont2cont_LAM
22.24 - cont_Abs_match Abs_match_inverse Rep_match_strict)
22.25 -
22.26 -translations
22.27 - "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2"
22.28 - == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
22.29 -
22.30 subsubsection {* Run operator *}
22.31
22.32 definition
22.33 run :: "'a match \<rightarrow> 'a::pcpo" where
22.34 - "run = match_case\<cdot>\<bottom>\<cdot>ID"
22.35 + "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
22.36
22.37 text {* rewrite rules for run *}
22.38
22.39 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
22.40 -by (simp add: run_def)
22.41 +unfolding run_def
22.42 +by (simp add: cont_Rep_match Rep_match_strict)
22.43
22.44 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
22.45 -by (simp add: run_def)
22.46 +unfolding run_def fail_def
22.47 +by (simp add: cont_Rep_match Abs_match_inverse)
22.48
22.49 lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x"
22.50 -by (simp add: run_def)
22.51 +unfolding run_def succeed_def
22.52 +by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
22.53
22.54 subsubsection {* Monad plus operator *}
22.55
22.56 definition
22.57 mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
22.58 - "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | succeed\<cdot>x \<Rightarrow> m1)"
22.59 + "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))"
22.60
22.61 abbreviation
22.62 mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match" (infixr "+++" 65) where
22.63 @@ -93,14 +80,19 @@
22.64
22.65 text {* rewrite rules for mplus *}
22.66
22.67 +lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
22.68 +
22.69 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
22.70 -by (simp add: mplus_def)
22.71 +unfolding mplus_def
22.72 +by (simp add: cont2cont_Rep_match Rep_match_strict)
22.73
22.74 lemma mplus_fail [simp]: "fail +++ m = m"
22.75 -by (simp add: mplus_def)
22.76 +unfolding mplus_def fail_def
22.77 +by (simp add: cont2cont_Rep_match Abs_match_inverse)
22.78
22.79 lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
22.80 -by (simp add: mplus_def)
22.81 +unfolding mplus_def succeed_def
22.82 +by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
22.83
22.84 lemma mplus_fail2 [simp]: "m +++ fail = m"
22.85 by (cases m, simp_all)
23.1 --- a/src/HOLCF/LowerPD.thy Sat Nov 27 19:41:28 2010 +0100
23.2 +++ b/src/HOLCF/LowerPD.thy Sat Nov 27 19:41:37 2010 +0100
23.3 @@ -195,7 +195,7 @@
23.4 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
23.5 done
23.6
23.7 -lemma lower_plus_below_iff:
23.8 +lemma lower_plus_below_iff [simp]:
23.9 "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
23.10 apply safe
23.11 apply (erule below_trans [OF lower_plus_below1])
23.12 @@ -203,7 +203,7 @@
23.13 apply (erule (1) lower_plus_least)
23.14 done
23.15
23.16 -lemma lower_unit_below_plus_iff:
23.17 +lemma lower_unit_below_plus_iff [simp]:
23.18 "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
23.19 apply (induct x rule: compact_basis.principal_induct, simp)
23.20 apply (induct ys rule: lower_pd.principal_induct, simp)
23.21 @@ -328,7 +328,7 @@
23.22 apply (erule lower_le_induct, safe)
23.23 apply (simp add: monofun_cfun)
23.24 apply (simp add: rev_below_trans [OF lower_plus_below1])
23.25 -apply (simp add: lower_plus_below_iff)
23.26 +apply simp
23.27 done
23.28
23.29 definition
23.30 @@ -389,14 +389,14 @@
23.31 apply default
23.32 apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
23.33 apply (induct_tac y rule: lower_pd_induct)
23.34 -apply (simp_all add: ep_pair.e_p_below monofun_cfun)
23.35 +apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
23.36 done
23.37
23.38 lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
23.39 apply default
23.40 apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
23.41 apply (induct_tac x rule: lower_pd_induct)
23.42 -apply (simp_all add: deflation.below monofun_cfun)
23.43 +apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
23.44 done
23.45
23.46 (* FIXME: long proof! *)
24.1 --- a/src/HOLCF/Powerdomains.thy Sat Nov 27 19:41:28 2010 +0100
24.2 +++ b/src/HOLCF/Powerdomains.thy Sat Nov 27 19:41:37 2010 +0100
24.3 @@ -42,10 +42,10 @@
24.4 deflation_upper_map deflation_lower_map deflation_convex_map
24.5
24.6 setup {*
24.7 - fold Domain_Take_Proofs.add_map_function
24.8 - [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
24.9 - (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
24.10 - (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
24.11 + fold Domain_Take_Proofs.add_rec_type
24.12 + [(@{type_name "upper_pd"}, [true]),
24.13 + (@{type_name "lower_pd"}, [true]),
24.14 + (@{type_name "convex_pd"}, [true])]
24.15 *}
24.16
24.17 end
25.1 --- a/src/HOLCF/Tools/Domain/domain.ML Sat Nov 27 19:41:28 2010 +0100
25.2 +++ b/src/HOLCF/Tools/Domain/domain.ML Sat Nov 27 19:41:37 2010 +0100
25.3 @@ -118,14 +118,14 @@
25.4 (* test for free type variables, illegal sort constraints on rhs,
25.5 non-pcpo-types and invalid use of recursive type;
25.6 replace sorts in type variables on rhs *)
25.7 - val map_tab = Domain_Take_Proofs.get_map_tab thy;
25.8 + val rec_tab = Domain_Take_Proofs.get_rec_tab thy;
25.9 fun check_rec rec_ok (T as TFree (v,_)) =
25.10 if AList.defined (op =) sorts v then T
25.11 else error ("Free type variable " ^ quote v ^ " on rhs.")
25.12 | check_rec rec_ok (T as Type (s, Ts)) =
25.13 (case AList.lookup (op =) dtnvs' s of
25.14 NONE =>
25.15 - let val rec_ok' = rec_ok andalso Symtab.defined map_tab s;
25.16 + let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s;
25.17 in Type (s, map (check_rec rec_ok') Ts) end
25.18 | SOME typevars =>
25.19 if typevars <> Ts
26.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 19:41:28 2010 +0100
26.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 19:41:37 2010 +0100
26.3 @@ -350,17 +350,17 @@
26.4 (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
26.5 (conjuncts deflation_map_binds deflation_map_thm);
26.6
26.7 - (* register map functions in theory data *)
26.8 + (* register indirect recursion in theory data *)
26.9 local
26.10 - fun register_map ((dname, map_name), args) =
26.11 - Domain_Take_Proofs.add_map_function (dname, map_name, args);
26.12 + fun register_map (dname, args) =
26.13 + Domain_Take_Proofs.add_rec_type (dname, args);
26.14 val dnames = map (fst o dest_Type o fst) dom_eqns;
26.15 val map_names = map (fst o dest_Const) map_consts;
26.16 fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [];
26.17 val argss = map args dom_eqns;
26.18 in
26.19 val thy =
26.20 - fold register_map (dnames ~~ map_names ~~ argss) thy;
26.21 + fold register_map (dnames ~~ argss) thy;
26.22 end;
26.23
26.24 (* register deflation theorems *)
27.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Nov 27 19:41:28 2010 +0100
27.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Nov 27 19:41:37 2010 +0100
27.3 @@ -55,8 +55,8 @@
27.4 val map_of_typ :
27.5 theory -> (typ * term) list -> typ -> term
27.6
27.7 - val add_map_function : (string * string * bool list) -> theory -> theory
27.8 - val get_map_tab : theory -> (string * bool list) Symtab.table
27.9 + val add_rec_type : (string * bool list) -> theory -> theory
27.10 + val get_rec_tab : theory -> (bool list) Symtab.table
27.11 val add_deflation_thm : thm -> theory -> theory
27.12 val get_deflation_thms : theory -> thm list
27.13 val map_ID_add : attribute
27.14 @@ -119,12 +119,10 @@
27.15 (******************************** theory data *********************************)
27.16 (******************************************************************************)
27.17
27.18 -structure MapData = Theory_Data
27.19 +structure Rec_Data = Theory_Data
27.20 (
27.21 - (* constant names like "foo_map" *)
27.22 - (* list indicates which type arguments correspond to map arguments *)
27.23 - (* alternatively, which type arguments allow indirect recursion *)
27.24 - type T = (string * bool list) Symtab.table;
27.25 + (* list indicates which type arguments allow indirect recursion *)
27.26 + type T = (bool list) Symtab.table;
27.27 val empty = Symtab.empty;
27.28 val extend = I;
27.29 fun merge data = Symtab.merge (K true) data;
27.30 @@ -142,13 +140,13 @@
27.31 val description = "theorems like foo_map$ID = ID"
27.32 );
27.33
27.34 -fun add_map_function (tname, map_name, bs) =
27.35 - MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
27.36 +fun add_rec_type (tname, bs) =
27.37 + Rec_Data.map (Symtab.insert (K true) (tname, bs));
27.38
27.39 fun add_deflation_thm thm =
27.40 Context.theory_map (DeflMapData.add_thm thm);
27.41
27.42 -val get_map_tab = MapData.get;
27.43 +val get_rec_tab = Rec_Data.get;
27.44 fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
27.45
27.46 val map_ID_add = Map_Id_Data.add;
28.1 --- a/src/HOLCF/UpperPD.thy Sat Nov 27 19:41:28 2010 +0100
28.2 +++ b/src/HOLCF/UpperPD.thy Sat Nov 27 19:41:37 2010 +0100
28.3 @@ -193,7 +193,7 @@
28.4 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
28.5 done
28.6
28.7 -lemma upper_below_plus_iff:
28.8 +lemma upper_below_plus_iff [simp]:
28.9 "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
28.10 apply safe
28.11 apply (erule below_trans [OF _ upper_plus_below1])
28.12 @@ -201,7 +201,7 @@
28.13 apply (erule (1) upper_plus_greatest)
28.14 done
28.15
28.16 -lemma upper_plus_below_unit_iff:
28.17 +lemma upper_plus_below_unit_iff [simp]:
28.18 "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
28.19 apply (induct xs rule: upper_pd.principal_induct, simp)
28.20 apply (induct ys rule: upper_pd.principal_induct, simp)
28.21 @@ -323,7 +323,7 @@
28.22 apply (erule upper_le_induct, safe)
28.23 apply (simp add: monofun_cfun)
28.24 apply (simp add: below_trans [OF upper_plus_below1])
28.25 -apply (simp add: upper_below_plus_iff)
28.26 +apply simp
28.27 done
28.28
28.29 definition
28.30 @@ -384,14 +384,14 @@
28.31 apply default
28.32 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
28.33 apply (induct_tac y rule: upper_pd_induct)
28.34 -apply (simp_all add: ep_pair.e_p_below monofun_cfun)
28.35 +apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
28.36 done
28.37
28.38 lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
28.39 apply default
28.40 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
28.41 apply (induct_tac x rule: upper_pd_induct)
28.42 -apply (simp_all add: deflation.below monofun_cfun)
28.43 +apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
28.44 done
28.45
28.46 (* FIXME: long proof! *)
29.1 --- a/src/HOLCF/ex/Pattern_Match.thy Sat Nov 27 19:41:28 2010 +0100
29.2 +++ b/src/HOLCF/ex/Pattern_Match.thy Sat Nov 27 19:41:37 2010 +0100
29.3 @@ -53,11 +53,24 @@
29.4
29.5 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
29.6
29.7 +subsection {* Bind operator for match monad *}
29.8 +
29.9 +definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
29.10 + "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
29.11 +
29.12 +lemma match_bind_simps [simp]:
29.13 + "match_bind\<cdot>\<bottom>\<cdot>k = \<bottom>"
29.14 + "match_bind\<cdot>fail\<cdot>k = fail"
29.15 + "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
29.16 +unfolding match_bind_def fail_def succeed_def
29.17 +by (simp_all add: cont2cont_Rep_match cont_Abs_match
29.18 + Rep_match_strict Abs_match_inverse)
29.19 +
29.20 subsection {* Case branch combinator *}
29.21
29.22 definition
29.23 branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
29.24 - "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
29.25 + "branch p \<equiv> \<Lambda> r x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))"
29.26
29.27 lemma branch_simps:
29.28 "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
29.29 @@ -72,7 +85,7 @@
29.30
29.31 definition
29.32 cases :: "'a match \<rightarrow> 'a::pcpo" where
29.33 - "cases = match_case\<cdot>\<bottom>\<cdot>ID"
29.34 + "cases = Fixrec.run"
29.35
29.36 text {* rewrite rules for cases *}
29.37
29.38 @@ -165,7 +178,7 @@
29.39 definition
29.40 cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
29.41 "cpair_pat p1 p2 = (\<Lambda>(x, y).
29.42 - match_case\<cdot>fail\<cdot>(\<Lambda> a. match_case\<cdot>fail\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
29.43 + match_bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. match_bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))))"
29.44
29.45 definition
29.46 spair_pat ::
29.47 @@ -313,7 +326,7 @@
29.48
29.49 definition
29.50 as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
29.51 - "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
29.52 + "as_pat p = (\<Lambda> x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. succeed\<cdot>(x, a)))"
29.53
29.54 definition
29.55 lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
29.56 @@ -544,7 +557,7 @@
29.57 val (fun1, fun2, taken) = pat_lhs (pat, args);
29.58 val defs = @{thm branch_def} :: pat_defs;
29.59 val goal = mk_trp (mk_strict fun1);
29.60 - val rules = @{thms match_case_simps} @ case_rews;
29.61 + val rules = @{thms match_bind_simps} @ case_rews;
29.62 val tacs = [simp_tac (beta_ss addsimps rules) 1];
29.63 in prove thy defs goal (K tacs) end;
29.64 fun pat_apps (i, (pat, (con, args))) =
29.65 @@ -559,7 +572,7 @@
29.66 val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
29.67 val goal = Logic.list_implies (assms, concl);
29.68 val defs = @{thm branch_def} :: pat_defs;
29.69 - val rules = @{thms match_case_simps} @ case_rews;
29.70 + val rules = @{thms match_bind_simps} @ case_rews;
29.71 val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
29.72 in prove thy defs goal (K tacs) end;
29.73 in map_index pat_app spec end;
30.1 --- a/src/Pure/Proof/reconstruct.ML Sat Nov 27 19:41:28 2010 +0100
30.2 +++ b/src/Pure/Proof/reconstruct.ML Sat Nov 27 19:41:37 2010 +0100
30.3 @@ -137,7 +137,7 @@
30.4 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
30.5 | SOME Ts => (Ts, env));
30.6 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
30.7 - (forall_intr_vfs prop) handle Library.UnequalLengths =>
30.8 + (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
30.9 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
30.10 in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
30.11
31.1 --- a/src/Pure/consts.ML Sat Nov 27 19:41:28 2010 +0100
31.2 +++ b/src/Pure/consts.ML Sat Nov 27 19:41:37 2010 +0100
31.3 @@ -215,7 +215,7 @@
31.4 let
31.5 val declT = type_scheme consts c;
31.6 val vars = map Term.dest_TVar (typargs consts (c, declT));
31.7 - val inst = vars ~~ Ts handle UnequalLengths =>
31.8 + val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
31.9 raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
31.10 in declT |> Term_Subst.instantiateT inst end;
31.11
32.1 --- a/src/Pure/drule.ML Sat Nov 27 19:41:28 2010 +0100
32.2 +++ b/src/Pure/drule.ML Sat Nov 27 19:41:37 2010 +0100
32.3 @@ -891,7 +891,7 @@
32.4 handle TYPE (msg, _, _) => err msg;
32.5
32.6 fun zip_vars xs ys =
32.7 - zip_options xs ys handle Library.UnequalLengths =>
32.8 + zip_options xs ys handle ListPair.UnequalLengths =>
32.9 err "more instantiations than variables in thm";
32.10
32.11 (*instantiate types first!*)
33.1 --- a/src/Pure/library.ML Sat Nov 27 19:41:28 2010 +0100
33.2 +++ b/src/Pure/library.ML Sat Nov 27 19:41:37 2010 +0100
33.3 @@ -58,7 +58,6 @@
33.4 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
33.5
33.6 (*lists*)
33.7 - exception UnequalLengths
33.8 val single: 'a -> 'a list
33.9 val the_single: 'a list -> 'a
33.10 val singleton: ('a list -> 'b list) -> 'a -> 'b
33.11 @@ -97,6 +96,7 @@
33.12 val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
33.13 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
33.14 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
33.15 + val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
33.16 val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
33.17 val zip_options: 'a list -> 'b option list -> ('a * 'b) list
33.18 val ~~ : 'a list * 'b list -> ('a * 'b) list
33.19 @@ -321,8 +321,6 @@
33.20
33.21 (** lists **)
33.22
33.23 -exception UnequalLengths;
33.24 -
33.25 fun single x = [x];
33.26
33.27 fun the_single [x] = x
33.28 @@ -495,7 +493,7 @@
33.29 let val (ps, qs) = chop (length xs) ys
33.30 in ps :: unflat xss qs end
33.31 | unflat [] [] = []
33.32 - | unflat _ _ = raise UnequalLengths;
33.33 + | unflat _ _ = raise ListPair.UnequalLengths;
33.34
33.35 fun burrow f xss = unflat xss (f (flat xss));
33.36
33.37 @@ -534,19 +532,21 @@
33.38
33.39 (* lists of pairs *)
33.40
33.41 -exception UnequalLengths;
33.42 -
33.43 fun map2 _ [] [] = []
33.44 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
33.45 - | map2 _ _ _ = raise UnequalLengths;
33.46 + | map2 _ _ _ = raise ListPair.UnequalLengths;
33.47
33.48 fun fold2 f [] [] z = z
33.49 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
33.50 - | fold2 f _ _ _ = raise UnequalLengths;
33.51 + | fold2 f _ _ _ = raise ListPair.UnequalLengths;
33.52 +
33.53 +fun fold_rev2 f [] [] z = z
33.54 + | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
33.55 + | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
33.56
33.57 fun forall2 P [] [] = true
33.58 | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
33.59 - | forall2 P _ _ = raise UnequalLengths;
33.60 + | forall2 P _ _ = raise ListPair.UnequalLengths;
33.61
33.62 fun map_split f [] = ([], [])
33.63 | map_split f (x :: xs) =
33.64 @@ -558,13 +558,13 @@
33.65 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
33.66 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
33.67 | zip_options _ [] = []
33.68 - | zip_options [] _ = raise UnequalLengths;
33.69 + | zip_options [] _ = raise ListPair.UnequalLengths;
33.70
33.71 (*combine two lists forming a list of pairs:
33.72 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*)
33.73 fun [] ~~ [] = []
33.74 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
33.75 - | _ ~~ _ = raise UnequalLengths;
33.76 + | _ ~~ _ = raise ListPair.UnequalLengths;
33.77
33.78 (*inverse of ~~; the old 'split':
33.79 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*)
33.80 @@ -843,10 +843,11 @@
33.81
33.82 fun map_transpose f xss =
33.83 let
33.84 - val n = case distinct (op =) (map length xss)
33.85 - of [] => 0
33.86 + val n =
33.87 + (case distinct (op =) (map length xss) of
33.88 + [] => 0
33.89 | [n] => n
33.90 - | _ => raise UnequalLengths;
33.91 + | _ => raise ListPair.UnequalLengths);
33.92 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
33.93
33.94
33.95 @@ -1066,3 +1067,5 @@
33.96
33.97 structure Basic_Library: BASIC_LIBRARY = Library;
33.98 open Basic_Library;
33.99 +
33.100 +datatype legacy = UnequalLengths;
34.1 --- a/src/Pure/pattern.ML Sat Nov 27 19:41:28 2010 +0100
34.2 +++ b/src/Pure/pattern.ML Sat Nov 27 19:41:37 2010 +0100
34.3 @@ -365,7 +365,7 @@
34.4 and cases(binders,env as (iTs,itms),pat,obj) =
34.5 let val (ph,pargs) = strip_comb pat
34.6 fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
34.7 - handle UnequalLengths => raise MATCH
34.8 + handle ListPair.UnequalLengths => raise MATCH
34.9 fun rigrig2((a:string,Ta),(b,Tb),oargs) =
34.10 if a <> b then raise MATCH
34.11 else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
35.1 --- a/src/Tools/eqsubst.ML Sat Nov 27 19:41:28 2010 +0100
35.2 +++ b/src/Tools/eqsubst.ML Sat Nov 27 19:41:37 2010 +0100
35.3 @@ -235,13 +235,13 @@
35.4 val initenv =
35.5 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
35.6 val useq = Unify.smash_unifiers thry [a] initenv
35.7 - handle UnequalLengths => Seq.empty
35.8 + handle ListPair.UnequalLengths => Seq.empty
35.9 | Term.TERM _ => Seq.empty;
35.10 fun clean_unify' useq () =
35.11 (case (Seq.pull useq) of
35.12 NONE => NONE
35.13 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
35.14 - handle UnequalLengths => NONE
35.15 + handle ListPair.UnequalLengths => NONE
35.16 | Term.TERM _ => NONE
35.17 in
35.18 (Seq.make (clean_unify' useq))
36.1 --- a/src/Tools/induct_tacs.ML Sat Nov 27 19:41:28 2010 +0100
36.2 +++ b/src/Tools/induct_tacs.ML Sat Nov 27 19:41:37 2010 +0100
36.3 @@ -96,7 +96,7 @@
36.4 val _ = Method.trace ctxt [rule'];
36.5
36.6 val concls = Logic.dest_conjunctions (Thm.concl_of rule);
36.7 - val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
36.8 + val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
36.9 error "Induction rule has different numbers of variables";
36.10 in res_inst_tac ctxt insts rule' i st end
36.11 handle THM _ => Seq.empty;