src/ZF/OrderArith.ML
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 8201 a81d18b0a9b1
child 9173 422968aeed49
permissions -rw-r--r--
plain ASCII;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
     1
(*  Title:      ZF/OrderArith.ML
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     5
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     6
Towards ordinal arithmetic 
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     7
*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     8
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     9
(**** Addition of relations -- disjoint sum ****)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    10
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    11
(** Rewrite rules.  Can be used to obtain introduction rules **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    12
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    13
Goalw [radd_def] 
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    14
    "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
    15
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    16
qed "radd_Inl_Inr_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    17
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    18
Goalw [radd_def] 
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
    19
    "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
    20
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    21
qed "radd_Inl_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    22
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    23
Goalw [radd_def] 
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
    24
    "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
    25
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    26
qed "radd_Inr_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    27
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    28
Goalw [radd_def] 
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    29
    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
    30
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    31
qed "radd_Inr_Inl_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    32
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    33
(** Elimination Rule **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    34
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
    35
val major::prems = Goalw [radd_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
    36
    "[| <p',p> : radd(A,r,B,s);                 \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
    37
\       !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;       \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
    38
\       !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
    39
\       !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q  \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    40
\    |] ==> Q";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    41
by (cut_facts_tac [major] 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    42
(*Split into the three cases*)
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
    43
by (REPEAT_FIRST  (*can't use safe_tac: don't want hyp_subst_tac*)
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    44
    (eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    45
(*Apply each premise to correct subgoal; can't just use fast_tac
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    46
  because hyp_subst_tac would delete equalities too quickly*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    47
by (EVERY (map (fn prem => 
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2469
diff changeset
    48
                EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac])
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
    49
           prems));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    50
qed "raddE";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    51
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    52
(** Type checking **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    53
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    54
Goalw [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    55
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    56
qed "radd_type";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    57
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
    58
bind_thm ("field_radd", radd_type RS field_rel_subset);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    59
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    60
(** Linearity **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    61
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
    62
Addsimps [radd_Inl_iff, radd_Inr_iff, 
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2469
diff changeset
    63
          radd_Inl_Inr_iff, radd_Inr_Inl_iff];
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    64
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
    65
Goalw [linear_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
    66
    "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
    67
by (Force_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    68
qed "linear_radd";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    69
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    70
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    71
(** Well-foundedness **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    72
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
    73
Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    74
by (rtac wf_onI2 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    75
by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    76
(*Proving the lemma, which is needed twice!*)
1957
58b60b558e48 Now uses thin_tac
paulson
parents: 1461
diff changeset
    77
by (thin_tac "y : A + B" 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    78
by (rtac ballI 2);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    79
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    80
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    81
(*Returning to main part of proof*)
5488
paulson
parents: 5268
diff changeset
    82
by Safe_tac;
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2925
diff changeset
    83
by (Blast_tac 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    84
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    85
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    86
qed "wf_on_radd";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    87
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
    88
Goal "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    89
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    90
by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    91
by (REPEAT (ares_tac [wf_on_radd] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
    92
qed "wf_radd";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    93
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
    94
Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    95
\           well_ord(A+B, radd(A,r,B,s))";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    96
by (rtac well_ordI 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    97
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    98
by (asm_full_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
    99
    (simpset() addsimps [well_ord_def, tot_ord_def, linear_radd]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   100
qed "well_ord_radd";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   101
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   102
(** An ord_iso congruence law **)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   103
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   104
Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   105
\        (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   106
by (res_inst_tac 
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   107
        [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   108
    lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   109
by Safe_tac;
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   110
by (ALLGOALS (asm_simp_tac bij_inverse_ss));
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   111
qed "sum_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   112
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   113
Goalw [ord_iso_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   114
    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>     \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   115
\           (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))            \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   116
\           : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   117
by (safe_tac (claset() addSIs [sum_bij]));
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   118
(*Do the beta-reductions now*)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   119
by (ALLGOALS (Asm_full_simp_tac));
4152
451104c223e2 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   120
by Safe_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   121
(*8 subgoals!*)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   122
by (ALLGOALS
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   123
    (asm_full_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   124
     (simpset() addcongs [conj_cong] addsimps [bij_is_fun RS apply_type])));
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   125
qed "sum_ord_iso_cong";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   126
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   127
(*Could we prove an ord_iso result?  Perhaps 
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   128
     ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   129
Goal "A Int B = 0 ==>     \
3840
e0baea4d485a fixed dots;
wenzelm
parents: 3016
diff changeset
   130
\           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5488
diff changeset
   131
by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")] 
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   132
    lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   133
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   134
qed "sum_disjoint_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   135
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   136
(** Associativity **)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   137
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   138
Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   139
\ : bij((A+B)+C, A+(B+C))";
3840
e0baea4d485a fixed dots;
wenzelm
parents: 3016
diff changeset
   140
by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   141
    lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   142
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   143
qed "sum_assoc_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   144
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   145
Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   146
\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   147
\           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   148
by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   149
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   150
qed "sum_assoc_ord_iso";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   151
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   152
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   153
(**** Multiplication of relations -- lexicographic product ****)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   154
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   155
(** Rewrite rule.  Can be used to obtain introduction rules **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   156
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   157
Goalw [rmult_def] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   158
    "<<a',b'>, <a,b>> : rmult(A,r,B,s) <->       \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   159
\           (<a',a>: r  & a':A & a:A & b': B & b: B) |  \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   160
\           (<b',b>: s  & a'=a & a:A & b': B & b: B)";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   161
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   162
qed "rmult_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   163
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   164
Addsimps [rmult_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   165
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   166
val major::prems = Goal
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   167
    "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);              \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   168
\       [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   169
\       [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   170
\    |] ==> Q";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   171
by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   172
by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   173
qed "rmultE";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   174
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   175
(** Type checking **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   176
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   177
Goalw [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   178
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   179
qed "rmult_type";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   180
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 770
diff changeset
   181
bind_thm ("field_rmult", (rmult_type RS field_rel_subset));
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   182
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   183
(** Linearity **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   184
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   185
val [lina,linb] = goal OrderArith.thy
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   186
    "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   187
by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   188
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   189
by (Asm_simp_tac 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   190
by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   191
by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   192
by (REPEAT_SOME (Blast_tac));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   193
qed "linear_rmult";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   194
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   195
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   196
(** Well-foundedness **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   197
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   198
Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   199
by (rtac wf_onI2 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   200
by (etac SigmaE 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   201
by (etac ssubst 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   202
by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   203
by (Blast_tac 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   204
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   205
by (rtac ballI 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   206
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   207
by (best_tac (claset() addSEs [rmultE, bspec RS mp]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   208
qed "wf_on_rmult";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   209
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   210
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   211
Goal "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   212
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   213
by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   214
by (REPEAT (ares_tac [wf_on_rmult] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   215
qed "wf_rmult";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   216
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   217
Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   218
\           well_ord(A*B, rmult(A,r,B,s))";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   219
by (rtac well_ordI 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   220
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   221
by (asm_full_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   222
    (simpset() addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   223
qed "well_ord_rmult";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   224
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   225
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   226
(** An ord_iso congruence law **)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   227
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   228
Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
1095
6d0aad5f50a5 Changed some definitions and proofs to use pattern-matching.
lcp
parents: 859
diff changeset
   229
\        (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
6d0aad5f50a5 Changed some definitions and proofs to use pattern-matching.
lcp
parents: 859
diff changeset
   230
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] 
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   231
    lam_bijective 1);
4152
451104c223e2 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   232
by Safe_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   233
by (ALLGOALS (asm_simp_tac bij_inverse_ss));
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   234
qed "prod_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   235
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   236
Goalw [ord_iso_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   237
    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>     \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   238
\           (lam <x,y>:A*B. <f`x, g`y>)                                 \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   239
\           : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   240
by (safe_tac (claset() addSIs [prod_bij]));
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   241
by (ALLGOALS
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   242
    (asm_full_simp_tac (simpset() addsimps [bij_is_fun RS apply_type])));
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   243
by (Blast_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   244
by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   245
qed "prod_ord_iso_cong";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   246
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   247
Goal "(lam z:A. <x,z>) : bij(A, {x}*A)";
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   248
by (res_inst_tac [("d", "snd")] lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   249
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   250
qed "singleton_prod_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   251
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   252
(*Used??*)
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   253
Goal "well_ord({x},xr) ==>  \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   254
\         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   255
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   256
by (Asm_simp_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   257
by (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   258
qed "singleton_prod_ord_iso";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   259
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   260
(*Here we build a complicated function term, then simplify it using
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   261
  case_cong, id_conv, comp_lam, case_case.*)
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   262
Goal "a~:C ==> \
3840
e0baea4d485a fixed dots;
wenzelm
parents: 3016
diff changeset
   263
\      (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   264
\      : bij(C*B + D, C*B Un {a}*D)";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   265
by (rtac subst_elem 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   266
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   267
by (rtac singleton_prod_bij 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   268
by (rtac sum_disjoint_bij 1);
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   269
by (Blast_tac 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   270
by (asm_simp_tac (simpset() addcongs [case_cong]) 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   271
by (resolve_tac [comp_lam RS trans RS sym] 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   272
by (fast_tac (claset() addSEs [case_type]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   273
by (asm_simp_tac (simpset() addsimps [case_case]) 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   274
qed "prod_sum_singleton_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   275
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   276
Goal "[| a:A;  well_ord(A,r) |] ==> \
3840
e0baea4d485a fixed dots;
wenzelm
parents: 3016
diff changeset
   277
\   (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   278
\   : ord_iso(pred(A,a,r)*B + pred(B,b,s),              \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   279
\                 radd(A*B, rmult(A,r,B,s), B, s),      \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   280
\             pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   281
by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1);
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   282
by (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   283
    (simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1957
diff changeset
   284
by (Asm_simp_tac 1);
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   285
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE]));
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2925
diff changeset
   286
by (ALLGOALS Asm_simp_tac);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   287
by (ALLGOALS (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_asym])));
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   288
qed "prod_sum_singleton_ord_iso";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   289
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   290
(** Distributive law **)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   291
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   292
Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   293
\ : bij((A+B)*C, (A*C)+(B*C))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   294
by (res_inst_tac
1095
6d0aad5f50a5 Changed some definitions and proofs to use pattern-matching.
lcp
parents: 859
diff changeset
   295
    [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   296
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   297
qed "sum_prod_distrib_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   298
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   299
Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   300
\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   301
\           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   302
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   303
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   304
qed "sum_prod_distrib_ord_iso";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   305
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   306
(** Associativity **)
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   307
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   308
Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
1095
6d0aad5f50a5 Changed some definitions and proofs to use pattern-matching.
lcp
parents: 859
diff changeset
   309
by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   310
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   311
qed "prod_assoc_bij";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   312
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   313
Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1095
diff changeset
   314
\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),  \
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   315
\           A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   316
by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   317
by Auto_tac;
859
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   318
qed "prod_assoc_ord_iso";
bc5f424c8c04 Proved sum_bij, sum_ord_iso_cong, prod_bij,
lcp
parents: 835
diff changeset
   319
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   320
(**** Inverse image of a relation ****)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   321
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   322
(** Rewrite rule **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   323
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   324
Goalw [rvimage_def] "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   325
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   326
qed "rvimage_iff";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   327
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   328
(** Type checking **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   329
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   330
Goalw [rvimage_def] "rvimage(A,f,r) <= A*A";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   331
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   332
qed "rvimage_type";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   333
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 770
diff changeset
   334
bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   335
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   336
Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   337
by (Blast_tac 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   338
qed "rvimage_converse";
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   339
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   340
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   341
(** Partial Ordering Properties **)
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   342
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   343
Goalw [irrefl_def, rvimage_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   344
    "[| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   345
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   346
qed "irrefl_rvimage";
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   347
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   348
Goalw [trans_on_def, rvimage_def] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   349
    "[| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   350
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   351
qed "trans_on_rvimage";
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   352
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   353
Goalw [part_ord_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   354
    "[| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   355
by (blast_tac (claset() addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   356
qed "part_ord_rvimage";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   357
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   358
(** Linearity **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   359
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   360
val [finj,lin] = goalw OrderArith.thy [inj_def]
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   361
    "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   362
by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   363
by (REPEAT_FIRST (ares_tac [ballI]));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   364
by (asm_simp_tac (simpset() addsimps [rvimage_iff]) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   365
by (cut_facts_tac [finj] 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   366
by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   367
by (REPEAT_SOME (blast_tac (claset() addIs [apply_funtype])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   368
qed "linear_rvimage";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   369
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   370
Goalw [tot_ord_def] 
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   371
    "[| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   372
by (blast_tac (claset() addSIs [part_ord_rvimage, linear_rvimage]) 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   373
qed "tot_ord_rvimage";
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   374
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   375
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   376
(** Well-foundedness **)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   377
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   378
Goal "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   379
by (rtac wf_onI2 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   380
by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
2925
b0ae2e13db93 Using Blast_tac
paulson
parents: 2493
diff changeset
   381
by (Blast_tac 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   382
by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   383
by (blast_tac (claset() addSIs [apply_funtype]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   384
by (blast_tac (claset() addSIs [apply_funtype] 
8201
a81d18b0a9b1 tidied some proofs
paulson
parents: 6068
diff changeset
   385
                        addSDs [rvimage_iff RS iffD1]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   386
qed "wf_on_rvimage";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   387
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   388
(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   389
Goal "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   390
by (rtac well_ordI 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
   391
by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   392
by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   393
by (blast_tac (claset() addSIs [linear_rvimage]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 662
diff changeset
   394
qed "well_ord_rvimage";
815
de2d8a63256d ord_iso_rvimage: new
lcp
parents: 782
diff changeset
   395
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   396
Goalw [ord_iso_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   397
    "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   398
by (asm_full_simp_tac (simpset() addsimps [rvimage_iff]) 1);
815
de2d8a63256d ord_iso_rvimage: new
lcp
parents: 782
diff changeset
   399
qed "ord_iso_rvimage";
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   400
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4152
diff changeset
   401
Goalw [ord_iso_def, rvimage_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   402
    "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2925
diff changeset
   403
by (Blast_tac 1);
835
313ac9b513f1 Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents: 815
diff changeset
   404
qed "ord_iso_rvimage_eq";