src/ZF/Order.thy
author wenzelm
Sat Oct 10 22:44:57 2015 +0200 (2015-10-10)
changeset 61400 045b4d7a53e2
parent 60770 240563fbf41d
child 61798 27f3c10b0b50
permissions -rw-r--r--
tuned syntax -- more symbols;
clasohm@1478
     1
(*  Title:      ZF/Order.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     3
    Copyright   1994  University of Cambridge
lcp@435
     4
paulson@13140
     5
Results from the book "Set Theory: an Introduction to Independence Proofs"
paulson@13140
     6
        by Kenneth Kunen.  Chapter 1, section 6.
ballarin@27703
     7
Additional definitions and lemmas for reflexive orders.
lcp@435
     8
*)
lcp@435
     9
wenzelm@60770
    10
section\<open>Partial and Total Orderings: Basic Definitions and Properties\<close>
paulson@13356
    11
haftmann@16417
    12
theory Order imports WF Perm begin
lcp@786
    13
wenzelm@60770
    14
text \<open>We adopt the following convention: @{text ord} is used for
ballarin@27703
    15
  strict orders and @{text order} is used for their reflexive
wenzelm@60770
    16
  counterparts.\<close>
ballarin@27703
    17
wenzelm@24893
    18
definition
wenzelm@32960
    19
  part_ord :: "[i,i]=>o"                (*Strict partial ordering*)  where
paulson@13140
    20
   "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
paulson@13140
    21
wenzelm@24893
    22
definition
wenzelm@32960
    23
  linear   :: "[i,i]=>o"                (*Strict total ordering*)  where
paulson@46820
    24
   "linear(A,r) == (\<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r | x=y | <y,x>:r)"
paulson@13140
    25
wenzelm@24893
    26
definition
wenzelm@32960
    27
  tot_ord  :: "[i,i]=>o"                (*Strict total ordering*)  where
paulson@13140
    28
   "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
paulson@13140
    29
wenzelm@24893
    30
definition
ballarin@27703
    31
  "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)"
ballarin@27703
    32
ballarin@27703
    33
definition                              (*Partial ordering*)
ballarin@27703
    34
  "partial_order_on(A, r) \<equiv> preorder_on(A, r) \<and> antisym(r)"
ballarin@27703
    35
ballarin@27703
    36
abbreviation
ballarin@27703
    37
  "Preorder(r) \<equiv> preorder_on(field(r), r)"
ballarin@27703
    38
ballarin@27703
    39
abbreviation
ballarin@27703
    40
  "Partial_order(r) \<equiv> partial_order_on(field(r), r)"
ballarin@27703
    41
ballarin@27703
    42
definition
wenzelm@32960
    43
  well_ord :: "[i,i]=>o"                (*Well-ordering*)  where
paulson@13140
    44
   "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
paulson@13140
    45
wenzelm@24893
    46
definition
wenzelm@32960
    47
  mono_map :: "[i,i,i,i]=>i"            (*Order-preserving maps*)  where
paulson@13140
    48
   "mono_map(A,r,B,s) ==
paulson@46953
    49
              {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
paulson@13140
    50
wenzelm@24893
    51
definition
wenzelm@61400
    52
  ord_iso  :: "[i,i,i,i]=>i"  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)  (*Order isomorphisms*)  where
wenzelm@61400
    53
   "\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> ==
paulson@46953
    54
              {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
paulson@13140
    55
wenzelm@24893
    56
definition
wenzelm@32960
    57
  pred     :: "[i,i,i]=>i"              (*Set of predecessors*)  where
paulson@46953
    58
   "pred(A,x,r) == {y \<in> A. <y,x>:r}"
paulson@13140
    59
wenzelm@24893
    60
definition
wenzelm@32960
    61
  ord_iso_map :: "[i,i,i,i]=>i"         (*Construction for linearity theorem*)  where
paulson@13140
    62
   "ord_iso_map(A,r,B,s) ==
paulson@13615
    63
     \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
paulson@13140
    64
wenzelm@24893
    65
definition
wenzelm@24893
    66
  first :: "[i, i, i] => o"  where
paulson@46953
    67
    "first(u, X, R) == u \<in> X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
paulson@2469
    68
wenzelm@60770
    69
subsection\<open>Immediate Consequences of the Definitions\<close>
paulson@13140
    70
paulson@13140
    71
lemma part_ord_Imp_asym:
paulson@46820
    72
    "part_ord(A,r) ==> asym(r \<inter> A*A)"
paulson@13140
    73
by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
paulson@13140
    74
paulson@13140
    75
lemma linearE:
paulson@46953
    76
    "[| linear(A,r);  x \<in> A;  y \<in> A;
paulson@13140
    77
        <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |]
paulson@13140
    78
     ==> P"
paulson@13140
    79
by (simp add: linear_def, blast)
paulson@13140
    80
paulson@13140
    81
paulson@13140
    82
(** General properties of well_ord **)
paulson@13140
    83
paulson@13140
    84
lemma well_ordI:
paulson@13140
    85
    "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"
paulson@13140
    86
apply (simp add: irrefl_def part_ord_def tot_ord_def
paulson@13140
    87
                 trans_on_def well_ord_def wf_on_not_refl)
paulson@13140
    88
apply (fast elim: linearE wf_on_asym wf_on_chain3)
paulson@13140
    89
done
paulson@13140
    90
paulson@13140
    91
