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