src/HOL/Library/List_Prefix.thy
author wenzelm
Wed Oct 25 18:31:21 2000 +0200 (2000-10-25)
changeset 10330 4362e906b745
child 10389 c7d8901ab269
permissions -rw-r--r--
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm@10330
     1
(*  Title:      HOL/Library/List_Prefix.thy
wenzelm@10330
     2
    ID:         $Id$
wenzelm@10330
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@10330
     4
*)
wenzelm@10330
     5
wenzelm@10330
     6
header {*
wenzelm@10330
     7
  \title{List prefixes}
wenzelm@10330
     8
  \author{Tobias Nipkow and Markus Wenzel}
wenzelm@10330
     9
*}
wenzelm@10330
    10
wenzelm@10330
    11
theory List_Prefix = Main:
wenzelm@10330
    12
wenzelm@10330
    13
subsection {* Prefix order on lists *}
wenzelm@10330
    14
wenzelm@10330
    15
instance list :: ("term") ord ..
wenzelm@10330
    16
wenzelm@10330
    17
defs (overloaded)
wenzelm@10330
    18
  prefix_def: "xs \<le> zs == \<exists>ys. zs = xs @ ys"
wenzelm@10330
    19
  strict_prefix_def: "xs < zs == xs \<le> zs \<and> xs \<noteq> (zs::'a list)"
wenzelm@10330
    20
wenzelm@10330
    21
instance list :: ("term") order
wenzelm@10330
    22
proof
wenzelm@10330
    23
  fix xs ys zs :: "'a list"
wenzelm@10330
    24
  show "xs \<le> xs" by (simp add: prefix_def)
wenzelm@10330
    25
  { assume "xs \<le> ys" and "ys \<le> zs" thus "xs \<le> zs" by (auto simp add: prefix_def) }
wenzelm@10330
    26
  { assume "xs \<le> ys" and "ys \<le> xs" thus "xs = ys" by (auto simp add: prefix_def) }
wenzelm@10330
    27
  show "(xs < zs) = (xs \<le> zs \<and> xs \<noteq> zs)" by (simp only: strict_prefix_def)
wenzelm@10330
    28
qed
wenzelm@10330
    29
wenzelm@10330
    30
constdefs
wenzelm@10330
    31
  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
wenzelm@10330
    32
  "xs \<parallel> ys == \<not> (xs \<le> ys) \<and> \<not> (ys \<le> xs)"
wenzelm@10330
    33
wenzelm@10330
    34
lemma parallelI [intro]: "\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> xs \<parallel> ys"
wenzelm@10330
    35
  by (unfold parallel_def) blast
wenzelm@10330
    36
wenzelm@10330
    37
lemma parellelE [elim]:
wenzelm@10330
    38
    "xs \<parallel> ys ==> (\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> C) ==> C"
wenzelm@10330
    39
  by (unfold parallel_def) blast
wenzelm@10330
    40
wenzelm@10330
    41
theorem prefix_cases:
wenzelm@10330
    42
  "(xs \<le> ys ==> C) ==>
wenzelm@10330
    43
    (ys \<le> xs ==> C) ==>
wenzelm@10330
    44
    (xs \<parallel> ys ==> C) ==> C"
wenzelm@10330
    45
  by (unfold parallel_def) blast
wenzelm@10330
    46
wenzelm@10330
    47
wenzelm@10330
    48
subsection {* Recursion equations *}
wenzelm@10330
    49
wenzelm@10330
    50
theorem Nil_prefix [iff]: "[] \<le> xs"
wenzelm@10330
    51
  apply (simp add: prefix_def)
wenzelm@10330
    52
  done
wenzelm@10330
    53
wenzelm@10330
    54
theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
wenzelm@10330
    55
  apply (induct_tac xs)
wenzelm@10330
    56
   apply simp
wenzelm@10330
    57
  apply (simp add: prefix_def)
wenzelm@10330
    58
  done
wenzelm@10330
    59
wenzelm@10330
    60
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
wenzelm@10330
    61
  apply (unfold prefix_def)
wenzelm@10330
    62
  apply (rule iffI)
wenzelm@10330
    63
   apply (erule exE)
wenzelm@10330
    64
   apply (rename_tac zs)
wenzelm@10330
    65
   apply (rule_tac xs = zs in rev_exhaust)
wenzelm@10330
    66
    apply simp
wenzelm@10330
    67
   apply hypsubst
wenzelm@10330
    68
   apply (simp del: append_assoc add: append_assoc [symmetric])
wenzelm@10330
    69
  apply force
