summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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