src/ZF/OrderType.ML
author lcp
Fri, 23 Dec 1994 16:32:02 +0100
changeset 831 60d850cc5fe6
parent 814 a32b420c33d4
child 849 013a16d3addb
permissions -rw-r--r--
Added Krzysztof's theorem pred_Memrel
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/OrderType.ML
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
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
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
     6
Order types in Zermelo-Fraenkel Set Theory 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
*)
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
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
open OrderType;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    12
(*** Proofs needing the combination of Ordinal.thy and Order.thy ***)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    13
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    14
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    15
by (rtac well_ordI 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    16
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    17
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    18
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    19
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    20
qed "well_ord_Memrel";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    21
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    22
(*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    23
  The smaller ordinal is an initial segment of the larger *)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    24
goalw OrderType.thy [pred_def, lt_def]
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    25
    "!!i j. j<i ==> j = pred(i, j, Memrel(i))";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    26
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    27
by (fast_tac (eq_cs addEs [Ord_trans]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    28
qed "lt_eq_pred";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    29
831
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    30
goalw OrderType.thy [pred_def,Memrel_def] 
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    31
      "!!A x. x:A ==> pred(A, x, Memrel(A)) = {b:A. b:x}";
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    32
by (fast_tac eq_cs 1);
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    33
qed "pred_Memrel";
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    34
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    35
goal OrderType.thy
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    36
    "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    37
by (forward_tac [lt_eq_pred] 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    38
by (etac ltE 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    39
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    40
    assume_tac 3 THEN assume_tac 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    41
by (etac subst 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    42
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    43
(*Combining the two simplifications causes looping*)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    44
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    45
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    46
qed "Ord_iso_implies_eq_lemma";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    47
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    48
(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    49
goal OrderType.thy
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    50
    "!!i. [| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))	\
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    51
\         |] ==> i=j";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    52
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    53
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    54
qed "Ord_iso_implies_eq";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    55
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    56
(*** Ordermap and ordertype ***)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    57
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    58
goalw OrderType.thy [ordermap_def,ordertype_def]
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    59
    "ordermap(A,r) : A -> ordertype(A,r)";
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    60
by (rtac lam_type 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    61
by (rtac (lamI RS imageI) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    62
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    63
qed "ordermap_type";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    64
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    65
(** Unfolding of ordermap **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    66
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    67
(*Useful for cardinality reasoning; see CardinalArith.ML*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    68
goalw OrderType.thy [ordermap_def, pred_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    69
    "!!r. [| wf[A](r);  x:A |] ==> \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    70
\         ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    71
by (asm_simp_tac ZF_ss 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    72
by (etac (wfrec_on RS trans) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    73
by (assume_tac 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    74
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    75
                                  vimage_singleton_iff]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    76
qed "ordermap_eq_image";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    77
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
    78
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    79
goal OrderType.thy 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    80
    "!!r. [| wf[A](r);  x:A |] ==> \
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    81
\         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    82
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    83
				  ordermap_type RS image_fun]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    84
qed "ordermap_pred_unfold";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    85
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    86
(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    87
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    88
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    89
(** Showing that ordermap, ordertype yield ordinals **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    90
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    91
fun ordermap_elim_tac i =
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    92
    EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    93
	   assume_tac (i+1),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    94
	   assume_tac i];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    95
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    96
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    97
    "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    98
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    99
by (wf_on_ind_tac "x" [] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   100
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   101
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   102
by (rewrite_goals_tac [pred_def,Transset_def]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   103
by (fast_tac ZF_cs 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   104
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   105
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   106
by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   107
qed "Ord_ordermap";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   108
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   109
goalw OrderType.thy [ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   110
    "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   111
by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   112
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   113
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   114
by (rewrite_goals_tac [Transset_def,well_ord_def]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   115
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   116
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   117
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   118
qed "Ord_ordertype";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   119
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   120
(** ordermap preserves the orderings in both directions **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   121
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   122
goal OrderType.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   123
    "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   124
\         ordermap(A,r)`w : ordermap(A,r)`x";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   125
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   126
by (assume_tac 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   127
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   128
qed "ordermap_mono";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   129
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   130
(*linearity of r is crucial here*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   131
goalw OrderType.thy [well_ord_def, tot_ord_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   132
    "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r);  \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   133
\            w: A; x: A |] ==> <w,x>: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   134
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   135
by (linear_case_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   136
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   137
by (dtac ordermap_mono 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   138
by (REPEAT_SOME assume_tac);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   139
by (etac mem_asym 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   140
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   141
qed "converse_ordermap_mono";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   142
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 788
diff changeset
   143
bind_thm ("ordermap_surj", 
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 788
diff changeset
   144
	  rewrite_rule [symmetric ordertype_def] 
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 788
diff changeset
   145
	      (ordermap_type RS surj_image));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   146
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   147
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   148
    "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   149
by (safe_tac ZF_cs);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   150
by (rtac ordermap_type 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   151
by (rtac ordermap_surj 2);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   152
by (linear_case_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   153
(*The two cases yield similar contradictions*)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   154
by (ALLGOALS (dtac ordermap_mono));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   155
by (REPEAT_SOME assume_tac);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   156
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   157
qed "ordermap_bij";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   158
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   159
(** Isomorphisms involving ordertype **)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   160
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   161
goalw OrderType.thy [ord_iso_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   162
 "!!r. well_ord(A,r) ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   163
\      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   164
by (safe_tac ZF_cs);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   165
by (rtac ordermap_bij 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   166
by (assume_tac 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   167
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   168
by (rewtac well_ord_def);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   169
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   170
			    ordermap_type RS apply_type]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   171
qed "ordertype_ord_iso";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   172
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   173
goal OrderType.thy
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   174
    "!!f. [| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==>	\
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   175
\    ordertype(A,r) = ordertype(B,s)";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   176
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   177
by (resolve_tac [Ord_iso_implies_eq] 1
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   178
    THEN REPEAT (eresolve_tac [Ord_ordertype] 1));
831
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
   179
by (deepen_tac (ZF_cs addIs  [ord_iso_trans, ord_iso_sym]
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
   180
                      addSEs [ordertype_ord_iso]) 0 1);
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   181
qed "ordertype_eq";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   182
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   183
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   184
(** Unfolding of ordertype **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   185
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   186
goalw OrderType.thy [ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   187
    "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   188
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   189
qed "ordertype_unfold";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   190
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   191
(*Ordertype of Memrel*)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   192
goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   193
by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   194
by (resolve_tac [ordertype_ord_iso] 3);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   195
by (REPEAT (ares_tac [well_ord_Memrel, Ord_ordertype] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   196
qed "ordertype_Memrel";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   197
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   198
(*Ordertype of rvimage*)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   199
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   200
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   201
(*Ordermap returns the same result if applied to an initial segment*)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   202
goal OrderType.thy
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   203
    "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>	\
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   204
\	  ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   205
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   206
by (wf_on_ind_tac "z" [] 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   207
by (safe_tac (ZF_cs addSEs [predE]));
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   208
by (asm_simp_tac
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   209
    (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   210
(*combining these two simplifications LOOPS! *)
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   211
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   212
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
807
3abd026e68a4 ran expandshort script
lcp
parents: 803
diff changeset
   213
by (rtac (refl RSN (2,RepFun_cong)) 1);
3abd026e68a4 ran expandshort script
lcp
parents: 803
diff changeset
   214
by (dtac well_ord_is_trans_on 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   215
by (fast_tac (eq_cs addSEs [trans_onD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   216
qed "ordermap_pred_eq_ordermap";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   217
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   218
(*Lemma for proving there exist ever larger cardinals*)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   219
goal OrderType.thy
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   220
    "!!r. [| well_ord(A,r);  i: ordertype(A,r) |] ==>	\
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   221
\	  EX B. B<=A & i = ordertype(B,r)";
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   222
by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1);
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   223
by (etac RepFunE 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   224
by (res_inst_tac [("x", "pred(A,y,r)")] exI 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   225
by (asm_simp_tac
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   226
    (ZF_ss addsimps [pred_subset, well_ord_is_wf RS ordermap_pred_unfold, 
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   227
		     ordertype_unfold, ordermap_pred_eq_ordermap]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   228
qed "ordertype_subset";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   229