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