--- 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]: