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