--- a/src/HOL/Datatype.thy Thu Sep 11 22:33:12 2003 +0200
+++ b/src/HOL/Datatype.thy Sun Sep 14 17:53:27 2003 +0200
@@ -194,9 +194,17 @@
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
by (simp add: option_map_def)
+lemma option_map_is_None[iff]:
+ "(option_map f opt = None) = (opt = None)"
+by (simp add: option_map_def split add: option.split)
+
lemma option_map_eq_Some [iff]:
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
- by (simp add: option_map_def split add: option.split)
+by (simp add: option_map_def split add: option.split)
+
+lemma option_map_comp:
+ "option_map f (option_map g opt) = option_map (f o g) opt"
+by (simp add: option_map_def split add: option.split)
lemma option_map_o_sum_case [simp]:
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
--- a/src/HOL/List.thy Thu Sep 11 22:33:12 2003 +0200
+++ b/src/HOL/List.thy Sun Sep 14 17:53:27 2003 +0200
@@ -737,10 +737,23 @@
"!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
by (induct xs) (auto split: nat.split)
+lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
+apply(induct xs)
+ apply simp
+apply(simp split:nat.splits)
+done
+
lemma list_update_same_conv:
"!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
by (induct xs) (auto split: nat.split)
+lemma list_update_append1:
+ "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
+apply(induct xs)
+ apply simp
+apply(simp split:nat.split)
+done
+
lemma update_zip:
"!!i xy xs. length xs = length ys ==>
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
@@ -796,6 +809,18 @@
declare take_Cons [simp del] and drop_Cons [simp del]
+lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
+by(cases xs, simp_all)
+
+lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
+by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
+
+lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
+apply(induct xs)
+ apply simp
+apply(simp add:drop_Cons nth_Cons split:nat.splits)
+done
+
lemma take_Suc_conv_app_nth:
"!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
apply(induct xs)
@@ -905,6 +930,12 @@
lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
by(induct xs)(auto simp:drop_Cons split:nat.split)
+lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
+using set_take_subset by fast
+
+lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
+using set_drop_subset by fast
+
lemma append_eq_conv_conj:
"!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
apply(induct xs)
--- a/src/HOL/Map.thy Thu Sep 11 22:33:12 2003 +0200
+++ b/src/HOL/Map.thy Sun Sep 14 17:53:27 2003 +0200
@@ -347,6 +347,24 @@
lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
by(simp add:map_upds_def)
+lemma map_upds_append1[simp]: "\<And>ys m. size xs < size ys \<Longrightarrow>
+ m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
+apply(induct xs)
+ apply(clarsimp simp add:neq_Nil_conv)
+apply(case_tac ys)
+ apply simp
+apply simp
+done
+
+lemma map_upds_list_update2_drop[simp]:
+ "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
+ \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
+apply(induct xs)
+ apply simp
+apply(case_tac ys)
+ apply simp
+apply(simp split:nat.split)
+done
lemma map_upd_upds_conv_if: "!!x y ys f.
(f(x|->y))(xs [|->] ys) =
@@ -478,9 +496,15 @@
lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
by(simp add:map_le_def)
+lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
+by(force simp add:map_le_def)
+
lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
by(fastsimp simp add:map_le_def)
+lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
+by(force simp add:map_le_def)
+
lemma map_le_upds[simp]:
"!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
apply(induct as)
@@ -495,11 +519,8 @@
lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
by (simp add: map_le_def)
-lemma map_le_trans: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m h"
- apply (clarsimp simp add: map_le_def)
- apply (drule_tac x="a" in bspec, fastsimp)+
- apply assumption
-done
+lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
+by(force simp add:map_le_def)
lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
apply (unfold map_le_def)