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"