src/HOL/Library/Sublist.thy
changeset 49107 ec34e9df0514
parent 49087 7a17ba4bc997
child 50516 ed6b40d15d1c
     1.1 --- a/src/HOL/Library/Sublist.thy	Mon Sep 03 22:51:33 2012 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Mon Sep 03 23:03:54 2012 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  
     1.5  subsection {* Prefix order on lists *}
     1.6  
     1.7 -definition prefixeq :: "'a list => 'a list => bool" where
     1.8 -  "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
     1.9 +definition prefixeq :: "'a list => 'a list => bool"
    1.10 +  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.11  
    1.12 -definition prefix :: "'a list => 'a list => bool" where
    1.13 -  "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    1.14 +definition prefix :: "'a list => 'a list => bool"
    1.15 +  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    1.16  
    1.17  interpretation prefix_order: order prefixeq prefix
    1.18    by default (auto simp: prefixeq_def prefix_def)
    1.19 @@ -149,7 +149,8 @@
    1.20    | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
    1.21    | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
    1.22  proof (cases ps)
    1.23 -  case Nil then show ?thesis using pfx by simp
    1.24 +  case Nil
    1.25 +  then show ?thesis using pfx by simp
    1.26  next
    1.27    case (Cons a as)
    1.28    note c = `ps = a#as`
    1.29 @@ -190,9 +191,8 @@
    1.30  
    1.31  subsection {* Parallel lists *}
    1.32  
    1.33 -definition
    1.34 -  parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50) where
    1.35 -  "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
    1.36 +definition parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50)
    1.37 +  where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
    1.38  
    1.39  lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
    1.40    unfolding parallel_def by blast
    1.41 @@ -229,7 +229,8 @@
    1.42            same_prefixeq_prefixeq snoc.prems ys)
    1.43      qed
    1.44    next
    1.45 -    assume "prefix ys xs" then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)
    1.46 +    assume "prefix ys xs"
    1.47 +    then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)
    1.48      with snoc have False by blast
    1.49      then show ?thesis ..
    1.50    next
    1.51 @@ -257,12 +258,11 @@
    1.52  
    1.53  subsection {* Suffix order on lists *}
    1.54  
    1.55 -definition
    1.56 -  suffixeq :: "'a list => 'a list => bool" where
    1.57 -  "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
    1.58 +definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.59 +  where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
    1.60  
    1.61 -definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.62 -  "suffix xs ys \<equiv> \<exists>us. ys = us @ xs \<and> us \<noteq> []"
    1.63 +definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.64 +  where "suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"
    1.65  
    1.66  lemma suffix_imp_suffixeq:
    1.67    "suffix xs ys \<Longrightarrow> suffixeq xs ys"
    1.68 @@ -297,9 +297,9 @@
    1.69  lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"
    1.70    by (auto simp add: suffixeq_def)
    1.71  
    1.72 -lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y#ys)"
    1.73 +lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y # ys)"
    1.74    by (auto simp add: suffixeq_def)
    1.75 -lemma suffixeq_ConsD: "suffixeq (x#xs) ys \<Longrightarrow> suffixeq xs ys"
    1.76 +lemma suffixeq_ConsD: "suffixeq (x # xs) ys \<Longrightarrow> suffixeq xs ys"
    1.77    by (auto simp add: suffixeq_def)
    1.78  
    1.79  lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)"
    1.80 @@ -313,10 +313,10 @@
    1.81  lemma suffixeq_set_subset:
    1.82    "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def)
    1.83  
    1.84 -lemma suffixeq_ConsD2: "suffixeq (x#xs) (y#ys) ==> suffixeq xs ys"
    1.85 +lemma suffixeq_ConsD2: "suffixeq (x # xs) (y # ys) \<Longrightarrow> suffixeq xs ys"
    1.86  proof -
    1.87 -  assume "suffixeq (x#xs) (y#ys)"
    1.88 -  then obtain zs where "y#ys = zs @ x#xs" ..
    1.89 +  assume "suffixeq (x # xs) (y # ys)"
    1.90 +  then obtain zs where "y # ys = zs @ x # xs" ..
    1.91    then show ?thesis
    1.92      by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
    1.93  qed
    1.94 @@ -348,26 +348,28 @@
    1.95    done
    1.96  
    1.97  lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
    1.98 -  by (clarsimp elim!: suffixeqE)
    1.99 +  by (auto elim!: suffixeqE)
   1.100  
   1.101 -lemma suffixeq_suffix_reflclp_conv:
   1.102 -  "suffixeq = suffix\<^sup>=\<^sup>="
   1.103 +lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>="
   1.104  proof (intro ext iffI)
   1.105    fix xs ys :: "'a list"
   1.106    assume "suffixeq xs ys"
   1.107    show "suffix\<^sup>=\<^sup>= xs ys"
   1.108    proof
   1.109      assume "xs \<noteq> ys"
   1.110 -    with `suffixeq xs ys` show "suffix xs ys" by (auto simp: suffixeq_def suffix_def)
   1.111 +    with `suffixeq xs ys` show "suffix xs ys"
   1.112 +      by (auto simp: suffixeq_def suffix_def)
   1.113    qed
   1.114  next
   1.115    fix xs ys :: "'a list"
   1.116    assume "suffix\<^sup>=\<^sup>= xs ys"
   1.117 -  thus "suffixeq xs ys"
   1.118 +  then show "suffixeq xs ys"
   1.119    proof
   1.120 -    assume "suffix xs ys" thus "suffixeq xs ys" by (rule suffix_imp_suffixeq)
   1.121 +    assume "suffix xs ys" then show "suffixeq xs ys"
   1.122 +      by (rule suffix_imp_suffixeq)
   1.123    next
   1.124 -    assume "xs = ys" thus "suffixeq xs ys" by (auto simp: suffixeq_def)
   1.125 +    assume "xs = ys" then show "suffixeq xs ys"
   1.126 +      by (auto simp: suffixeq_def)
   1.127    qed
   1.128  qed
   1.129  
   1.130 @@ -411,19 +413,16 @@
   1.131    qed
   1.132  qed
   1.133  
   1.134 -lemma suffix_reflclp_conv:
   1.135 -  "suffix\<^sup>=\<^sup>= = suffixeq"
   1.136 +lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"
   1.137    by (intro ext) (auto simp: suffixeq_def suffix_def)
   1.138  
   1.139 -lemma suffix_lists:
   1.140 -  "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
   1.141 +lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
   1.142    unfolding suffix_def by auto
   1.143  
   1.144  
   1.145  subsection {* Embedding on lists *}
   1.146  
   1.147 -inductive
   1.148 -  emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.149 +inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.150    for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
   1.151  where
   1.152    emb_Nil [intro, simp]: "emb P [] ys"
   1.153 @@ -434,19 +433,17 @@
   1.154    assumes "emb P xs []" shows "xs = []"
   1.155    using assms by (cases rule: emb.cases) auto
   1.156  
   1.157 -lemma emb_Cons_Nil [simp]:
   1.158 -  "emb P (x#xs) [] = False"
   1.159 +lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False"
   1.160  proof -
   1.161    { assume "emb P (x#xs) []"
   1.162      from emb_Nil2 [OF this] have False by simp
   1.163    } moreover {
   1.164      assume False
   1.165 -    hence "emb P (x#xs) []" by simp
   1.166 +    then have "emb P (x#xs) []" by simp
   1.167    } ultimately show ?thesis by blast
   1.168  qed
   1.169  
   1.170 -lemma emb_append2 [intro]:
   1.171 -  "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
   1.172 +lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
   1.173    by (induct zs) auto
   1.174  
   1.175  lemma emb_prefix [intro]:
   1.176 @@ -458,11 +455,12 @@
   1.177    assumes "emb P (x#xs) ys"
   1.178    shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
   1.179  using assms
   1.180 -proof (induct x\<equiv>"x#xs" y\<equiv>"ys" arbitrary: x xs ys)
   1.181 -  case emb_Cons thus ?case by (metis append_Cons)
   1.182 +proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
   1.183 +  case emb_Cons
   1.184 +  then show ?case by (metis append_Cons)
   1.185  next
   1.186    case (emb_Cons2 x y xs ys)
   1.187 -  thus ?case by (cases xs) (auto, blast+)
   1.188 +  then show ?case by (cases xs) (auto, blast+)
   1.189  qed
   1.190  
   1.191  lemma emb_appendD:
   1.192 @@ -470,7 +468,7 @@
   1.193    shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
   1.194  using assms
   1.195  proof (induction xs arbitrary: ys zs)
   1.196 -  case Nil thus ?case by auto
   1.197 +  case Nil then show ?case by auto
   1.198  next
   1.199    case (Cons x xs)
   1.200    then obtain us v vs where "zs = us @ v # vs"
   1.201 @@ -492,8 +490,8 @@
   1.202    by (induct rule: emb.induct) auto
   1.203  
   1.204  (*FIXME: move*)
   1.205 -definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.206 -  "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c"
   1.207 +definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   1.208 +  where "transp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c)"
   1.209  lemma transp_onI [Pure.intro]:
   1.210    "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"
   1.211    unfolding transp_on_def by blast
   1.212 @@ -505,15 +503,15 @@
   1.213    fix xs ys zs
   1.214    assume "emb P xs ys" and "emb P ys zs"
   1.215      and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
   1.216 -  thus "emb P xs zs"
   1.217 +  then show "emb P xs zs"
   1.218    proof (induction arbitrary: zs)
   1.219      case emb_Nil show ?case by blast
   1.220    next
   1.221      case (emb_Cons xs ys y)
   1.222      from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
   1.223        where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
   1.224 -    hence "emb P ys (v#vs)" by blast
   1.225 -    hence "emb P ys zs" unfolding zs by (rule emb_append2)
   1.226 +    then have "emb P ys (v#vs)" by blast
   1.227 +    then have "emb P ys zs" unfolding zs by (rule emb_append2)
   1.228      from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
   1.229    next
   1.230      case (emb_Cons2 x y xs ys)
   1.231 @@ -528,15 +526,15 @@
   1.232          unfolding transp_on_def by blast
   1.233      qed
   1.234      ultimately have "emb P (x#xs) (v#vs)" by blast
   1.235 -    thus ?case unfolding zs by (rule emb_append2)
   1.236 +    then show ?case unfolding zs by (rule emb_append2)
   1.237    qed
   1.238  qed
   1.239  
   1.240  
   1.241  subsection {* Sublists (special case of embedding) *}
   1.242  
   1.243 -abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.244 -  "sub xs ys \<equiv> emb (op =) xs ys"
   1.245 +abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.246 +  where "sub xs ys \<equiv> emb (op =) xs ys"
   1.247  
   1.248  lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
   1.249  
   1.250 @@ -581,9 +579,11 @@
   1.251    case emb_Nil
   1.252    from emb_Nil2 [OF this] show ?case by simp
   1.253  next
   1.254 -  case emb_Cons2 thus ?case by simp
   1.255 +  case emb_Cons2
   1.256 +  then show ?case by simp
   1.257  next
   1.258 -  case emb_Cons thus ?case
   1.259 +  case emb_Cons
   1.260 +  then show ?case
   1.261      by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
   1.262  qed
   1.263  
   1.264 @@ -601,10 +601,11 @@
   1.265  
   1.266  lemma emb_append_mono:
   1.267    "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')"
   1.268 -apply (induct rule: emb.induct)
   1.269 -  apply (metis eq_Nil_appendI emb_append2)
   1.270 - apply (metis append_Cons emb_Cons)
   1.271 -by (metis append_Cons emb_Cons2)
   1.272 +  apply (induct rule: emb.induct)
   1.273 +    apply (metis eq_Nil_appendI emb_append2)
   1.274 +   apply (metis append_Cons emb_Cons)
   1.275 +  apply (metis append_Cons emb_Cons2)
   1.276 +  done
   1.277  
   1.278  
   1.279  subsection {* Appending elements *}
   1.280 @@ -613,29 +614,29 @@
   1.281    "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
   1.282  proof
   1.283    { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
   1.284 -    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
   1.285 +    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
   1.286      proof (induct arbitrary: xs ys zs)
   1.287        case emb_Nil show ?case by simp
   1.288      next
   1.289        case (emb_Cons xs' ys' x)
   1.290 -      { assume "ys=[]" hence ?case using emb_Cons(1) by auto }
   1.291 +      { assume "ys=[]" then have ?case using emb_Cons(1) by auto }
   1.292        moreover
   1.293        { fix us assume "ys = x#us"
   1.294 -        hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
   1.295 +        then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
   1.296        ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.297      next
   1.298        case (emb_Cons2 x y xs' ys')
   1.299 -      { assume "xs=[]" hence ?case using emb_Cons2(1) by auto }
   1.300 +      { assume "xs=[]" then have ?case using emb_Cons2(1) by auto }
   1.301        moreover
   1.302 -      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto}
   1.303 +      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto}
   1.304        moreover
   1.305 -      { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp }
   1.306 +      { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp }
   1.307        ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
   1.308      qed }
   1.309    moreover assume ?l
   1.310    ultimately show ?r by blast
   1.311  next
   1.312 -  assume ?r thus ?l by (metis emb_append_mono sub_refl)
   1.313 +  assume ?r then show ?l by (metis emb_append_mono sub_refl)
   1.314  qed
   1.315  
   1.316  lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
   1.317 @@ -658,33 +659,33 @@
   1.318    assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
   1.319    using assms by (induct) auto
   1.320  
   1.321 -lemma "sub xs ys \<longleftrightarrow> (\<exists> N. xs = sublist ys N)" (is "?L = ?R")
   1.322 +lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
   1.323  proof
   1.324    assume ?L
   1.325 -  thus ?R
   1.326 +  then show ?R
   1.327    proof (induct)
   1.328      case emb_Nil show ?case by (metis sublist_empty)
   1.329    next
   1.330      case (emb_Cons xs ys x)
   1.331      then obtain N where "xs = sublist ys N" by blast
   1.332 -    hence "xs = sublist (x#ys) (Suc ` N)"
   1.333 +    then have "xs = sublist (x#ys) (Suc ` N)"
   1.334        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.335 -    thus ?case by blast
   1.336 +    then show ?case by blast
   1.337    next
   1.338      case (emb_Cons2 x y xs ys)
   1.339      then obtain N where "xs = sublist ys N" by blast
   1.340 -    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.341 +    then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.342        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.343 -    thus ?case unfolding `x = y` by blast
   1.344 +    then show ?case unfolding `x = y` by blast
   1.345    qed
   1.346  next
   1.347    assume ?R
   1.348    then obtain N where "xs = sublist ys N" ..
   1.349    moreover have "sub (sublist ys N) ys"
   1.350 -  proof (induct ys arbitrary:N)
   1.351 +  proof (induct ys arbitrary: N)
   1.352      case Nil show ?case by simp
   1.353    next
   1.354 -    case Cons thus ?case by (auto simp: sublist_Cons)
   1.355 +    case Cons then show ?case by (auto simp: sublist_Cons)
   1.356    qed
   1.357    ultimately show ?L by simp
   1.358  qed