author wenzelm Thu, 08 Nov 2007 20:09:17 +0100 changeset 25355 69c0a39ba028 parent 25354 69560579abf1 child 25356 059c03630d6e
avoid implicit use of prems; tuned proofs;
```--- a/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:08:11 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:09:17 2007 +0100
@@ -162,7 +162,7 @@
apply simp
done

-lemma map_prefixI:
+lemma map_prefixI:
"xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
by (clarsimp simp: prefix_def)

@@ -188,36 +188,33 @@
apply (case_tac ys, simp_all)
done

-lemma not_prefix_cases:
+lemma not_prefix_cases:
assumes pfx: "\<not> ps \<le> ls"
and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R"
and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"
and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"
-  shows "R"
+  shows "R"
proof (cases ps)
-  case Nil thus ?thesis using pfx by simp
+  case Nil then show ?thesis using pfx by simp
next
case (Cons a as)
-
-  hence c: "ps = a#as" .
-
+  then have c: "ps = a#as" .
+
show ?thesis
proof (cases ls)
-    case Nil thus ?thesis
-      by (intro c1, simp add: Cons)
+    case Nil
+    have "ps \<noteq> []" by (simp add: Nil Cons)
+    from this and Nil show ?thesis by (rule c1)
next
case (Cons x xs)
show ?thesis
proof (cases "x = a")
-      case True
-      show ?thesis
-      proof (intro c2)
-     	  show "\<not> as \<le> xs" using pfx c Cons True
-	        by simp
-      qed
-    next
-      case False
-      show ?thesis by (rule c3)
+      case True
+      have "\<not> as \<le> xs" using pfx c Cons True by simp
+      with c Cons True show ?thesis by (rule c2)
+    next
+      case False
+      with c Cons show ?thesis by (rule c3)
qed
qed
qed
@@ -230,17 +227,17 @@
shows "P ps ls"
using np
proof (induct ls arbitrary: ps)
-  case Nil thus ?case
+  case Nil then show ?case
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
next
-  case (Cons y ys)
-  hence npfx: "\<not> ps \<le> (y # ys)" by simp
-  then obtain x xs where pv: "ps = x # xs"
+  case (Cons y ys)
+  then have npfx: "\<not> ps \<le> (y # ys)" by simp
+  then obtain x xs where pv: "ps = x # xs"
by (rule not_prefix_cases) auto

from Cons
have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp
-
+
show ?case using npfx
by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
qed
@@ -305,16 +302,16 @@

lemma parallel_append:
"a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
-  by (rule parallelI)
-     (erule parallelE, erule conjE,
+  by (rule parallelI)
+     (erule parallelE, erule conjE,
induct rule: not_prefix_induct, simp+)+

-lemma parallel_appendI:
+lemma parallel_appendI:
"\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"
by simp (rule parallel_append)

lemma parallel_commute:
-  "(a \<parallel> b) = (b \<parallel> a)"
+  "(a \<parallel> b) = (b \<parallel> a)"
unfolding parallel_def by auto

subsection {* Postfix order on lists *}
@@ -389,7 +386,7 @@
using dx pf by (clarsimp elim!: postfixE)

lemma postfix_map:
-  assumes pf: "xs >>= ys"
+  assumes pf: "xs >>= ys"
shows   "map f xs >>= map f ys"
using pf by (auto elim!: postfixE intro: postfixI)

@@ -402,15 +399,15 @@
"xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
by (clarsimp elim!: postfixE)

-lemma parallelD1:
+lemma parallelD1:
"x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast

-lemma parallelD2:
+lemma parallelD2:
"x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast
-
-lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
+
+lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
unfolding parallel_def by simp
-
+
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
unfolding parallel_def by simp

@@ -418,7 +415,7 @@
"a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto

lemma Cons_parallelI2:
-  "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
+  "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
apply simp
apply (rule parallelI)
apply simp
@@ -432,25 +429,24 @@
and     len: "length xs = length ys"
shows   "xs \<parallel> ys"
using len neq
-proof (induct rule: list_induct2)
-  case 1 thus ?case by simp
+proof (induct rule: list_induct2)
+  case 1 then show ?case by simp
next
case (2 a as b bs)
+  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact

-  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" .
-
show ?case
proof (cases "a = b")
-    case True
-    hence "as \<noteq> bs" using 2 by simp
-
-    thus ?thesis by (rule Cons_parallelI2 [OF True ih])
+    case True
+    then have "as \<noteq> bs" using 2 by simp
+    then show ?thesis by (rule Cons_parallelI2 [OF True ih])
next
case False
-    thus ?thesis by (rule Cons_parallelI1)
+    then show ?thesis by (rule Cons_parallelI1)
qed
qed

+
subsection {* Exeuctable code *}

lemma less_eq_code [code func]:```