--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Decision_Procs.thy Mon Feb 09 10:39:57 2009 +0100
@@ -0,0 +1,5 @@
+theory Decision_Procs
+imports Cooper Ferrack MIR Approximation Dense_Linear_Order
+begin
+
+end
\ No newline at end of file
--- a/src/HOL/Integration.thy Mon Feb 09 10:37:59 2009 +0100
+++ b/src/HOL/Integration.thy Mon Feb 09 10:39:57 2009 +0100
@@ -558,7 +558,7 @@
apply (frule partition_eq_bound)
apply (drule_tac [2] partition_gt, auto)
apply (metis linear not_less partition_rhs partition_rhs2)
-apply (metis add_diff_inverse diff_is_0_eq le0 le_diff_conv nat_add_commute partition partition_eq_bound partition_rhs real_less_def termination_basic_simps(5))
+apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs)
done
lemma lemma_additivity4_psize_eq:
--- a/src/HOL/Library/Mapping.thy Mon Feb 09 10:37:59 2009 +0100
+++ b/src/HOL/Library/Mapping.thy Mon Feb 09 10:39:57 2009 +0100
@@ -39,6 +39,9 @@
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
"tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
+definition bulkload :: "'a list \<Rightarrow> (nat, 'a) map" where
+ "bulkload xs = Map (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
+
subsection {* Properties *}
@@ -63,6 +66,10 @@
"lookup (tabulate ks f) = (Some o f) |` set ks"
by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
+lemma lookup_bulkload:
+ "lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
+ unfolding bulkload_def by simp
+
lemma update_update:
"update k v (update k w m) = update k v m"
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
@@ -120,4 +127,9 @@
"size (tabulate ks f) = length (remdups ks)"
by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
+lemma bulkload_tabulate:
+ "bulkload xs = tabulate [0..<length xs] (nth xs)"
+ by (rule sym)
+ (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
+
end
\ No newline at end of file
--- a/src/HOL/List.thy Mon Feb 09 10:37:59 2009 +0100
+++ b/src/HOL/List.thy Mon Feb 09 10:39:57 2009 +0100
@@ -1215,10 +1215,10 @@
subsubsection {* @{text nth} *}
-lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
+lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
by auto
-lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
+lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
by auto
declare nth.simps [simp del]
@@ -1375,6 +1375,12 @@
apply auto
done
+lemma list_update_code [code]:
+ "[][i := y] = []"
+ "(x # xs)[0 := y] = y # xs"
+ "(x # xs)[Suc i := y] = x # xs[i := y]"
+ by simp_all
+
subsubsection {* @{text last} and @{text butlast} *}
@@ -1846,6 +1852,15 @@
"(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
by(blast dest: set_zip_leftD set_zip_rightD)
+lemma zip_map_fst_snd:
+ "zip (map fst zs) (map snd zs) = zs"
+ by (induct zs) simp_all
+
+lemma zip_eq_conv:
+ "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
+ by (auto simp add: zip_map_fst_snd)
+
+
subsubsection {* @{text list_all2} *}
lemma list_all2_lengthD [intro?]:
--- a/src/HOL/OrderedGroup.thy Mon Feb 09 10:37:59 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Mon Feb 09 10:39:57 2009 +0100
@@ -598,12 +598,12 @@
by (simp add: algebra_simps)
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
class ordered_ab_semigroup_add =
linorder + pordered_ab_semigroup_add
@@ -1310,9 +1310,9 @@
add_less_le_mono add_le_less_mono add_strict_mono)
text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
+lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
-lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
+lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
ML {*
structure ab_group_add_cancel = Abel_Cancel
--- a/src/HOL/Ring_and_Field.thy Mon Feb 09 10:37:59 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Feb 09 10:39:57 2009 +0100
@@ -232,8 +232,8 @@
by (rule equals_zero_I) (simp add: right_distrib [symmetric])
text{*Extract signs from products*}
-lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
lemma minus_mult_minus [simp]: "- a * - b = a * b"
by simp
@@ -247,11 +247,11 @@
lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
by (simp add: left_distrib diff_minus)
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
lemma eq_add_iff1:
"a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -263,7 +263,7 @@
end
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
class comm_ring = comm_semiring + ab_group_add
@@ -751,7 +751,7 @@
subclass pordered_ab_group_add ..
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
lemma less_add_iff1:
"a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
@@ -960,7 +960,7 @@
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
class pordered_comm_ring = comm_ring + pordered_comm_semiring
@@ -1107,7 +1107,7 @@
text {* Simprules for comparisons where common factors can be cancelled. *}
-lemmas mult_compare_simps =
+lemmas mult_compare_simps[noatp] =
mult_le_cancel_right mult_le_cancel_left
mult_le_cancel_right1 mult_le_cancel_right2
mult_le_cancel_left1 mult_le_cancel_left2
@@ -1219,7 +1219,7 @@
lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
by (simp add: divide_inverse mult_ac)
-lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
lemma divide_divide_eq_right [simp,noatp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
@@ -1297,8 +1297,8 @@
text{*The effect is to extract signs from divisions*}
-lemmas divide_minus_left = minus_divide_left [symmetric]
-lemmas divide_minus_right = minus_divide_right [symmetric]
+lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
+lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
declare divide_minus_left [simp] divide_minus_right [simp]
lemma minus_divide_divide [simp]:
@@ -1359,7 +1359,7 @@
by (subst eq_divide_eq, simp)
-lemmas field_eq_simps = algebra_simps
+lemmas field_eq_simps[noatp] = algebra_simps
(* pull / out*)
add_divide_eq_iff divide_add_eq_iff
diff_divide_eq_iff divide_diff_eq_iff
@@ -1720,7 +1720,7 @@
(for inequations). Can be too aggressive and is therefore separate from the
more benign @{text algebra_simps}. *}
-lemmas field_simps = field_eq_simps
+lemmas field_simps[noatp] = field_eq_simps
(* multiply ineqn *)
pos_divide_less_eq neg_divide_less_eq
pos_less_divide_eq neg_less_divide_eq
@@ -1732,7 +1732,7 @@
sign_simps} to @{text field_simps} because the former can lead to case
explosions. *}
-lemmas sign_simps = group_simps
+lemmas sign_simps[noatp] = group_simps
zero_less_mult_iff mult_less_0_iff
(* Only works once linear arithmetic is installed:
@@ -1856,9 +1856,9 @@
lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
-declare zero_less_divide_1_iff [simp]
+declare zero_less_divide_1_iff [simp,noatp]
declare divide_less_0_1_iff [simp,noatp]
-declare zero_le_divide_1_iff [simp]
+declare zero_le_divide_1_iff [simp,noatp]
declare divide_le_0_1_iff [simp,noatp]
@@ -2234,7 +2234,7 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
-lemmas eq_minus_self_iff = equal_neg_zero
+lemmas eq_minus_self_iff[noatp] = equal_neg_zero
lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
--- a/src/Tools/code/code_haskell.ML Mon Feb 09 10:37:59 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Mon Feb 09 10:39:57 2009 +0100
@@ -407,6 +407,8 @@
| (_, (_, NONE)) => NONE) stmts));
val serialize_module =
if null stmt_names then serialize_module1 else pair "" o serialize_module2;
+ fun check_destination destination =
+ (File.check destination; destination);
fun write_module destination (modlname, content) =
let
val filename = case modlname
@@ -421,7 +423,8 @@
end
in
Code_Target.mk_serialization target NONE
- (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))
+ (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map
+ (write_module (check_destination file)))
(rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd))
(map (uncurry pr_module) includes
@ map serialize_module (Symtab.dest hs_program))