src/HOL/UNITY/ListOrder.thy
author haftmann
Fri, 25 Jul 2008 12:03:34 +0200
changeset 27682 25aceefd4786
parent 23767 7272a839ccd9
child 30198 922f944f03b2
permissions -rw-r--r--
added class preorder
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6708
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/ListOrder
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
     2
    ID:         $Id$
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
     5
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
     6
Lists are partially ordered by Charpentier's Generalized Prefix Relation
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
     7
   (xs,ys) : genPrefix(r)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
     8
     if ys = xs' @ zs where length xs = length xs'
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
     9
     and corresponding elements of xs, xs' are pairwise related by r
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    10
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    11
Also overloads <= and < for lists!
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    12
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    13
Based on Lex/Prefix
6708
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
    14
*)
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
    15
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    16
header {*The Prefix Ordering on Lists*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    17
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    18
theory ListOrder
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    19
imports Main
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    20
begin
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    21
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    22
inductive_set
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    23
  genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    24
  for r :: "('a * 'a)set"
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    25
 where
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    26
   Nil:     "([],[]) : genPrefix(r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    27
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    28
 | prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    29
	     (x#xs, y#ys) : genPrefix(r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    30
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    31
 | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    32
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    33
instantiation list :: (type) ord 
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    34
begin
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    35
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    36
definition
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    37
  prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    38
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    39
definition
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    40
  strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    41
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    42
instance ..  
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    43
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    44
(*Constants for the <= and >= relations, used below in translations*)
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    45
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    46
end
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
    47
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    48
constdefs
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    49
  Le :: "(nat*nat) set"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    50
    "Le == {(x,y). x <= y}"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    51
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    52
  Ge :: "(nat*nat) set"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    53
    "Ge == {(x,y). y <= x}"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    54
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    55
abbreviation
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    56
  pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    57
  "xs pfixLe ys == (xs,ys) : genPrefix Le"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    58
23767
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    59
abbreviation
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    60
  pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
7272a839ccd9 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    61
  "xs pfixGe ys == (xs,ys) : genPrefix Ge"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    62
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    63
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    64
subsection{*preliminary lemmas*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    65
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    66
lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    67
by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    68
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    69
lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    70
by (erule genPrefix.induct, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    71
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    72
lemma cdlemma:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    73
     "[| (xs', ys'): genPrefix r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    74
      ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    75
apply (erule genPrefix.induct, blast, blast)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    76
apply (force intro: genPrefix.append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    77
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    78
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    79
(*As usual converting it to an elimination rule is tiresome*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    80
lemma cons_genPrefixE [elim!]: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    81
     "[| (x#xs, zs): genPrefix r;   
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    82
         !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    83
      |] ==> P"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    84
by (drule cdlemma, simp, blast)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    85
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    86
lemma Cons_genPrefix_Cons [iff]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    87
     "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    88
by (blast intro: genPrefix.prepend)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    89
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    90
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    91
subsection{*genPrefix is a partial order*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    92
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    93
lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    94
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    95
apply (unfold refl_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    96
apply (induct_tac "x")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    97
prefer 2 apply (blast intro: genPrefix.prepend)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    98
apply (blast intro: genPrefix.Nil)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
    99
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   100
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   101
lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   102
by (erule reflD [OF refl_genPrefix UNIV_I])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   103
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   104
lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   105
apply clarify
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   106
apply (erule genPrefix.induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   107
apply (auto intro: genPrefix.append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   108
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   109
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   110
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   111
(** Transitivity **)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   112
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   113
(*A lemma for proving genPrefix_trans_O*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   114
lemma append_genPrefix [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   115
     "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   116
by (induct_tac "xs", auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   117
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   118
(*Lemma proving transitivity and more*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   119
lemma genPrefix_trans_O [rule_format]: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   120
     "(x, y) : genPrefix r  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   121
      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   122
apply (erule genPrefix.induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   123
  prefer 3 apply (blast dest: append_genPrefix)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   124
 prefer 2 apply (blast intro: genPrefix.prepend, blast)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   125
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   126
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   127
lemma genPrefix_trans [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   128
     "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   129
      ==> (x,z) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   130
apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   131
 apply assumption
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   132
apply (blast intro: genPrefix_trans_O)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   133
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   134
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   135
lemma prefix_genPrefix_trans [rule_format]: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   136
     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   137
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   138
apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   139
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   140
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   141
lemma genPrefix_prefix_trans [rule_format]: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   142
     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   143
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   144
apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   145
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   146
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   147
lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   148
by (blast intro: transI genPrefix_trans)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   149
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   150
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   151
(** Antisymmetry **)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   152
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   153
lemma genPrefix_antisym [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   154
     "[| (xs,ys) : genPrefix r;  antisym r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   155
      ==> (ys,xs) : genPrefix r --> xs = ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   156
apply (erule genPrefix.induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   157
  txt{*Base case*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   158
  apply blast
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   159
 txt{*prepend case*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   160
 apply (simp add: antisym_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   161
txt{*append case is the hardest*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   162
apply clarify
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   163
apply (subgoal_tac "length zs = 0", force)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   164
apply (drule genPrefix_length_le)+
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   165
apply (simp del: length_0_conv)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   166
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   167
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   168
lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   169
by (blast intro: antisymI genPrefix_antisym)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   170
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   171
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   172
subsection{*recursion equations*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   173
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   174
lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   175
apply (induct_tac "xs")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   176
prefer 2 apply blast
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   177
apply simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   178
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   179
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   180
lemma same_genPrefix_genPrefix [simp]: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   181
    "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   182
apply (unfold refl_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   183
apply (induct_tac "xs")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   184
apply (simp_all (no_asm_simp))
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   185
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   186
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   187
lemma genPrefix_Cons:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   188
     "((xs, y#ys) : genPrefix r) =  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   189
      (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   190
by (case_tac "xs", auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   191
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   192
lemma genPrefix_take_append:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   193
     "[| reflexive r;  (xs,ys) : genPrefix r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   194
      ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   195
apply (erule genPrefix.induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   196
apply (frule_tac [3] genPrefix_length_le)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   197
apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   198
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   199
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   200
lemma genPrefix_append_both:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   201
     "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   202
      ==>  (xs@zs, ys @ zs) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   203
apply (drule genPrefix_take_append, assumption)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   204
apply (simp add: take_all)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   205
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   206
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   207
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   208
(*NOT suitable for rewriting since [y] has the form y#ys*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   209
lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   210
by auto
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   211
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   212
lemma aolemma:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   213
     "[| (xs,ys) : genPrefix r;  reflexive r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   214
      ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   215
apply (erule genPrefix.induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   216
  apply blast
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   217
 apply simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   218
txt{*Append case is hardest*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   219
apply simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   220
apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   221
apply (erule disjE)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   222
apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   223
apply (blast intro: genPrefix.append, auto)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 13798
diff changeset
   224
apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   225
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   226
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   227
lemma append_one_genPrefix:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   228
     "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |]  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   229
      ==> (xs @ [ys ! length xs], ys) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   230
by (blast intro: aolemma [THEN mp])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   231
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   232
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   233
(** Proving the equivalence with Charpentier's definition **)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   234
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   235
lemma genPrefix_imp_nth [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   236
     "ALL i ys. i < length xs  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   237
                --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   238
apply (induct_tac "xs", auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   239
apply (case_tac "i", auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   240
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   241
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   242
lemma nth_imp_genPrefix [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   243
     "ALL ys. length xs <= length ys   
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   244
      --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   245
      --> (xs, ys) : genPrefix r"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   246
apply (induct_tac "xs")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   247
apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   248
apply clarify
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   249
apply (case_tac "ys")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   250
apply (force+)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   251
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   252
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   253
lemma genPrefix_iff_nth:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   254
     "((xs,ys) : genPrefix r) =  
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   255
      (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   256
apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   257
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   258
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   259
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   260
subsection{*The type of lists is partially ordered*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   261
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   262
declare reflexive_Id [iff] 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   263
        antisym_Id [iff] 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   264
        trans_Id [iff]
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   265
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   266
lemma prefix_refl [iff]: "xs <= (xs::'a list)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   267
by (simp add: prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   268
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   269
lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   270
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   271
apply (blast intro: genPrefix_trans)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   272
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   273
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   274
lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   275
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   276
apply (blast intro: genPrefix_antisym)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   277
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   278
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
   279
lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   280
by (unfold strict_prefix_def, auto)
6708
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
   281
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 6810
diff changeset
   282
instance list :: (type) order
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   283
  by (intro_classes,
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   284
      (assumption | rule prefix_refl prefix_trans prefix_antisym
27682
25aceefd4786 added class preorder
haftmann
parents: 23767
diff changeset
   285
                     prefix_less_le_not_le)+)
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   286
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   287
(*Monotonicity of "set" operator WRT prefix*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   288
lemma set_mono: "xs <= ys ==> set xs <= set ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   289
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   290
apply (erule genPrefix.induct, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   291
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   292
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   293
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   294
(** recursion equations **)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   295
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   296
lemma Nil_prefix [iff]: "[] <= xs"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   297
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   298
apply (simp add: Nil_genPrefix)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   299
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   300
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   301
lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   302
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   303
apply (simp add: genPrefix_Nil)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   304
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   305
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   306
lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   307
by (simp add: prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   308
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   309
lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   310
by (simp add: prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   311
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   312
lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   313
by (insert same_prefix_prefix [of xs ys "[]"], simp)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   314
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   315
lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   316
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   317
apply (erule genPrefix.append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   318
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   319
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   320
lemma prefix_Cons: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   321
   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   322
by (simp add: prefix_def genPrefix_Cons)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   323
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   324
lemma append_one_prefix: 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   325
  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   326
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   327
apply (simp add: append_one_genPrefix)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   328
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   329
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   330
lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   331
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   332
apply (erule genPrefix_length_le)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   333
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   334
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   335
lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   336
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   337
apply (erule genPrefix.induct, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   338
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   339
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   340
lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   341
apply (unfold strict_prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   342
apply (blast intro: splemma [THEN mp])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   343
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   344
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   345
lemma mono_length: "mono length"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   346
by (blast intro: monoI prefix_length_le)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   347
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   348
(*Equivalence to the definition used in Lex/Prefix.thy*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   349
lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   350
apply (unfold prefix_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   351
apply (auto simp add: genPrefix_iff_nth nth_append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   352
apply (rule_tac x = "drop (length xs) zs" in exI)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   353
apply (rule nth_equalityI)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   354
apply (simp_all (no_asm_simp) add: nth_append)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   355
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   356
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   357
lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   358
apply (simp add: prefix_iff)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   359
apply (rule iffI)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   360
 apply (erule exE)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   361
 apply (rename_tac "zs")
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   362
 apply (rule_tac xs = zs in rev_exhaust)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   363
  apply simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   364
 apply clarify
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   365
 apply (simp del: append_assoc add: append_assoc [symmetric], force)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   366
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   367
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   368
lemma prefix_append_iff:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   369
     "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   370
apply (rule_tac xs = zs in rev_induct)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   371
 apply force
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   372
apply (simp del: append_assoc add: append_assoc [symmetric], force)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   373
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   374
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   375
(*Although the prefix ordering is not linear, the prefixes of a list
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   376
  are linearly ordered.*)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   377
lemma common_prefix_linear [rule_format]:
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   378
     "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   379
by (rule_tac xs = zs in rev_induct, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   380
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   381
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   382
subsection{*pfixLe, pfixGe: properties inherited from the translations*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   383
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   384
(** pfixLe **)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   385
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   386
lemma reflexive_Le [iff]: "reflexive Le"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   387
by (unfold refl_def Le_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   388
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   389
lemma antisym_Le [iff]: "antisym Le"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   390
by (unfold antisym_def Le_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   391
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   392
lemma trans_Le [iff]: "trans Le"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   393
by (unfold trans_def Le_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   394
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   395
lemma pfixLe_refl [iff]: "x pfixLe x"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   396
by simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   397
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   398
lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   399
by (blast intro: genPrefix_trans)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   400
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   401
lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   402
by (blast intro: genPrefix_antisym)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   403
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   404
lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   405
apply (unfold prefix_def Le_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   406
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   407
done
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   408
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   409
lemma reflexive_Ge [iff]: "reflexive Ge"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   410
by (unfold refl_def Ge_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   411
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   412
lemma antisym_Ge [iff]: "antisym Ge"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   413
by (unfold antisym_def Ge_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   414
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   415
lemma trans_Ge [iff]: "trans Ge"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   416
by (unfold trans_def Ge_def, auto)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   417
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   418
lemma pfixGe_refl [iff]: "x pfixGe x"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   419
by simp
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   420
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   421
lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   422
by (blast intro: genPrefix_trans)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   423
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   424
lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   425
by (blast intro: genPrefix_antisym)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   426
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   427
lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   428
apply (unfold prefix_def Ge_def)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   429
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 12338
diff changeset
   430
done
6708
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
   431
62beb3336b02 lists are partially ordered by the prefix relation
paulson
parents:
diff changeset
   432
end