lemma well_ord_is_wf:
paulson@13140
    92
    "well_ord(A,r) ==> wf[A](r)"
paulson@13140
    93
by (unfold well_ord_def, safe)
paulson@13140
    94
paulson@13140
    95
lemma well_ord_is_trans_on:
paulson@13140
    96
    "well_ord(A,r) ==> trans[A](r)"
paulson@13140
    97
by (unfold well_ord_def tot_ord_def part_ord_def, safe)
paulson@13140
    98
paulson@13140
    99
lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)"
paulson@13140
   100
by (unfold well_ord_def tot_ord_def, blast)
paulson@13140
   101
paulson@13140
   102
paulson@13140
   103
(** Derived rules for pred(A,x,r) **)
paulson@13140
   104
paulson@46953
   105
lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y \<in> A"
paulson@13140
   106
by (unfold pred_def, blast)
paulson@13140
   107
paulson@13140
   108
lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
paulson@13140
   109
paulson@46953
   110
lemma predE: "[| y \<in> pred(A,x,r);  [| y \<in> A; <y,x>:r |] ==> P |] ==> P"
paulson@13140
   111
by (simp add: pred_def)
paulson@13140
   112
paulson@46820
   113
lemma pred_subset_under: "pred(A,x,r) \<subseteq> r -`` {x}"
paulson@13140
   114
by (simp add: pred_def, blast)
paulson@13140
   115
paulson@46820
   116
lemma pred_subset: "pred(A,x,r) \<subseteq> A"
paulson@13140
   117
by (simp add: pred_def, blast)
paulson@13140
   118
paulson@13140
   119
lemma pred_pred_eq:
paulson@46820
   120
    "pred(pred(A,x,r), y, r) = pred(A,x,r) \<inter> pred(A,y,r)"
paulson@13140
   121
by (simp add: pred_def, blast)
paulson@13140
   122
paulson@13140
   123
lemma trans_pred_pred_eq:
paulson@46953
   124
    "[| trans[A](r);  <y,x>:r;  x \<in> A;  y \<in> A |]
paulson@13140
   125
     ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
paulson@13140
   126
by (unfold trans_on_def pred_def, blast)
paulson@13140
   127
paulson@13140
   128
wenzelm@60770
   129
subsection\<open>Restricting an Ordering's Domain\<close>
paulson@13356
   130
paulson@13140
   131
(** The ordering's properties hold over all subsets of its domain
paulson@13140
   132
    [including initial segments of the form pred(A,x,r) **)
paulson@13140
   133
paulson@13140
   134
(*Note: a relation s such that s<=r need not be a partial ordering*)
paulson@13140
   135
lemma part_ord_subset:
paulson@13140
   136
    "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)"
paulson@13140
   137
by (unfold part_ord_def irrefl_def trans_on_def, blast)
paulson@13140
   138
paulson@13140
   139
lemma linear_subset:
paulson@13140
   140
    "[| linear(A,r);  B<=A |] ==> linear(B,r)"
paulson@13140
   141
by (unfold linear_def, blast)
paulson@13140
   142
paulson@13140
   143
lemma tot_ord_subset:
paulson@13140
   144
    "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)"
paulson@13140
   145
apply (unfold tot_ord_def)
paulson@13140
   146
apply (fast elim!: part_ord_subset linear_subset)
paulson@13140
   147
done
paulson@13140
   148
paulson@13140
   149
lemma well_ord_subset:
paulson@13140
   150
    "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)"
paulson@13140
   151
apply (unfold well_ord_def)
paulson@13140
   152
apply (fast elim!: tot_ord_subset wf_on_subset_A)
paulson@13140
   153
done
paulson@13140
   154
paulson@13140
   155
paulson@13140
   156
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
paulson@13140
   157
paulson@46821
   158
lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) \<longleftrightarrow> irrefl(A,r)"
paulson@13140
   159
by (unfold irrefl_def, blast)
paulson@13140
   160
paulson@46821
   161
lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) \<longleftrightarrow> trans[A](r)"
paulson@13140
   162
by (unfold trans_on_def, blast)
paulson@13140
   163
paulson@46821
   164
lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
paulson@13140
   165
apply (unfold part_ord_def)
paulson@13140
   166
apply (simp add: irrefl_Int_iff trans_on_Int_iff)
paulson@13140
   167
done
paulson@13140
   168
paulson@46821
   169
lemma linear_Int_iff: "linear(A,r \<inter> A*A) \<longleftrightarrow> linear(A,r)"
paulson@13140
   170
by (unfold linear_def, blast)
paulson@13140
   171
paulson@46821
   172
lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
paulson@13140
   173
apply (unfold tot_ord_def)
paulson@13140
   174
apply (simp add: part_ord_Int_iff linear_Int_iff)
paulson@13140
   175
done
paulson@13140
   176
paulson@46821
   177
lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) \<longleftrightarrow> wf[A](r)"
wenzelm@24893
   178
apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
paulson@13140
   179
done
paulson@13140
   180
paulson@46821
   181
lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
paulson@13140
   182
apply (unfold well_ord_def)
paulson@13140
   183
apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
paulson@13140
   184
done
paulson@13140
   185
paulson@13140
   186
wenzelm@60770
   187
subsection\<open>Empty and Unit Domains\<close>
paulson@13356
   188
paulson@13701
   189
(*The empty relation is well-founded*)
paulson@13701
   190
lemma wf_on_any_0: "wf[A](0)"
paulson@13701
   191
by (simp add: wf_on_def wf_def, fast)
paulson@13701
   192
wenzelm@60770
   193
subsubsection\<open>Relations over the Empty Set\<close>
paulson@13140
   194
paulson@13140
   195
lemma irrefl_0: "irrefl(0,r)"
paulson@13140
   196
by (unfold irrefl_def, blast)
paulson@13140
   197
paulson@13140
   198
lemma trans_on_0: "trans[0](r)"
paulson@13140
   199
by (unfold trans_on_def, blast)
paulson@13140
   200
paulson@13140
   201
lemma part_ord_0: "part_ord(0,r)"
paulson@13140
   202
apply (unfold part_ord_def)
paulson@13140
   203
apply (simp add: irrefl_0 trans_on_0)
paulson@13140
   204
done
paulson@13140
   205
paulson@13140
   206
lemma linear_0: "linear(0,r)"
paulson@13140
   207
by (unfold linear_def, blast)
paulson@13140
   208
paulson@13140
   209
lemma tot_ord_0: "tot_ord(0,r)"
paulson@13140
   210
apply (unfold tot_ord_def)
paulson@13140
   211
apply (simp add: part_ord_0 linear_0)
paulson@13140
   212
done
paulson@13140
   213
paulson@13140
   214
lemma wf_on_0: "wf[0](r)"
paulson@13140
   215
by (unfold wf_on_def wf_def, blast)
paulson@13140
   216
paulson@13140
   217
lemma well_ord_0: "well_ord(0,r)"
paulson@13140
   218
apply (unfold well_ord_def)
paulson@13140
   219
apply (simp add: tot_ord_0 wf_on_0)
paulson@13140
   220
done
paulson@13140
   221
paulson@13140
   222
wenzelm@60770
   223
subsubsection\<open>The Empty Relation Well-Orders the Unit Set\<close>
paulson@13701
   224
wenzelm@60770
   225
text\<open>by Grabczewski\<close>
paulson@13140
   226
paulson@13140
   227
lemma tot_ord_unit: "tot_ord({a},0)"
paulson@13140
   228
by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
paulson@13140
   229
paulson@13140
   230
lemma well_ord_unit: "well_ord({a},0)"
paulson@13140
   231
apply (unfold well_ord_def)
paulson@13701
   232
apply (simp add: tot_ord_unit wf_on_any_0)
paulson@13140
   233
done
paulson@13140
   234
paulson@13140
   235
wenzelm@60770
   236
subsection\<open>Order-Isomorphisms\<close>
paulson@13356
   237
wenzelm@60770
   238
text\<open>Suppes calls them "similarities"\<close>
paulson@13356
   239
paulson@13140
   240
(** Order-preserving (monotone) maps **)
paulson@13140
   241
paulson@46953
   242
lemma mono_map_is_fun: "f \<in> mono_map(A,r,B,s) ==> f \<in> A->B"
paulson@13140
   243
by (simp add: mono_map_def)
paulson@13140
   244
paulson@13140
   245
lemma mono_map_is_inj:
paulson@46953
   246
    "[| linear(A,r);  wf[B](s);  f \<in> mono_map(A,r,B,s) |] ==> f \<in> inj(A,B)"
paulson@13140
   247
apply (unfold mono_map_def inj_def, clarify)
paulson@13140
   248
apply (erule_tac x=w and y=x in linearE, assumption+)
paulson@13140
   249
apply (force intro: apply_type dest: wf_on_not_refl)+
paulson@13140
   250
done
paulson@13140
   251
paulson@13140
   252
lemma ord_isoI:
paulson@46953
   253
    "[| f \<in> bij(A, B);
paulson@46953
   254
        !!x y. [| x \<in> A; y \<in> A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
paulson@46953
   255
     ==> f \<in> ord_iso(A,r,B,s)"
paulson@13140
   256
by (simp add: ord_iso_def)
paulson@13140
   257
paulson@13140
   258
lemma ord_iso_is_mono_map:
paulson@46953
   259
    "f \<in> ord_iso(A,r,B,s) ==> f \<in> mono_map(A,r,B,s)"
paulson@13140
   260
apply (simp add: ord_iso_def mono_map_def)
paulson@13140
   261
apply (blast dest!: bij_is_fun)
paulson@13140
   262
done
paulson@13140
   263
paulson@13140
   264
lemma ord_iso_is_bij:
paulson@46953
   265
    "f \<in> ord_iso(A,r,B,s) ==> f \<in> bij(A,B)"
paulson@13140
   266
by (simp add: ord_iso_def)
paulson@13140
   267
paulson@13140
   268
(*Needed?  But ord_iso_converse is!*)
paulson@13140
   269
lemma ord_iso_apply:
paulson@46953
   270
    "[| f \<in> ord_iso(A,r,B,s);  <x,y>: r;  x \<in> A;  y \<in> A |] ==> <f`x, f`y> \<in> s"
berghofe@13611
   271
by (simp add: ord_iso_def)
paulson@13140
   272
paulson@13140
   273
lemma ord_iso_converse:
paulson@46953
   274
    "[| f \<in> ord_iso(A,r,B,s);  <x,y>: s;  x \<in> B;  y \<in> B |]
paulson@46820
   275
     ==> <converse(f) ` x, converse(f) ` y> \<in> r"
paulson@13140
   276
apply (simp add: ord_iso_def, clarify)
paulson@13140
   277
apply (erule bspec [THEN bspec, THEN iffD2])
paulson@13140
   278
apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+
paulson@13140
   279
apply (auto simp add: right_inverse_bij)
paulson@13140
   280
done
paulson@13140
   281
paulson@13140
   282
paulson@13140
   283
(** Symmetry and Transitivity Rules **)
paulson@13140
   284
paulson@13140
   285
(*Reflexivity of similarity*)
paulson@13140
   286
lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)"
paulson@13140
   287
by (rule id_bij [THEN ord_isoI], simp)
paulson@13140
   288
paulson@13140
   289
(*Symmetry of similarity*)
paulson@46953
   290
lemma ord_iso_sym: "f \<in> ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
paulson@13140
   291
apply (simp add: ord_iso_def)
paulson@13140
   292
apply (auto simp add: right_inverse_bij bij_converse_bij
paulson@13140
   293
                      bij_is_fun [THEN apply_funtype])
paulson@13140
   294
done
paulson@13140
   295
paulson@13140
   296
(*Transitivity of similarity*)
paulson@13140
   297
lemma mono_map_trans:
paulson@46953
   298
    "[| g \<in> mono_map(A,r,B,s);  f \<in> mono_map(B,s,C,t) |]
paulson@13140
   299
     ==> (f O g): mono_map(A,r,C,t)"
paulson@13140
   300
apply (unfold mono_map_def)
paulson@13140
   301
apply (auto simp add: comp_fun)
paulson@13140
   302
done
paulson@13140
   303
paulson@13140
   304
(*Transitivity of similarity: the order-isomorphism relation*)
paulson@13140
   305
lemma ord_iso_trans:
paulson@46953
   306
    "[| g \<in> ord_iso(A,r,B,s);  f \<in> ord_iso(B,s,C,t) |]
paulson@13140
   307
     ==> (f O g): ord_iso(A,r,C,t)"
paulson@13140
   308
apply (unfold ord_iso_def, clarify)
paulson@13140
   309
apply (frule bij_is_fun [of f])
paulson@13140
   310
apply (frule bij_is_fun [of g])
paulson@13140
   311
apply (auto simp add: comp_bij)
paulson@13140
   312
done
paulson@13140
   313
paulson@13140
   314
(** Two monotone maps can make an order-isomorphism **)
paulson@13140
   315
paulson@13140
   316
lemma mono_ord_isoI:
paulson@46953
   317
    "[| f \<in> mono_map(A,r,B,s);  g \<in> mono_map(B,s,A,r);
paulson@46953
   318
        f O g = id(B);  g O f = id(A) |] ==> f \<in> ord_iso(A,r,B,s)"
paulson@13140
   319
apply (simp add: ord_iso_def mono_map_def, safe)
paulson@13140
   320
apply (intro fg_imp_bijective, auto)
paulson@46820
   321
apply (subgoal_tac "<g` (f`x), g` (f`y) > \<in> r")
paulson@13140
   322
apply (simp add: comp_eq_id_iff [THEN iffD1])
paulson@13140
   323
apply (blast intro: apply_funtype)
paulson@13140
   324
done
paulson@13140
   325
paulson@13140
   326
lemma well_ord_mono_ord_isoI:
paulson@13140
   327
     "[| well_ord(A,r);  well_ord(B,s);
paulson@46953
   328
         f \<in> mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
paulson@46953
   329
      ==> f \<in> ord_iso(A,r,B,s)"
paulson@13140
   330
apply (intro mono_ord_isoI, auto)
paulson@13140
   331
apply (frule mono_map_is_fun [THEN fun_is_rel])
paulson@13140
   332
apply (erule converse_converse [THEN subst], rule left_comp_inverse)
paulson@13140
   333
apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear
paulson@13140
   334
                    well_ord_is_wf)+
paulson@13140
   335
done
paulson@13140
   336
paulson@13140
   337
paulson@13140
   338
(** Order-isomorphisms preserve the ordering's properties **)
paulson@13140
   339
paulson@13140
   340
lemma part_ord_ord_iso:
paulson@46953
   341
    "[| part_ord(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
paulson@13140
   342
apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
paulson@13140
   343
apply (fast intro: bij_is_fun [THEN apply_type])
paulson@13140
   344
done
paulson@13140
   345
paulson@13140
   346
lemma linear_ord_iso:
paulson@46953
   347
    "[| linear(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> linear(A,r)"
paulson@13140
   348
apply (simp add: linear_def ord_iso_def, safe)
paulson@13339
   349
apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec])
paulson@13140
   350
apply (safe elim!: bij_is_fun [THEN apply_type])
paulson@13140
   351
apply (drule_tac t = "op ` (converse (f))" in subst_context)
paulson@13140
   352
apply (simp add: left_inverse_bij)
paulson@13140
   353
done
paulson@13140
   354
paulson@13140
   355
lemma wf_on_ord_iso:
paulson@46953
   356
    "[| wf[B](s);  f \<in> ord_iso(A,r,B,s) |] ==> wf[A](r)"
paulson@13140
   357
apply (simp add: wf_on_def wf_def ord_iso_def, safe)
paulson@46953
   358
apply (drule_tac x = "{f`z. z \<in> Z \<inter> A}" in spec)
paulson@13140
   359
apply (safe intro!: equalityI)
paulson@13140
   360
apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
paulson@13140
   361
done
paulson@13140
   362
paulson@13140
   363
lemma well_ord_ord_iso:
paulson@46953
   364
    "[| well_ord(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
