src/ZF/OrderType.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
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: 1032
diff changeset
     1
(*  Title:      ZF/OrderType.ML
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
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
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
     6
Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
     7
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
     8
Ordinal arithmetic is traditionally defined in terms of order types, as here.
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
     9
But a definition by transfinite recursion would be much simpler!
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
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
open OrderType;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    15
(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    16
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    17
val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    18
by (rtac well_ordI 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    19
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    20
by (resolve_tac [prem RS ltE] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    21
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
    22
                                  [ltI, prem] MRS lt_trans2 RS ltD]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    23
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    24
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    25
qed "le_well_ord_Memrel";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    26
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    27
(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    28
bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel);
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    29
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    30
(*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
    31
  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
    32
goalw OrderType.thy [pred_def, lt_def]
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    33
    "!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    34
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
    35
by (fast_tac (eq_cs addEs [Ord_trans]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    36
qed "lt_pred_Memrel";
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    37
831
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    38
goalw OrderType.thy [pred_def,Memrel_def] 
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    39
      "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
831
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    40
by (fast_tac eq_cs 1);
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    41
qed "pred_Memrel";
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
    42
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    43
goal OrderType.thy
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    44
    "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    45
by (forward_tac [lt_pred_Memrel] 1);
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    46
by (etac ltE 1);
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    47
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
    48
    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
    49
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
    50
(*Combining the two simplifications causes looping*)
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    51
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
    52
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
    53
qed "Ord_iso_implies_eq_lemma";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    54
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    55
(*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
    56
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
    57
    "!!i. [| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))     \
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    58
\         |] ==> i=j";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    59
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
    60
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
    61
qed "Ord_iso_implies_eq";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    62
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    63
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    64
(**** Ordermap and ordertype ****)
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
    65
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    66
goalw OrderType.thy [ordermap_def,ordertype_def]
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    67
    "ordermap(A,r) : A -> ordertype(A,r)";
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    68
by (rtac lam_type 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    69
by (rtac (lamI RS imageI) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    70
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    71
qed "ordermap_type";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    72
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    73
(*** Unfolding of ordermap ***)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    74
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    75
(*Useful for cardinality reasoning; see CardinalArith.ML*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    76
goalw OrderType.thy [ordermap_def, pred_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    77
    "!!r. [| wf[A](r);  x:A |] ==> \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    78
\         ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    79
by (asm_simp_tac ZF_ss 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    80
by (etac (wfrec_on RS trans) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    81
by (assume_tac 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    82
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    83
                                  vimage_singleton_iff]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    84
qed "ordermap_eq_image";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    85
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
    86
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    87
goal OrderType.thy 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    88
    "!!r. [| wf[A](r);  x:A |] ==> \
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    89
\         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    90
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
    91
                                  ordermap_type RS image_fun]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
    92
qed "ordermap_pred_unfold";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    93
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    94
(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    95
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    96
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
    97
(*** Showing that ordermap, ordertype yield ordinals ***)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    98
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    99
fun ordermap_elim_tac i =
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   100
    EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   101
           assume_tac (i+1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   102
           assume_tac i];
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   103
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   104
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
   105
    "!!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
   106
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   107
by (wf_on_ind_tac "x" [] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   108
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   109
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   110
by (rewrite_goals_tac [pred_def,Transset_def]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   111
by (fast_tac ZF_cs 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   112
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   113
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   114
by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   115
qed "Ord_ordermap";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   116
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   117
goalw OrderType.thy [ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   118
    "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   119
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
   120
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   121
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   122
by (rewrite_goals_tac [Transset_def,well_ord_def]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   123
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   124
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   125
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   126
qed "Ord_ordertype";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   127
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   128
(*** ordermap preserves the orderings in both directions ***)
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
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   131
    "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>    \
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   132
\         ordermap(A,r)`w : ordermap(A,r)`x";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   133
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   134
by (assume_tac 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   135
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   136
qed "ordermap_mono";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   137
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   138
(*linearity of r is crucial here*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   139
goalw OrderType.thy [well_ord_def, tot_ord_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   140
    "!!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
   141
\            w: A; x: A |] ==> <w,x>: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   142
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   143
by (linear_case_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   144
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   145
by (dtac ordermap_mono 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   146
by (REPEAT_SOME assume_tac);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   147
by (etac mem_asym 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   148
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   149
qed "converse_ordermap_mono";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   150
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 788
diff changeset
   151
bind_thm ("ordermap_surj", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   152
          rewrite_rule [symmetric ordertype_def] 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   153
              (ordermap_type RS surj_image));
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   154
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   155
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
   156
    "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   157
by (fast_tac (ZF_cs addSIs [ordermap_type, ordermap_surj]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   158
                    addEs [linearE]
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   159
                    addDs [ordermap_mono]
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   160
                    addss (ZF_ss addsimps [mem_not_refl])) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   161
qed "ordermap_bij";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   162
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   163
(*** Isomorphisms involving ordertype ***)
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   164
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   165
goalw OrderType.thy [ord_iso_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   166
 "!!r. well_ord(A,r) ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   167
\      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
   168
by (safe_tac ZF_cs);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   169
by (rtac ordermap_bij 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   170
by (assume_tac 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   171
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   172
by (rewtac well_ord_def);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   173
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   174
                            ordermap_type RS apply_type]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   175
qed "ordertype_ord_iso";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   176
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   177
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   178
    "!!f. [| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   179
\    ordertype(A,r) = ordertype(B,s)";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   180
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   181
by (rtac Ord_iso_implies_eq 1
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   182
    THEN REPEAT (etac Ord_ordertype 1));
831
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
   183
by (deepen_tac (ZF_cs addIs  [ord_iso_trans, ord_iso_sym]
60d850cc5fe6 Added Krzysztof's theorem pred_Memrel
lcp
parents: 814
diff changeset
   184
                      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
   185
qed "ordertype_eq";
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   186
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   187
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   188
    "!!A B. [| ordertype(A,r) = ordertype(B,s); \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   189
\              well_ord(A,r);  well_ord(B,s) \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   190
\           |] ==> EX f. f: ord_iso(A,r,B,s)";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   191
by (rtac exI 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   192
by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   193
by (assume_tac 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   194
by (etac ssubst 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   195
by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   196
qed "ordertype_eq_imp_ord_iso";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   197
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   198
(*** Basic equalities for ordertype ***)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   199
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   200
(*Ordertype of Memrel*)
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   201
goal OrderType.thy "!!i. j le i ==> ordertype(j,Memrel(i)) = j";
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   202
by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   203
by (etac ltE 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   204
by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   205
by (rtac ord_iso_trans 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   206
by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   207
by (resolve_tac [id_bij RS ord_isoI] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   208
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   209
by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   210
qed "le_ordertype_Memrel";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   211
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   212
(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   213
bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   214
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   215
goal OrderType.thy "ordertype(0,r) = 0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   216
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   217
by (etac emptyE 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   218
by (rtac well_ord_0 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   219
by (resolve_tac [Ord_0 RS ordertype_Memrel] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   220
qed "ordertype_0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   221
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   222
(*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   223
                         ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   224
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   225
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   226
(*** A fundamental unfolding law for ordertype. ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   227
814
a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents: 807
diff changeset
   228
(*Ordermap returns the same result if applied to an initial segment*)
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   229
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   230
    "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   231
\         ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   232
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
   233
by (wf_on_ind_tac "z" [] 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   234
by (safe_tac (ZF_cs addSEs [predE]));
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   235
by (asm_simp_tac
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   236
    (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   237
(*combining these two simplifications LOOPS! *)
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   238
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   239
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
807
3abd026e68a4 ran expandshort script
lcp
parents: 803
diff changeset
   240
by (rtac (refl RSN (2,RepFun_cong)) 1);
3abd026e68a4 ran expandshort script
lcp
parents: 803
diff changeset
   241
by (dtac well_ord_is_trans_on 1);
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   242
by (fast_tac (eq_cs addSEs [trans_onD]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 467
diff changeset
   243
qed "ordermap_pred_eq_ordermap";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   244
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   245
goalw OrderType.thy [ordertype_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   246
    "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   247
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   248
qed "ordertype_unfold";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   249
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   250
(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   251
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   252
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   253
    "!!r. [| well_ord(A,r);  x:A |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   254
\         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   255
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   256
                  pred_subset RSN (2, well_ord_subset)]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   257
by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   258
                    addEs [predE]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   259
qed "ordertype_pred_subset";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   260
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   261
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   262
    "!!r. [| well_ord(A,r);  x:A |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   263
\         ordertype(pred(A,x,r),r) < ordertype(A,r)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   264
by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   265
by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   266
by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   267
by (etac well_ord_iso_predE 3);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   268
by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   269
qed "ordertype_pred_lt";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   270
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   271
(*May rewrite with this -- provided no rules are supplied for proving that
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   272
        well_ord(pred(A,x,r), r) *)
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   273
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   274
    "!!A r. well_ord(A,r) ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   275
\           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   276
by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   277
by (fast_tac
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   278
    (ZF_cs addss
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   279
     (ZF_ss addsimps [ordertype_def, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   280
                      well_ord_is_wf RS ordermap_eq_image, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   281
                      ordermap_type RS image_fun, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   282
                      ordermap_pred_eq_ordermap, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   283
                      pred_subset]))
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   284
    1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   285
qed "ordertype_pred_unfold";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   286
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   287
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   288
(**** Alternative definition of ordinal ****)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   289
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   290
(*proof by Krzysztof Grabczewski*)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   291
goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   292
by (rtac conjI 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   293
by (etac well_ord_Memrel 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   294
by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   295
by (fast_tac eq_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   296
qed "Ord_is_Ord_alt";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   297
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   298
(*proof by lcp*)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   299
goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   300
                     tot_ord_def, part_ord_def, trans_on_def] 
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   301
    "!!i. Ord_alt(i) ==> Ord(i)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   302
by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   303
by (safe_tac ZF_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   304
by (fast_tac (ZF_cs addSDs [equalityD1]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   305
by (subgoal_tac "xa: i" 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   306
by (fast_tac (ZF_cs addSDs [equalityD1]) 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   307
by (fast_tac (ZF_cs addSDs [equalityD1]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   308
                    addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   309
qed "Ord_alt_is_Ord";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   310
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   311
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   312
(**** Ordinal Addition ****)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   313
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   314
(*** Order Type calculations for radd ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   315
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   316
(** Addition with 0 **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   317
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   318
goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   319
by (res_inst_tac [("d", "Inl")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   320
by (safe_tac sum_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   321
by (ALLGOALS (asm_simp_tac sum_ss));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   322
qed "bij_sum_0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   323
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   324
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   325
 "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   326
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   327
by (assume_tac 2);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   328
by (fast_tac (sum_cs addss (sum_ss addsimps [radd_Inl_iff, Memrel_iff])) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   329
qed "ordertype_sum_0_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   330
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   331
goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   332
by (res_inst_tac [("d", "Inr")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   333
by (safe_tac sum_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   334
by (ALLGOALS (asm_simp_tac sum_ss));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   335
qed "bij_0_sum";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   336
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   337
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   338
 "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   339
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   340
by (assume_tac 2);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   341
by (fast_tac (sum_cs addss (sum_ss addsimps [radd_Inr_iff, Memrel_iff])) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   342
qed "ordertype_0_sum_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   343
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   344
(** Initial segments of radd.  Statements by Grabczewski **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   345
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   346
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   347
goalw OrderType.thy [pred_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   348
 "!!A B. a:A ==>  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   349
\        (lam x:pred(A,a,r). Inl(x))    \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   350
\        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   351
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   352
by (safe_tac sum_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   353
by (ALLGOALS
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   354
    (asm_full_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   355
     (sum_ss addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   356
qed "pred_Inl_bij";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   357
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   358
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   359
 "!!A B. [| a:A;  well_ord(A,r) |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   360
\        ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   361
\        ordertype(pred(A,a,r), r)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   362
by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   363
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   364
by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   365
qed "ordertype_pred_Inl_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   366
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   367
goalw OrderType.thy [pred_def, id_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   368
 "!!A B. b:B ==>  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   369
\        id(A+pred(B,b,s))      \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   370
\        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   371
by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   372
by (safe_tac sum_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   373
by (ALLGOALS (asm_full_simp_tac radd_ss));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   374
qed "pred_Inr_bij";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   375
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   376
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   377
 "!!A B. [| b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   378
\        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   379
\        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   380
by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   381
by (fast_tac (sum_cs addss (radd_ss addsimps [pred_def, id_def])) 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   382
by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   383
qed "ordertype_pred_Inr_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   384
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   385
(*** Basic laws for ordinal addition ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   386
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   387
goalw OrderType.thy [oadd_def] 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   388
    "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i++j)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   389
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   390
qed "Ord_oadd";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   391
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   392
(** Ordinal addition with zero **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   393
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   394
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   395
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   396
                                  ordertype_Memrel, well_ord_Memrel]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   397
qed "oadd_0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   398
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   399
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   400
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   401
                                  ordertype_Memrel, well_ord_Memrel]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   402
qed "oadd_0_left";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   403
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   404
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   405
(*** Further properties of ordinal addition.  Statements by Grabczewski,
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   406
    proofs by lcp. ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   407
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   408
goalw OrderType.thy [oadd_def] "!!i j k. [| k<i;  Ord(j) |] ==> k < i++j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   409
by (rtac ltE 1 THEN assume_tac 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   410
by (rtac ltI 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   411
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   412
by (asm_simp_tac 
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   413
    (ZF_ss addsimps [ordertype_pred_unfold, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   414
                     well_ord_radd, well_ord_Memrel,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   415
                     ordertype_pred_Inl_eq, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   416
                     lt_pred_Memrel, leI RS le_ordertype_Memrel]
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   417
           setloop rtac (InlI RSN (2,RepFun_eqI))) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   418
qed "lt_oadd1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   419
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   420
(*Thus also we obtain the rule  i++j = k ==> i le k *)
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   421
goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le i++j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   422
by (rtac all_lt_imp_le 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   423
by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   424
qed "oadd_le_self";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   425
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   426
(** A couple of strange but necessary results! **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   427
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   428
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   429
    "!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   430
by (resolve_tac [id_bij RS ord_isoI] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   431
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   432
by (fast_tac ZF_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   433
qed "id_ord_iso_Memrel";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   434
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   435
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   436
    "!!k. [| well_ord(A,r);  k<j |] ==>                 \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   437
\            ordertype(A+k, radd(A, r, k, Memrel(j))) = \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   438
\            ordertype(A+k, radd(A, r, k, Memrel(k)))";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   439
by (etac ltE 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   440
by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   441
by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   442
by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   443
qed "ordertype_sum_Memrel";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   444
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   445
goalw OrderType.thy [oadd_def] "!!i j k. [| k<j;  Ord(i) |] ==> i++k < i++j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   446
by (rtac ltE 1 THEN assume_tac 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   447
by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   448
by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel]));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   449
by (rtac RepFun_eqI 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   450
by (etac InrI 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   451
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   452
    (ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   453
                     lt_pred_Memrel, leI RS le_ordertype_Memrel,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   454
                     ordertype_sum_Memrel]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   455
qed "oadd_lt_mono2";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   456
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   457
goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   458
    "!!i j k. [| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   459
by (rtac Ord_linear_lt 1);
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   460
by (REPEAT_SOME assume_tac);
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   461
by (ALLGOALS
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   462
    (fast_tac (ZF_cs addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   463
qed "oadd_lt_cancel2";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   464
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   465
goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   466
    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   467
by (fast_tac (ZF_cs addSIs [oadd_lt_mono2] addSEs [oadd_lt_cancel2]) 1);
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   468
qed "oadd_lt_iff2";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   469
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   470
goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   471
    "!!i j k. [| i++j = i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j=k";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   472
by (rtac Ord_linear_lt 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   473
by (REPEAT_SOME assume_tac);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   474
by (ALLGOALS
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   475
    (fast_tac (ZF_cs addDs [oadd_lt_mono2] 
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   476
                     addss (ZF_ss addsimps [lt_not_refl]))));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   477
qed "oadd_inject";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   478
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   479
goalw OrderType.thy [oadd_def] 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   480
    "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==> k<i | (EX l:j. k = i++l )";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   481
(*Rotate the hypotheses so that simplification will work*)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   482
by (etac revcut_rl 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   483
by (asm_full_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   484
    (ZF_ss addsimps [ordertype_pred_unfold, well_ord_radd,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   485
                     well_ord_Memrel]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   486
by (eresolve_tac [ltD RS RepFunE] 1);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   487
by (fast_tac (sum_cs addss 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   488
              (ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   489
                               ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   490
                               ordertype_pred_Inr_eq, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   491
                               ordertype_sum_Memrel])) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   492
qed "lt_oadd_disj";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   493
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   494
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   495
(*** Ordinal addition with successor -- via associativity! ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   496
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   497
goalw OrderType.thy [oadd_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   498
    "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i++j)++k = i++(j++k)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   499
by (resolve_tac [ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   500
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   501
          sum_ord_iso_cong) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   502
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   503
by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   504
by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   505
          ordertype_eq) 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   506
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   507
qed "oadd_assoc";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   508
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   509
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   510
    "!!i j. [| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   511
by (rtac (subsetI RS equalityI) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   512
by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   513
by (REPEAT (ares_tac [Ord_oadd] 1));
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   514
by (fast_tac (ZF_cs addIs [lt_oadd1, oadd_lt_mono2]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   515
                    addss (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   516
by (fast_tac ZF_cs 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   517
by (fast_tac (ZF_cs addSEs [ltE]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   518
qed "oadd_unfold";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   519
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   520
goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   521
by (asm_simp_tac (ZF_ss addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   522
by (fast_tac eq_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   523
qed "oadd_1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   524
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   525
goal OrderType.thy
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   526
    "!!i. [| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   527
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   528
    (ZF_ss addsimps [oadd_1 RS sym, Ord_oadd, oadd_assoc, Ord_1]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   529
qed "oadd_succ";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   530
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   531
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   532
(** Ordinal addition with limit ordinals **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   533
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   534
val prems = goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   535
    "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   536
\    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   537
by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   538
                                    lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   539
                     addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   540
qed "oadd_UN";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   541
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   542
goal OrderType.thy 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   543
    "!!i j. [| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   544
by (forward_tac [Limit_has_0 RS ltD] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   545
by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   546
                                  oadd_UN RS sym, Union_eq_UN RS sym, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   547
                                  Limit_Union_eq]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   548
qed "oadd_Limit";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   549
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   550
(** Order/monotonicity properties of ordinal addition **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   551
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   552
goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le j++i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   553
by (eres_inst_tac [("i","i")] trans_induct3 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   554
by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   555
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   556
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   557
by (rtac le_trans 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   558
by (rtac le_implies_UN_le_UN 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   559
by (fast_tac ZF_cs 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   560
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   561
                                  le_refl, Limit_is_Ord]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   562
qed "oadd_le_self2";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   563
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   564
goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k++i le j++i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   565
by (forward_tac [lt_Ord] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   566
by (forward_tac [le_Ord2] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   567
by (etac trans_induct3 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   568
by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   569
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   570
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   571
by (rtac le_implies_UN_le_UN 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   572
by (fast_tac ZF_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   573
qed "oadd_le_mono1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   574
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   575
goal OrderType.thy "!!i j. [| i' le i;  j'<j |] ==> i'++j' < i++j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   576
by (rtac lt_trans1 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   577
by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   578
                          Ord_succD] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   579
qed "oadd_lt_mono";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   580
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   581
goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'++j' le i++j";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   582
by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   583
qed "oadd_le_mono";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   584
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   585
goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   586
    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   587
by (asm_simp_tac (ZF_ss addsimps [oadd_lt_iff2, oadd_succ RS sym, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   588
                                  Ord_succ]) 1);
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   589
qed "oadd_le_iff2";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   590
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   591
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   592
(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   593
    Probably simpler to define the difference recursively!
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   594
**)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   595
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   596
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   597
    "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   598
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   599
by (fast_tac (sum_cs addSIs [if_type]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   600
by (fast_tac (ZF_cs addSIs [case_type]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   601
by (etac sumE 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   602
by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   603
qed "bij_sum_Diff";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   604
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   605
goal OrderType.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   606
    "!!i j. i le j ==>  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   607
\           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =       \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   608
\           ordertype(j, Memrel(j))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   609
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   610
by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   611
by (etac well_ord_Memrel 3);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   612
by (assume_tac 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   613
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   614
     (radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   615
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   616
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   617
by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   618
by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   619
qed "ordertype_sum_Diff";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   620
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   621
goalw OrderType.thy [oadd_def, odiff_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   622
    "!!i j. i le j ==>  \
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   623
\           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   624
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   625
by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   626
by (etac id_ord_iso_Memrel 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   627
by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   628
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   629
                      Diff_subset] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   630
qed "oadd_ordertype_Diff";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   631
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   632
goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   633
by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   634
                                  ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   635
qed "oadd_odiff_inverse";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   636
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   637
goalw OrderType.thy [odiff_def] 
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   638
    "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i--j)";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   639
by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   640
                      Diff_subset] 1));
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   641
qed "Ord_odiff";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   642
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   643
(*By oadd_inject, the difference between i and j is unique.  Note that we get
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   644
  i++j = k  ==>  j = k--i.  *)
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   645
goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   646
    "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   647
by (rtac oadd_inject 1);
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   648
by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   649
by (asm_simp_tac (ZF_ss addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   650
qed "odiff_oadd_inverse";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   651
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   652
val [i_lt_j, k_le_i] = goal OrderType.thy
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   653
    "[| i<j;  k le i |] ==> i--k < j--k";
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   654
by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   655
by (simp_tac
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   656
    (ZF_ss addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   657
                     oadd_odiff_inverse]) 1);
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   658
by (REPEAT (resolve_tac (Ord_odiff :: 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   659
                         ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
1032
54b9f670c67e Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents: 984
diff changeset
   660
qed "odiff_lt_mono2";
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   661
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   662
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   663
(**** Ordinal Multiplication ****)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   664
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   665
goalw OrderType.thy [omult_def] 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   666
    "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i**j)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   667
by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   668
qed "Ord_omult";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   669
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   670
(*** A useful unfolding law ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   671
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   672
goalw OrderType.thy [pred_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   673
 "!!A B. [| a:A;  b:B |] ==>  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   674
\        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   675
\        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   676
by (safe_tac eq_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   677
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   678
by (ALLGOALS (fast_tac ZF_cs));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   679
qed "pred_Pair_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   680
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   681
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   682
 "!!A B. [| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   683
\        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   684
\        ordertype(pred(A,a,r)*B + pred(B,b,s),                 \
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   685
\                 radd(A*B, rmult(A,r,B,s), B, s))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   686
by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   687
by (resolve_tac [ordertype_eq RS sym] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   688
by (rtac prod_sum_singleton_ord_iso 1);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   689
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   690
by (fast_tac (ZF_cs addSEs [predE]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   691
qed "ordertype_pred_Pair_eq";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   692
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   693
goalw OrderType.thy [oadd_def, omult_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   694
 "!!i j. [| i'<i;  j'<j |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   695
\        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   696
\                  rmult(i,Memrel(i),j,Memrel(j))) = \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   697
\        j**i' ++ j'";
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   698
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   699
                                  ltD, lt_Ord2, well_ord_Memrel]) 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   700
by (rtac trans 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   701
by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   702
by (rtac ord_iso_refl 3);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   703
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   704
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   705
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   706
                            Ord_ordertype]));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   707
by (ALLGOALS 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   708
    (asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   709
by (safe_tac ZF_cs);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   710
by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   711
qed "ordertype_pred_Pair_lemma";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   712
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   713
goalw OrderType.thy [omult_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   714
 "!!i j. [| Ord(i);  Ord(j);  k<j**i |] ==>  \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   715
\        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   716
by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   717
                                       well_ord_rmult, well_ord_Memrel]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   718
by (step_tac (ZF_cs addSEs [ltE]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   719
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   720
                                  symmetric omult_def]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   721
by (fast_tac (ZF_cs addIs [ltI]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   722
qed "lt_omult";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   723
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   724
goalw OrderType.thy [omult_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   725
 "!!i j. [| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   726
by (rtac ltI 1);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   727
by (asm_simp_tac
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   728
    (ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   729
                     lt_Ord2]) 2);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   730
by (asm_simp_tac 
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   731
    (ZF_ss addsimps [ordertype_pred_unfold, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   732
                     well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   733
by (rtac RepFun_eqI 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   734
by (fast_tac (ZF_cs addSEs [ltE]) 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   735
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   736
    (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   737
qed "omult_oadd_lt";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   738
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   739
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   740
 "!!i j. [| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   741
by (rtac (subsetI RS equalityI) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   742
by (resolve_tac [lt_omult RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   743
by (etac ltI 3);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   744
by (REPEAT (ares_tac [Ord_omult] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   745
by (fast_tac (ZF_cs addSEs [ltE]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   746
by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   747
qed "omult_unfold";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   748
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   749
(*** Basic laws for ordinal multiplication ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   750
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   751
(** Ordinal multiplication by zero **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   752
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   753
goalw OrderType.thy [omult_def] "i**0 = 0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   754
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   755
qed "omult_0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   756
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   757
goalw OrderType.thy [omult_def] "0**i = 0";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   758
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   759
qed "omult_0_left";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   760
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   761
(** Ordinal multiplication by 1 **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   762
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   763
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   764
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   765
by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   766
by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   767
                                well_ord_Memrel, ordertype_Memrel]));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   768
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   769
qed "omult_1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   770
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   771
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   772
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   773
by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   774
by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   775
                                well_ord_Memrel, ordertype_Memrel]));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   776
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   777
qed "omult_1_left";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   778
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   779
(** Distributive law for ordinal multiplication and addition **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   780
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   781
goalw OrderType.thy [omult_def, oadd_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   782
    "!!i. [| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   783
by (resolve_tac [ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   784
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   785
          prod_ord_iso_cong) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   786
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   787
                      Ord_ordertype] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   788
by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   789
by (rtac ordertype_eq 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   790
by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   791
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   792
                      Ord_ordertype] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   793
qed "oadd_omult_distrib";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   794
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   795
goal OrderType.thy "!!i. [| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   796
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   797
    (ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   798
qed "omult_succ";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   799
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   800
(** Associative law **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   801
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   802
goalw OrderType.thy [omult_def]
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   803
    "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   804
by (resolve_tac [ordertype_eq RS trans] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   805
by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   806
          prod_ord_iso_cong) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   807
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   808
by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   809
                 ordertype_eq RS trans] 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   810
by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   811
          ordertype_eq) 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   812
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   813
qed "omult_assoc";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   814
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   815
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   816
(** Ordinal multiplication with limit ordinals **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   817
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   818
val prems = goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   819
    "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   820
\    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   821
by (asm_simp_tac (ZF_ss addsimps (prems@[Ord_UN, omult_unfold])) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   822
by (fast_tac eq_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   823
qed "omult_UN";
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
   824
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   825
goal OrderType.thy 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   826
    "!!i j. [| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   827
by (asm_simp_tac 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   828
    (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   829
                     Union_eq_UN RS sym, Limit_Union_eq]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   830
qed "omult_Limit";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   831
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   832
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   833
(*** Ordering/monotonicity properties of ordinal multiplication ***)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   834
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   835
(*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   836
goal OrderType.thy "!!i j. [| k<i;  0<j |] ==> k < i**j";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   837
by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   838
by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   839
by (REPEAT (etac UN_I 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   840
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   841
qed "lt_omult1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   842
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   843
goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le i**j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   844
by (rtac all_lt_imp_le 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   845
by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   846
qed "omult_le_self";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   847
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   848
goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k**i le j**i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   849
by (forward_tac [lt_Ord] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   850
by (forward_tac [le_Ord2] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   851
by (etac trans_induct3 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   852
by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   853
by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   854
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   855
by (rtac le_implies_UN_le_UN 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   856
by (fast_tac ZF_cs 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   857
qed "omult_le_mono1";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   858
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   859
goal OrderType.thy "!!i j k. [| k<j;  0<i |] ==> i**k < i**j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   860
by (rtac ltI 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   861
by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   862
by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult]));
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   863
by (REPEAT (etac UN_I 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   864
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   865
qed "omult_lt_mono2";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   866
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   867
goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> i**k le i**j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   868
by (rtac subset_imp_le 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   869
by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   870
by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   871
by (deepen_tac (ZF_cs addEs [Ord_trans, UN_I]) 0 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   872
qed "omult_le_mono2";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   873
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   874
goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'**j' le i**j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   875
by (rtac le_trans 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   876
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   877
                          Ord_succD] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   878
qed "omult_le_mono";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   879
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   880
goal OrderType.thy
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   881
      "!!i j. [| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   882
by (rtac lt_trans1 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   883
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   884
                          Ord_succD] 1));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   885
qed "omult_lt_mono";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   886
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   887
goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le j**i";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   888
by (forward_tac [lt_Ord2] 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   889
by (eres_inst_tac [("i","i")] trans_induct3 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   890
by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   891
by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   892
by (etac lt_trans1 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   893
by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   894
    rtac oadd_lt_mono2 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   895
by (REPEAT (ares_tac [Ord_omult] 1));
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   896
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   897
by (rtac le_trans 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   898
by (rtac le_implies_UN_le_UN 2);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   899
by (fast_tac ZF_cs 2);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   900
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1032
diff changeset
   901
                                  Limit_is_Ord RS le_refl]) 1);
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   902
qed "omult_le_self2";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   903
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   904
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   905
(** Further properties of ordinal multiplication **)
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   906
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   907
goal OrderType.thy "!!i j. [| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   908
by (rtac Ord_linear_lt 1);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   909
by (REPEAT_SOME assume_tac);
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   910
by (ALLGOALS
984
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   911
    (fast_tac (ZF_cs addDs [omult_lt_mono2] 
4fb1d099ba45 Tried the new addss in many proofs, and tidied others
lcp
parents: 849
diff changeset
   912
                     addss (ZF_ss addsimps [lt_not_refl]))));
849
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   913
qed "omult_inject";
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   914
013a16d3addb Proved equivalence of Ord and Ord_alt. Proved
lcp
parents: 831
diff changeset
   915