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