# HG changeset patch
# User nipkow
# Date 1063554807 -7200
# Node ID 26dfcd0ac436744cbe4207d845faf8556932f203
# Parent  6d2a494e33be2a591e7164f762f7fe205314608b
Added new theorems

diff -r 6d2a494e33be -r 26dfcd0ac436 src/HOL/Datatype.thy
--- 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)"
diff -r 6d2a494e33be -r 26dfcd0ac436 src/HOL/List.thy
--- 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)
diff -r 6d2a494e33be -r 26dfcd0ac436 src/HOL/Map.thy
--- 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)