src/ZF/OrderType.ML
author lcp
Tue, 21 Jun 1994 17:20:34 +0200
changeset 435 ca5356bd315a
child 437 435875e4b21d
permissions -rw-r--r--
Addition of cardinals and order types, various tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/OrderType.ML
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     6
For OrderType.thy.  Order types in Zermelo-Fraenkel Set Theory 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     8
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     9
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    12
br well_ordI 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
br (wf_Memrel RS wf_imp_wf_on) 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    15
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    16
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    17
val well_ord_Memrel = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    19
open OrderType;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    20
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    21
(** Unfolding of ordermap **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    23
goalw OrderType.thy [ordermap_def, pred_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    24
    "!!r. [| wf[A](r);  x:A |] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    25
\         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    26
by (asm_simp_tac ZF_ss 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    27
be (wfrec_on RS trans) 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    28
ba 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    29
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    30
                                  vimage_singleton_iff]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    31
val ordermap_pred_unfold = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    32
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    33
(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    34
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    35
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    36
goalw OrderType.thy [ordermap_def,ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    37
    "ordermap(A,r) : A -> ordertype(A,r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    38
br lam_type 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    39
by (rtac (lamI RS imageI) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    40
by (REPEAT (assume_tac 1));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    41
val ordermap_type = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    42
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    43
(** Showing that ordermap, ordertype yield ordinals **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    44
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    45
fun ordermap_elim_tac i =
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    46
    EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    47
	   assume_tac (i+1),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    48
	   assume_tac i];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    49
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    50
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
    51
    "!!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
    52
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    53
by (wf_on_ind_tac "x" [] 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    54
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    55
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    56
bws [pred_def,Transset_def];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    57
by (fast_tac ZF_cs 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    58
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    59
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    60
by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    61
val Ord_ordermap = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    62
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    63
goalw OrderType.thy [ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    64
    "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    65
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
    66
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    67
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    68
bws [Transset_def,well_ord_def];
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    69
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    70
by (ordermap_elim_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    71
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    72
val Ord_ordertype = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    73
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    74
(** ordermap preserves the orderings in both directions **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    75
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    76
goal OrderType.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    77
    "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    78
\         ordermap(A,r)`w : ordermap(A,r)`x";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    79
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    80
ba 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    81
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    82
val less_imp_ordermap_in = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    83
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    84
(*linearity of r is crucial here*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    85
goalw OrderType.thy [well_ord_def, tot_ord_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    86
    "!!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
    87
\            w: A; x: A |] ==> <w,x>: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    88
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    89
by (linear_case_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    90
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    91
bd less_imp_ordermap_in 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    92
by (REPEAT_SOME assume_tac);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    93
be mem_anti_sym 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    94
ba 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    95
val ordermap_in_imp_less = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    96
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    97
val ordermap_surj = 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    98
    (ordermap_type RS surj_image) |>
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    99
    rewrite_rule [symmetric ordertype_def] |> 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   100
    standard;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   101
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   102
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
   103
    "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   104
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   105
br ordermap_type 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   106
br ordermap_surj 2;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   107
by (linear_case_tac 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   108
(*The two cases yield similar contradictions*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   109
by (ALLGOALS (dtac less_imp_ordermap_in));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   110
by (REPEAT_SOME assume_tac);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   111
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   112
val ordertype_bij = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   113
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   114
goalw OrderType.thy [ord_iso_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   115
 "!!r. well_ord(A,r) ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   116
\      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
   117
by (safe_tac ZF_cs);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   118
br ordertype_bij 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   119
ba 1;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   120
by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   121
bw well_ord_def;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   122
by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   123
			    ordermap_type RS apply_type]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   124
val ordertype_ord_iso = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   125
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   126
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   127
(** Unfolding of ordertype **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   128
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   129
goalw OrderType.thy [ordertype_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   130
    "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   131
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
   132
val ordertype_unfold = result();