--- a/Admin/isatest/settings/at64-poly-5.1-para Thu Feb 18 14:21:44 2010 -0800
+++ b/Admin/isatest/settings/at64-poly-5.1-para Thu Feb 18 14:28:26 2010 -0800
@@ -1,10 +1,10 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500"
+ ML_OPTIONS="-H 1000"
ISABELLE_HOME_USER=~/isabelle-at64-poly-para-e
--- a/src/HOL/Library/AssocList.thy Thu Feb 18 14:21:44 2010 -0800
+++ b/src/HOL/Library/AssocList.thy Thu Feb 18 14:28:26 2010 -0800
@@ -688,6 +688,10 @@
"Mapping.keys (AList xs) = set (map fst xs)"
by (simp add: keys_def dom_map_of_conv_image_fst)
+lemma ordered_keys_AList [code]:
+ "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
+ by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+
lemma size_AList [code]:
"Mapping.size (AList xs) = length (remdups (map fst xs))"
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
--- a/src/HOL/Library/Mapping.thy Thu Feb 18 14:21:44 2010 -0800
+++ b/src/HOL/Library/Mapping.thy Thu Feb 18 14:28:26 2010 -0800
@@ -28,6 +28,9 @@
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
"keys m = dom (lookup m)"
+definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
+ "ordered_keys m = sorted_list_of_set (keys m)"
+
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
"is_empty m \<longleftrightarrow> dom (lookup m) = {}"
@@ -139,6 +142,6 @@
by (cases m) simp
-hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
+hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
end
\ No newline at end of file
--- a/src/HOL/Library/Tree.thy Thu Feb 18 14:21:44 2010 -0800
+++ b/src/HOL/Library/Tree.thy Thu Feb 18 14:28:26 2010 -0800
@@ -124,6 +124,9 @@
"Mapping.update k v (Tree t) = Tree (update k v t)"
by (simp add: Tree_def lookup_update)
+lemma [code, code del]:
+ "Mapping.ordered_keys = Mapping.ordered_keys " ..
+
lemma keys_Tree [code]:
"Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
by (simp add: Mapping.keys_def lookup_Tree dom_lookup)
--- a/src/HOL/List.thy Thu Feb 18 14:21:44 2010 -0800
+++ b/src/HOL/List.thy Thu Feb 18 14:28:26 2010 -0800
@@ -284,9 +284,8 @@
"insort_key f x [] = [x]" |
"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
-primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"sort_key f [] = []" |
-"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"sort_key f xs = foldr (insort_key f) xs []"
abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
@@ -721,6 +720,11 @@
lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
by (induct xs) auto
+lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"
+apply(rule ext)
+apply(simp)
+done
+
lemma rev_map: "rev (map f xs) = map f (rev xs)"
by (induct xs) auto
@@ -2266,6 +2270,12 @@
==> foldr f l a = foldr g k b"
by (induct k arbitrary: a b l) simp_all
+lemma foldl_fun_comm:
+ assumes "\<And>x y s. f (f s x) y = f (f s y) x"
+ shows "f (foldl f s xs) x = foldl f (f s x) xs"
+ by (induct xs arbitrary: s)
+ (simp_all add: assms)
+
lemma (in semigroup_add) foldl_assoc:
shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
by (induct zs arbitrary: y) (simp_all add:add_assoc)
@@ -2274,6 +2284,15 @@
shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
by (induct zs) (simp_all add:foldl_assoc)
+lemma foldl_rev:
+ assumes "\<And>x y s. f (f s x) y = f (f s y) x"
+ shows "foldl f s (rev xs) = foldl f s xs"
+proof (induct xs arbitrary: s)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
+qed
+
text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
@@ -2342,6 +2361,10 @@
text {* @{const Finite_Set.fold} and @{const foldl} *}
+lemma (in fun_left_comm) fold_set_remdups:
+ "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
+ by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
+
lemma (in fun_left_comm_idem) fold_set:
"fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
@@ -3438,6 +3461,24 @@
lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
by (induct xs, auto)
+lemma insort_left_comm:
+ "insort x (insort y xs) = insort y (insort x xs)"
+ by (induct xs) auto
+
+lemma fun_left_comm_insort:
+ "fun_left_comm insort"
+proof
+qed (fact insort_left_comm)
+
+lemma sort_key_simps [simp]:
+ "sort_key f [] = []"
+ "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+ by (simp_all add: sort_key_def)
+
+lemma sort_foldl_insort:
+ "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
+ by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
+
lemma length_sort[simp]: "length (sort_key f xs) = length xs"
by (induct xs, auto)
@@ -3800,27 +3841,35 @@
sets to lists but one should convert in the other direction (via
@{const set}). *}
-
context linorder
begin
-definition
- sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
-
-lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
- set(sorted_list_of_set A) = A &
- sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
-apply(simp add:sorted_list_of_set_def)
-apply(rule the1I2)
- apply(simp_all add: finite_sorted_distinct_unique)
-done
-
-lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
-unfolding sorted_list_of_set_def
-apply(subst the_equality[of _ "[]"])
-apply simp_all
-done
+definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
+ "sorted_list_of_set = Finite_Set.fold insort []"
+
+lemma sorted_list_of_set_empty [simp]:
+ "sorted_list_of_set {} = []"
+ by (simp add: sorted_list_of_set_def)
+
+lemma sorted_list_of_set_insert [simp]:
+ assumes "finite A"
+ shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
+proof -
+ interpret fun_left_comm insort by (fact fun_left_comm_insort)
+ with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
+qed
+
+lemma sorted_list_of_set [simp]:
+ "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
+ \<and> distinct (sorted_list_of_set A)"
+ by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
+
+lemma sorted_list_of_set_sort_remdups:
+ "sorted_list_of_set (set xs) = sort (remdups xs)"
+proof -
+ interpret fun_left_comm insort by (fact fun_left_comm_insort)
+ show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
+qed
end
--- a/src/Pure/Isar/proof_context.ML Thu Feb 18 14:21:44 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML Thu Feb 18 14:28:26 2010 -0800
@@ -492,7 +492,7 @@
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
in
if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
- else Pattern.rewrite_term thy [] [match_abbrev] t
+ else Pattern.rewrite_term_top thy [] [match_abbrev] t
end;
--- a/src/Pure/Syntax/syn_trans.ML Thu Feb 18 14:21:44 2010 -0800
+++ b/src/Pure/Syntax/syn_trans.ML Thu Feb 18 14:28:26 2010 -0800
@@ -510,7 +510,7 @@
("_DDDOT", dddot_tr),
("_update_name", update_name_tr),
("_index", index_tr)],
- [],
+ ([]: (string * (term list -> term)) list),
[("_abs", abs_ast_tr'),
("_idts", idtyp_ast_tr' "_idts"),
("_pttrns", idtyp_ast_tr' "_pttrns"),
--- a/src/Pure/pattern.ML Thu Feb 18 14:21:44 2010 -0800
+++ b/src/Pure/pattern.ML Thu Feb 18 14:28:26 2010 -0800
@@ -29,6 +29,7 @@
val pattern: term -> bool
val match_rew: theory -> term -> term * term -> (term * term) option
val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
+ val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
exception Unif
exception MATCH
exception Pattern
@@ -432,7 +433,7 @@
handle MATCH => NONE
end;
-fun rewrite_term thy rules procs tm =
+fun gen_rewrite_term bot thy rules procs tm =
let
val skel0 = Bound 0;
@@ -448,42 +449,53 @@
NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
| x => x);
- fun rew1 bounds (Var _) _ = NONE
- | rew1 bounds skel tm = (case rew2 bounds skel tm of
- SOME tm1 => (case rew tm1 of
- SOME (tm2, skel') => SOME (the_default tm2 (rew1 bounds skel' tm2))
- | NONE => SOME tm1)
- | NONE => (case rew tm of
- SOME (tm1, skel') => SOME (the_default tm1 (rew1 bounds skel' tm1))
- | NONE => NONE))
-
- and rew2 bounds skel (tm1 $ tm2) = (case tm1 of
+ fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
Abs (_, _, body) =>
let val tm' = subst_bound (tm2, body)
- in SOME (the_default tm' (rew2 bounds skel0 tm')) end
+ in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
| _ =>
let val (skel1, skel2) = (case skel of
skel1 $ skel2 => (skel1, skel2)
| _ => (skel0, skel0))
- in case rew1 bounds skel1 tm1 of
- SOME tm1' => (case rew1 bounds skel2 tm2 of
+ in case r bounds skel1 tm1 of
+ SOME tm1' => (case r bounds skel2 tm2 of
SOME tm2' => SOME (tm1' $ tm2')
| NONE => SOME (tm1' $ tm2))
- | NONE => (case rew1 bounds skel2 tm2 of
+ | NONE => (case r bounds skel2 tm2 of
SOME tm2' => SOME (tm1 $ tm2')
| NONE => NONE)
end)
- | rew2 bounds skel (Abs body) =
+ | rew_sub r bounds skel (Abs body) =
let
val (abs, tm') = variant_absfree bounds body;
val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
- in case rew1 (bounds + 1) skel' tm' of
+ in case r (bounds + 1) skel' tm' of
SOME tm'' => SOME (abs tm'')
| NONE => NONE
end
- | rew2 _ _ _ = NONE;
+ | rew_sub _ _ _ _ = NONE;
+
+ fun rew_bot bounds (Var _) _ = NONE
+ | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
+ SOME tm1 => (case rew tm1 of
+ SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
+ | NONE => SOME tm1)
+ | NONE => (case rew tm of
+ SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
+ | NONE => NONE));
- in the_default tm (rew1 0 skel0 tm) end;
+ fun rew_top bounds _ tm = (case rew tm of
+ SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
+ SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
+ | NONE => SOME tm1)
+ | NONE => (case rew_sub rew_top bounds skel0 tm of
+ SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
+ | NONE => NONE));
+
+ in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
+
+val rewrite_term = gen_rewrite_term true;
+val rewrite_term_top = gen_rewrite_term false;
end;