paulson@13140
   365
apply (unfold well_ord_def tot_ord_def)
paulson@13140
   366
apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
paulson@13140
   367
done
paulson@9683
   368
paulson@9683
   369
wenzelm@60770
   370
subsection\<open>Main results of Kunen, Chapter 1 section 6\<close>
paulson@13140
   371
paulson@13140
   372
(*Inductive argument for Kunen's Lemma 6.1, etc.
paulson@13140
   373
  Simple proof from Halmos, page 72*)
paulson@13140
   374
lemma well_ord_iso_subset_lemma:
paulson@46953
   375
     "[| well_ord(A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A |]
paulson@13140
   376
      ==> ~ <f`y, y>: r"
paulson@13140
   377
apply (simp add: well_ord_def ord_iso_def)
paulson@13140
   378
apply (elim conjE CollectE)
paulson@13140
   379
apply (rule_tac a=y in wf_on_induct, assumption+)
paulson@13140
   380
apply (blast dest: bij_is_fun [THEN apply_type])
paulson@13140
   381
done
paulson@13140
   382
paulson@46953
   383
(*Kunen's Lemma 6.1 \<in> there's no order-isomorphism to an initial segment
paulson@13140
   384
                     of a well-ordering*)
paulson@13140
   385
lemma well_ord_iso_predE:
paulson@46953
   386
     "[| well_ord(A,r);  f \<in> ord_iso(A, r, pred(A,x,r), r);  x \<in> A |] ==> P"
paulson@13140
   387
apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
paulson@13140
   388
apply (simp add: pred_subset)
paulson@13140
   389
(*Now we know  f`x < x *)
paulson@13140
   390
apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
paulson@46820
   391
(*Now we also know @{term"f`x \<in> pred(A,x,r)"}: contradiction! *)
paulson@13140
   392
apply (simp add: well_ord_def pred_def)
paulson@13140
   393
done
paulson@13140
   394
paulson@13140
   395
(*Simple consequence of Lemma 6.1*)
paulson@13140
   396
lemma well_ord_iso_pred_eq:
paulson@46820
   397
     "[| well_ord(A,r);  f \<in> ord_iso(pred(A,a,r), r, pred(A,c,r), r);
paulson@46953
   398
         a \<in> A;  c \<in> A |] ==> a=c"
paulson@13140
   399
apply (frule well_ord_is_trans_on)
paulson@13140
   400
apply (frule well_ord_is_linear)
paulson@13140
   401
apply (erule_tac x=a and y=c in linearE, assumption+)
paulson@13140
   402
apply (drule ord_iso_sym)
paulson@13140
   403
(*two symmetric cases*)
paulson@13140
   404
apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE]
paulson@13140
   405
            intro!: predI
paulson@13140
   406
            simp add: trans_pred_pred_eq)
paulson@13140
   407
done
paulson@13140
   408
paulson@13140
   409
(*Does not assume r is a wellordering!*)
paulson@13140
   410
lemma ord_iso_image_pred:
paulson@46953
   411
     "[|f \<in> ord_iso(A,r,B,s);  a \<in> A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
paulson@13140
   412
apply (unfold ord_iso_def pred_def)
paulson@13140
   413
apply (erule CollectE)
paulson@13140
   414
apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
paulson@13140
   415
apply (rule equalityI)
paulson@13140
   416
apply (safe elim!: bij_is_fun [THEN apply_type])
paulson@13140
   417
apply (rule RepFun_eqI)
paulson@13140
   418
apply (blast intro!: right_inverse_bij [symmetric])
paulson@13140
   419
apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
paulson@13140
   420
done
paulson@13140
   421
paulson@13212
   422
lemma ord_iso_restrict_image:
paulson@46820
   423
     "[| f \<in> ord_iso(A,r,B,s);  C<=A |]
paulson@46820
   424
      ==> restrict(f,C) \<in> ord_iso(C, r, f``C, s)"
paulson@46820
   425
apply (simp add: ord_iso_def)
paulson@46820
   426
apply (blast intro: bij_is_inj restrict_bij)
paulson@13212
   427
done
paulson@13212
   428
paulson@13140
   429
(*But in use, A and B may themselves be initial segments.  Then use
paulson@13140
   430
  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
paulson@13212
   431
lemma ord_iso_restrict_pred:
paulson@46953
   432
   "[| f \<in> ord_iso(A,r,B,s);   a \<in> A |]
paulson@46820
   433
    ==> restrict(f, pred(A,a,r)) \<in> ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
paulson@46820
   434
apply (simp add: ord_iso_image_pred [symmetric])
paulson@46820
   435
apply (blast intro: ord_iso_restrict_image elim: predE)
paulson@13140
   436
done
paulson@13140
   437
paulson@13140
   438
(*Tricky; a lot of forward proof!*)
paulson@13140
   439
lemma well_ord_iso_preserving:
paulson@13140
   440
     "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;
paulson@46820
   441
         f \<in> ord_iso(pred(A,a,r), r, pred(B,b,s), s);
paulson@46820
   442
         g \<in> ord_iso(pred(A,c,r), r, pred(B,d,s), s);
paulson@46953
   443
         a \<in> A;  c \<in> A;  b \<in> B;  d \<in> B |] ==> <b,d>: s"
paulson@13140
   444
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
paulson@13140
   445
apply (subgoal_tac "b = g`a")
paulson@13140
   446
