--- a/NEWS Sat Nov 27 19:41:28 2010 +0100
+++ b/NEWS Sat Nov 27 19:41:37 2010 +0100
@@ -521,6 +521,9 @@
*** ML ***
+* Former exception Library.UnequalLengths now coincides with
+ListPair.UnequalLengths.
+
* Renamed raw "explode" function to "raw_explode" to emphasize its
meaning. Note that internally to Isabelle, Symbol.explode is used in
almost all situations.
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Sat Nov 27 19:41:28 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Sat Nov 27 19:41:37 2010 +0100
@@ -3,23 +3,7 @@
% further packages required for unusual symbols (see also isabellesym.sty)
% use only when needed
-\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
- % \<sqsupset>, \<mho>, \<Join>,
- % \<lhd>, \<lesssim>, \<greatersim>,
- % \<lessapprox>, \<greaterapprox>,
- % \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[greek,english]{babel} % greek for \<euro>,
- % english for \<guillemotleft>,
- % \<guillemotright>
- % default language = last
-%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
- % \<twosuperior>, \<onehalf>,
- % \<threesuperior>, \<threequarters>,
- % \<degree>
-%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
-%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
- % (only needed if amssymb not used)
-%\usepackage{textcomp} % for \<cent>, \<currency>
+\usepackage{amssymb}
\usepackage{mathpartir}
--- a/doc-src/Main/main.tex Sat Nov 27 19:41:28 2010 +0100
+++ b/doc-src/Main/main.tex Sat Nov 27 19:41:37 2010 +0100
@@ -9,31 +9,8 @@
\textheight=234mm
\usepackage{../isabelle,../isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
- %option greek for \<euro>
- %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
-
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<cent>, \<currency>
% this should be the last package used
\usepackage{../pdfsetup}
--- a/src/HOL/Fun.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Fun.thy Sat Nov 27 19:41:37 2010 +0100
@@ -155,11 +155,6 @@
shows "inj f"
using assms unfolding inj_on_def by auto
-text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
-lemma datatype_injI:
- "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
-by (simp add: inj_on_def)
-
theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
by (unfold inj_on_def, blast)
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Nov 27 19:41:37 2010 +0100
@@ -103,11 +103,6 @@
fun iszero (k,r) = r =/ rat_0;
-fun fold_rev2 f l1 l2 b =
- case (l1,l2) of
- ([],[]) => b
- | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
- | _ => error "fold_rev2";
(* Vectors. Conventionally indexed 1..n. *)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Nov 27 19:41:37 2010 +0100
@@ -19,7 +19,7 @@
lemma injective_scaleR:
assumes "(c :: real) ~= 0"
shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
-by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+ by (metis assms injI real_vector.scale_cancel_left)
lemma linear_add_cmul:
fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
--- a/src/HOL/Multivariate_Analysis/normarith.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Nov 27 19:41:37 2010 +0100
@@ -117,13 +117,6 @@
[] => []
| h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
-
-fun forall2 p l1 l2 = case (l1,l2) of
- ([],[]) => true
- | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
- | _ => false;
-
-
fun vertices vs eqs =
let
fun vertex cmb = case solve(vs,cmb) of
@@ -131,16 +124,16 @@
| SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
val rawvs = map_filter vertex (combinations (length vs) eqs)
val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
- in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
+ in fold_rev (insert (eq_list op =/)) unset []
end
-fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
+val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
fun subsume todo dun = case todo of
[] => dun
|v::ovs =>
- let val dun' = if exists (fn w => subsumes w v) dun then dun
- else v::(filter (fn w => not(subsumes v w)) dun)
+ let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
+ else v:: filter (fn w => not (subsumes (v, w))) dun
in subsume ovs dun'
end;
@@ -246,10 +239,6 @@
Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
| _ => raise CTERM ("norm_canon_conv", [ct])
-fun fold_rev2 f [] [] z = z
- | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
- | fold_rev2 f _ _ _ = raise UnequalLengths;
-
fun int_flip v eq =
if FuncUtil.Intfunc.defined eq v
then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
--- a/src/HOL/Statespace/document/root.tex Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Statespace/document/root.tex Sat Nov 27 19:41:37 2010 +0100
@@ -1,31 +1,5 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
- %option greek for \<euro>
- %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
-
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<cent>, \<currency>
-
% this should be the last package used
\usepackage{pdfsetup}
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Nov 27 19:41:37 2010 +0100
@@ -54,6 +54,8 @@
val Suml_inject = @{thm Suml_inject};
val Sumr_inject = @{thm Sumr_inject};
+val datatype_injI =
+ @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
(** proof of characteristic theorems **)
@@ -438,8 +440,7 @@
Lim_inject :: inj_thms') @ fun_congs) 1),
atac 1]))])])])]);
- val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
- (split_conj_thm inj_thm);
+ val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
val elem_thm =
Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sat Nov 27 19:41:37 2010 +0100
@@ -324,7 +324,7 @@
\ nested recursion")
| (SOME {index, descr, ...}) =>
let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
- val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
+ val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
typ_error T ("Type constructor " ^ tname ^ " used with wrong\
\ number of arguments")
in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Nov 27 19:41:37 2010 +0100
@@ -48,8 +48,8 @@
fun make_tnames Ts =
let
- fun type_name (TFree (name, _)) = implode (tl (raw_explode name)) (* FIXME Symbol.explode (?) *)
- | type_name (Type (name, _)) =
+ fun type_name (TFree (name, _)) = unprefix "'" name
+ | type_name (Type (name, _)) =
let val name' = Long_Name.base_name name
in if Syntax.is_identifier name' then name' else "x" end;
in indexify_names (map type_name Ts) end;
--- a/src/HOL/Tools/Function/function_lib.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Sat Nov 27 19:41:37 2010 +0100
@@ -44,11 +44,11 @@
fun map4 _ [] [] [] [] = []
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
- | map4 _ _ _ _ _ = raise Library.UnequalLengths;
+ | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
fun map7 _ [] [] [] [] [] [] [] = []
| 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
- | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
+ | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
--- a/src/HOL/Tools/Function/size.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Sat Nov 27 19:41:37 2010 +0100
@@ -71,7 +71,7 @@
val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
map (fn T as TFree (s, _) =>
let
- val name = "f" ^ implode (tl (raw_explode s)); (* FIXME Symbol.explode (?) *)
+ val name = "f" ^ unprefix "'" s;
val U = T --> HOLogic.natT
in
(((s, Free (name, U)), U), name)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Nov 27 19:41:37 2010 +0100
@@ -393,7 +393,7 @@
| do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
accum =
(accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
- handle Library.UnequalLengths =>
+ handle ListPair.UnequalLengths =>
raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
| do_mtype_comp _ _ (MType _) (MType _) accum =
accum (* no need to compare them thanks to the cache *)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Nov 27 19:41:37 2010 +0100
@@ -527,7 +527,7 @@
| NONE =>
Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
$ Abs (s, T, kill ss Ts ts))
- | kill _ _ _ = raise UnequalLengths
+ | kill _ _ _ = raise ListPair.UnequalLengths
fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
gather (ss @ [s1]) (Ts @ [T1]) t1
| gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Nov 27 19:41:37 2010 +0100
@@ -204,7 +204,7 @@
fun map3 _ [] [] [] = []
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
- | map3 _ _ _ _ = raise UnequalLengths
+ | map3 _ _ _ _ = raise ListPair.UnequalLengths
fun double_lookup eq ps key =
case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
--- a/src/HOL/Tools/groebner.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/groebner.ML Sat Nov 27 19:41:37 2010 +0100
@@ -233,14 +233,9 @@
fun align ((p,hp),(q,hq)) =
if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
-fun forall2 p l1 l2 =
- case (l1,l2) of
- ([],[]) => true
- | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
- | _ => false;
fun poly_eq p1 p2 =
- forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
+ eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
fun memx ((p1,h1),(p2,h2)) ppairs =
not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
--- a/src/HOL/Tools/record.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/record.ML Sat Nov 27 19:41:37 2010 +0100
@@ -917,7 +917,7 @@
val fields' = extern f :: map Long_Name.base_name fs;
val (args', more) = split_last args;
in (fields' ~~ args') @ strip_fields more end
- handle Library.UnequalLengths => [("", t)])
+ handle ListPair.UnequalLengths => [("", t)])
| NONE => [("", t)])
| NONE => [("", t)])
| _ => [("", t)]);
--- a/src/HOL/Tools/refute.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOL/Tools/refute.ML Sat Nov 27 19:41:37 2010 +0100
@@ -2953,9 +2953,7 @@
fun stlc_printer ctxt model T intr assignment =
let
(* string -> string *)
- fun strip_leading_quote s =
- (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
- o raw_explode) s (* FIXME Symbol.explode (?) *)
+ val strip_leading_quote = perhaps (try (unprefix "'"))
(* Term.typ -> string *)
fun string_of_typ (Type (s, _)) = s
| string_of_typ (TFree (x, _)) = strip_leading_quote x
--- a/src/HOLCF/Cont.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Cont.thy Sat Nov 27 19:41:37 2010 +0100
@@ -97,22 +97,26 @@
done
lemma contI2:
+ fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes mono: "monofun f"
assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
shows "cont f"
-apply (rule contI)
-apply (rule thelubE)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule below_antisym)
-apply (rule is_lub_thelub)
-apply (erule ch2ch_monofun [OF mono])
-apply (rule ub2ub_monofun [OF mono])
-apply (rule is_lubD1)
-apply (erule cpo_lubI)
-apply (rule below, assumption)
-apply (erule ch2ch_monofun [OF mono])
-done
+proof (rule contI)
+ fix Y :: "nat \<Rightarrow> 'a"
+ assume Y: "chain Y"
+ with mono have fY: "chain (\<lambda>i. f (Y i))"
+ by (rule ch2ch_monofun)
+ have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)"
+ apply (rule below_antisym)
+ apply (rule lub_below [OF fY])
+ apply (rule monofunE [OF mono])
+ apply (rule is_ub_thelub [OF Y])
+ apply (rule below [OF Y fY])
+ done
+ with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+ by (rule thelubE)
+qed
subsection {* Collection of continuity rules *}
--- a/src/HOLCF/Domain.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Domain.thy Sat Nov 27 19:41:37 2010 +0100
@@ -340,13 +340,13 @@
deflation_sprod_map deflation_cprod_map deflation_u_map
setup {*
- fold Domain_Take_Proofs.add_map_function
- [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
- (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
- (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
- (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
- (@{type_name prod}, @{const_name cprod_map}, [true, true]),
- (@{type_name "u"}, @{const_name u_map}, [true])]
+ fold Domain_Take_Proofs.add_rec_type
+ [(@{type_name cfun}, [true, true]),
+ (@{type_name "sfun"}, [true, true]),
+ (@{type_name ssum}, [true, true]),
+ (@{type_name sprod}, [true, true]),
+ (@{type_name prod}, [true, true]),
+ (@{type_name "u"}, [true])]
*}
end
--- a/src/HOLCF/Fixrec.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Sat Nov 27 19:41:37 2010 +0100
@@ -26,10 +26,6 @@
succeed :: "'a \<rightarrow> 'a match" where
"succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))"
-definition
- match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where
- "match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))"
-
lemma matchE [case_names bottom fail succeed, cases type: match]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
unfolding fail_def succeed_def
@@ -52,40 +48,31 @@
"succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
-lemma match_case_simps [simp]:
- "match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
- "match_case\<cdot>f\<cdot>r\<cdot>fail = f"
- "match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x"
-by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match
- cont2cont_LAM
- cont_Abs_match Abs_match_inverse Rep_match_strict)
-
-translations
- "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2"
- == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
-
subsubsection {* Run operator *}
definition
run :: "'a match \<rightarrow> 'a::pcpo" where
- "run = match_case\<cdot>\<bottom>\<cdot>ID"
+ "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
text {* rewrite rules for run *}
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
-by (simp add: run_def)
+unfolding run_def
+by (simp add: cont_Rep_match Rep_match_strict)
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
-by (simp add: run_def)
+unfolding run_def fail_def
+by (simp add: cont_Rep_match Abs_match_inverse)
lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x"
-by (simp add: run_def)
+unfolding run_def succeed_def
+by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
subsubsection {* Monad plus operator *}
definition
mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
- "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | succeed\<cdot>x \<Rightarrow> m1)"
+ "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))"
abbreviation
mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match" (infixr "+++" 65) where
@@ -93,14 +80,19 @@
text {* rewrite rules for mplus *}
+lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
+
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
-by (simp add: mplus_def)
+unfolding mplus_def
+by (simp add: cont2cont_Rep_match Rep_match_strict)
lemma mplus_fail [simp]: "fail +++ m = m"
-by (simp add: mplus_def)
+unfolding mplus_def fail_def
+by (simp add: cont2cont_Rep_match Abs_match_inverse)
lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
-by (simp add: mplus_def)
+unfolding mplus_def succeed_def
+by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
lemma mplus_fail2 [simp]: "m +++ fail = m"
by (cases m, simp_all)
--- a/src/HOLCF/LowerPD.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Sat Nov 27 19:41:37 2010 +0100
@@ -195,7 +195,7 @@
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma lower_plus_below_iff:
+lemma lower_plus_below_iff [simp]:
"xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
apply safe
apply (erule below_trans [OF lower_plus_below1])
@@ -203,7 +203,7 @@
apply (erule (1) lower_plus_least)
done
-lemma lower_unit_below_plus_iff:
+lemma lower_unit_below_plus_iff [simp]:
"{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
apply (induct x rule: compact_basis.principal_induct, simp)
apply (induct ys rule: lower_pd.principal_induct, simp)
@@ -328,7 +328,7 @@
apply (erule lower_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: rev_below_trans [OF lower_plus_below1])
-apply (simp add: lower_plus_below_iff)
+apply simp
done
definition
@@ -389,14 +389,14 @@
apply default
apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: lower_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
done
lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
apply default
apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: lower_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
done
(* FIXME: long proof! *)
--- a/src/HOLCF/Powerdomains.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Powerdomains.thy Sat Nov 27 19:41:37 2010 +0100
@@ -42,10 +42,10 @@
deflation_upper_map deflation_lower_map deflation_convex_map
setup {*
- fold Domain_Take_Proofs.add_map_function
- [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
- (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
- (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
+ fold Domain_Take_Proofs.add_rec_type
+ [(@{type_name "upper_pd"}, [true]),
+ (@{type_name "lower_pd"}, [true]),
+ (@{type_name "convex_pd"}, [true])]
*}
end
--- a/src/HOLCF/Tools/Domain/domain.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain.ML Sat Nov 27 19:41:37 2010 +0100
@@ -118,14 +118,14 @@
(* test for free type variables, illegal sort constraints on rhs,
non-pcpo-types and invalid use of recursive type;
replace sorts in type variables on rhs *)
- val map_tab = Domain_Take_Proofs.get_map_tab thy;
+ val rec_tab = Domain_Take_Proofs.get_rec_tab thy;
fun check_rec rec_ok (T as TFree (v,_)) =
if AList.defined (op =) sorts v then T
else error ("Free type variable " ^ quote v ^ " on rhs.")
| check_rec rec_ok (T as Type (s, Ts)) =
(case AList.lookup (op =) dtnvs' s of
NONE =>
- let val rec_ok' = rec_ok andalso Symtab.defined map_tab s;
+ let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s;
in Type (s, map (check_rec rec_ok') Ts) end
| SOME typevars =>
if typevars <> Ts
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Nov 27 19:41:37 2010 +0100
@@ -350,17 +350,17 @@
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts deflation_map_binds deflation_map_thm);
- (* register map functions in theory data *)
+ (* register indirect recursion in theory data *)
local
- fun register_map ((dname, map_name), args) =
- Domain_Take_Proofs.add_map_function (dname, map_name, args);
+ fun register_map (dname, args) =
+ Domain_Take_Proofs.add_rec_type (dname, args);
val dnames = map (fst o dest_Type o fst) dom_eqns;
val map_names = map (fst o dest_Const) map_consts;
fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [];
val argss = map args dom_eqns;
in
val thy =
- fold register_map (dnames ~~ map_names ~~ argss) thy;
+ fold register_map (dnames ~~ argss) thy;
end;
(* register deflation theorems *)
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Nov 27 19:41:37 2010 +0100
@@ -55,8 +55,8 @@
val map_of_typ :
theory -> (typ * term) list -> typ -> term
- val add_map_function : (string * string * bool list) -> theory -> theory
- val get_map_tab : theory -> (string * bool list) Symtab.table
+ val add_rec_type : (string * bool list) -> theory -> theory
+ val get_rec_tab : theory -> (bool list) Symtab.table
val add_deflation_thm : thm -> theory -> theory
val get_deflation_thms : theory -> thm list
val map_ID_add : attribute
@@ -119,12 +119,10 @@
(******************************** theory data *********************************)
(******************************************************************************)
-structure MapData = Theory_Data
+structure Rec_Data = Theory_Data
(
- (* constant names like "foo_map" *)
- (* list indicates which type arguments correspond to map arguments *)
- (* alternatively, which type arguments allow indirect recursion *)
- type T = (string * bool list) Symtab.table;
+ (* list indicates which type arguments allow indirect recursion *)
+ type T = (bool list) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
@@ -142,13 +140,13 @@
val description = "theorems like foo_map$ID = ID"
);
-fun add_map_function (tname, map_name, bs) =
- MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
+fun add_rec_type (tname, bs) =
+ Rec_Data.map (Symtab.insert (K true) (tname, bs));
fun add_deflation_thm thm =
Context.theory_map (DeflMapData.add_thm thm);
-val get_map_tab = MapData.get;
+val get_rec_tab = Rec_Data.get;
fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
val map_ID_add = Map_Id_Data.add;
--- a/src/HOLCF/UpperPD.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Sat Nov 27 19:41:37 2010 +0100
@@ -193,7 +193,7 @@
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma upper_below_plus_iff:
+lemma upper_below_plus_iff [simp]:
"xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
apply safe
apply (erule below_trans [OF _ upper_plus_below1])
@@ -201,7 +201,7 @@
apply (erule (1) upper_plus_greatest)
done
-lemma upper_plus_below_unit_iff:
+lemma upper_plus_below_unit_iff [simp]:
"xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
apply (induct xs rule: upper_pd.principal_induct, simp)
apply (induct ys rule: upper_pd.principal_induct, simp)
@@ -323,7 +323,7 @@
apply (erule upper_le_induct, safe)
apply (simp add: monofun_cfun)
apply (simp add: below_trans [OF upper_plus_below1])
-apply (simp add: upper_below_plus_iff)
+apply simp
done
definition
@@ -384,14 +384,14 @@
apply default
apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: upper_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
done
lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
apply default
apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: upper_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
done
(* FIXME: long proof! *)
--- a/src/HOLCF/ex/Pattern_Match.thy Sat Nov 27 19:41:28 2010 +0100
+++ b/src/HOLCF/ex/Pattern_Match.thy Sat Nov 27 19:41:37 2010 +0100
@@ -53,11 +53,24 @@
lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
+subsection {* Bind operator for match monad *}
+
+definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
+ "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
+
+lemma match_bind_simps [simp]:
+ "match_bind\<cdot>\<bottom>\<cdot>k = \<bottom>"
+ "match_bind\<cdot>fail\<cdot>k = fail"
+ "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
+unfolding match_bind_def fail_def succeed_def
+by (simp_all add: cont2cont_Rep_match cont_Abs_match
+ Rep_match_strict Abs_match_inverse)
+
subsection {* Case branch combinator *}
definition
branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
- "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
+ "branch p \<equiv> \<Lambda> r x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))"
lemma branch_simps:
"p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
@@ -72,7 +85,7 @@
definition
cases :: "'a match \<rightarrow> 'a::pcpo" where
- "cases = match_case\<cdot>\<bottom>\<cdot>ID"
+ "cases = Fixrec.run"
text {* rewrite rules for cases *}
@@ -165,7 +178,7 @@
definition
cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
"cpair_pat p1 p2 = (\<Lambda>(x, y).
- 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))"
+ match_bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. match_bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))))"
definition
spair_pat ::
@@ -313,7 +326,7 @@
definition
as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
- "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
+ "as_pat p = (\<Lambda> x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. succeed\<cdot>(x, a)))"
definition
lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
@@ -544,7 +557,7 @@
val (fun1, fun2, taken) = pat_lhs (pat, args);
val defs = @{thm branch_def} :: pat_defs;
val goal = mk_trp (mk_strict fun1);
- val rules = @{thms match_case_simps} @ case_rews;
+ val rules = @{thms match_bind_simps} @ case_rews;
val tacs = [simp_tac (beta_ss addsimps rules) 1];
in prove thy defs goal (K tacs) end;
fun pat_apps (i, (pat, (con, args))) =
@@ -559,7 +572,7 @@
val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
val goal = Logic.list_implies (assms, concl);
val defs = @{thm branch_def} :: pat_defs;
- val rules = @{thms match_case_simps} @ case_rews;
+ val rules = @{thms match_bind_simps} @ case_rews;
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
in prove thy defs goal (K tacs) end;
in map_index pat_app spec end;
--- a/src/Pure/Proof/reconstruct.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sat Nov 27 19:41:37 2010 +0100
@@ -137,7 +137,7 @@
NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
- (forall_intr_vfs prop) handle Library.UnequalLengths =>
+ (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
--- a/src/Pure/consts.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Pure/consts.ML Sat Nov 27 19:41:37 2010 +0100
@@ -215,7 +215,7 @@
let
val declT = type_scheme consts c;
val vars = map Term.dest_TVar (typargs consts (c, declT));
- val inst = vars ~~ Ts handle UnequalLengths =>
+ val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
in declT |> Term_Subst.instantiateT inst end;
--- a/src/Pure/drule.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Pure/drule.ML Sat Nov 27 19:41:37 2010 +0100
@@ -891,7 +891,7 @@
handle TYPE (msg, _, _) => err msg;
fun zip_vars xs ys =
- zip_options xs ys handle Library.UnequalLengths =>
+ zip_options xs ys handle ListPair.UnequalLengths =>
err "more instantiations than variables in thm";
(*instantiate types first!*)
--- a/src/Pure/library.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Pure/library.ML Sat Nov 27 19:41:37 2010 +0100
@@ -58,7 +58,6 @@
val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
(*lists*)
- exception UnequalLengths
val single: 'a -> 'a list
val the_single: 'a list -> 'a
val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -97,6 +96,7 @@
val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val zip_options: 'a list -> 'b option list -> ('a * 'b) list
val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -321,8 +321,6 @@
(** lists **)
-exception UnequalLengths;
-
fun single x = [x];
fun the_single [x] = x
@@ -495,7 +493,7 @@
let val (ps, qs) = chop (length xs) ys
in ps :: unflat xss qs end
| unflat [] [] = []
- | unflat _ _ = raise UnequalLengths;
+ | unflat _ _ = raise ListPair.UnequalLengths;
fun burrow f xss = unflat xss (f (flat xss));
@@ -534,19 +532,21 @@
(* lists of pairs *)
-exception UnequalLengths;
-
fun map2 _ [] [] = []
| map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
- | map2 _ _ _ = raise UnequalLengths;
+ | map2 _ _ _ = raise ListPair.UnequalLengths;
fun fold2 f [] [] z = z
| fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
- | fold2 f _ _ _ = raise UnequalLengths;
+ | fold2 f _ _ _ = raise ListPair.UnequalLengths;
+
+fun fold_rev2 f [] [] z = z
+ | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
+ | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
fun forall2 P [] [] = true
| forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
- | forall2 P _ _ = raise UnequalLengths;
+ | forall2 P _ _ = raise ListPair.UnequalLengths;
fun map_split f [] = ([], [])
| map_split f (x :: xs) =
@@ -558,13 +558,13 @@
fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
| zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
| zip_options _ [] = []
- | zip_options [] _ = raise UnequalLengths;
+ | zip_options [] _ = raise ListPair.UnequalLengths;
(*combine two lists forming a list of pairs:
[x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*)
fun [] ~~ [] = []
| (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
- | _ ~~ _ = raise UnequalLengths;
+ | _ ~~ _ = raise ListPair.UnequalLengths;
(*inverse of ~~; the old 'split':
[(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*)
@@ -843,10 +843,11 @@
fun map_transpose f xss =
let
- val n = case distinct (op =) (map length xss)
- of [] => 0
+ val n =
+ (case distinct (op =) (map length xss) of
+ [] => 0
| [n] => n
- | _ => raise UnequalLengths;
+ | _ => raise ListPair.UnequalLengths);
in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
@@ -1066,3 +1067,5 @@
structure Basic_Library: BASIC_LIBRARY = Library;
open Basic_Library;
+
+datatype legacy = UnequalLengths;
--- a/src/Pure/pattern.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Pure/pattern.ML Sat Nov 27 19:41:37 2010 +0100
@@ -365,7 +365,7 @@
and cases(binders,env as (iTs,itms),pat,obj) =
let val (ph,pargs) = strip_comb pat
fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
- handle UnequalLengths => raise MATCH
+ handle ListPair.UnequalLengths => raise MATCH
fun rigrig2((a:string,Ta),(b,Tb),oargs) =
if a <> b then raise MATCH
else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
--- a/src/Tools/eqsubst.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Tools/eqsubst.ML Sat Nov 27 19:41:37 2010 +0100
@@ -235,13 +235,13 @@
val initenv =
Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
val useq = Unify.smash_unifiers thry [a] initenv
- handle UnequalLengths => Seq.empty
+ handle ListPair.UnequalLengths => Seq.empty
| Term.TERM _ => Seq.empty;
fun clean_unify' useq () =
(case (Seq.pull useq) of
NONE => NONE
| SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
- handle UnequalLengths => NONE
+ handle ListPair.UnequalLengths => NONE
| Term.TERM _ => NONE
in
(Seq.make (clean_unify' useq))
--- a/src/Tools/induct_tacs.ML Sat Nov 27 19:41:28 2010 +0100
+++ b/src/Tools/induct_tacs.ML Sat Nov 27 19:41:37 2010 +0100
@@ -96,7 +96,7 @@
val _ = Method.trace ctxt [rule'];
val concls = Logic.dest_conjunctions (Thm.concl_of rule);
- val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
+ val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
error "Induction rule has different numbers of variables";
in res_inst_tac ctxt insts rule' i st end
handle THM _ => Seq.empty;