wenzelm@10330
    70
  done
wenzelm@10330
    71
wenzelm@10330
    72
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
wenzelm@10330
    73
  apply (auto simp add: prefix_def)
wenzelm@10330
    74
  done
wenzelm@10330
    75
wenzelm@10330
    76
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
wenzelm@10330
    77
  apply (induct_tac xs)
wenzelm@10330
    78
   apply simp_all
wenzelm@10330
    79
  done
wenzelm@10330
    80
wenzelm@10330
    81
lemma [iff]: "(xs @ ys \<le> xs) = (ys = [])"
wenzelm@10330
    82
  apply (insert same_prefix_prefix [where ?zs = "[]"])
wenzelm@10330
    83
  apply simp
wenzelm@10330
    84
  apply blast
wenzelm@10330
    85
  done
wenzelm@10330
    86
wenzelm@10330
    87
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
wenzelm@10330
    88
  apply (unfold prefix_def)
wenzelm@10330
    89
  apply clarify
wenzelm@10330
    90
  apply simp
wenzelm@10330
    91
  done
wenzelm@10330
    92
wenzelm@10330
    93
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
wenzelm@10330
    94
  apply (unfold prefix_def)
wenzelm@10330
    95
  apply (case_tac xs)
wenzelm@10330
    96
   apply auto
wenzelm@10330
    97
  done
wenzelm@10330
    98
wenzelm@10330
    99
theorem prefix_append:
wenzelm@10330
   100
    "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
wenzelm@10330
   101
  apply (induct zs rule: rev_induct)
wenzelm@10330
   102
   apply force
wenzelm@10330
   103
  apply (simp del: append_assoc add: append_assoc [symmetric])
wenzelm@10330
   104
  apply simp
wenzelm@10330
   105
  apply blast
wenzelm@10330
   106
  done
wenzelm@10330
   107
wenzelm@10330
   108
lemma append_one_prefix:
wenzelm@10330
   109
    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
wenzelm@10330
   110
  apply (unfold prefix_def)
wenzelm@10330
   111
  apply (auto simp add: nth_append)
wenzelm@10330
   112
  apply (case_tac ys)
wenzelm@10330
   113
   apply auto
wenzelm@10330
   114
  done
wenzelm@10330
   115
wenzelm@10330
   116
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
wenzelm@10330
   117
  apply (auto simp add: prefix_def)
wenzelm@10330
   118
  done
wenzelm@10330
   119
wenzelm@10330
   120
wenzelm@10330
   121
subsection {* Prefix cases *}
wenzelm@10330
   122
wenzelm@10330
   123
lemma prefix_Nil_cases [case_names Nil]:
wenzelm@10330
   124
  "xs \<le> [] ==>
wenzelm@10330
   125
    (xs = [] ==> C) ==> C"
wenzelm@10330
   126
  by simp
wenzelm@10330
   127
wenzelm@10330
   128
lemma prefix_Cons_cases [case_names Nil Cons]:
wenzelm@10330
   129
  "xs \<le> y # ys ==>
wenzelm@10330
   130
    (xs = [] ==> C) ==>
wenzelm@10330
   131
    (!!zs. xs = y # zs ==> zs \<le> ys ==> C) ==> C"
wenzelm@10330
   132
  by (simp only: prefix_Cons) blast
wenzelm@10330
   133
wenzelm@10330
   134
lemma prefix_snoc_cases [case_names prefix snoc]:
wenzelm@10330
   135
  "xs \<le> ys @ [y] ==>
wenzelm@10330
   136
    (xs \<le> ys ==> C) ==>
wenzelm@10330
   137
    (xs = ys @ [y] ==> C) ==> C"
wenzelm@10330
   138
  by (simp only: prefix_snoc) blast
wenzelm@10330
   139
wenzelm@10330
   140
lemma prefix_append_cases [case_names prefix append]:
wenzelm@10330
   141
  "xs \<le> ys @ zs ==>
wenzelm@10330
   142
    (xs \<le> ys ==> C) ==>
wenzelm@10330
   143
    (!!us. xs = ys @ us ==> us \<le> zs ==> C) ==> C"
wenzelm@10330
   144
  by (simp only: prefix_append) blast
wenzelm@10330
   145
wenzelm@10330
   146
lemmas prefix_any_cases [cases set: prefix] =    (*dummy set name*)
wenzelm@10330
   147
  prefix_Nil_cases prefix_Cons_cases
wenzelm@10330
   148
  prefix_snoc_cases prefix_append_cases
wenzelm@10330
   149
wenzelm@10330
   150
end