tuned proofs, document;
authorwenzelm
Tue Dec 18 16:26:46 2007 +0100 (2007-12-18)
changeset 25692eda4958ab0d2
parent 25691 8f8d83af100a
child 25693 31232fe5a6ad
tuned proofs, document;
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Tue Dec 18 14:37:00 2007 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Tue Dec 18 16:26:46 2007 +0100
     1.3 @@ -77,10 +77,10 @@
     1.4    by (induct xs) simp_all
     1.5  
     1.6  lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
     1.7 -by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
     1.8 +  by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
     1.9  
    1.10  lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
    1.11 -by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
    1.12 +  by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
    1.13  
    1.14  lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
    1.15    by (auto simp add: prefix_def)
    1.16 @@ -98,41 +98,40 @@
    1.17  
    1.18  lemma append_one_prefix:
    1.19    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
    1.20 -by (unfold prefix_def)
    1.21 -   (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj eq_Nil_appendI nth_drop')
    1.22 +  unfolding prefix_def
    1.23 +  by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
    1.24 +    eq_Nil_appendI nth_drop')
    1.25  
    1.26  theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
    1.27    by (auto simp add: prefix_def)
    1.28  
    1.29  lemma prefix_same_cases:
    1.30    "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
    1.31 -by (unfold prefix_def) (metis append_eq_append_conv2)
    1.32 +  unfolding prefix_def by (metis append_eq_append_conv2)
    1.33  
    1.34  lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.35 -by (auto simp add: prefix_def)
    1.36 +  by (auto simp add: prefix_def)
    1.37  
    1.38  lemma take_is_prefix: "take n xs \<le> xs"
    1.39 -by (unfold prefix_def) (metis append_take_drop_id)
    1.40 +  unfolding prefix_def by (metis append_take_drop_id)
    1.41  
    1.42 -lemma map_prefixI:
    1.43 -  "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
    1.44 -by (clarsimp simp: prefix_def)
    1.45 +lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
    1.46 +  by (auto simp: prefix_def)
    1.47  
    1.48 -lemma prefix_length_less:
    1.49 -  "xs < ys \<Longrightarrow> length xs < length ys"
    1.50 -by (clarsimp simp: strict_prefix_def prefix_def)
    1.51 +lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
    1.52 +  by (auto simp: strict_prefix_def prefix_def)
    1.53  
    1.54  lemma strict_prefix_simps [simp]:
    1.55 -  "xs < [] = False"
    1.56 -  "[] < (x # xs) = True"
    1.57 -  "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
    1.58 -by (simp_all add: strict_prefix_def cong: conj_cong)
    1.59 +    "xs < [] = False"
    1.60 +    "[] < (x # xs) = True"
    1.61 +    "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
    1.62 +  by (simp_all add: strict_prefix_def cong: conj_cong)
    1.63  
    1.64  lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
    1.65 -apply (induct n arbitrary: xs ys)
    1.66 - apply (case_tac ys, simp_all)[1]
    1.67 -apply (metis order_less_trans strict_prefixI take_is_prefix)
    1.68 -done
    1.69 +  apply (induct n arbitrary: xs ys)
    1.70 +   apply (case_tac ys, simp_all)[1]
    1.71 +  apply (metis order_less_trans strict_prefixI take_is_prefix)
    1.72 +  done
    1.73  
    1.74  lemma not_prefix_cases:
    1.75    assumes pfx: "\<not> ps \<le> ls"
    1.76 @@ -141,13 +140,13 @@
    1.77    | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"
    1.78    | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
    1.79  proof (cases ps)
    1.80 -  case Nil thus ?thesis using pfx by simp
    1.81 +  case Nil then show ?thesis using pfx by simp
    1.82  next
    1.83    case (Cons a as)
    1.84 -  hence c: "ps = a#as" .
    1.85 +  note c = `ps = a#as`
    1.86    show ?thesis
    1.87    proof (cases ls)
    1.88 -    case Nil thus ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
    1.89 +    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
    1.90    next
    1.91      case (Cons x xs)
    1.92      show ?thesis
    1.93 @@ -187,16 +186,16 @@
    1.94    "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
    1.95  
    1.96  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
    1.97 -unfolding parallel_def by blast
    1.98 +  unfolding parallel_def by blast
    1.99  
   1.100  lemma parallelE [elim]:
   1.101 -assumes "xs \<parallel> ys"
   1.102 -obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   1.103 -using assms unfolding parallel_def by blast
   1.104 +  assumes "xs \<parallel> ys"
   1.105 +  obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   1.106 +  using assms unfolding parallel_def by blast
   1.107  
   1.108  theorem prefix_cases:
   1.109 -obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
   1.110 -unfolding parallel_def strict_prefix_def by blast
   1.111 +  obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
   1.112 +  unfolding parallel_def strict_prefix_def by blast
   1.113  
   1.114  theorem parallel_decomp:
   1.115    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
   1.116 @@ -213,11 +212,12 @@
   1.117      show ?thesis
   1.118      proof (cases ys')
   1.119        assume "ys' = []"
   1.120 -      thus ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
   1.121 +      then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
   1.122      next
   1.123        fix c cs assume ys': "ys' = c # cs"
   1.124 -      thus ?thesis
   1.125 -	by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI same_prefix_prefix snoc.prems ys)
   1.126 +      then show ?thesis
   1.127 +        by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI
   1.128 +          same_prefix_prefix snoc.prems ys)
   1.129      qed
   1.130    next
   1.131      assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
   1.132 @@ -234,15 +234,16 @@
   1.133  qed
   1.134  
   1.135  lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
   1.136 -by (rule parallelI)
   1.137 -   (erule parallelE, erule conjE,
   1.138 -          induct rule: not_prefix_induct, simp+)+
   1.139 +  apply (rule parallelI)
   1.140 +    apply (erule parallelE, erule conjE,
   1.141 +      induct rule: not_prefix_induct, simp+)+
   1.142 +  done
   1.143  
   1.144 -lemma parallel_appendI: "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"
   1.145 -by simp (rule parallel_append)
   1.146 +lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
   1.147 +  by (simp add: parallel_append)
   1.148  
   1.149 -lemma parallel_commute: "(a \<parallel> b) = (b \<parallel> a)"
   1.150 -unfolding parallel_def by auto
   1.151 +lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
   1.152 +  unfolding parallel_def by auto
   1.153  
   1.154  
   1.155  subsection {* Postfix order on lists *}
   1.156 @@ -252,12 +253,12 @@
   1.157    "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
   1.158  
   1.159  lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"
   1.160 -unfolding postfix_def by blast
   1.161 +  unfolding postfix_def by blast
   1.162  
   1.163  lemma postfixE [elim?]:
   1.164 -assumes "xs >>= ys"
   1.165 -obtains zs where "xs = zs @ ys"
   1.166 -using assms unfolding postfix_def by blast
   1.167 +  assumes "xs >>= ys"
   1.168 +  obtains zs where "xs = zs @ ys"
   1.169 +  using assms unfolding postfix_def by blast
   1.170  
   1.171  lemma postfix_refl [iff]: "xs >>= xs"
   1.172    by (auto simp add: postfix_def)
   1.173 @@ -311,35 +312,37 @@
   1.174  qed
   1.175  
   1.176  lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys"
   1.177 -by (clarsimp elim!: postfixE)
   1.178 +  by (clarsimp elim!: postfixE)
   1.179  
   1.180  lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys"
   1.181 -by (auto elim!: postfixE intro: postfixI)
   1.182 +  by (auto elim!: postfixE intro: postfixI)
   1.183  
   1.184  lemma postfix_drop: "as >>= drop n as"
   1.185 -unfolding postfix_def
   1.186 -by (rule exI [where x = "take n as"]) simp
   1.187 +  unfolding postfix_def
   1.188 +  apply (rule exI [where x = "take n as"])
   1.189 +  apply simp
   1.190 +  done
   1.191  
   1.192  lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
   1.193 -by (clarsimp elim!: postfixE)
   1.194 +  by (clarsimp elim!: postfixE)
   1.195  
   1.196  lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
   1.197 -by blast
   1.198 +  by blast
   1.199  
   1.200  lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"
   1.201 -by blast
   1.202 +  by blast
   1.203  
   1.204  lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
   1.205 -unfolding parallel_def by simp
   1.206 +  unfolding parallel_def by simp
   1.207  
   1.208  lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
   1.209 -unfolding parallel_def by simp
   1.210 +  unfolding parallel_def by simp
   1.211  
   1.212  lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
   1.213 -by auto
   1.214 +  by auto
   1.215  
   1.216  lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
   1.217 -by (metis Cons_prefix_Cons parallelE parallelI)
   1.218 +  by (metis Cons_prefix_Cons parallelE parallelI)
   1.219  
   1.220  lemma not_equal_is_parallel:
   1.221    assumes neq: "xs \<noteq> ys"