apply (simp (no_asm_simp))
paulson@13140
   447
apply (rule well_ord_iso_pred_eq, auto)
paulson@13140
   448
apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+)
paulson@13140
   449
apply (simp add: well_ord_is_trans_on trans_pred_pred_eq)
paulson@13140
   450
apply (erule ord_iso_sym [THEN ord_iso_trans], assumption)
paulson@13140
   451
done
paulson@13140
   452
paulson@13140
   453
(*See Halmos, page 72*)
paulson@13140
   454
lemma well_ord_iso_unique_lemma:
paulson@13140
   455
     "[| well_ord(A,r);
paulson@46953
   456
         f \<in> ord_iso(A,r, B,s);  g \<in> ord_iso(A,r, B,s);  y \<in> A |]
paulson@46820
   457
      ==> ~ <g`y, f`y> \<in> s"
paulson@13140
   458
apply (frule well_ord_iso_subset_lemma)
paulson@13140
   459
apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
paulson@13140
   460
apply auto
paulson@13140
   461
apply (blast intro: ord_iso_sym)
paulson@13140
   462
apply (frule ord_iso_is_bij [of f])
paulson@13140
   463
apply (frule ord_iso_is_bij [of g])
paulson@13140
   464
apply (frule ord_iso_converse)
paulson@13140
   465
apply (blast intro!: bij_converse_bij
paulson@13140
   466
             intro: bij_is_fun apply_funtype)+
paulson@13140
   467
apply (erule notE)
paulson@13176
   468
apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B])
paulson@13140
   469
done
paulson@13140
   470
paulson@13140
   471
paulson@13140
   472
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
paulson@13140
   473
lemma well_ord_iso_unique: "[| well_ord(A,r);
paulson@46953
   474
         f \<in> ord_iso(A,r, B,s);  g \<in> ord_iso(A,r, B,s) |] ==> f = g"
paulson@13140
   475
apply (rule fun_extension)
paulson@13140
   476
apply (erule ord_iso_is_bij [THEN bij_is_fun])+
paulson@46820
   477
apply (subgoal_tac "f`x \<in> B & g`x \<in> B & linear(B,s)")
paulson@13140
   478
 apply (simp add: linear_def)
paulson@13140
   479
 apply (blast dest: well_ord_iso_unique_lemma)
paulson@13140
   480
apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
paulson@13140
   481
                    well_ord_is_linear well_ord_ord_iso ord_iso_sym)
paulson@13140
   482
done
paulson@13140
   483
wenzelm@60770
   484
subsection\<open>Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation\<close>
paulson@13140
   485
paulson@46820
   486
lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) \<subseteq> A*B"
paulson@13140
   487
by (unfold ord_iso_map_def, blast)
paulson@13140
   488
paulson@46820
   489
lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) \<subseteq> A"
paulson@13140
   490
by (unfold ord_iso_map_def, blast)
paulson@13140
   491
paulson@46820
   492
lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) \<subseteq> B"
paulson@13140
   493
by (unfold ord_iso_map_def, blast)
paulson@13140
   494
paulson@13140
   495
lemma converse_ord_iso_map:
paulson@13140
   496
    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
paulson@13140
   497
apply (unfold ord_iso_map_def)
paulson@13140
   498
apply (blast intro: ord_iso_sym)
paulson@13140
   499
done
paulson@13140
   500
paulson@13140
   501
lemma function_ord_iso_map:
paulson@13140
   502
    "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"
paulson@13140
   503
apply (unfold ord_iso_map_def function_def)
paulson@13140
   504
apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
paulson@13140
   505
done
paulson@13140
   506
paulson@13140
   507
lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s)
paulson@46820
   508
           \<in> domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"
paulson@13140
   509
by (simp add: Pi_iff function_ord_iso_map
paulson@13140
   510
                 ord_iso_map_subset [THEN domain_times_range])
paulson@13140
   511
paulson@13140
   512
lemma ord_iso_map_mono_map:
paulson@13140
   513
    "[| well_ord(A,r);  well_ord(B,s) |]
paulson@13140
   514
     ==> ord_iso_map(A,r,B,s)
paulson@46820
   515
           \<in> mono_map(domain(ord_iso_map(A,r,B,s)), r,
paulson@13140
   516
                      range(ord_iso_map(A,r,B,s)), s)"
paulson@13140
   517
apply (unfold mono_map_def)
paulson@13140
   518
apply (simp (no_asm_simp) add: ord_iso_map_fun)
paulson@13140
   519
apply safe
paulson@46953
   520
apply (subgoal_tac "x \<in> A & ya:A & y \<in> B & yb:B")
paulson@13140
   521
 apply (simp add: apply_equality [OF _  ord_iso_map_fun])
paulson@13140
   522
 apply (unfold ord_iso_map_def)
paulson@13140
   523
 apply (blast intro: well_ord_iso_preserving, blast)
paulson@13140
   524
done
paulson@13140
   525
paulson@13140
   526
lemma ord_iso_map_ord_iso:
paulson@13140
   527
    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)
paulson@46820
   528
           \<in> ord_iso(domain(ord_iso_map(A,r,B,s)), r,
paulson@13140
   529
                      range(ord_iso_map(A,r,B,s)), s)"
paulson@13140
   530
apply (rule well_ord_mono_ord_isoI)
paulson@13140
   531
   prefer 4
paulson@13140
   532
   apply (rule converse_ord_iso_map [THEN subst])
