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