src/HOL/Library/List_Prefix.thy
author wenzelm
Thu Jan 11 19:37:46 2001 +0100 (2001-01-11)
changeset 10870 9444e3cf37e1
parent 10512 d34192966cd8
child 11780 d17ee2241257
permissions -rw-r--r--
added strict_prefixI', strict_prefixE';
     1 (*  Title:      HOL/Library/List_Prefix.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {*
     7   \title{List prefixes}
     8   \author{Tobias Nipkow and Markus Wenzel}
     9 *}
    10 
    11 theory List_Prefix = Main:
    12 
    13 subsection {* Prefix order on lists *}
    14 
    15 instance list :: ("term") ord ..
    16 
    17 defs (overloaded)
    18   prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
    19   strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    20 
    21 instance list :: ("term") order
    22   by intro_classes (auto simp add: prefix_def strict_prefix_def)
    23 
    24 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    25   by (unfold prefix_def) blast
    26 
    27 lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
    28   by (unfold prefix_def) blast
    29 
    30 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    31   by (unfold strict_prefix_def prefix_def) blast
    32 
    33 lemma strict_prefixE' [elim?]:
    34     "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"
    35 proof -
    36   assume r: "!!z zs. ys = xs @ z # zs ==> C"
    37   assume "xs < ys"
    38   then obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    39     by (unfold strict_prefix_def prefix_def) blast
    40   with r show ?thesis by (auto simp add: neq_Nil_conv)
    41 qed
    42 
    43 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    44   by (unfold strict_prefix_def) blast
    45 
    46 lemma strict_prefixE [elim?]:
    47     "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
    48   by (unfold strict_prefix_def) blast
    49 
    50 
    51 subsection {* Basic properties of prefixes *}
    52 
    53 theorem Nil_prefix [iff]: "[] \<le> xs"
    54   by (simp add: prefix_def)
    55 
    56 theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
    57   by (induct xs) (simp_all add: prefix_def)
    58 
    59 lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    60 proof
    61   assume "xs \<le> ys @ [y]"
    62   then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    63   show "xs = ys @ [y] \<or> xs \<le> ys"
    64   proof (cases zs rule: rev_cases)
    65     assume "zs = []"
    66     with zs have "xs = ys @ [y]" by simp
    67     thus ?thesis ..
    68   next
    69     fix z zs' assume "zs = zs' @ [z]"
    70     with zs have "ys = xs @ zs'" by simp
    71     hence "xs \<le> ys" ..
    72     thus ?thesis ..
    73   qed
    74 next
    75   assume "xs = ys @ [y] \<or> xs \<le> ys"
    76   thus "xs \<le> ys @ [y]"
    77   proof
    78     assume "xs = ys @ [y]"
    79     thus ?thesis by simp
    80   next
    81     assume "xs \<le> ys"
    82     then obtain zs where "ys = xs @ zs" ..
    83     hence "ys @ [y] = xs @ (zs @ [y])" by simp
    84     thus ?thesis ..
    85   qed
    86 qed
    87 
    88 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    89   by (auto simp add: prefix_def)
    90 
    91 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    92   by (induct xs) simp_all
    93 
    94 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
    95 proof -
    96   have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
    97   thus ?thesis by simp
    98 qed
    99 
   100 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
   101 proof -
   102   assume "xs \<le> ys"
   103   then obtain us where "ys = xs @ us" ..
   104   hence "ys @ zs = xs @ (us @ zs)" by simp
   105   thus ?thesis ..
   106 qed
   107 
   108 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
   109   by (cases xs) (auto simp add: prefix_def)
   110 
   111 theorem prefix_append:
   112     "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   113   apply (induct zs rule: rev_induct)
   114    apply force
   115   apply (simp del: append_assoc add: append_assoc [symmetric])
   116   apply simp
   117   apply blast
   118   done
   119 
   120 lemma append_one_prefix:
   121     "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   122   apply (unfold prefix_def)
   123   apply (auto simp add: nth_append)
   124   apply (case_tac zs)
   125    apply auto
   126   done
   127 
   128 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   129   by (auto simp add: prefix_def)
   130 
   131 
   132 subsection {* Parallel lists *}
   133 
   134 constdefs
   135   parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
   136   "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   137 
   138 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   139   by (unfold parallel_def) blast
   140 
   141 lemma parallelE [elim]:
   142     "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
   143   by (unfold parallel_def) blast
   144 
   145 theorem prefix_cases:
   146   "(xs \<le> ys ==> C) ==>
   147     (ys < xs ==> C) ==>
   148     (xs \<parallel> ys ==> C) ==> C"
   149   by (unfold parallel_def strict_prefix_def) blast
   150 
   151 theorem parallel_decomp:
   152   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
   153   (is "PROP ?P xs" concl is "?E xs")
   154 proof (induct xs rule: rev_induct)
   155   assume "[] \<parallel> ys" hence False by auto
   156   thus "?E []" ..
   157 next
   158   fix x xs
   159   assume hyp: "PROP ?P xs"
   160   assume asm: "xs @ [x] \<parallel> ys"
   161   show "?E (xs @ [x])"
   162   proof (rule prefix_cases)
   163     assume le: "xs \<le> ys"
   164     then obtain ys' where ys: "ys = xs @ ys'" ..
   165     show ?thesis
   166     proof (cases ys')
   167       assume "ys' = []" with ys have "xs = ys" by simp
   168       with asm have "[x] \<parallel> []" by auto
   169       hence False by blast
   170       thus ?thesis ..
   171     next
   172       fix c cs assume ys': "ys' = c # cs"
   173       with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
   174       hence "x \<noteq> c" by auto
   175       moreover have "xs @ [x] = xs @ x # []" by simp
   176       moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
   177       ultimately show ?thesis by blast
   178     qed
   179   next
   180     assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
   181     with asm have False by blast
   182     thus ?thesis ..
   183   next
   184     assume "xs \<parallel> ys"
   185     with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
   186       and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
   187       by blast
   188     from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
   189     with neq ys show ?thesis by blast
   190   qed
   191 qed
   192 
   193 end