src/ZF/Arith.ML
author lcp
Thu, 23 Jun 1994 17:38:12 +0200
changeset 437 435875e4b21d
parent 435 ca5356bd315a
child 760 f0200e91b272
permissions -rw-r--r--
modifications for cardinal arithmetic
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/arith.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For arith.thy.  Arithmetic operators and their definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Proofs about elementary arithmetic: addition, multiplication, etc.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
Could prove def_rec_0, def_rec_succ...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
open Arith;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*"Difference" is subtraction of natural numbers.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  There are no negative numbers; we have
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  Also, rec(m, 0, %z w.z) is pred(m).   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(** rec -- better than nat_rec; the succ case has no type requirement! **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val rec_trans = rec_def RS def_transrec RS trans;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
goal Arith.thy "rec(0,a,b) = a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (rtac rec_trans 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (rtac nat_case_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val rec_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (rtac rec_trans 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    32
by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val rec_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val major::prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
    "[| n: nat;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
\       a: C(0);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
\    |] ==> rec(n,a,b) : C(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (rtac (major RS nat_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    42
    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val rec_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
    45
val nat_le_refl = nat_into_Ord RS le_refl;
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    46
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    47
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    49
val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    50
		 nat_le_refl];
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    51
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
    52
val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(** Addition **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val add_type = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "[| m:nat;  n:nat |] ==> m #+ n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val add_0 = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    "0 #+ n = n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val add_succ = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
    "succ(m) #+ n = succ(m #+ n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
 (fn _=> [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
(** Multiplication **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val mult_type = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "[| m:nat;  n:nat |] ==> m #* n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val mult_0 = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "0 #* n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val mult_succ = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
    "succ(m) #* n = n #+ (m #* n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
 (fn _ => [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(** Difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
val diff_type = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    "[| m:nat;  n:nat |] ==> m #- n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
val diff_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
    "m #- 0 = m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
    "n:nat ==> 0 #- n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  [ (rtac (prem RS nat_induct) 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    98
    (ALLGOALS (asm_simp_tac nat_ss)) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
 (fn prems=>
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   105
  [ (asm_simp_tac (nat_ss addsimps prems) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
    (nat_ind_tac "n" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   107
    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
val prems = goal Arith.thy 
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   110
    "[| m:nat;  n:nat |] ==> m #- n le m";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   111
by (rtac (prems MRS diff_induct) 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   112
by (etac leE 3);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   114
    (asm_simp_tac
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   115
     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   116
				diff_succ_succ, nat_into_Ord]))));
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   117
val diff_le_self = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*** Simplification over add, mult, diff ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val arith_typechecks = [add_type, mult_type, diff_type];
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   122
val arith_simps = [add_0, add_succ,
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   123
		   mult_0, mult_succ,
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   124
		   diff_0, diff_0_eq_0, diff_succ_succ];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   126
val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(*** Addition ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
(*Associative law for addition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val add_assoc = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   135
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
(*The following two lemmas are used for add_commute and sometimes
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
  elsewhere, since they are safe for rewriting.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val add_0_right = prove_goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
    "m:nat ==> m #+ 0 = m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   143
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
val add_succ_right = prove_goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   149
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
(*Commutative law for addition*)  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
val add_commute = prove_goal Arith.thy 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   153
    "!!m n. [| m:nat;  n:nat |] ==> m #+ n = n #+ m"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   154
 (fn _ =>
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   155
  [ (nat_ind_tac "n" [] 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
    (ALLGOALS
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   157
     (asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   158
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   159
(*for a/c rewriting*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   160
val add_left_commute = prove_goal Arith.thy
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   161
    "!!m n k. [| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)"
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   162
 (fn _ => [asm_simp_tac (ZF_ss addsimps [add_assoc RS sym, add_commute]) 1]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   163
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   164
(*Addition is an AC-operator*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   165
val add_ac = [add_assoc, add_commute, add_left_commute];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
(*Cancellation law on the left*)
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   168
val [eqn,knat] = goal Arith.thy 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   169
    "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (rtac (eqn RS rev_mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
by (nat_ind_tac "k" [knat] 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   172
by (ALLGOALS (simp_tac arith_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
val add_left_cancel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
(*** Multiplication ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(*right annihilation in product*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
val mult_0_right = prove_goal Arith.thy 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   180
    "!!m. m:nat ==> m #* 0 = 0"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   181
 (fn _=>
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   182
  [ (nat_ind_tac "m" [] 1),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   183
    (ALLGOALS (asm_simp_tac arith_ss))  ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*right successor law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val mult_succ_right = prove_goal Arith.thy 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   187
    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   188
 (fn _ =>
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   189
  [ (nat_ind_tac "m" [] 1),
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   190
    (ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
(*Commutative law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val mult_commute = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
    "[| m:nat;  n:nat |] ==> m #* n = n #* m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   197
    (ALLGOALS (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   198
	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
(*addition distributes over multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val add_mult_distrib = prove_goal Arith.thy 
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   202
    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   203
 (fn _=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   204
  [ (etac nat_induct 1),
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   205
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(*Distributive law on the left; requires an extra typing premise*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
val add_mult_distrib_left = prove_goal Arith.thy 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   209
    "!!m. [| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
 (fn prems=>
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   211
  [ (nat_ind_tac "m" [] 1),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   212
    (asm_simp_tac (arith_ss addsimps [mult_0_right]) 1),
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   213
    (asm_simp_tac (arith_ss addsimps ([mult_succ_right] @ add_ac)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
(*Associative law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val mult_assoc = prove_goal Arith.thy 
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   217
    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   218
 (fn _=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   219
  [ (etac nat_induct 1),
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   220
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   222
(*for a/c rewriting*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   223
val mult_left_commute = prove_goal Arith.thy 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   224
    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)"
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   225
 (fn _ => [rtac (mult_commute RS trans) 1, 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   226
           rtac (mult_assoc RS trans) 3, 
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   227
	   rtac (mult_commute RS subst_context) 6,
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   228
	   REPEAT (ares_tac [mult_type] 1)]);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   229
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   230
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   231
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(*** Difference ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
val diff_self_eq_0 = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    "m:nat ==> m #- m = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   239
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   241
(*Addition is the inverse of subtraction*)
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   242
goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   243
by (forward_tac [lt_nat_in_nat] 1);
127
eec6bb9c58ea Misc modifs such as expandshort
lcp
parents: 25
diff changeset
   244
by (etac nat_succI 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   245
by (etac rev_mp 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   247
by (ALLGOALS (asm_simp_tac arith_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
val add_diff_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
(*Subtraction is the inverse of addition. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
val [mnat,nnat] = goal Arith.thy
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   252
    "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (rtac (nnat RS nat_induct) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   254
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val diff_add_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   257
goal Arith.thy
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   258
    "!!m n. [| m:nat;  n:nat |] ==> (m#+n) #- n = m";
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   259
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   260
by (REPEAT (ares_tac [diff_add_inverse] 1));
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   261
val diff_add_inverse2 = result();
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   262
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
val [mnat,nnat] = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
by (rtac (nnat RS nat_induct) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   266
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
val diff_add_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
(*** Remainder ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   272
goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   273
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (etac rev_mp 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (etac rev_mp 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   277
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
val div_termination = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   280
val div_rls =	(*for mod and div*)
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   281
    nat_typechecks @
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   282
    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   283
     nat_into_Ord, not_lt_iff_le RS iffD1];
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   284
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   285
val div_ss = ZF_ss addsimps [nat_into_Ord, div_termination RS ltD,
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   286
			     not_lt_iff_le RS iffD2];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
(*Type checking depends upon termination!*)
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   289
goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   290
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
val mod_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   293
goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
by (rtac (mod_def RS def_transrec RS trans) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   295
by (asm_simp_tac div_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
val mod_less = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   298
goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   299
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
by (rtac (mod_def RS def_transrec RS trans) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   301
by (asm_simp_tac div_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
val mod_geq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
(*** Quotient ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
(*Type checking depends upon termination!*)
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   307
goalw Arith.thy [div_def]
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   308
    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   309
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
val div_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   312
goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
by (rtac (div_def RS def_transrec RS trans) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   314
by (asm_simp_tac div_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
val div_less = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   317
goal Arith.thy
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   318
 "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   319
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
by (rtac (div_def RS def_transrec RS trans) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   321
by (asm_simp_tac div_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
val div_geq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
(*Main Result.*)
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   325
goal Arith.thy
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   326
    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   327
by (etac complete_induct 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   328
by (excluded_middle_tac "x<n" 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   329
(*case x<n*)
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   330
by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   331
(*case n le x*)
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   332
by (asm_full_simp_tac
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   333
     (arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   334
			 mod_geq, div_geq, add_assoc,
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   335
			 div_termination RS ltD, add_diff_inverse]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
val mod_div_equality = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   339
(**** Additional theorems about "le" ****)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   341
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   342
by (etac nat_induct 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   343
by (ALLGOALS (asm_simp_tac arith_ss));
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   344
val add_le_self = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   345
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   346
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   347
by (rtac (add_commute RS ssubst) 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   348
by (REPEAT (ares_tac [add_le_self] 1));
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   349
val add_le_self2 = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   350
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   351
(** Monotonicity of addition **)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   352
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   353
(*strict, in 1st argument*)
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   354
goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   355
by (forward_tac [lt_nat_in_nat] 1);
127
eec6bb9c58ea Misc modifs such as expandshort
lcp
parents: 25
diff changeset
   356
by (assume_tac 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   357
by (etac succ_lt_induct 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   358
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   359
val add_lt_mono1 = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   360
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   361
(*strict, in both arguments*)
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   362
goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   363
by (rtac (add_lt_mono1 RS lt_trans) 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   364
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   365
by (EVERY [rtac (add_commute RS ssubst) 1,
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   366
	   rtac (add_commute RS ssubst) 3,
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   367
	   rtac add_lt_mono1 5]);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   368
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   369
val add_lt_mono = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   370
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   371
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   372
val lt_mono::ford::prems = goal Ordinal.thy
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   373
     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   374
\        !!i. i:k ==> Ord(f(i));		\
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   375
\        i le j;  j:k				\
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   376
\     |] ==> f(i) le f(j)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   377
by (cut_facts_tac prems 1);
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   378
by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   379
val Ord_lt_mono_imp_le_mono = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   380
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   381
(*le monotonicity, 1st argument*)
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   382
goal Arith.thy
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   383
    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   384
by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 127
diff changeset
   385
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   386
val add_le_mono1 = result();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   387
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   388
(* le monotonicity, BOTH arguments*)
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   389
goal Arith.thy
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   390
    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   391
by (rtac (add_le_mono1 RS le_trans) 1);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   392
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   393
by (EVERY [rtac (add_commute RS ssubst) 1,
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   394
	   rtac (add_commute RS ssubst) 3,
25
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   395
	   rtac add_le_mono1 5]);
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   396
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
3ac1c0c0016e ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents: 14
diff changeset
   397
val add_le_mono = result();