paulson@13140
   533
   apply (simp add: ord_iso_map_mono_map
wenzelm@32960
   534
                    ord_iso_map_subset [THEN converse_converse])
paulson@13140
   535
apply (blast intro!: domain_ord_iso_map range_ord_iso_map
paulson@13140
   536
             intro: well_ord_subset ord_iso_map_mono_map)+
paulson@13140
   537
done
paulson@13140
   538
paulson@13140
   539
paulson@13140
   540
(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
paulson@13140
   541
lemma domain_ord_iso_map_subset:
paulson@13140
   542
     "[| well_ord(A,r);  well_ord(B,s);
paulson@46953
   543
         a \<in> A;  a \<notin> domain(ord_iso_map(A,r,B,s)) |]
paulson@46820
   544
      ==>  domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)"
paulson@13140
   545
apply (unfold ord_iso_map_def)
paulson@13140
   546
apply (safe intro!: predI)
paulson@13140
   547
(*Case analysis on  xa vs a in r *)
paulson@13140
   548
apply (simp (no_asm_simp))
paulson@13140
   549
apply (frule_tac A = A in well_ord_is_linear)
paulson@13140
   550
apply (rename_tac b y f)
paulson@13140
   551
apply (erule_tac x=b and y=a in linearE, assumption+)
paulson@13140
   552
(*Trivial case: b=a*)
paulson@13140
   553
apply clarify
paulson@13140
   554
apply blast
paulson@13140
   555
(*Harder case: <a, xa>: r*)
paulson@13140
   556
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type],
paulson@13140
   557
       (erule asm_rl predI predE)+)
paulson@13140
   558
apply (frule ord_iso_restrict_pred)
paulson@13140
   559
 apply (simp add: pred_iff)
paulson@13140
   560
apply (simp split: split_if_asm
paulson@13140
   561
          add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast)
paulson@13140
   562
done
paulson@13140
   563
paulson@13140
   564
(*For the 4-way case analysis in the main result*)
paulson@13140
   565
lemma domain_ord_iso_map_cases:
paulson@13140
   566
     "[| well_ord(A,r);  well_ord(B,s) |]
paulson@13140
   567
      ==> domain(ord_iso_map(A,r,B,s)) = A |
paulson@46820
   568
          (\<exists>x\<in>A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
paulson@13140
   569
apply (frule well_ord_is_wf)
paulson@13140
   570
apply (unfold wf_on_def wf_def)
paulson@13140
   571
apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
paulson@13140
   572
apply safe
paulson@13140
   573
(*The first case: the domain equals A*)
paulson@13140
   574
apply (rule domain_ord_iso_map [THEN equalityI])
paulson@13140
   575
apply (erule Diff_eq_0_iff [THEN iffD1])
paulson@13140
   576
(*The other case: the domain equals an initial segment*)
paulson@13140
   577
apply (blast del: domainI subsetI
wenzelm@32960
   578
             elim!: predE
wenzelm@32960
   579
             intro!: domain_ord_iso_map_subset
paulson@13140
   580
             intro: subsetI)+
paulson@13140
   581
done
paulson@13140
   582
paulson@13140
   583
(*As above, by duality*)
paulson@13140
   584
lemma range_ord_iso_map_cases:
paulson@13140
   585
    "[| well_ord(A,r);  well_ord(B,s) |]
paulson@13140
   586
     ==> range(ord_iso_map(A,r,B,s)) = B |
paulson@46820
   587
         (\<exists>y\<in>B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))"
paulson@13140
   588
apply (rule converse_ord_iso_map [THEN subst])
paulson@13140
   589
apply (simp add: domain_ord_iso_map_cases)
paulson@13140
   590
done
paulson@13140
   591
wenzelm@60770
   592
text\<open>Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets\<close>
paulson@13356
   593
theorem well_ord_trichotomy:
paulson@13140
   594
   "[| well_ord(A,r);  well_ord(B,s) |]
paulson@46820
   595
    ==> ord_iso_map(A,r,B,s) \<in> ord_iso(A, r, B, s) |
paulson@46820
   596
        (\<exists>x\<in>A. ord_iso_map(A,r,B,s) \<in> ord_iso(pred(A,x,r), r, B, s)) |
paulson@46820
   597
        (\<exists>y\<in>B. ord_iso_map(A,r,B,s) \<in> ord_iso(A, r, pred(B,y,s), s))"
paulson@13140
   598
apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)
paulson@13140
   599
apply (frule_tac B = B in range_ord_iso_map_cases, assumption)
paulson@13140
   600
apply (drule ord_iso_map_ord_iso, assumption)
paulson@13140
   601
apply (elim disjE bexE)
paulson@13140
   602
   apply (simp_all add: bexI)
paulson@13140
   603
apply (rule wf_on_not_refl [THEN notE])
paulson@13140
   604
  apply (erule well_ord_is_wf)
paulson@13140
   605
 apply assumption
paulson@13140
   606
apply (subgoal_tac "<x,y>: ord_iso_map (A,r,B,s) ")
paulson@13140
   607
 apply (drule rangeI)
paulson@13140
   608
 apply (simp add: pred_def)
paulson@13140
   609
apply (unfold ord_iso_map_def, blast)
paulson@13140
   610
done
paulson@13140
   611
paulson@13140
   612
wenzelm@60770
   613
subsection\<open>Miscellaneous Results by Krzysztof Grabczewski\<close>
paulson@13356
   614
