src/HOL/Library/List_Prefix.thy
author wenzelm
Wed Nov 22 21:47:04 2000 +0100 (2000-11-22)
changeset 10512 d34192966cd8
parent 10408 d8b3613158b1
child 10870 9444e3cf37e1
permissions -rw-r--r--
tuned;
     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?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    31   by (unfold strict_prefix_def) blast
    32 
    33 lemma strict_prefixE [elim?]:
    34     "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
    35   by (unfold strict_prefix_def) blast
    36 
    37 
    38 subsection {* Basic properties of prefixes *}
    39 
    40 theorem Nil_prefix [iff]: "[] \<le> xs"
    41   by (simp add: prefix_def)
    42 
    43 theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
    44   by (induct xs) (simp_all add: prefix_def)
    45 
    46 lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    47 proof
    48   assume "xs \<le> ys @ [y]"
    49   then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    50   show "xs = ys @ [y] \<or> xs \<le> ys"
    51   proof (cases zs rule: rev_cases)
    52     assume "zs = []"
    53     with zs have "xs = ys @ [y]" by simp
    54     thus ?thesis ..
    55   next
    56     fix z zs' assume "zs = zs' @ [z]"
    57     with zs have "ys = xs @ zs'" by simp
    58     hence "xs \<le> ys" ..
    59     thus ?thesis ..
    60   qed
    61 next
    62   assume "xs = ys @ [y] \<or> xs \<le> ys"
    63   thus "xs \<le> ys @ [y]"
    64   proof
    65     assume "xs = ys @ [y]"
    66     thus ?thesis by simp
    67   next
    68     assume "xs \<le> ys"
    69     then obtain zs where "ys = xs @ zs" ..
    70     hence "ys @ [y] = xs @ (zs @ [y])" by simp
    71     thus ?thesis ..
    72   qed
    73 qed
    74 
    75 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    76   by (auto simp add: prefix_def)
    77 
    78 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    79   by (induct xs) simp_all
    80 
    81 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
    82 proof -
    83   have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)
    84   thus ?thesis by simp
    85 qed
    86 
    87 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
    88 proof -
    89   assume "xs \<le> ys"
    90   then obtain us where "ys = xs @ us" ..
    91   hence "ys @ zs = xs @ (us @ zs)" by simp
    92   thus ?thesis ..
    93 qed
    94 
    95 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
    96   by (cases xs) (auto simp add: prefix_def)
    97 
    98 theorem prefix_append:
    99     "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   100   apply (induct zs rule: rev_induct)
   101    apply force
   102   apply (simp del: append_assoc add: append_assoc [symmetric])
   103   apply simp
   104   apply blast
   105   done
   106 
   107 lemma append_one_prefix:
   108     "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   109   apply (unfold prefix_def)
   110   apply (auto simp add: nth_append)
   111   apply (case_tac zs)
   112    apply auto
   113   done
   114 
   115 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   116   by (auto simp add: prefix_def)
   117 
   118 
   119 subsection {* Parallel lists *}
   120 
   121 constdefs
   122   parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
   123   "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   124 
   125 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   126   by (unfold parallel_def) blast
   127 
   128 lemma parallelE [elim]:
   129     "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
   130   by (unfold parallel_def) blast
   131 
   132 theorem prefix_cases:
   133   "(xs \<le> ys ==> C) ==>
   134     (ys < xs ==> C) ==>
   135     (xs \<parallel> ys ==> C) ==> C"
   136   by (unfold parallel_def strict_prefix_def) blast
   137 
   138 theorem parallel_decomp:
   139   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
   140   (is "PROP ?P xs" concl is "?E xs")
   141 proof (induct xs rule: rev_induct)
   142   assume "[] \<parallel> ys" hence False by auto
   143   thus "?E []" ..
   144 next
   145   fix x xs
   146   assume hyp: "PROP ?P xs"
   147   assume asm: "xs @ [x] \<parallel> ys"
   148   show "?E (xs @ [x])"
   149   proof (rule prefix_cases)
   150     assume le: "xs \<le> ys"
   151     then obtain ys' where ys: "ys = xs @ ys'" ..
   152     show ?thesis
   153     proof (cases ys')
   154       assume "ys' = []" with ys have "xs = ys" by simp
   155       with asm have "[x] \<parallel> []" by auto
   156       hence False by blast
   157       thus ?thesis ..
   158     next
   159       fix c cs assume ys': "ys' = c # cs"
   160       with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
   161       hence "x \<noteq> c" by auto
   162       moreover have "xs @ [x] = xs @ x # []" by simp
   163       moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
   164       ultimately show ?thesis by blast
   165     qed
   166   next
   167     assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
   168     with asm have False by blast
   169     thus ?thesis ..
   170   next
   171     assume "xs \<parallel> ys"
   172     with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
   173       and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
   174       by blast
   175     from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
   176     with neq ys show ?thesis by blast
   177   qed
   178 qed
   179 
   180 end