src/ZF/Order.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1791 6b38717439c6
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
     1
(*  Title:      ZF/Order.ML
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
     6
Orders in Zermelo-Fraenkel Set Theory 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
     7
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
     8
Results from the book "Set Theory: an Introduction to Independence Proofs"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
     9
        by Ken Kunen.  Chapter 1, section 6.
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    12
open Order;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
val bij_apply_cs = ZF_cs addSEs [bij_converse_bij]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    15
                         addIs  [bij_is_fun, apply_type];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    16
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    17
(** Basic properties of the definitions **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    19
(*needed?*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    20
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    21
    "!!r. part_ord(A,r) ==> asym(r Int A*A)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
    23
qed "part_ord_Imp_asym";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    24
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    25
val major::premx::premy::prems = goalw Order.thy [linear_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    26
    "[| linear(A,r);  x:A;  y:A;  \
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    27
\       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    28
by (cut_facts_tac [major,premx,premy] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    29
by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    30
by (EVERY1 (map etac prems));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    31
by (ALLGOALS contr_tac);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    32
qed "linearE";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    33
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    34
(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    35
val linear_case_tac =
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    36
    SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
    37
                        REPEAT_SOME (assume_tac ORELSE' contr_tac)]);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    38
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    39
(** General properties of well_ord **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    40
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    41
goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
    42
                 trans_on_def, well_ord_def]
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    43
    "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    44
by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1);
990
9ec3c7bd774e Tried the new addss in many proofs, and tidied others involving simplification.
lcp
parents: 848
diff changeset
    45
by (fast_tac (ZF_cs addEs [linearE, wf_on_asym, wf_on_chain3]) 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    46
qed "well_ordI";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    47
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    48
goalw Order.thy [well_ord_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    49
    "!!r. well_ord(A,r) ==> wf[A](r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    50
by (safe_tac ZF_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    51
qed "well_ord_is_wf";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    52
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    53
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    54
    "!!r. well_ord(A,r) ==> trans[A](r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    55
by (safe_tac ZF_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    56
qed "well_ord_is_trans_on";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    57
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    58
goalw Order.thy [well_ord_def, tot_ord_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    59
  "!!r. well_ord(A,r) ==> linear(A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    60
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    61
qed "well_ord_is_linear";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    62
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    63
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    64
(** Derived rules for pred(A,x,r) **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    65
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    66
goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    67
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    68
qed "pred_iff";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    69
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    70
bind_thm ("predI", conjI RS (pred_iff RS iffD2));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    71
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    72
val [major,minor] = goalw Order.thy [pred_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    73
    "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    74
by (rtac (major RS CollectE) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    75
by (REPEAT (ares_tac [minor] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    76
qed "predE";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    77
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    78
goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    79
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    80
qed "pred_subset_under";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    81
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    82
goalw Order.thy [pred_def] "pred(A,x,r) <= A";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    83
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    84
qed "pred_subset";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    85
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    86
goalw Order.thy [pred_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    87
    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    88
by (fast_tac eq_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    89
qed "pred_pred_eq";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    90
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    91
goalw Order.thy [trans_on_def, pred_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    92
    "!!r. [| trans[A](r);  <y,x>:r;  x:A;  y:A \
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    93
\         |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    94
by (fast_tac eq_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    95
qed "trans_pred_pred_eq";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    96
836
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
    97
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    98
(** The ordering's properties hold over all subsets of its domain 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
    99
    [including initial segments of the form pred(A,x,r) **)
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   100
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   101
(*Note: a relation s such that s<=r need not be a partial ordering*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   102
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   103
    "!!A B r. [| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   104
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   105
qed "part_ord_subset";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   106
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   107
goalw Order.thy [linear_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   108
    "!!A B r. [| linear(A,r);  B<=A |] ==> linear(B,r)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   109
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   110
qed "linear_subset";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   111
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   112
goalw Order.thy [tot_ord_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   113
    "!!A B r. [| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   114
by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   115
qed "tot_ord_subset";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   116
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   117
goalw Order.thy [well_ord_def]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   118
    "!!A B r. [| well_ord(A,r);  B<=A |] ==> well_ord(B,r)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   119
by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   120
qed "well_ord_subset";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   121
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
   122
836
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   123
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   124
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   125
goalw Order.thy [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   126
by (fast_tac ZF_cs 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   127
qed "irrefl_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   128
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   129
goalw Order.thy [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   130
by (fast_tac ZF_cs 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   131
qed "trans_on_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   132
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   133
goalw Order.thy [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   134
by (simp_tac (ZF_ss addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   135
qed "part_ord_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   136
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   137
goalw Order.thy [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   138
by (fast_tac ZF_cs 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   139
qed "linear_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   140
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   141
goalw Order.thy [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   142
by (simp_tac (ZF_ss addsimps [part_ord_Int_iff, linear_Int_iff]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   143
qed "tot_ord_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   144
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   145
goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   146
by (fast_tac ZF_cs 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   147
qed "wf_on_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   148
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   149
goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   150
by (simp_tac (ZF_ss addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   151
qed "well_ord_Int_iff";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   152
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   153
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   154
(** Relations over the Empty Set **)
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   155
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   156
goalw Order.thy [irrefl_def] "irrefl(0,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   157
by (fast_tac ZF_cs 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   158
qed "irrefl_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   159
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   160
goalw Order.thy [trans_on_def] "trans[0](r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   161
by (fast_tac ZF_cs 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   162
qed "trans_on_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   163
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   164
goalw Order.thy [part_ord_def] "part_ord(0,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   165
by (simp_tac (ZF_ss addsimps [irrefl_0, trans_on_0]) 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   166
qed "part_ord_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   167
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   168
goalw Order.thy [linear_def] "linear(0,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   169
by (fast_tac ZF_cs 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   170
qed "linear_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   171
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   172
goalw Order.thy [tot_ord_def] "tot_ord(0,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   173
by (simp_tac (ZF_ss addsimps [part_ord_0, linear_0]) 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   174
qed "tot_ord_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   175
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   176
goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   177
by (fast_tac eq_cs 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   178
qed "wf_on_0";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   179
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   180
goalw Order.thy [well_ord_def] "well_ord(0,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   181
by (simp_tac (ZF_ss addsimps [tot_ord_0, wf_on_0]) 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   182
qed "well_ord_0";
836
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   183
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   184
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   185
(** Order-preserving (monotone) maps **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   186
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   187
goalw Order.thy [mono_map_def] 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   188
    "!!f. f: mono_map(A,r,B,s) ==> f: A->B";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   189
by (etac CollectD1 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   190
qed "mono_map_is_fun";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   191
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   192
goalw Order.thy [mono_map_def, inj_def] 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   193
    "!!f. [| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   194
by (step_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   195
by (linear_case_tac 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   196
by (REPEAT 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   197
    (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   198
            etac ssubst 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   199
            fast_tac ZF_cs 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   200
            REPEAT (ares_tac [apply_type] 1)]));
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   201
qed "mono_map_is_inj";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   202
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   203
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   204
(** Order-isomorphisms -- or similarities, as Suppes calls them **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   205
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   206
val prems = goalw Order.thy [ord_iso_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   207
    "[| f: bij(A, B);   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   208
\       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   209
\    |] ==> f: ord_iso(A,r,B,s)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   210
by (fast_tac (ZF_cs addSIs prems) 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   211
qed "ord_isoI";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   212
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   213
goalw Order.thy [ord_iso_def, mono_map_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   214
    "!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   215
by (fast_tac (ZF_cs addSDs [bij_is_fun]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   216
qed "ord_iso_is_mono_map";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   217
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   218
goalw Order.thy [ord_iso_def] 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   219
    "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   220
by (etac CollectD1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   221
qed "ord_iso_is_bij";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   222
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   223
(*Needed?  But ord_iso_converse is!*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   224
goalw Order.thy [ord_iso_def] 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   225
    "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   226
\         <f`x, f`y> : s";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   227
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   228
qed "ord_iso_apply";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   229
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   230
goalw Order.thy [ord_iso_def] 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   231
    "!!f. [| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   232
\         <converse(f) ` x, converse(f) ` y> : r";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   233
by (etac CollectE 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   234
by (etac (bspec RS bspec RS iffD2) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   235
by (REPEAT (eresolve_tac [asm_rl, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   236
                          bij_converse_bij RS bij_is_fun RS apply_type] 1));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   237
by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   238
qed "ord_iso_converse";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   239
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   240
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   241
(*Rewriting with bijections and converse (function inverse)*)
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   242
val bij_inverse_ss = 
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   243
    ZF_ss setsolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   244
                                    bij_converse_bij, comp_fun, comp_bij])
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   245
          addsimps [right_inverse_bij, left_inverse_bij, comp_fun_apply];
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   246
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   247
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   248
(** Symmetry and Transitivity Rules **)
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   249
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   250
(*Reflexivity of similarity*)
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   251
goal Order.thy "id(A): ord_iso(A,r,A,r)";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   252
by (resolve_tac [id_bij RS ord_isoI] 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   253
by (asm_simp_tac (ZF_ss addsimps [id_conv]) 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   254
qed "ord_iso_refl";
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   255
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   256
(*Symmetry of similarity*)
769
66cdfde4ec5d not_well_ord_iso_pred: removed needless quantifier
lcp
parents: 760
diff changeset
   257
goalw Order.thy [ord_iso_def] 
66cdfde4ec5d not_well_ord_iso_pred: removed needless quantifier
lcp
parents: 760
diff changeset
   258
    "!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
990
9ec3c7bd774e Tried the new addss in many proofs, and tidied others involving simplification.
lcp
parents: 848
diff changeset
   259
by (fast_tac (ZF_cs addss bij_inverse_ss) 1);
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 769
diff changeset
   260
qed "ord_iso_sym";
769
66cdfde4ec5d not_well_ord_iso_pred: removed needless quantifier
lcp
parents: 760
diff changeset
   261
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   262
(*Transitivity of similarity*)
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   263
goalw Order.thy [mono_map_def] 
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   264
    "!!f. [| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |] ==> \
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   265
\         (f O g): mono_map(A,r,C,t)";
990
9ec3c7bd774e Tried the new addss in many proofs, and tidied others involving simplification.
lcp
parents: 848
diff changeset
   266
by (fast_tac (ZF_cs addss bij_inverse_ss) 1);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   267
qed "mono_map_trans";
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   268
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   269
(*Transitivity of similarity: the order-isomorphism relation*)
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   270
goalw Order.thy [ord_iso_def] 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   271
    "!!f. [| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |] ==> \
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   272
\         (f O g): ord_iso(A,r,C,t)";
990
9ec3c7bd774e Tried the new addss in many proofs, and tidied others involving simplification.
lcp
parents: 848
diff changeset
   273
by (fast_tac (ZF_cs addss bij_inverse_ss) 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   274
qed "ord_iso_trans";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   275
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   276
(** Two monotone maps can make an order-isomorphism **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   277
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   278
goalw Order.thy [ord_iso_def, mono_map_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   279
    "!!f g. [| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);     \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   280
\              f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   281
by (safe_tac ZF_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   282
by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   283
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   284
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   285
by (fast_tac (ZF_cs addIs [apply_type] addSEs [bspec RS bspec RS mp]) 2);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   286
by (asm_full_simp_tac 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   287
    (ZF_ss addsimps [comp_eq_id_iff RS iffD1]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   288
qed "mono_ord_isoI";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   289
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   290
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   291
    "!!B. [| well_ord(A,r);  well_ord(B,s);                             \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   292
\            f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r)      \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   293
\         |] ==> f: ord_iso(A,r,B,s)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   294
by (REPEAT (ares_tac [mono_ord_isoI] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   295
by (forward_tac [mono_map_is_fun RS fun_is_rel] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   296
by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   297
by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   298
          ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   299
qed "well_ord_mono_ord_isoI";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   300
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   301
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   302
(** Order-isomorphisms preserve the ordering's properties **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   303
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   304
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   305
    "!!A B r. [| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   306
by (asm_simp_tac ZF_ss 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   307
by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   308
qed "part_ord_ord_iso";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   309
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   310
goalw Order.thy [linear_def, ord_iso_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   311
    "!!A B r. [| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   312
by (asm_simp_tac ZF_ss 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   313
by (safe_tac ZF_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   314
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   315
by (safe_tac (ZF_cs addSEs [bij_is_fun RS apply_type]));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   316
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   317
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   318
qed "linear_ord_iso";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   319
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   320
goalw Order.thy [wf_on_def, wf_def, ord_iso_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   321
    "!!A B r. [| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   322
(*reversed &-congruence rule handles context of membership in A*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   323
by (asm_full_simp_tac (ZF_ss addcongs [conj_cong2]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   324
by (safe_tac ZF_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   325
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   326
by (safe_tac eq_cs);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   327
by (dtac equalityD1 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   328
by (fast_tac (ZF_cs addSIs [bexI]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   329
by (fast_tac (ZF_cs addSIs [bexI]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   330
              addIs [bij_is_fun RS apply_type]) 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   331
qed "wf_on_ord_iso";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   332
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   333
goalw Order.thy [well_ord_def, tot_ord_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   334
    "!!A B r. [| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   335
by (fast_tac
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   336
    (ZF_cs addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   337
qed "well_ord_ord_iso";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   338
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   339
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   340
(*** Main results of Kunen, Chapter 1 section 6 ***)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   341
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   342
(*Inductive argument for Kunen's Lemma 6.1, etc. 
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   343
  Simple proof from Halmos, page 72*)
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   344
goalw Order.thy [well_ord_def, ord_iso_def]
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   345
  "!!r. [| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |] \
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   346
\       ==> ~ <f`y, y>: r";
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   347
by (REPEAT (eresolve_tac [conjE, CollectE] 1));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   348
by (wf_on_ind_tac "y" [] 1);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   349
by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   350
by (assume_tac 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   351
by (fast_tac ZF_cs 1);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   352
qed "well_ord_iso_subset_lemma";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   353
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   354
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   355
                     of a well-ordering*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   356
goal Order.thy
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   357
    "!!r. [| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   358
by (metacut_tac well_ord_iso_subset_lemma 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   359
by (REPEAT_FIRST (ares_tac [pred_subset]));
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   360
(*Now we know  f`x < x *)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   361
by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   362
             assume_tac]);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   363
(*Now we also know f`x : pred(A,x,r);  contradiction! *)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   364
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   365
qed "well_ord_iso_predE";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   366
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   367
(*Simple consequence of Lemma 6.1*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   368
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   369
 "!!r. [| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   370
\         a:A;  c:A |] ==> a=c";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   371
by (forward_tac [well_ord_is_trans_on] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   372
by (forward_tac [well_ord_is_linear] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   373
by (linear_case_tac 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   374
by (dtac ord_iso_sym 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   375
by (REPEAT   (*because there are two symmetric cases*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   376
    (EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   377
                          well_ord_iso_predE] 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   378
            fast_tac (ZF_cs addSIs [predI]) 2,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   379
            asm_simp_tac (ZF_ss addsimps [trans_pred_pred_eq]) 1]));
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   380
qed "well_ord_iso_pred_eq";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   381
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   382
(*Does not assume r is a wellordering!*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   383
goalw Order.thy [ord_iso_def, pred_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   384
 "!!r. [| f : ord_iso(A,r,B,s);   a:A |] ==>    \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   385
\      f `` pred(A,a,r) = pred(B, f`a, s)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   386
by (etac CollectE 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   387
by (asm_simp_tac 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   388
    (ZF_ss addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   389
by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type]));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   390
by (rtac RepFun_eqI 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   391
by (fast_tac (ZF_cs addSIs [right_inverse_bij RS sym]) 1);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   392
by (asm_simp_tac bij_inverse_ss 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   393
qed "ord_iso_image_pred";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   394
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   395
(*But in use, A and B may themselves be initial segments.  Then use
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   396
  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   397
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   398
 "!!r. [| f : ord_iso(A,r,B,s);   a:A |] ==>    \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   399
\      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   400
by (asm_simp_tac (ZF_ss addsimps [ord_iso_image_pred RS sym]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   401
by (rewtac ord_iso_def);
848
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   402
by (etac CollectE 1);
b1dc15d86081 Proved ord_isoI, ord_iso_refl. Simplified proof of
lcp
parents: 836
diff changeset
   403
by (rtac CollectI 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   404
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 2);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   405
by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   406
qed "ord_iso_restrict_pred";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   407
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   408
(*Tricky; a lot of forward proof!*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   409
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   410
 "!!r. [| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   411
\         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   412
\         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);  \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   413
\         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   414
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   415
    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   416
by (subgoal_tac "b = g`a" 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   417
by (asm_simp_tac ZF_ss 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   418
by (rtac well_ord_iso_pred_eq 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   419
by (REPEAT_SOME assume_tac);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   420
by (forward_tac [ord_iso_restrict_pred] 1  THEN
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   421
    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   422
by (asm_full_simp_tac
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   423
    (ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   424
by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   425
by (assume_tac 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   426
qed "well_ord_iso_preserving";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   427
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   428
(*See Halmos, page 72*)
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   429
goal Order.thy
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   430
    "!!r. [| well_ord(A,r);  \
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   431
\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   432
\         ==> ~ <g`y, f`y> : s";
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   433
by (forward_tac [well_ord_iso_subset_lemma] 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   434
by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   435
by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   436
by (safe_tac ZF_cs);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   437
by (forward_tac [ord_iso_converse] 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   438
by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 1));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   439
by (asm_full_simp_tac bij_inverse_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   440
qed "well_ord_iso_unique_lemma";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   441
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   442
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   443
goal Order.thy
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   444
    "!!r. [| well_ord(A,r);  \
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   445
\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   446
by (rtac fun_extension 1);
812
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   447
by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   448
by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   449
by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 3));
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   450
by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   451
by (asm_full_simp_tac (ZF_ss addsimps [tot_ord_def, well_ord_def]) 2);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   452
by (linear_case_tac 1);
bf4b7c37db2c Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents: 794
diff changeset
   453
by (DEPTH_SOLVE (eresolve_tac [asm_rl, well_ord_iso_unique_lemma RS notE] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 484
diff changeset
   454
qed "well_ord_iso_unique";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   455
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   456
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   457
(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   458
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   459
goalw Order.thy [ord_iso_map_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   460
    "ord_iso_map(A,r,B,s) <= A*B";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   461
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   462
qed "ord_iso_map_subset";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   463
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   464
goalw Order.thy [ord_iso_map_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   465
    "domain(ord_iso_map(A,r,B,s)) <= A";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   466
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   467
qed "domain_ord_iso_map";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   468
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   469
goalw Order.thy [ord_iso_map_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   470
    "range(ord_iso_map(A,r,B,s)) <= B";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   471
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   472
qed "range_ord_iso_map";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   473
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   474
goalw Order.thy [ord_iso_map_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   475
    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   476
by (fast_tac (eq_cs addIs [ord_iso_sym]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   477
qed "converse_ord_iso_map";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   478
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   479
goalw Order.thy [ord_iso_map_def, function_def]
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   480
    "!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   481
by (safe_tac ZF_cs);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   482
by (rtac well_ord_iso_pred_eq 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   483
by (REPEAT_SOME assume_tac);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   484
by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   485
by (assume_tac 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   486
qed "function_ord_iso_map";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   487
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   488
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   489
    "!!B. well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   490
\          : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   491
by (asm_simp_tac 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   492
    (ZF_ss addsimps [Pi_iff, function_ord_iso_map,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   493
                     ord_iso_map_subset RS domain_times_range]) 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   494
qed "ord_iso_map_fun";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   495
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   496
goalw Order.thy [mono_map_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   497
    "!!B. [| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   498
\          : mono_map(domain(ord_iso_map(A,r,B,s)), r,  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   499
\                     range(ord_iso_map(A,r,B,s)), s)";
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   500
by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun]) 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   501
by (safe_tac ZF_cs);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   502
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   503
by (REPEAT 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   504
    (fast_tac (ZF_cs addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   505
by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   506
by (rewtac ord_iso_map_def);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   507
by (safe_tac (ZF_cs addSEs [UN_E]));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   508
by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   509
qed "ord_iso_map_mono_map";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   510
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   511
goalw Order.thy [mono_map_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   512
    "!!B. [| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   513
\          : ord_iso(domain(ord_iso_map(A,r,B,s)), r,   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   514
\                     range(ord_iso_map(A,r,B,s)), s)";
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   515
by (rtac well_ord_mono_ord_isoI 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   516
by (resolve_tac [converse_ord_iso_map RS subst] 4);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   517
by (asm_simp_tac 
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   518
    (ZF_ss addsimps [ord_iso_map_subset RS converse_converse, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   519
                     domain_converse, range_converse]) 4);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   520
by (REPEAT (ares_tac [ord_iso_map_mono_map] 3));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   521
by (ALLGOALS (etac well_ord_subset));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   522
by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map]));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   523
qed "ord_iso_map_ord_iso";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   524
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   525
(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   526
goalw Order.thy [ord_iso_map_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   527
  "!!B. [| well_ord(A,r);  well_ord(B,s);               \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   528
\          a: A;  a ~: domain(ord_iso_map(A,r,B,s))     \
1015
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   529
\       |] ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)";
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   530
by (safe_tac (ZF_cs addSIs [predI]));
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   531
(*Case analysis on  xaa vs a in r *)
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   532
by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   533
by (linear_case_tac 1);
1015
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   534
(*Trivial case: a=xa*)
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   535
by (fast_tac ZF_cs 2);
75110179587d Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents: 990
diff changeset
   536
(*Harder case: <a, xa>: r*)
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   537
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   538
    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   539
by (forward_tac [ord_iso_restrict_pred] 1  THEN
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   540
    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   541
by (asm_full_simp_tac
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   542
    (ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   543
by (fast_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   544
qed "domain_ord_iso_map_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   545
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   546
(*For the 4-way case analysis in the main result*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   547
goal Order.thy
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   548
  "!!B. [| well_ord(A,r);  well_ord(B,s) |] ==> \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   549
\       domain(ord_iso_map(A,r,B,s)) = A |      \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   550
\       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   551
by (forward_tac [well_ord_is_wf] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   552
by (rewrite_goals_tac [wf_on_def, wf_def]);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   553
by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   554
by (step_tac ZF_cs 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   555
(*The first case: the domain equals A*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   556
by (rtac (domain_ord_iso_map RS equalityI) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   557
by (etac (Diff_eq_0_iff RS iffD1) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   558
(*The other case: the domain equals an initial segment*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   559
by (swap_res_tac [bexI] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   560
by (assume_tac 2);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   561
by (rtac equalityI 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   562
(*not ZF_cs below; that would use rules like domainE!*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   563
by (fast_tac (pair_cs addSEs [predE]) 2);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   564
by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   565
qed "domain_ord_iso_map_cases";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   566
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   567
(*As above, by duality*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   568
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   569
  "!!B. [| well_ord(A,r);  well_ord(B,s) |] ==> \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   570
\       range(ord_iso_map(A,r,B,s)) = B |       \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   571
\       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   572
by (resolve_tac [converse_ord_iso_map RS subst] 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   573
by (asm_simp_tac
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   574
    (ZF_ss addsimps [range_converse, domain_ord_iso_map_cases]) 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   575
qed "range_ord_iso_map_cases";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   576
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   577
(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   578
goal Order.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   579
  "!!B. [| well_ord(A,r);  well_ord(B,s) |] ==>         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   580
\       ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |    \
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   581
\       (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   582
\       (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   583
by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   584
by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   585
by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE]));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   586
by (ALLGOALS (dtac ord_iso_map_ord_iso THEN' assume_tac THEN' 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   587
              asm_full_simp_tac (ZF_ss addsimps [bexI])));
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   588
by (resolve_tac [wf_on_not_refl RS notE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   589
by (etac well_ord_is_wf 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   590
by (assume_tac 1);
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   591
by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   592
by (dtac rangeI 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   593
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1015
diff changeset
   594
by (rewtac ord_iso_map_def);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   595
by (fast_tac ZF_cs 1);
789
30bdc59198ff well_ord_iso_predE replaces not_well_ord_iso_pred
lcp
parents: 782
diff changeset
   596
qed "well_ord_trichotomy";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   597
836
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   598
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   599
(*** Properties of converse(r), by Krzysztof Grabczewski ***)
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   600
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   601
goalw Order.thy [irrefl_def] 
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   602
            "!!A. irrefl(A,r) ==> irrefl(A,converse(r))";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   603
by (fast_tac (ZF_cs addSIs [converseI]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   604
qed "irrefl_converse";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   605
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   606
goalw Order.thy [trans_on_def] 
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   607
    "!!A. trans[A](r) ==> trans[A](converse(r))";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   608
by (fast_tac (ZF_cs addSIs [converseI]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   609
qed "trans_on_converse";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   610
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   611
goalw Order.thy [part_ord_def] 
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   612
    "!!A. part_ord(A,r) ==> part_ord(A,converse(r))";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   613
by (fast_tac (ZF_cs addSIs [irrefl_converse, trans_on_converse]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   614
qed "part_ord_converse";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   615
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   616
goalw Order.thy [linear_def] 
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   617
    "!!A. linear(A,r) ==> linear(A,converse(r))";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   618
by (fast_tac (ZF_cs addSIs [converseI]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   619
qed "linear_converse";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   620
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   621
goalw Order.thy [tot_ord_def] 
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   622
    "!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))";
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   623
by (fast_tac (ZF_cs addSIs [part_ord_converse, linear_converse]) 1);
627f4842b020 Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents: 812
diff changeset
   624
qed "tot_ord_converse";