src/HOL/Library/List_Prefix.thy
author wenzelm
Fri Nov 03 21:35:36 2000 +0100 (2000-11-03)
changeset 10389 c7d8901ab269
parent 10330 4362e906b745
child 10408 d8b3613158b1
permissions -rw-r--r--
proper setup of "parallel";
removed unused rules;
     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 \<le> xs ==> C) ==>
   135     (xs \<parallel> ys ==> C) ==> C"
   136   by (unfold parallel_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   (concl is "?E xs")
   141 proof -
   142   assume "xs \<parallel> ys"
   143   have "?this --> ?E xs" (is "?P xs")
   144   proof (induct (stripped) xs rule: rev_induct)
   145     assume "[] \<parallel> ys" hence False by auto
   146     thus "?E []" ..
   147   next
   148     fix x xs
   149     assume hyp: "?P xs"
   150     assume asm: "xs @ [x] \<parallel> ys"
   151     show "?E (xs @ [x])"
   152     proof (rule prefix_cases)
   153       assume le: "xs \<le> ys"
   154       then obtain ys' where ys: "ys = xs @ ys'" ..
   155       show ?thesis
   156       proof (cases ys')
   157         assume "ys' = []" with ys have "xs = ys" by simp
   158         with asm have "[x] \<parallel> []" by auto
   159         hence False by blast
   160         thus ?thesis ..
   161       next
   162         fix c cs assume ys': "ys' = c # cs"
   163         with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
   164         hence "x \<noteq> c" by auto
   165         moreover have "xs @ [x] = xs @ x # []" by simp
   166         moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
   167         ultimately show ?thesis by blast
   168       qed
   169     next
   170       assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
   171       with asm have False by blast
   172       thus ?thesis ..
   173     next
   174       assume "xs \<parallel> ys"
   175       with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
   176           and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
   177 	by blast
   178       from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
   179       with neq ys show ?thesis by blast
   180     qed
   181   qed
   182   thus ?thesis ..
   183 qed
   184 
   185 end