1.1 --- a/NEWS Fri Nov 26 15:24:11 2010 -0800
1.2 +++ b/NEWS Fri Nov 26 15:49:59 2010 -0800
1.3 @@ -104,14 +104,13 @@
1.4 avoid confusion with finite sets. INCOMPATIBILITY.
1.5
1.6 * Quickcheck's generator for random generation is renamed from "code" to
1.7 -"random". INCOMPATIBILITY.
1.8 +"random". INCOMPATIBILITY.
1.9
1.10 * Theory Multiset provides stable quicksort implementation of sort_key.
1.11
1.12 * Quickcheck now has a configurable time limit which is set to 30 seconds
1.13 by default. This can be changed by adding [timeout = n] to the quickcheck
1.14 -command. The time limit for auto quickcheck is still set independently,
1.15 -by default to 5 seconds.
1.16 +command. The time limit for Auto Quickcheck is still set independently.
1.17
1.18 * New command 'partial_function' provides basic support for recursive
1.19 function definitions over complete partial orders. Concrete instances
1.20 @@ -357,11 +356,26 @@
1.21 (and "ms" and "min" are no longer supported)
1.22 INCOMPATIBILITY.
1.23
1.24 +* Metis and Meson now have configuration options "meson_trace", "metis_trace",
1.25 + and "metis_verbose" that can be enabled to diagnose these tools. E.g.
1.26 +
1.27 + using [[metis_trace = true]]
1.28 +
1.29 * Nitpick:
1.30 - Renamed options:
1.31 nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
1.32 nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
1.33 INCOMPATIBILITY.
1.34 + - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.
1.35 + - Added support for partial quotient types.
1.36 + - Added local versions of the "Nitpick.register_xxx" functions.
1.37 + - Added "whack" option.
1.38 + - Allow registration of quotient types as codatatypes.
1.39 + - Improved "merge_type_vars" option to merge more types.
1.40 + - Removed unsound "fast_descrs" option.
1.41 + - Added custom symmetry breaking for datatypes, making it possible to reach
1.42 + higher cardinalities.
1.43 + - Prevent the expansion of too large definitions.
1.44
1.45 * Changed SMT configuration options:
1.46 - Renamed:
1.47 @@ -507,6 +521,9 @@
1.48
1.49 *** ML ***
1.50
1.51 +* Former exception Library.UnequalLengths now coincides with
1.52 +ListPair.UnequalLengths.
1.53 +
1.54 * Renamed raw "explode" function to "raw_explode" to emphasize its
1.55 meaning. Note that internally to Isabelle, Symbol.explode is used in
1.56 almost all situations.
1.57 @@ -650,7 +667,7 @@
1.58
1.59 Tracing is then active for all invocations of the simplifier in
1.60 subsequent goal refinement steps. Tracing may also still be enabled or
1.61 -disabled via the ProofGeneral settings menu.
1.62 +disabled via the Proof General settings menu.
1.63
1.64 * Separate commands 'hide_class', 'hide_type', 'hide_const',
1.65 'hide_fact' replace the former 'hide' KIND command. Minor
2.1 --- a/doc-src/LaTeXsugar/Sugar/document/root.tex Fri Nov 26 15:24:11 2010 -0800
2.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
3.2 +++ b/doc-src/Main/main.tex Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
4.2 +++ b/src/HOL/Fun.thy Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
5.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
6.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
7.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
8.2 +++ b/src/HOL/Statespace/document/root.tex Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
10.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
11.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
12.2 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Nov 26 15:49:59 2010 -0800
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 Fri Nov 26 15:24:11 2010 -0800
13.2 +++ b/src/HOL/Tools/Function/size.ML Fri Nov 26 15:49:59 2010 -0800
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/Meson/meson.ML Fri Nov 26 15:24:11 2010 -0800
14.2 +++ b/src/HOL/Tools/Meson/meson.ML Fri Nov 26 15:49:59 2010 -0800
14.3 @@ -46,7 +46,7 @@
14.4 structure Meson : MESON =
14.5 struct
14.6
14.7 -val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
14.8 +val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
14.9
14.10 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
14.11
15.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 15:24:11 2010 -0800
15.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 15:49:59 2010 -0800
15.3 @@ -31,8 +31,8 @@
15.4
15.5 open Metis_Translate
15.6
15.7 -val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
15.8 -val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
15.9 +val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
15.10 +val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
15.11
15.12 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
15.13 fun verbose_warning ctxt msg =
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 15:24:11 2010 -0800
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 15:49:59 2010 -0800
16.3 @@ -393,7 +393,7 @@
16.4 | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
16.5 accum =
16.6 (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
16.7 - handle Library.UnequalLengths =>
16.8 + handle ListPair.UnequalLengths =>
16.9 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
16.10 | do_mtype_comp _ _ (MType _) (MType _) accum =
16.11 accum (* no need to compare them thanks to the cache *)
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 15:24:11 2010 -0800
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 15:49:59 2010 -0800
17.3 @@ -527,7 +527,7 @@
17.4 | NONE =>
17.5 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
17.6 $ Abs (s, T, kill ss Ts ts))
17.7 - | kill _ _ _ = raise UnequalLengths
17.8 + | kill _ _ _ = raise ListPair.UnequalLengths
17.9 fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
17.10 gather (ss @ [s1]) (Ts @ [T1]) t1
17.11 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
18.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 15:24:11 2010 -0800
18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 15:49:59 2010 -0800
18.3 @@ -204,7 +204,7 @@
18.4
18.5 fun map3 _ [] [] [] = []
18.6 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
18.7 - | map3 _ _ _ _ = raise UnequalLengths
18.8 + | map3 _ _ _ _ = raise ListPair.UnequalLengths
18.9
18.10 fun double_lookup eq ps key =
18.11 case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 15:24:11 2010 -0800
19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 15:49:59 2010 -0800
19.3 @@ -440,7 +440,7 @@
19.4 val smt_iter_timeout_divisor = 2
19.5 val smt_monomorph_limit = 4
19.6
19.7 -fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
19.8 +fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
19.9 let
19.10 val ctxt = Proof.context_of state
19.11 fun iter timeout iter_num outcome0 msecs_so_far facts =
19.12 @@ -534,6 +534,7 @@
19.13 val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
19.14 val {outcome, used_facts, run_time_in_msecs} =
19.15 smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
19.16 + val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
19.17 val outcome = outcome |> Option.map failure_from_smt_failure
19.18 val message =
19.19 case outcome of
19.20 @@ -547,8 +548,9 @@
19.21 in
19.22 try_command_line (proof_banner auto)
19.23 (apply_on_subgoal subgoal subgoal_count ^
19.24 - command_call method (map (fst o fst) used_facts)) ^
19.25 - minimize_line minimize_command (map (fst o fst) used_facts)
19.26 + command_call method (map fst other_lemmas)) ^
19.27 + minimize_line minimize_command
19.28 + (map fst (other_lemmas @ chained_lemmas))
19.29 end
19.30 | SOME failure => string_for_failure "SMT solver" failure
19.31 in
20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 15:24:11 2010 -0800
20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 15:49:59 2010 -0800
20.3 @@ -24,7 +24,9 @@
20.4 val command_call : string -> string list -> string
20.5 val try_command_line : string -> string -> string
20.6 val minimize_line : ('a list -> string) -> 'a list -> string
20.7 - val metis_proof_text : metis_params -> text_result
20.8 + val split_used_facts :
20.9 + (string * locality) list
20.10 + -> (string * locality) list * (string * locality) list
20.11 val isar_proof_text : isar_params -> metis_params -> text_result
20.12 val proof_text : bool -> isar_params -> metis_params -> text_result
20.13 end;
20.14 @@ -159,15 +161,15 @@
20.15 fun used_facts_in_tstplike_proof fact_names =
20.16 atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
20.17
20.18 -fun used_facts fact_names =
20.19 - used_facts_in_tstplike_proof fact_names
20.20 - #> List.partition (curry (op =) Chained o snd)
20.21 +val split_used_facts =
20.22 + List.partition (curry (op =) Chained o snd)
20.23 #> pairself (sort_distinct (string_ord o pairself fst))
20.24
20.25 fun metis_proof_text (banner, full_types, minimize_command,
20.26 tstplike_proof, fact_names, goal, i) =
20.27 let
20.28 - val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
20.29 + val (chained_lemmas, other_lemmas) =
20.30 + split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
20.31 val n = Logic.count_prems (prop_of goal)
20.32 in
20.33 (metis_line banner full_types i n (map fst other_lemmas) ^
20.34 @@ -912,14 +914,14 @@
20.35 in do_proof end
20.36
20.37 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
20.38 - (other_params as (_, full_types, _, tstplike_proof,
20.39 + (metis_params as (_, full_types, _, tstplike_proof,
20.40 fact_names, goal, i)) =
20.41 let
20.42 val (params, hyp_ts, concl_t) = strip_subgoal goal i
20.43 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
20.44 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
20.45 val n = Logic.count_prems (prop_of goal)
20.46 - val (one_line_proof, lemma_names) = metis_proof_text other_params
20.47 + val (one_line_proof, lemma_names) = metis_proof_text metis_params
20.48 fun isar_proof_for () =
20.49 case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
20.50 isar_shrink_factor tstplike_proof conjecture_shape fact_names
20.51 @@ -940,8 +942,8 @@
20.52 |> the_default "\nWarning: The Isar proof construction failed."
20.53 in (one_line_proof ^ isar_proof, lemma_names) end
20.54
20.55 -fun proof_text isar_proof isar_params other_params =
20.56 +fun proof_text isar_proof isar_params metis_params =
20.57 (if isar_proof then isar_proof_text isar_params else metis_proof_text)
20.58 - other_params
20.59 + metis_params
20.60
20.61 end;
21.1 --- a/src/HOL/Tools/code_evaluation.ML Fri Nov 26 15:24:11 2010 -0800
21.2 +++ b/src/HOL/Tools/code_evaluation.ML Fri Nov 26 15:49:59 2010 -0800
21.3 @@ -54,7 +54,7 @@
21.4
21.5 (* code equations for datatypes *)
21.6
21.7 -fun mk_term_of_eq thy ty (c, tys) =
21.8 +fun mk_term_of_eq thy ty (c, (_, tys)) =
21.9 let
21.10 val t = list_comb (Const (c, tys ---> ty),
21.11 map Free (Name.names Name.context "a" tys));
21.12 @@ -74,7 +74,7 @@
21.13 val vs = map (fn (v, sort) =>
21.14 (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
21.15 val ty = Type (tyco, map TFree vs);
21.16 - val cs = (map o apsnd o map o map_atyps)
21.17 + val cs = (map o apsnd o apsnd o map o map_atyps)
21.18 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
21.19 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
21.20 val eqs = map (mk_term_of_eq thy ty) cs;
21.21 @@ -121,7 +121,7 @@
21.22 |> Code.add_eqn eq
21.23 end;
21.24
21.25 -fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
21.26 +fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
21.27 let
21.28 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
21.29 in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
22.1 --- a/src/HOL/Tools/groebner.ML Fri Nov 26 15:24:11 2010 -0800
22.2 +++ b/src/HOL/Tools/groebner.ML Fri Nov 26 15:49:59 2010 -0800
22.3 @@ -233,14 +233,9 @@
22.4
22.5 fun align ((p,hp),(q,hq)) =
22.6 if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
22.7 -fun forall2 p l1 l2 =
22.8 - case (l1,l2) of
22.9 - ([],[]) => true
22.10 - | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
22.11 - | _ => false;
22.12
22.13 fun poly_eq p1 p2 =
22.14 - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
22.15 + eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
22.16
22.17 fun memx ((p1,h1),(p2,h2)) ppairs =
22.18 not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
23.1 --- a/src/HOL/Tools/record.ML Fri Nov 26 15:24:11 2010 -0800
23.2 +++ b/src/HOL/Tools/record.ML Fri Nov 26 15:49:59 2010 -0800
23.3 @@ -917,7 +917,7 @@
23.4 val fields' = extern f :: map Long_Name.base_name fs;
23.5 val (args', more) = split_last args;
23.6 in (fields' ~~ args') @ strip_fields more end
23.7 - handle Library.UnequalLengths => [("", t)])
23.8 + handle ListPair.UnequalLengths => [("", t)])
23.9 | NONE => [("", t)])
23.10 | NONE => [("", t)])
23.11 | _ => [("", t)]);
24.1 --- a/src/HOL/Tools/refute.ML Fri Nov 26 15:24:11 2010 -0800
24.2 +++ b/src/HOL/Tools/refute.ML Fri Nov 26 15:49:59 2010 -0800
24.3 @@ -2953,9 +2953,7 @@
24.4 fun stlc_printer ctxt model T intr assignment =
24.5 let
24.6 (* string -> string *)
24.7 - fun strip_leading_quote s =
24.8 - (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
24.9 - o raw_explode) s (* FIXME Symbol.explode (?) *)
24.10 + val strip_leading_quote = perhaps (try (unprefix "'"))
24.11 (* Term.typ -> string *)
24.12 fun string_of_typ (Type (s, _)) = s
24.13 | string_of_typ (TFree (x, _)) = strip_leading_quote x
25.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 15:24:11 2010 -0800
25.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 15:49:59 2010 -0800
25.3 @@ -66,7 +66,7 @@
25.4 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
25.5
25.6 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
25.7 - by normalization rule+
25.8 + by normalization
25.9 lemma "rev [a, b, c] = [c, b, a]" by normalization
25.10 value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
25.11 value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
25.12 @@ -108,10 +108,13 @@
25.13 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
25.14 value [nbe] "Suc 0 \<in> set ms"
25.15
25.16 +(* non-left-linear patterns, equality by extensionality *)
25.17 +
25.18 lemma "f = f" by normalization
25.19 lemma "f x = f x" by normalization
25.20 lemma "(f o g) x = f (g x)" by normalization
25.21 lemma "(f o id) x = f x" by normalization
25.22 +lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
25.23 value [nbe] "(\<lambda>x. x)"
25.24
25.25 (* Church numerals: *)
26.1 --- a/src/Pure/Isar/code.ML Fri Nov 26 15:24:11 2010 -0800
26.2 +++ b/src/Pure/Isar/code.ML Fri Nov 26 15:49:59 2010 -0800
26.3 @@ -21,7 +21,7 @@
26.4
26.5 (*constructor sets*)
26.6 val constrset_of_consts: theory -> (string * typ) list
26.7 - -> string * ((string * sort) list * (string * typ list) list)
26.8 + -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
26.9
26.10 (*code equations and certificates*)
26.11 val mk_eqn: theory -> thm * bool -> thm * bool
26.12 @@ -48,11 +48,11 @@
26.13 val add_datatype: (string * typ) list -> theory -> theory
26.14 val add_datatype_cmd: string list -> theory -> theory
26.15 val datatype_interpretation:
26.16 - (string * ((string * sort) list * (string * typ list) list)
26.17 + (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
26.18 -> theory -> theory) -> theory -> theory
26.19 val add_abstype: thm -> theory -> theory
26.20 val abstype_interpretation:
26.21 - (string * ((string * sort) list * ((string * typ) * (string * thm)))
26.22 + (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
26.23 -> theory -> theory) -> theory -> theory
26.24 val add_eqn: thm -> theory -> theory
26.25 val add_nbe_eqn: thm -> theory -> theory
26.26 @@ -66,7 +66,8 @@
26.27 val del_eqns: string -> theory -> theory
26.28 val add_case: thm -> theory -> theory
26.29 val add_undefined: string -> theory -> theory
26.30 - val get_type: theory -> string -> ((string * sort) list * ((string * string list) * typ list) list)
26.31 + val get_type: theory -> string
26.32 + -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
26.33 val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
26.34 val is_constr: theory -> string -> bool
26.35 val is_abstr: theory -> string -> bool
26.36 @@ -147,11 +148,11 @@
26.37
26.38 (* datatypes *)
26.39
26.40 -datatype typ_spec = Constructors of (string * typ list) list
26.41 - | Abstractor of (string * typ) * (string * thm);
26.42 +datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list
26.43 + | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
26.44
26.45 fun constructors_of (Constructors cos) = (cos, false)
26.46 - | constructors_of (Abstractor ((co, ty), _)) = ([(co, [ty])], true);
26.47 + | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
26.48
26.49
26.50 (* functions *)
26.51 @@ -412,7 +413,8 @@
26.52 let
26.53 val the_v = the o AList.lookup (op =) (vs ~~ vs');
26.54 val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
26.55 - in (c, (fst o strip_type) ty') end;
26.56 + val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
26.57 + in (c, (vs'', (fst o strip_type) ty')) end;
26.58 val c' :: cs' = map (ty_sorts thy) cs;
26.59 val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
26.60 val vs = Name.names Name.context Name.aT sorts;
26.61 @@ -423,7 +425,7 @@
26.62 of (_, entry) :: _ => SOME entry
26.63 | _ => NONE;
26.64
26.65 -fun get_type_spec thy tyco = case get_type_entry thy tyco
26.66 +fun get_type thy tyco = case get_type_entry thy tyco
26.67 of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
26.68 | NONE => arity_number thy tyco
26.69 |> Name.invents Name.context Name.aT
26.70 @@ -435,17 +437,9 @@
26.71 of SOME (vs, Abstractor spec) => (vs, spec)
26.72 | _ => error ("Not an abstract type: " ^ tyco);
26.73
26.74 -fun get_type thy tyco =
26.75 - let
26.76 - val ((vs, cos), _) = get_type_spec thy tyco;
26.77 - fun args_of c tys = map (fst o dest_TFree)
26.78 - (Sign.const_typargs thy (c, tys ---> Type (tyco, map TFree vs)));
26.79 - fun add_typargs (c, tys) = ((c, args_of c tys), tys);
26.80 - in (vs, map add_typargs cos) end;
26.81 -
26.82 fun get_type_of_constr_or_abstr thy c =
26.83 case (snd o strip_type o const_typ thy) c
26.84 - of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
26.85 + of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
26.86 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
26.87 | _ => NONE;
26.88
26.89 @@ -683,8 +677,9 @@
26.90 val _ = if param = rhs then () else bad "Not an abstype certificate";
26.91 val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
26.92 val ty = domain_type ty';
26.93 + val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
26.94 val ty_abs = range_type ty';
26.95 - in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end;
26.96 + in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
26.97
26.98
26.99 (* code equation certificates *)
26.100 @@ -784,7 +779,7 @@
26.101
26.102 fun cert_of_proj thy c tyco =
26.103 let
26.104 - val (vs, ((abs, ty), (rep, cert))) = get_abstype_spec thy tyco;
26.105 + val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
26.106 val _ = if c = rep then () else
26.107 error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
26.108 in Projection (mk_proj tyco vs ty abs rep, tyco) end;
26.109 @@ -979,8 +974,8 @@
26.110 pretty_typ typ
26.111 :: Pretty.str "="
26.112 :: (if abstract then [Pretty.str "(abstract)"] else [])
26.113 - @ separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
26.114 - | (c, tys) =>
26.115 + @ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c)
26.116 + | (c, (_, tys)) =>
26.117 (Pretty.block o Pretty.breaks)
26.118 (Pretty.str (string_of_const thy c)
26.119 :: Pretty.str "of"
26.120 @@ -1202,7 +1197,7 @@
26.121 Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
26.122
26.123 fun datatype_interpretation f = Datatype_Interpretation.interpretation
26.124 - (fn (tyco, _) => fn thy => f (tyco, fst (get_type_spec thy tyco)) thy);
26.125 + (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
26.126
26.127 fun add_datatype proto_constrs thy =
26.128 let
26.129 @@ -1226,7 +1221,7 @@
26.130
26.131 fun add_abstype proto_thm thy =
26.132 let
26.133 - val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
26.134 + val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
26.135 error_thm (check_abstype_cert thy) proto_thm;
26.136 in
26.137 thy
27.1 --- a/src/Pure/Proof/reconstruct.ML Fri Nov 26 15:24:11 2010 -0800
27.2 +++ b/src/Pure/Proof/reconstruct.ML Fri Nov 26 15:49:59 2010 -0800
27.3 @@ -137,7 +137,7 @@
27.4 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
27.5 | SOME Ts => (Ts, env));
27.6 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
27.7 - (forall_intr_vfs prop) handle Library.UnequalLengths =>
27.8 + (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
27.9 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
27.10 in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
27.11
28.1 --- a/src/Pure/consts.ML Fri Nov 26 15:24:11 2010 -0800
28.2 +++ b/src/Pure/consts.ML Fri Nov 26 15:49:59 2010 -0800
28.3 @@ -215,7 +215,7 @@
28.4 let
28.5 val declT = type_scheme consts c;
28.6 val vars = map Term.dest_TVar (typargs consts (c, declT));
28.7 - val inst = vars ~~ Ts handle UnequalLengths =>
28.8 + val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
28.9 raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
28.10 in declT |> Term_Subst.instantiateT inst end;
28.11
29.1 --- a/src/Pure/drule.ML Fri Nov 26 15:24:11 2010 -0800
29.2 +++ b/src/Pure/drule.ML Fri Nov 26 15:49:59 2010 -0800
29.3 @@ -891,7 +891,7 @@
29.4 handle TYPE (msg, _, _) => err msg;
29.5
29.6 fun zip_vars xs ys =
29.7 - zip_options xs ys handle Library.UnequalLengths =>
29.8 + zip_options xs ys handle ListPair.UnequalLengths =>
29.9 err "more instantiations than variables in thm";
29.10
29.11 (*instantiate types first!*)
30.1 --- a/src/Pure/library.ML Fri Nov 26 15:24:11 2010 -0800
30.2 +++ b/src/Pure/library.ML Fri Nov 26 15:49:59 2010 -0800
30.3 @@ -58,7 +58,6 @@
30.4 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
30.5
30.6 (*lists*)
30.7 - exception UnequalLengths
30.8 val single: 'a -> 'a list
30.9 val the_single: 'a list -> 'a
30.10 val singleton: ('a list -> 'b list) -> 'a -> 'b
30.11 @@ -97,6 +96,7 @@
30.12 val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
30.13 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
30.14 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
30.15 + val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
30.16 val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
30.17 val zip_options: 'a list -> 'b option list -> ('a * 'b) list
30.18 val ~~ : 'a list * 'b list -> ('a * 'b) list
30.19 @@ -321,8 +321,6 @@
30.20
30.21 (** lists **)
30.22
30.23 -exception UnequalLengths;
30.24 -
30.25 fun single x = [x];
30.26
30.27 fun the_single [x] = x
30.28 @@ -495,7 +493,7 @@
30.29 let val (ps, qs) = chop (length xs) ys
30.30 in ps :: unflat xss qs end
30.31 | unflat [] [] = []
30.32 - | unflat _ _ = raise UnequalLengths;
30.33 + | unflat _ _ = raise ListPair.UnequalLengths;
30.34
30.35 fun burrow f xss = unflat xss (f (flat xss));
30.36
30.37 @@ -534,19 +532,21 @@
30.38
30.39 (* lists of pairs *)
30.40
30.41 -exception UnequalLengths;
30.42 -
30.43 fun map2 _ [] [] = []
30.44 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
30.45 - | map2 _ _ _ = raise UnequalLengths;
30.46 + | map2 _ _ _ = raise ListPair.UnequalLengths;
30.47
30.48 fun fold2 f [] [] z = z
30.49 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
30.50 - | fold2 f _ _ _ = raise UnequalLengths;
30.51 + | fold2 f _ _ _ = raise ListPair.UnequalLengths;
30.52 +
30.53 +fun fold_rev2 f [] [] z = z
30.54 + | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
30.55 + | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
30.56
30.57 fun forall2 P [] [] = true
30.58 | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
30.59 - | forall2 P _ _ = false;
30.60 + | forall2 P _ _ = raise ListPair.UnequalLengths;
30.61
30.62 fun map_split f [] = ([], [])
30.63 | map_split f (x :: xs) =
30.64 @@ -558,13 +558,13 @@
30.65 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
30.66 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
30.67 | zip_options _ [] = []
30.68 - | zip_options [] _ = raise UnequalLengths;
30.69 + | zip_options [] _ = raise ListPair.UnequalLengths;
30.70
30.71 (*combine two lists forming a list of pairs:
30.72 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*)
30.73 fun [] ~~ [] = []
30.74 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
30.75 - | _ ~~ _ = raise UnequalLengths;
30.76 + | _ ~~ _ = raise ListPair.UnequalLengths;
30.77
30.78 (*inverse of ~~; the old 'split':
30.79 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*)
30.80 @@ -843,10 +843,11 @@
30.81
30.82 fun map_transpose f xss =
30.83 let
30.84 - val n = case distinct (op =) (map length xss)
30.85 - of [] => 0
30.86 + val n =
30.87 + (case distinct (op =) (map length xss) of
30.88 + [] => 0
30.89 | [n] => n
30.90 - | _ => raise UnequalLengths;
30.91 + | _ => raise ListPair.UnequalLengths);
30.92 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
30.93
30.94
30.95 @@ -1066,3 +1067,5 @@
30.96
30.97 structure Basic_Library: BASIC_LIBRARY = Library;
30.98 open Basic_Library;
30.99 +
30.100 +datatype legacy = UnequalLengths;
31.1 --- a/src/Pure/pattern.ML Fri Nov 26 15:24:11 2010 -0800
31.2 +++ b/src/Pure/pattern.ML Fri Nov 26 15:49:59 2010 -0800
31.3 @@ -365,7 +365,7 @@
31.4 and cases(binders,env as (iTs,itms),pat,obj) =
31.5 let val (ph,pargs) = strip_comb pat
31.6 fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
31.7 - handle UnequalLengths => raise MATCH
31.8 + handle ListPair.UnequalLengths => raise MATCH
31.9 fun rigrig2((a:string,Ta),(b,Tb),oargs) =
31.10 if a <> b then raise MATCH
31.11 else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
32.1 --- a/src/Tools/Code/code_runtime.ML Fri Nov 26 15:24:11 2010 -0800
32.2 +++ b/src/Tools/Code/code_runtime.ML Fri Nov 26 15:49:59 2010 -0800
32.3 @@ -258,7 +258,7 @@
32.4
32.5 fun check_datatype thy tyco some_consts =
32.6 let
32.7 - val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
32.8 + val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
32.9 val _ = case some_consts
32.10 of SOME consts =>
32.11 let
33.1 --- a/src/Tools/Code/code_thingol.ML Fri Nov 26 15:24:11 2010 -0800
33.2 +++ b/src/Tools/Code/code_thingol.ML Fri Nov 26 15:49:59 2010 -0800
33.3 @@ -573,12 +573,12 @@
33.4
33.5 fun ensure_tyco thy algbr eqngr permissive tyco =
33.6 let
33.7 - val (vs, cos) = Code.get_type thy tyco;
33.8 + val ((vs, cos), _) = Code.get_type thy tyco;
33.9 val stmt_datatype =
33.10 fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
33.11 - ##>> fold_map (fn ((c, vs), tys) =>
33.12 + ##>> fold_map (fn (c, (vs, tys)) =>
33.13 ensure_const thy algbr eqngr permissive c
33.14 - ##>> pair (map (unprefix "'") vs)
33.15 + ##>> pair (map (unprefix "'" o fst) vs)
33.16 ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
33.17 #>> (fn info => Datatype (tyco, info));
33.18 in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
34.1 --- a/src/Tools/eqsubst.ML Fri Nov 26 15:24:11 2010 -0800
34.2 +++ b/src/Tools/eqsubst.ML Fri Nov 26 15:49:59 2010 -0800
34.3 @@ -235,13 +235,13 @@
34.4 val initenv =
34.5 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
34.6 val useq = Unify.smash_unifiers thry [a] initenv
34.7 - handle UnequalLengths => Seq.empty
34.8 + handle ListPair.UnequalLengths => Seq.empty
34.9 | Term.TERM _ => Seq.empty;
34.10 fun clean_unify' useq () =
34.11 (case (Seq.pull useq) of
34.12 NONE => NONE
34.13 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
34.14 - handle UnequalLengths => NONE
34.15 + handle ListPair.UnequalLengths => NONE
34.16 | Term.TERM _ => NONE
34.17 in
34.18 (Seq.make (clean_unify' useq))
35.1 --- a/src/Tools/induct_tacs.ML Fri Nov 26 15:24:11 2010 -0800
35.2 +++ b/src/Tools/induct_tacs.ML Fri Nov 26 15:49:59 2010 -0800
35.3 @@ -96,7 +96,7 @@
35.4 val _ = Method.trace ctxt [rule'];
35.5
35.6 val concls = Logic.dest_conjunctions (Thm.concl_of rule);
35.7 - val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
35.8 + val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
35.9 error "Induction rule has different numbers of variables";
35.10 in res_inst_tac ctxt insts rule' i st end
35.11 handle THM _ => Seq.empty;
36.1 --- a/src/Tools/nbe.ML Fri Nov 26 15:24:11 2010 -0800
36.2 +++ b/src/Tools/nbe.ML Fri Nov 26 15:49:59 2010 -0800
36.3 @@ -18,7 +18,7 @@
36.4 val apps: Univ -> Univ list -> Univ (*explicit applications*)
36.5 val abss: int -> (Univ list -> Univ) -> Univ
36.6 (*abstractions as closures*)
36.7 - val same: Univ -> Univ -> bool
36.8 + val eq_Univ: Univ * Univ -> bool
36.9
36.10 val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
36.11 val trace: bool Unsynchronized.ref
36.12 @@ -170,11 +170,6 @@
36.13 | Abs of (int * (Univ list -> Univ)) * Univ list
36.14 (*abstractions as closures*);
36.15
36.16 -fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
36.17 - | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
36.18 - | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
36.19 - | same _ _ = false;
36.20 -
36.21
36.22 (* constructor functions *)
36.23
36.24 @@ -188,6 +183,28 @@
36.25 | apps (Const (name, xs)) ys = Const (name, ys @ xs)
36.26 | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
36.27
36.28 +fun satisfy_abs (abs as ((n, f), xs)) some_k =
36.29 + let
36.30 + val ys = case some_k
36.31 + of NONE => replicate n (BVar (0, []))
36.32 + | SOME k => map_range (fn l => BVar (k + l, [])) n;
36.33 + in (apps (Abs abs) ys, ys) end;
36.34 +
36.35 +fun maxidx (Const (_, xs)) = fold maxidx xs
36.36 + | maxidx (DFree _) = I
36.37 + | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
36.38 + | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
36.39 +
36.40 +fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
36.41 + | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
36.42 + | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
36.43 + | eq_Univ (x as Abs abs, y) =
36.44 + let
36.45 + val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
36.46 + in eq_Univ (x, apps y ys) end
36.47 + | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
36.48 + | eq_Univ _ = false;
36.49 +
36.50
36.51 (** assembling and compiling ML code from terms **)
36.52
36.53 @@ -241,7 +258,7 @@
36.54 val name_const = prefix ^ "Const";
36.55 val name_abss = prefix ^ "abss";
36.56 val name_apps = prefix ^ "apps";
36.57 - val name_same = prefix ^ "same";
36.58 + val name_eq = prefix ^ "eq_Univ";
36.59 in
36.60
36.61 val univs_cookie = (Univs.get, put_result, name_put);
36.62 @@ -267,7 +284,7 @@
36.63 fun nbe_abss 0 f = f `$` ml_list []
36.64 | nbe_abss n f = name_abss `$$` [string_of_int n, f];
36.65
36.66 -fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
36.67 +fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
36.68
36.69 end;
36.70
36.71 @@ -353,7 +370,7 @@
36.72 val (samepairs, args') = subst_nonlin_vars args;
36.73 val s_args = map assemble_arg args';
36.74 val s_rhs = if null samepairs then assemble_rhs rhs
36.75 - else ml_if (ml_and (map (uncurry nbe_same) samepairs))
36.76 + else ml_if (ml_and (map nbe_eq samepairs))
36.77 (assemble_rhs rhs) default_rhs;
36.78 val eqns = if is_eval then
36.79 [([ml_list (rev (dicts @ s_args))], s_rhs)]