tuned proofs;
authorwenzelm
Sat Nov 11 16:11:42 2006 +0100 (2006-11-11)
changeset 21305d41eddfd2b66
parent 21304 01968a336533
child 21306 7ab6e95e6b0b
tuned proofs;
src/HOL/Library/List_Prefix.thy
     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.81    by (simp add: postfix_def)
    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