src/HOL/Library/List_Prefix.thy
 changeset 25665 faabc08af882 parent 25595 6c48275f9c76 child 25692 eda4958ab0d2
```     1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Dec 17 11:11:43 2007 +0100
1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Dec 17 17:01:54 2007 +0100
1.3 @@ -64,33 +64,10 @@
1.4    then obtain zs where zs: "ys @ [y] = xs @ zs" ..
1.5    show "xs = ys @ [y] \<or> xs \<le> ys"
1.6      by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
1.7 -(*
1.8 -  proof (cases zs rule: rev_cases)
1.9 -    assume "zs = []"
1.10 -    with zs have "xs = ys @ [y]" by simp
1.11 -    then show ?thesis ..
1.12 -  next
1.13 -    fix z zs' assume "zs = zs' @ [z]"
1.14 -    with zs have "ys = xs @ zs'" by simp
1.15 -    then have "xs \<le> ys" ..
1.16 -    then show ?thesis ..
1.17 -  qed
1.18 -*)
1.19  next
1.20    assume "xs = ys @ [y] \<or> xs \<le> ys"
1.21    then show "xs \<le> ys @ [y]"
1.22      by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
1.23 -(*
1.24 -  proof
1.25 -    assume "xs = ys @ [y]"
1.26 -    then show ?thesis by simp
1.27 -  next
1.28 -    assume "xs \<le> ys"
1.29 -    then obtain zs where "ys = xs @ zs" ..
1.30 -    then have "ys @ [y] = xs @ (zs @ [y])" by simp
1.31 -    then show ?thesis ..
1.32 -  qed
1.33 -*)
1.34  qed
1.35
1.36  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
1.37 @@ -101,22 +78,10 @@
1.38
1.39  lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
1.40  by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
1.41 -(*
1.42 -proof -
1.43 -  have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
1.44 -  then show ?thesis by simp
1.45 -qed
1.46 -*)
1.47 +
1.48  lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
1.49  by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
1.50 -(*
1.51 -proof -
1.52 -  assume "xs \<le> ys"
1.53 -  then obtain us where "ys = xs @ us" ..
1.54 -  then have "ys @ zs = xs @ (us @ zs)" by simp
1.55 -  then show ?thesis ..
1.56 -qed
1.57 -*)
1.58 +
1.59  lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
1.60    by (auto simp add: prefix_def)
1.61
1.62 @@ -129,54 +94,26 @@
1.63     apply force
1.64    apply (simp del: append_assoc add: append_assoc [symmetric])
1.65    apply (metis append_eq_appendI)
1.66 -(*
1.67 -  apply simp
1.68 -  apply blast
1.69 -*)
1.70    done
1.71
1.72  lemma append_one_prefix:
1.73    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
1.74  by (unfold prefix_def)
1.75     (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj eq_Nil_appendI nth_drop')
1.76 -(*
1.77 -  apply (auto simp add: nth_append)
1.78 -  apply (case_tac zs)
1.79 -   apply auto
1.80 -  done
1.81 -*)
1.82 +
1.83  theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
1.84    by (auto simp add: prefix_def)
1.85
1.86  lemma prefix_same_cases:
1.87    "(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.88  by (unfold prefix_def) (metis append_eq_append_conv2)
1.89 -(*
1.90 -  apply (erule exE)+
1.91 -  apply (simp add: append_eq_append_conv_if split: if_splits)
1.92 -   apply (rule disjI2)
1.93 -   apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
1.94 -   apply clarify
1.95 -   apply (drule sym)
1.96 -   apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1])
1.97 -   apply simp
1.98 -  apply (rule disjI1)
1.99 -  apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
1.100 -  apply clarify
1.101 -  apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2])
1.102 -  apply simp
1.103 -  done
1.104 -*)
1.105 +
1.106  lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
1.107  by (auto simp add: prefix_def)
1.108
1.109  lemma take_is_prefix: "take n xs \<le> xs"
1.110  by (unfold prefix_def) (metis append_take_drop_id)
1.111 -(*
1.112 -  apply (rule_tac x="drop n xs" in exI)
1.113 -  apply simp
1.114 -  done
1.115 -*)
1.116 +
1.117  lemma map_prefixI:
1.118    "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
1.119  by (clarsimp simp: prefix_def)
1.120 @@ -184,12 +121,7 @@
1.121  lemma prefix_length_less:
1.122    "xs < ys \<Longrightarrow> length xs < length ys"
1.123  by (clarsimp simp: strict_prefix_def prefix_def)
1.124 -(*
1.125 -  apply (frule prefix_length_le)
1.126 -  apply (rule ccontr, simp)
1.127 -  apply (clarsimp simp: prefix_def)
1.128 -  done
1.129 -*)
1.130 +
1.131  lemma strict_prefix_simps [simp]:
1.132    "xs < [] = False"
1.133    "[] < (x # xs) = True"
1.134 @@ -200,10 +132,6 @@
1.135  apply (induct n arbitrary: xs ys)
1.136   apply (case_tac ys, simp_all)[1]
1.137  apply (metis order_less_trans strict_prefixI take_is_prefix)
1.138 -(*
1.139 -  apply (case_tac xs, simp)
1.140 -  apply (case_tac ys, simp_all)
1.141 -*)
1.142  done
1.143
1.144  lemma not_prefix_cases:
1.145 @@ -220,10 +148,6 @@
1.146    show ?thesis
1.147    proof (cases ls)
1.148      case Nil thus ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
1.149 -(*
1.150 -    have "ps \<noteq> []" by (simp add: Nil Cons)
1.151 -    from this and Nil show ?thesis by (rule c1)
1.152 -*)
1.153    next
1.154      case (Cons x xs)
1.155      show ?thesis
1.156 @@ -253,13 +177,6 @@
1.157    then obtain x xs where pv: "ps = x # xs"
1.158      by (rule not_prefix_cases) auto
1.159    show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)
1.160 -(*
1.161 -  from Cons
1.162 -  have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp
1.163 -
1.164 -  show ?case using npfx
1.165 -    by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
1.166 -*)
1.167  qed
1.168
1.169
1.170 @@ -297,23 +214,10 @@
1.171      proof (cases ys')
1.172        assume "ys' = []"
1.173        thus ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
1.174 -(*
1.175 -      with ys have "xs = ys" by simp
1.176 -      with snoc have "[x] \<parallel> []" by auto
1.177 -      then have False by blast
1.178 -      then show ?thesis ..
1.179 -*)
1.180      next
1.181        fix c cs assume ys': "ys' = c # cs"
1.182        thus ?thesis
1.183  	by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI same_prefix_prefix snoc.prems ys)
1.184 -(*
1.185 -      with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
1.186 -      then have "x \<noteq> c" by auto
1.187 -      moreover have "xs @ [x] = xs @ x # []" by simp
1.188 -      moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
1.189 -      ultimately show ?thesis by blast
1.190 -*)
1.191      qed
1.192    next
1.193      assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
1.194 @@ -436,15 +340,7 @@
1.195
1.196  lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
1.197  by (metis Cons_prefix_Cons parallelE parallelI)
1.198 -(*
1.199 -  apply simp
1.200 -  apply (rule parallelI)
1.201 -   apply simp
1.202 -   apply (erule parallelD1)
1.203 -  apply simp
1.204 -  apply (erule parallelD2)
1.205 - done
1.206 -*)
1.207 +
1.208  lemma not_equal_is_parallel:
1.209    assumes neq: "xs \<noteq> ys"
1.210      and len: "length xs = length ys"
```