paulson@13356
   615
(** Properties of converse(r) **)
paulson@13140
   616
paulson@13140
   617
lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
paulson@13140
   618
by (unfold irrefl_def, blast)
paulson@13140
   619
paulson@13140
   620
lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"
paulson@13140
   621
by (unfold trans_on_def, blast)
paulson@13140
   622
paulson@13140
   623
lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))"
paulson@13140
   624
apply (unfold part_ord_def)
paulson@13140
   625
apply (blast intro!: irrefl_converse trans_on_converse)
paulson@13140
   626
done
paulson@13140
   627
paulson@13140
   628
lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))"
paulson@13140
   629
by (unfold linear_def, blast)
paulson@13140
   630
paulson@13140
   631
lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))"
paulson@13140
   632
apply (unfold tot_ord_def)
paulson@13140
   633
apply (blast intro!: part_ord_converse linear_converse)
paulson@13140
   634
done
paulson@13140
   635
paulson@13140
   636
paulson@13140
   637
(** By Krzysztof Grabczewski.
paulson@13140
   638
    Lemmas involving the first element of a well ordered set **)
paulson@13140
   639
paulson@46953
   640
lemma first_is_elem: "first(b,B,r) ==> b \<in> B"
paulson@13140
   641
by (unfold first_def, blast)
paulson@13140
   642
paulson@13140
   643
lemma well_ord_imp_ex1_first:
paulson@46820
   644
        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (EX! b. first(b,B,r))"
paulson@13140
   645
apply (unfold well_ord_def wf_on_def wf_def first_def)
paulson@13140
   646
apply (elim conjE allE disjE, blast)
paulson@13140
   647
apply (erule bexE)
paulson@13140
   648
apply (rule_tac a = x in ex1I, auto)
paulson@13140
   649
apply (unfold tot_ord_def linear_def, blast)
paulson@13140
   650
done
paulson@13140
   651
paulson@13140
   652
lemma the_first_in:
paulson@46820
   653
     "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (THE b. first(b,B,r)) \<in> B"
paulson@13140
   654
apply (drule well_ord_imp_ex1_first, assumption+)
paulson@13140
   655
apply (rule first_is_elem)
paulson@13140
   656
apply (erule theI)
paulson@13140
   657
done
paulson@13140
   658
ballarin@27703
   659
wenzelm@60770
   660
subsection \<open>Lemmas for the Reflexive Orders\<close>
ballarin@27703
   661
ballarin@27703
   662
lemma subset_vimage_vimage_iff:
ballarin@27703
   663
  "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
paulson@46821
   664
  r -`` A \<subseteq> r -`` B \<longleftrightarrow> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
ballarin@27703
   665
  apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
ballarin@27703
   666
   apply blast
ballarin@27703
   667
  unfolding trans_on_def
wenzelm@59788
   668
  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
wenzelm@59788
   669
          \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
ballarin@27703
   670
    (* instance obtained from proof term generated by best *)
ballarin@27703
   671
   apply best
ballarin@27703
   672
  apply blast
ballarin@27703
   673
  done
ballarin@27703
   674
ballarin@27703
   675
lemma subset_vimage1_vimage1_iff:
paulson@46820
   676
  "[| Preorder(r); a \<in> field(r); b \<in> field(r) |] ==>
paulson@46821
   677
  r -`` {a} \<subseteq> r -`` {b} \<longleftrightarrow> <a, b> \<in> r"
ballarin@27703
   678
  by (simp add: subset_vimage_vimage_iff)
ballarin@27703
   679
ballarin@27703
   680
lemma Refl_antisym_eq_Image1_Image1_iff:
paulson@46820
   681
  "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
paulson@46821
   682
  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
ballarin@27703
   683
  apply rule
ballarin@27703
   684
   apply (frule equality_iffD)
ballarin@27703
   685
   apply (drule equality_iffD)
ballarin@27703
   686
   apply (simp add: antisym_def refl_def)
ballarin@27703
   687
   apply best
ballarin@27703
   688
  apply (simp add: antisym_def refl_def)
ballarin@27703
   689
  done
ballarin@27703
   690
ballarin@27703
   691
lemma Partial_order_eq_Image1_Image1_iff:
paulson@46820
   692
  "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
paulson@46821
   693
  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
ballarin@27703
   694
  by (simp add: partial_order_on_def preorder_on_def
ballarin@27703
   695
    Refl_antisym_eq_Image1_Image1_iff)
ballarin@27703
   696
ballarin@27703
   697
lemma Refl_antisym_eq_vimage1_vimage1_iff:
paulson@46820
   698
  "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
paulson@46821
   699
  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
ballarin@27703
   700
  apply rule
ballarin@27703
   701
   apply (frule equality_iffD)
ballarin@27703
   702
   apply (drule equality_iffD)
ballarin@27703
   703
   apply (simp add: antisym_def refl_def)
ballarin@27703
   704
   apply best
ballarin@27703
   705
  apply (simp add: antisym_def refl_def)
ballarin@27703
   706
  done
ballarin@27703
   707
ballarin@27703
   708
lemma Partial_order_eq_vimage1_vimage1_iff:
paulson@46820
   709
  "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
paulson@46821
   710
  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
ballarin@27703
   711
  by (simp add: partial_order_on_def preorder_on_def
ballarin@27703
   712
    Refl_antisym_eq_vimage1_vimage1_iff)
ballarin@27703
   713
lcp@435
   714
end