src/ZF/arith.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 25 3ac1c0c0016e
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    47
val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(** Addition **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
val add_type = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    "[| m:nat;  n:nat |] ==> m #+ n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val add_0 = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
    "0 #+ n = n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val add_succ = prove_goalw Arith.thy [add_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    "succ(m) #+ n = succ(m #+ n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
 (fn _=> [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
(** Multiplication **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val mult_type = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
    "[| m:nat;  n:nat |] ==> m #* n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val mult_0 = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "0 #* n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val mult_succ = prove_goalw Arith.thy [mult_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "succ(m) #* n = n #+ (m #* n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
 (fn _ => [ (rtac rec_succ 1) ]); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
(** Difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val diff_type = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    "[| m:nat;  n:nat |] ==> m #- n : nat"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val diff_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    "m #- 0 = m"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
 (fn _ => [ (rtac rec_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    "n:nat ==> 0 #- n = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  [ (rtac (prem RS nat_induct) 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    93
    (ALLGOALS (asm_simp_tac nat_ss)) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
 (fn prems=>
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   100
  [ (asm_simp_tac (nat_ss addsimps prems) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
    (nat_ind_tac "n" prems 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   102
    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   104
(*The conclusion is equivalent to m#-n <= m *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val prems = goal Arith.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (etac succE 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (ALLGOALS
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   112
    (asm_simp_tac
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   113
     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   114
				diff_succ_succ]))));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   115
val diff_less_succ = result();
0
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 
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   196
    "!!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
   197
 (fn _=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   198
  [ (etac nat_induct 1),
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   199
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
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 
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   212
    "!!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
   213
 (fn _=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   214
  [ (etac nat_induct 1),
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   215
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [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
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   234
	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   235
					 naturals_are_ordinals]))));
0
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);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   260
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,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);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   338
by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
0
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();
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   341
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   342
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   343
by (rtac (add_less_succ_self RS member_succD) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   344
by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   345
val add_leq_self = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   346
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   347
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   348
by (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
   349
by (REPEAT (ares_tac [add_leq_self] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   350
val add_leq_self2 = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   351
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   352
(** Monotonicity of addition **)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   353
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   354
(*strict, in 1st argument*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   355
goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   356
by (etac succ_less_induct 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   357
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   358
val add_less_mono1 = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   359
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   360
(*strict, in both arguments*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   361
goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   362
by (rtac (add_less_mono1 RS Ord_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   363
by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   364
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
   365
	   rtac (add_commute RS ssubst) 3,
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   366
	   rtac add_less_mono1 5]);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   367
by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   368
val add_less_mono = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   369
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   370
(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   371
val less_mono::ford::prems = goal Ord.thy
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   372
     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   373
\        !!i. i:k ==> f(i):k;			\
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   374
\        i<=j;  i:k;  j:k;  Ord(k)		\
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   375
\     |] ==> f(i) <= f(j)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   376
by (cut_facts_tac prems 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   377
by (rtac member_succD 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   378
by (dtac member_succI 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   379
by (fast_tac (ZF_cs addSIs [less_mono]) 3);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   380
by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   381
val Ord_less_mono_imp_mono = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   382
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   383
(*<=, in 1st argument*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   384
goal Arith.thy
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   385
    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   386
by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   387
by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   388
val add_mono1 = result();
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   389
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   390
(*<=, in both arguments*)
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   391
goal Arith.thy
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   392
    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   393
by (rtac (add_mono1 RS subset_trans) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   394
by (REPEAT (assume_tac 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   395
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
   396
	   rtac (add_commute RS ssubst) 3,
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   397
	   rtac add_mono1 5]);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   398
by (REPEAT (assume_tac 1));
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   399
val add_mono = result();