src/ZF/Arith.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
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
val rec_ss = ZF_ss 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    32
      addsimps [nat_case_succ, nat_succI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (rtac rec_trans 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    34
by (simp_tac rec_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val rec_succ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val major::prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
    "[| n: nat;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
\       a: C(0);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
\    |] ==> rec(n,a,b) : C(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (rtac (major RS nat_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    44
    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val rec_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    49
val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(** Addition **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val add_type = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    "[| m:nat;  n:nat |] ==> m #+ n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val add_0 = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "0 #+ n = n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val add_succ = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    "succ(m) #+ n = succ(m #+ n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
 (fn _=> [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(** Multiplication **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val mult_type = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
    "[| m:nat;  n:nat |] ==> m #* n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val mult_0 = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    "0 #* n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val mult_succ = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
    "succ(m) #* n = n #+ (m #* n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
 (fn _ => [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(** Difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val diff_type = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
    "[| m:nat;  n:nat |] ==> m #- n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val diff_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    "m #- 0 = m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    "n:nat ==> 0 #- n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  [ (rtac (prem RS nat_induct) 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    95
    (ALLGOALS (asm_simp_tac nat_ss)) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
 (fn prems=>
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   102
  [ (asm_simp_tac (nat_ss addsimps prems) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    (nat_ind_tac "n" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   104
    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val prems = goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (etac succE 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   113
    (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   114
     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
val diff_leq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*** Simplification over add, mult, diff ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
val arith_typechecks = [add_type, mult_type, diff_type];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val arith_rews = [add_0, add_succ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
		  mult_0, mult_succ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
		  diff_0, diff_0_eq_0, diff_succ_succ];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   124
val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
(*** Addition ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(*Associative law for addition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val add_assoc = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   133
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
(*The following two lemmas are used for add_commute and sometimes
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
  elsewhere, since they are safe for rewriting.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
val add_0_right = prove_goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
    "m:nat ==> m #+ 0 = m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   141
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
val add_succ_right = prove_goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   147
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*Commutative law for addition*)  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val add_commute = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
  [ (nat_ind_tac "n" prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
    (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   155
     (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   156
      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*Cancellation law on the left*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val [knat,eqn] = goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
    "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (rtac (eqn RS rev_mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
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
   163
by (ALLGOALS (simp_tac arith_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
val add_left_cancel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
(*** Multiplication ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
(*right annihilation in product*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val mult_0_right = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
    "m:nat ==> m #* 0 = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   174
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
(*right successor law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
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
   178
    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   179
 (fn _=>
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   180
  [ (nat_ind_tac "m" [] 1),
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   181
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
       (*The final goal requires the commutative law for addition*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   183
    (rtac (add_commute RS subst_context) 1),
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   184
    (REPEAT (assume_tac 1))  ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
(*Commutative law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val mult_commute = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    "[| m:nat;  n:nat |] ==> m #* n = n #* m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   191
    (ALLGOALS (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   192
	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
(*addition distributes over multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
val add_mult_distrib = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   199
    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
(*Distributive law on the left; requires an extra typing premise*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
val add_mult_distrib_left = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
    "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
      let val mult_commute' = read_instantiate [("m","k")] mult_commute
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   206
          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   207
      in [ (simp_tac ss 1) ]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
      end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(*Associative law for multiplication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val mult_assoc = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   215
    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*** Difference ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
val diff_self_eq_0 = prove_goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    "m:nat ==> m #- m = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
  [ (nat_ind_tac "m" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   224
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
val notless::prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
by (rtac (notless RS rev_mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
by (resolve_tac prems 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   233
by (ALLGOALS (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   234
	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
				  naturals_are_ordinals]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
val add_diff_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
(*Subtraction is the inverse of addition. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
val [mnat,nnat] = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
    "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
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
   243
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
val diff_add_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
val [mnat,nnat] = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
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
   249
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
val diff_add_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
(*** Remainder ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   256
goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
by (etac rev_mp 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
by (etac rev_mp 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   260
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
val div_termination = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
val div_rls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
    nat_typechecks;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
(*Type checking depends upon termination!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
val prems = goalw Arith.thy [mod_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
val mod_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   273
val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
by (rtac (mod_def RS def_transrec RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   277
by (simp_tac (div_ss addsimps prems) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
val mod_less = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
val prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (rtac (mod_def RS def_transrec RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   283
by (simp_tac (div_ss addsimps prems) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
val mod_geq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
(*** Quotient ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
(*Type checking depends upon termination!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
val prems = goalw Arith.thy [div_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
val div_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
val prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
by (rtac (div_def RS def_transrec RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   297
by (simp_tac (div_ss addsimps prems) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val div_less = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
val prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
by (rtac (div_def RS def_transrec RS trans) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   303
by (simp_tac (div_ss addsimps prems) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
val div_geq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
(*Main Result.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
val prems = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
by (res_inst_tac [("i","m")] complete_induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
by (ALLGOALS 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   313
    (asm_simp_tac
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   314
     (arith_ss addsimps ([mod_type,div_type] @ prems @
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
        [mod_less,mod_geq, div_less, div_geq,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
	 add_assoc, add_diff_inverse, div_termination]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
val mod_div_equality = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
(**** Additional theorems about "less than" ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
val [mnat,nnat] = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (rtac (mnat RS nat_induct) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   325
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
by (rtac notI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
by (etac notE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
by (etac (succI1 RS Ord_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
by (rtac (nnat RS naturals_are_ordinals) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
val add_not_less_self = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
val [mnat,nnat] = goal Arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (rtac (mnat RS nat_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
by (rtac (add_0 RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
by (rtac (add_succ RS ssubst) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
		      naturals_are_ordinals, nat_succI, add_type] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
val add_less_succ_self = result();