1.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Dec 17 16:23:52 2003 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Dec 18 08:20:36 2003 +0100
     1.3 @@ -106,6 +106,9 @@
     1.4    thus ?thesis ..
     1.5  qed
     1.6  
     1.7 +lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
     1.8 +by(simp add:prefix_def) blast
     1.9 +
    1.10  theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
    1.11    by (cases xs) (auto simp add: prefix_def)
    1.12  
    1.13 @@ -130,6 +133,29 @@
    1.14    by (auto simp add: prefix_def)
    1.15  
    1.16  
    1.17 +lemma prefix_same_cases:
    1.18 + "\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
    1.19 +apply(simp add:prefix_def)
    1.20 +apply(erule exE)+
    1.21 +apply(simp add: append_eq_append_conv_if split:if_splits)
    1.22 + apply(rule disjI2)
    1.23 + apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
    1.24 + apply clarify
    1.25 + apply(drule sym)
    1.26 + apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1])
    1.27 + apply simp
    1.28 +apply(rule disjI1)
    1.29 +apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
    1.30 +apply clarify
    1.31 +apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2])
    1.32 +apply simp
    1.33 +done
    1.34 +
    1.35 +lemma set_mono_prefix:
    1.36 + "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.37 +by(fastsimp simp add:prefix_def)
    1.38 +
    1.39 +
    1.40  subsection {* Parallel lists *}
    1.41  
    1.42  constdefs

     2.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Dec 17 16:23:52 2003 +0100
     2.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 18 08:20:36 2003 +0100
     2.3 @@ -68,6 +68,17 @@
     2.4  
     2.5  hide const while_aux
     2.6  
     2.7 +lemma def_while_unfold: assumes fdef: "f == while test do"
     2.8 +      shows "f x = (if test x then f(do x) else x)"
     2.9 +proof -
    2.10 +  have "f x = while test do x" using fdef by simp
    2.11 +  also have "\<dots> = (if test x then while test do (do x) else x)"
    2.12 +    by(rule while_unfold)
    2.13 +  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
    2.14 +  finally show ?thesis .
    2.15 +qed
    2.16 +
    2.17 +
    2.18  text {*
    2.19   The proof rule for @{term while}, where @{term P} is the invariant.
    2.20  *}

     3.1 --- a/src/HOL/List.thy	Wed Dec 17 16:23:52 2003 +0100
     3.2 +++ b/src/HOL/List.thy	Thu Dec 18 08:20:36 2003 +0100
     3.3 @@ -362,6 +362,11 @@
     3.4  by (simp add: tl_append split: list.split)
     3.5  
     3.6  
     3.7 +lemma Cons_eq_append_conv: "x#xs = ys@zs =
     3.8 + (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
     3.9 +by(cases ys) auto
    3.10 +
    3.11 +
    3.12  text {* Trivial rules for solving @{text "@"}-equations automatically. *}
    3.13  
    3.14  lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
    3.15 @@ -902,6 +907,17 @@
    3.16  apply (case_tac i, simp_all) 
    3.17  done
    3.18  
    3.19 +lemma append_eq_append_conv_if:
    3.20 + "!! ys\<^isub>1. (xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
    3.21 +  (if size xs\<^isub>1 \<le> size ys\<^isub>1
    3.22 +   then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
    3.23 +   else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
    3.24 +apply(induct xs\<^isub>1)
    3.25 + apply simp
    3.26 +apply(case_tac ys\<^isub>1)
    3.27 +apply simp_all
    3.28 +done
    3.29 +
    3.30  
    3.31  subsection {* @{text takeWhile} and @{text dropWhile} *}
    3.32  

     4.1 --- a/src/HOL/Map.thy	Wed Dec 17 16:23:52 2003 +0100
     4.2 +++ b/src/HOL/Map.thy	Thu Dec 18 08:20:36 2003 +0100
     4.3 @@ -369,6 +369,23 @@
     4.4   apply(auto simp: map_upd_upds_conv_if)
     4.5  done
     4.6  
     4.7 +lemma fun_upds_append_drop[simp]:
     4.8 +  "!!m ys. size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
     4.9 +apply(induct xs)
    4.10 + apply (simp)
    4.11 +apply(case_tac ys)
    4.12 +apply simp_all
    4.13 +done
    4.14 +
    4.15 +lemma fun_upds_append2_drop[simp]:
    4.16 +  "!!m ys. size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
    4.17 +apply(induct xs)
    4.18 + apply (simp)
    4.19 +apply(case_tac ys)
    4.20 +apply simp_all
    4.21 +done
    4.22 +
    4.23 +
    4.24  lemma restrict_map_upds[simp]: "!!m ys.
    4.25   \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
    4.26   \<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] ys)"