# HG changeset patch
# User nipkow
# Date 1071732036 -3600
# Node ID bf8b8c9425c3e5591c5913b9d08fa124bc9b1aba
# Parent  0b5c0b0a3eba92732ad25499d9cb127198091f92
*** empty log message ***

diff -r 0b5c0b0a3eba -r bf8b8c9425c3 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Wed Dec 17 16:23:52 2003 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Dec 18 08:20:36 2003 +0100
@@ -106,6 +106,9 @@
   thus ?thesis ..
 qed
 
+lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
+by(simp add:prefix_def) blast
+
 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   by (cases xs) (auto simp add: prefix_def)
 
@@ -130,6 +133,29 @@
   by (auto simp add: prefix_def)
 
 
+lemma prefix_same_cases:
+ "\<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"
+apply(simp add:prefix_def)
+apply(erule exE)+
+apply(simp add: append_eq_append_conv_if split:if_splits)
+ apply(rule disjI2)
+ apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
+ apply clarify
+ apply(drule sym)
+ apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1])
+ apply simp
+apply(rule disjI1)
+apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
+apply clarify
+apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2])
+apply simp
+done
+
+lemma set_mono_prefix:
+ "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
+by(fastsimp simp add:prefix_def)
+
+
 subsection {* Parallel lists *}
 
 constdefs
diff -r 0b5c0b0a3eba -r bf8b8c9425c3 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Dec 17 16:23:52 2003 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 18 08:20:36 2003 +0100
@@ -68,6 +68,17 @@
 
 hide const while_aux
 
+lemma def_while_unfold: assumes fdef: "f == while test do"
+      shows "f x = (if test x then f(do x) else x)"
+proof -
+  have "f x = while test do x" using fdef by simp
+  also have "\<dots> = (if test x then while test do (do x) else x)"
+    by(rule while_unfold)
+  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
+  finally show ?thesis .
+qed
+
+
 text {*
  The proof rule for @{term while}, where @{term P} is the invariant.
 *}
diff -r 0b5c0b0a3eba -r bf8b8c9425c3 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 17 16:23:52 2003 +0100
+++ b/src/HOL/List.thy	Thu Dec 18 08:20:36 2003 +0100
@@ -362,6 +362,11 @@
 by (simp add: tl_append split: list.split)
 
 
+lemma Cons_eq_append_conv: "x#xs = ys@zs =
+ (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
+by(cases ys) auto
+
+
 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
 
 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
@@ -902,6 +907,17 @@
 apply (case_tac i, simp_all) 
 done
 
+lemma append_eq_append_conv_if:
+ "!! ys\<^isub>1. (xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
+  (if size xs\<^isub>1 \<le> size ys\<^isub>1
+   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
+   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)"
+apply(induct xs\<^isub>1)
+ apply simp
+apply(case_tac ys\<^isub>1)
+apply simp_all
+done
+
 
 subsection {* @{text takeWhile} and @{text dropWhile} *}
 
diff -r 0b5c0b0a3eba -r bf8b8c9425c3 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Dec 17 16:23:52 2003 +0100
+++ b/src/HOL/Map.thy	Thu Dec 18 08:20:36 2003 +0100
@@ -369,6 +369,23 @@
  apply(auto simp: map_upd_upds_conv_if)
 done
 
+lemma fun_upds_append_drop[simp]:
+  "!!m ys. size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
+apply(induct xs)
+ apply (simp)
+apply(case_tac ys)
+apply simp_all
+done
+
+lemma fun_upds_append2_drop[simp]:
+  "!!m ys. size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
+apply(induct xs)
+ apply (simp)
+apply(case_tac ys)
+apply simp_all
+done
+
+
 lemma restrict_map_upds[simp]: "!!m ys.
  \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
  \<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] ys)"