author wenzelm Sat Nov 11 16:11:42 2006 +0100 (2006-11-11) changeset 21305 d41eddfd2b66 parent 21304 01968a336533 child 21306 7ab6e95e6b0b
tuned proofs;
```     1.1 --- a/src/HOL/Library/List_Prefix.thy	Sat Nov 11 16:11:41 2006 +0100
1.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Nov 11 16:11:42 2006 +0100
1.3 @@ -23,28 +23,31 @@
1.4  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
1.5    unfolding prefix_def by blast
1.6
1.7 -lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
1.8 -  unfolding prefix_def by blast
1.9 +lemma prefixE [elim?]:
1.10 +  assumes "xs \<le> ys"
1.11 +  obtains zs where "ys = xs @ zs"
1.12 +  using prems unfolding prefix_def by blast
1.13
1.14  lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
1.15    unfolding strict_prefix_def prefix_def by blast
1.16
1.17  lemma strict_prefixE' [elim?]:
1.18 -  assumes lt: "xs < ys"
1.19 -    and r: "!!z zs. ys = xs @ z # zs ==> C"
1.20 -  shows C
1.21 +  assumes "xs < ys"
1.22 +  obtains z zs where "ys = xs @ z # zs"
1.23  proof -
1.24 -  from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
1.25 +  from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
1.26      unfolding strict_prefix_def prefix_def by blast
1.27 -  with r show ?thesis by (auto simp add: neq_Nil_conv)
1.28 +  with that show ?thesis by (auto simp add: neq_Nil_conv)
1.29  qed
1.30
1.31  lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
1.32    unfolding strict_prefix_def by blast
1.33
1.34  lemma strict_prefixE [elim?]:
1.35 -    "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
1.36 -  unfolding strict_prefix_def by blast
1.37 +  fixes xs ys :: "'a list"
1.38 +  assumes "xs < ys"
1.39 +  obtains "xs \<le> ys" and "xs \<noteq> ys"
1.40 +  using prems unfolding strict_prefix_def by blast
1.41
1.42
1.43  subsection {* Basic properties of prefixes *}
1.44 @@ -163,13 +166,12 @@
1.45    unfolding parallel_def by blast
1.46
1.47  lemma parallelE [elim]:
1.48 -    "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
1.49 -  unfolding parallel_def by blast
1.50 +  assumes "xs \<parallel> ys"
1.51 +  obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
1.52 +  using prems unfolding parallel_def by blast
1.53
1.54  theorem prefix_cases:
1.55 -  "(xs \<le> ys ==> C) ==>
1.56 -    (ys < xs ==> C) ==>
1.57 -    (xs \<parallel> ys ==> C) ==> C"
1.58 +  obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
1.59    unfolding parallel_def strict_prefix_def by blast
1.60
1.61  theorem parallel_decomp:
1.62 @@ -219,7 +221,15 @@
1.63    postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
1.64    "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
1.65
1.66 -lemma postfix_refl [simp, intro!]: "xs >>= xs"
1.67 +lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"
1.68 +  unfolding postfix_def by blast
1.69 +
1.70 +lemma postfixE [elim?]:
1.71 +  assumes "xs >>= ys"
1.72 +  obtains zs where "xs = zs @ ys"
1.73 +  using prems unfolding postfix_def by blast
1.74 +
1.75 +lemma postfix_refl [iff]: "xs >>= xs"
1.76    by (auto simp add: postfix_def)
1.77  lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"
1.78    by (auto simp add: postfix_def)
1.79 @@ -229,7 +239,7 @@
1.80  lemma Nil_postfix [iff]: "xs >>= []"
1.82  lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"
1.83 -  by (auto simp add:postfix_def)
1.84 +  by (auto simp add: postfix_def)
1.85
1.86  lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"
1.87    by (auto simp add: postfix_def)
1.88 @@ -239,23 +249,35 @@
1.89  lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
1.90    by (auto simp add: postfix_def)
1.91  lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"
1.92 -  by(auto simp add: postfix_def)
1.93 +  by (auto simp add: postfix_def)
1.94
1.95 -lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
1.96 -  by (induct zs) auto
1.97 -lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs"
1.98 -  by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
1.99 +lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs"
1.100 +proof -
1.101 +  assume "xs >>= ys"
1.102 +  then obtain zs where "xs = zs @ ys" ..
1.103 +  then show ?thesis by (induct zs) auto
1.104 +qed
1.105
1.106 -lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys"
1.107 -  by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
1.108 -lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys"
1.109 -  by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
1.110 +lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys"
1.111 +proof -
1.112 +  assume "x#xs >>= y#ys"
1.113 +  then obtain zs where "x#xs = zs @ y#ys" ..
1.114 +  then show ?thesis
1.115 +    by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
1.116 +qed
1.117
1.118 -lemma postfix2prefix: "(xs >>= ys) = (rev ys <= rev xs)"
1.119 -  apply (unfold prefix_def postfix_def, safe)
1.120 -   apply (rule_tac x = "rev zs" in exI, simp)
1.121 -  apply (rule_tac x = "rev zs" in exI)
1.122 -  apply (rule rev_is_rev_conv [THEN iffD1], simp)
1.123 -  done
1.124 +lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
1.125 +proof
1.126 +  assume "xs >>= ys"
1.127 +  then obtain zs where "xs = zs @ ys" ..
1.128 +  then have "rev xs = rev ys @ rev zs" by simp
1.129 +  then show "rev ys <= rev xs" ..
1.130 +next
1.131 +  assume "rev ys <= rev xs"
1.132 +  then obtain zs where "rev xs = rev ys @ zs" ..
1.133 +  then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp
1.134 +  then have "xs = rev zs @ ys" by simp
1.135 +  then show "xs >>= ys" ..
1.136 +qed
1.137
1.138  end
```