# HG changeset patch
# User nipkow
# Date 1197907314 -3600
# Node ID faabc08af8822004049b8999e0a78577cf412da8
# Parent  156660ab8a39c8063191acd3541e6e701fe9b7c0
removed legacy proofs

diff -r 156660ab8a39 -r faabc08af882 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Mon Dec 17 11:11:43 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Mon Dec 17 17:01:54 2007 +0100
@@ -64,33 +64,10 @@
   then obtain zs where zs: "ys @ [y] = xs @ zs" ..
   show "xs = ys @ [y] \<or> xs \<le> ys"
     by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
-(*
-  proof (cases zs rule: rev_cases)
-    assume "zs = []"
-    with zs have "xs = ys @ [y]" by simp
-    then show ?thesis ..
-  next
-    fix z zs' assume "zs = zs' @ [z]"
-    with zs have "ys = xs @ zs'" by simp
-    then have "xs \<le> ys" ..
-    then show ?thesis ..
-  qed
-*)
 next
   assume "xs = ys @ [y] \<or> xs \<le> ys"
   then show "xs \<le> ys @ [y]"
     by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
-(*
-  proof
-    assume "xs = ys @ [y]"
-    then show ?thesis by simp
-  next
-    assume "xs \<le> ys"
-    then obtain zs where "ys = xs @ zs" ..
-    then have "ys @ [y] = xs @ (zs @ [y])" by simp
-    then show ?thesis ..
-  qed
-*)
 qed
 
 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
@@ -101,22 +78,10 @@
 
 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
 by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
-(*
-proof -
-  have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
-  then show ?thesis by simp
-qed
-*)
+
 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
 by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
-(*
-proof -
-  assume "xs \<le> ys"
-  then obtain us where "ys = xs @ us" ..
-  then have "ys @ zs = xs @ (us @ zs)" by simp
-  then show ?thesis ..
-qed
-*)
+
 lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
   by (auto simp add: prefix_def)
 
@@ -129,54 +94,26 @@
    apply force
   apply (simp del: append_assoc add: append_assoc [symmetric])
   apply (metis append_eq_appendI)
-(*
-  apply simp
-  apply blast
-*)
   done
 
 lemma append_one_prefix:
   "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
 by (unfold prefix_def)
    (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj eq_Nil_appendI nth_drop')
-(*
-  apply (auto simp add: nth_append)
-  apply (case_tac zs)
-   apply auto
-  done
-*)
+
 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   by (auto simp add: prefix_def)
 
 lemma prefix_same_cases:
   "(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"
 by (unfold prefix_def) (metis append_eq_append_conv2)
-(*
-  apply (erule exE)+
-  apply (simp add: append_eq_append_conv_if split: if_splits)
-   apply (rule disjI2)
-   apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
-   apply clarify
-   apply (drule sym)
-   apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1])
-   apply simp
-  apply (rule disjI1)
-  apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
-  apply clarify
-  apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2])
-  apply simp
-  done
-*)
+
 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
 by (auto simp add: prefix_def)
 
 lemma take_is_prefix: "take n xs \<le> xs"
 by (unfold prefix_def) (metis append_take_drop_id)
-(*
-  apply (rule_tac x="drop n xs" in exI)
-  apply simp
-  done
-*)
+
 lemma map_prefixI:
   "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
 by (clarsimp simp: prefix_def)
@@ -184,12 +121,7 @@
 lemma prefix_length_less:
   "xs < ys \<Longrightarrow> length xs < length ys"
 by (clarsimp simp: strict_prefix_def prefix_def)
-(*
-  apply (frule prefix_length_le)
-  apply (rule ccontr, simp)
-  apply (clarsimp simp: prefix_def)
-  done
-*)
+
 lemma strict_prefix_simps [simp]:
   "xs < [] = False"
   "[] < (x # xs) = True"
@@ -200,10 +132,6 @@
 apply (induct n arbitrary: xs ys)
  apply (case_tac ys, simp_all)[1]
 apply (metis order_less_trans strict_prefixI take_is_prefix)
-(*
-  apply (case_tac xs, simp)
-  apply (case_tac ys, simp_all)
-*)
 done
 
 lemma not_prefix_cases:
@@ -220,10 +148,6 @@
   show ?thesis
   proof (cases ls)
     case Nil thus ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
-(*
-    have "ps \<noteq> []" by (simp add: Nil Cons)
-    from this and Nil show ?thesis by (rule c1)
-*)
   next
     case (Cons x xs)
     show ?thesis
@@ -253,13 +177,6 @@
   then obtain x xs where pv: "ps = x # xs"
     by (rule not_prefix_cases) auto
   show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)
-(*
-  from Cons
-  have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp
-
-  show ?case using npfx
-    by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
-*)
 qed
 
 
@@ -297,23 +214,10 @@
     proof (cases ys')
       assume "ys' = []"
       thus ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
-(*
-      with ys have "xs = ys" by simp
-      with snoc have "[x] \<parallel> []" by auto
-      then have False by blast
-      then show ?thesis ..
-*)
     next
       fix c cs assume ys': "ys' = c # cs"
       thus ?thesis
 	by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI same_prefix_prefix snoc.prems ys)
-(*
-      with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
-      then have "x \<noteq> c" by auto
-      moreover have "xs @ [x] = xs @ x # []" by simp
-      moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
-      ultimately show ?thesis by blast
-*)
     qed
   next
     assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
@@ -436,15 +340,7 @@
 
 lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
 by (metis Cons_prefix_Cons parallelE parallelI)
-(*
-  apply simp
-  apply (rule parallelI)
-   apply simp
-   apply (erule parallelD1)
-  apply simp
-  apply (erule parallelD2)
- done
-*)
+
 lemma not_equal_is_parallel:
   assumes neq: "xs \<noteq> ys"
     and len: "length xs = length ys"