Added new theorems
authornipkow
Sun Sep 14 17:53:27 2003 +0200 (2003-09-14)
changeset 1418726dfcd0ac436
parent 14186 6d2a494e33be
child 14188 f471cd4c7282
Added new theorems
src/HOL/Datatype.thy
src/HOL/List.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Datatype.thy	Thu Sep 11 22:33:12 2003 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sun Sep 14 17:53:27 2003 +0200
     1.3 @@ -194,9 +194,17 @@
     1.4  lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
     1.5    by (simp add: option_map_def)
     1.6  
     1.7 +lemma option_map_is_None[iff]:
     1.8 + "(option_map f opt = None) = (opt = None)"
     1.9 +by (simp add: option_map_def split add: option.split)
    1.10 +
    1.11  lemma option_map_eq_Some [iff]:
    1.12      "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
    1.13 -  by (simp add: option_map_def split add: option.split)
    1.14 +by (simp add: option_map_def split add: option.split)
    1.15 +
    1.16 +lemma option_map_comp:
    1.17 + "option_map f (option_map g opt) = option_map (f o g) opt"
    1.18 +by (simp add: option_map_def split add: option.split)
    1.19  
    1.20  lemma option_map_o_sum_case [simp]:
    1.21      "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
     2.1 --- a/src/HOL/List.thy	Thu Sep 11 22:33:12 2003 +0200
     2.2 +++ b/src/HOL/List.thy	Sun Sep 14 17:53:27 2003 +0200
     2.3 @@ -737,10 +737,23 @@
     2.4  "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
     2.5  by (induct xs) (auto split: nat.split)
     2.6  
     2.7 +lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
     2.8 +apply(induct xs)
     2.9 + apply simp
    2.10 +apply(simp split:nat.splits)
    2.11 +done
    2.12 +
    2.13  lemma list_update_same_conv:
    2.14  "!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
    2.15  by (induct xs) (auto split: nat.split)
    2.16  
    2.17 +lemma list_update_append1:
    2.18 + "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
    2.19 +apply(induct xs)
    2.20 + apply simp
    2.21 +apply(simp split:nat.split)
    2.22 +done
    2.23 +
    2.24  lemma update_zip:
    2.25  "!!i xy xs. length xs = length ys ==>
    2.26  (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
    2.27 @@ -796,6 +809,18 @@
    2.28  
    2.29  declare take_Cons [simp del] and drop_Cons [simp del]
    2.30  
    2.31 +lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
    2.32 +by(cases xs, simp_all)
    2.33 +
    2.34 +lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
    2.35 +by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
    2.36 +
    2.37 +lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
    2.38 +apply(induct xs)
    2.39 + apply simp
    2.40 +apply(simp add:drop_Cons nth_Cons split:nat.splits)
    2.41 +done
    2.42 +
    2.43  lemma take_Suc_conv_app_nth:
    2.44   "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
    2.45  apply(induct xs)
    2.46 @@ -905,6 +930,12 @@
    2.47  lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
    2.48  by(induct xs)(auto simp:drop_Cons split:nat.split)
    2.49  
    2.50 +lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
    2.51 +using set_take_subset by fast
    2.52 +
    2.53 +lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
    2.54 +using set_drop_subset by fast
    2.55 +
    2.56  lemma append_eq_conv_conj:
    2.57  "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
    2.58  apply(induct xs)
     3.1 --- a/src/HOL/Map.thy	Thu Sep 11 22:33:12 2003 +0200
     3.2 +++ b/src/HOL/Map.thy	Sun Sep 14 17:53:27 2003 +0200
     3.3 @@ -347,6 +347,24 @@
     3.4  lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
     3.5  by(simp add:map_upds_def)
     3.6  
     3.7 +lemma map_upds_append1[simp]: "\<And>ys m. size xs < size ys \<Longrightarrow>
     3.8 +  m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
     3.9 +apply(induct xs)
    3.10 + apply(clarsimp simp add:neq_Nil_conv)
    3.11 +apply(case_tac ys)
    3.12 + apply simp
    3.13 +apply simp
    3.14 +done
    3.15 +
    3.16 +lemma map_upds_list_update2_drop[simp]:
    3.17 + "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
    3.18 +     \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
    3.19 +apply(induct xs)
    3.20 + apply simp
    3.21 +apply(case_tac ys)
    3.22 + apply simp
    3.23 +apply(simp split:nat.split)
    3.24 +done
    3.25  
    3.26  lemma map_upd_upds_conv_if: "!!x y ys f.
    3.27   (f(x|->y))(xs [|->] ys) =
    3.28 @@ -478,9 +496,15 @@
    3.29  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    3.30  by(simp add:map_le_def)
    3.31  
    3.32 +lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    3.33 +by(force simp add:map_le_def)
    3.34 +
    3.35  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
    3.36  by(fastsimp simp add:map_le_def)
    3.37  
    3.38 +lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    3.39 +by(force simp add:map_le_def)
    3.40 +
    3.41  lemma map_le_upds[simp]:
    3.42   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
    3.43  apply(induct as)
    3.44 @@ -495,11 +519,8 @@
    3.45  lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
    3.46    by (simp add: map_le_def)
    3.47  
    3.48 -lemma map_le_trans: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m h"
    3.49 -  apply (clarsimp simp add: map_le_def)
    3.50 -  apply (drule_tac x="a" in bspec, fastsimp)+
    3.51 -  apply assumption
    3.52 -done
    3.53 +lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
    3.54 +by(force simp add:map_le_def)
    3.55  
    3.56  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
    3.57    apply (unfold map_le_def)