# HG changeset patch # User haftmann # Date 1290883297 -3600 # Node ID 1554681757509734228a0ebdb0befea29482149e # Parent 1ef64dcb24b750ee8e5fb457d0eacf301ac4195a# Parent 35781a159d1cc9bf06e119caf589e5aeb84b28f9 merged diff -r 1ef64dcb24b7 -r 155468175750 NEWS --- 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. diff -r 1ef64dcb24b7 -r 155468175750 doc-src/LaTeXsugar/Sugar/document/root.tex --- 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 \, \, \, - % \, \, \, - % \, \, \, - % \, \, - % \, \, \ -%\usepackage[greek,english]{babel} % greek for \, - % english for \, - % \ - % default language = last -%\usepackage[latin1]{inputenc} % for \, \, - % \, \, - % \, \, - % \ -%\usepackage[only,bigsqcap]{stmaryrd} % for \ -%\usepackage{eufrak} % for \ ... \, \ ... \ - % (only needed if amssymb not used) -%\usepackage{textcomp} % for \, \ +\usepackage{amssymb} \usepackage{mathpartir} diff -r 1ef64dcb24b7 -r 155468175750 doc-src/Main/main.tex --- 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 \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ - -%\usepackage[latin1]{inputenc} - %for \, \, \, \, - %\, \, \ - \usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \ % this should be the last package used \usepackage{../pdfsetup} diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Fun.thy --- 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 \ b : range f = (EX! x. b = f x)" by (unfold inj_on_def, blast) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- 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. *) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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)" diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Multivariate_Analysis/normarith.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Statespace/document/root.tex --- 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 \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ - -%\usepackage[latin1]{inputenc} - %for \, \, \, \, - %\, \, \ - -%\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \ - % this should be the last package used \usepackage{pdfsetup} diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Datatype/datatype.ML --- 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)) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Datatype/datatype_aux.ML --- 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, diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Datatype/datatype_prop.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Function/function_lib.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Function/size.ML --- 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) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 *) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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) diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/groebner.ML --- 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); diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/record.ML --- 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)]); diff -r 1ef64dcb24b7 -r 155468175750 src/HOL/Tools/refute.ML --- 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 diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Cont.thy --- 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 \ 'b::cpo" assumes mono: "monofun f" assumes below: "\Y. \chain Y; chain (\i. f (Y i))\ \ f (\i. Y i) \ (\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 \ 'a" + assume Y: "chain Y" + with mono have fY: "chain (\i. f (Y i))" + by (rule ch2ch_monofun) + have "(\i. f (Y i)) = f (\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 (\i. f (Y i)) <<| f (\i. Y i)" + by (rule thelubE) +qed subsection {* Collection of continuity rules *} diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Domain.thy --- 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 diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Fixrec.thy --- 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 \ 'a match" where "succeed = (\ x. Abs_match (sinr\(up\x)))" -definition - match_case :: "'b \ ('a \ 'b) \ 'a match \ 'b::pcpo" where - "match_case = (\ f r m. sscase\(\ x. f)\(fup\r)\(Rep_match m))" - lemma matchE [case_names bottom fail succeed, cases type: match]: "\p = \ \ Q; p = fail \ Q; \x. p = succeed\x \ Q\ \ Q" unfolding fail_def succeed_def @@ -52,40 +48,31 @@ "succeed\x \ fail" "fail \ succeed\x" by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) -lemma match_case_simps [simp]: - "match_case\f\r\\ = \" - "match_case\f\r\fail = f" - "match_case\f\r\(succeed\x) = r\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 \ t1 | XCONST succeed\x \ t2" - == "CONST match_case\t1\(\ x. t2)\m" - subsubsection {* Run operator *} definition run :: "'a match \ 'a::pcpo" where - "run = match_case\\\ID" + "run = (\ m. sscase\\\(fup\ID)\(Rep_match m))" text {* rewrite rules for run *} lemma run_strict [simp]: "run\\ = \" -by (simp add: run_def) +unfolding run_def +by (simp add: cont_Rep_match Rep_match_strict) lemma run_fail [simp]: "run\fail = \" -by (simp add: run_def) +unfolding run_def fail_def +by (simp add: cont_Rep_match Abs_match_inverse) lemma run_succeed [simp]: "run\(succeed\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 \ 'a match \ 'a match" where - "mplus = (\ m1 m2. case m1 of fail \ m2 | succeed\x \ m1)" + "mplus = (\ m1 m2. sscase\(\ _. m2)\(\ _. m1)\(Rep_match m1))" abbreviation mplus_syn :: "['a match, 'a match] \ '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]: "\ +++ m = \" -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\x +++ m = succeed\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) diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/LowerPD.thy --- 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 +\ ys \ zs \ xs \ zs \ ys \ 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}\ \ ys +\ zs \ {x}\ \ ys \ {x}\ \ 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 \ deflation (lower_map\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! *) diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Powerdomains.thy --- 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 diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Tools/Domain/domain.ML --- 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 diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 *) diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/UpperPD.thy --- 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 \ ys +\ zs \ xs \ ys \ xs \ 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 +\ ys \ {z}\ \ xs \ {z}\ \ ys \ {z}\" 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 \ deflation (upper_map\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! *) diff -r 1ef64dcb24b7 -r 155468175750 src/HOLCF/ex/Pattern_Match.thy --- 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 \ ('a \ 'b match) \ 'b match" where + "match_bind = (\ m k. sscase\(\ _. fail)\(fup\k)\(Rep_match m))" + +lemma match_bind_simps [simp]: + "match_bind\\\k = \" + "match_bind\fail\k = fail" + "match_bind\(succeed\x)\k = k\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 \ 'b match) \ ('b \ 'c) \ ('a \ 'c match)" where - "branch p \ \ r x. match_case\fail\(\ y. succeed\(r\y))\(p\x)" + "branch p \ \ r x. match_bind\(p\x)\(\ y. succeed\(r\y))" lemma branch_simps: "p\x = \ \ branch p\r\x = \" @@ -72,7 +85,7 @@ definition cases :: "'a match \ 'a::pcpo" where - "cases = match_case\\\ID" + "cases = Fixrec.run" text {* rewrite rules for cases *} @@ -165,7 +178,7 @@ definition cpair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a \ 'b, 'c \ 'd) pat" where "cpair_pat p1 p2 = (\(x, y). - match_case\fail\(\ a. match_case\fail\(\ b. succeed\(a, b))\(p2\y))\(p1\x))" + match_bind\(p1\x)\(\ a. match_bind\(p2\y)\(\ b. succeed\(a, b))))" definition spair_pat :: @@ -313,7 +326,7 @@ definition as_pat :: "('a \ 'b match) \ 'a \ ('a \ 'b) match" where - "as_pat p = (\ x. match_case\fail\(\ a. succeed\(x, a))\(p\x))" + "as_pat p = (\ x. match_bind\(p\x)\(\ a. succeed\(x, a)))" definition lazy_pat :: "('a \ 'b::pcpo match) \ ('a \ '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; diff -r 1ef64dcb24b7 -r 155468175750 src/Pure/Proof/reconstruct.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/Pure/consts.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/Pure/drule.ML --- 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!*) diff -r 1ef64dcb24b7 -r 155468175750 src/Pure/library.ML --- 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; diff -r 1ef64dcb24b7 -r 155468175750 src/Pure/pattern.ML --- 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) diff -r 1ef64dcb24b7 -r 155468175750 src/Tools/eqsubst.ML --- 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)) diff -r 1ef64dcb24b7 -r 155468175750 src/Tools/induct_tacs.ML --- 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;