# HG changeset patch # User huffman # Date 1266532106 28800 # Node ID 01e9684324676310d9deb10f1cffcc992a31224d # Parent 7641e8d831d2754af71de9f2cbc438bcef8ee0a4# Parent 5cc73912ebce9fca26c285cb8e38e48627303d74 merged diff -r 7641e8d831d2 -r 01e968432467 Admin/isatest/settings/at64-poly-5.1-para --- 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 diff -r 7641e8d831d2 -r 01e968432467 src/HOL/Library/AssocList.thy --- 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) diff -r 7641e8d831d2 -r 01e968432467 src/HOL/Library/Mapping.thy --- 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 \ 'a set" where "keys m = dom (lookup m)" +definition ordered_keys :: "('a\linorder, 'b) mapping \ 'a list" where + "ordered_keys m = sorted_list_of_set (keys m)" + definition is_empty :: "('a, 'b) mapping \ bool" where "is_empty m \ 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 diff -r 7641e8d831d2 -r 01e968432467 src/HOL/Library/Tree.thy --- 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 (\k. lookup t k \ None) (remdups (keys t)))" by (simp add: Mapping.keys_def lookup_Tree dom_lookup) diff -r 7641e8d831d2 -r 01e968432467 src/HOL/List.thy --- 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 \ f y then (x#y#ys) else y#(insort_key f x ys))" -primrec sort_key :: "('b \ 'a) \ 'b list \ 'b list" where -"sort_key f [] = []" | -"sort_key f (x#xs) = insort_key f x (sort_key f xs)" +definition sort_key :: "('b \ 'a) \ 'b list \ 'b list" where +"sort_key f xs = foldr (insort_key f) xs []" abbreviation "sort \ sort_key (\x. x)" abbreviation "insort \ insort_key (\x. x)" @@ -721,6 +720,11 @@ lemma map_map [simp]: "map f (map g xs) = map (f \ 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 "\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 "\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 (\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 (\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 (\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 \ '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 \ - 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 \ '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 \ set (sorted_list_of_set A) = A \ sorted (sorted_list_of_set A) + \ 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 diff -r 7641e8d831d2 -r 01e968432467 src/Pure/Isar/proof_context.ML --- 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; diff -r 7641e8d831d2 -r 01e968432467 src/Pure/Syntax/syn_trans.ML --- 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"), diff -r 7641e8d831d2 -r 01e968432467 src/Pure/pattern.ML --- 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;