src/CTT/Arith.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1459 d12da312eff4
child 3837 d7f033c74b38
permissions -rw-r--r--
Cosmetic re-ordering of declarations
clasohm@1459
     1
(*  Title:      CTT/arith
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Theorems for arith.thy (Arithmetic operators)
clasohm@0
     7
clasohm@0
     8
Proofs about elementary arithmetic: addition, multiplication, etc.
clasohm@0
     9
Tests definitions and simplifier.
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
open Arith;
clasohm@0
    13
val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
clasohm@0
    14
clasohm@0
    15
clasohm@0
    16
(** Addition *)
clasohm@0
    17
clasohm@0
    18
(*typing of add: short and long versions*)
clasohm@0
    19
clasohm@1294
    20
qed_goalw "add_typing" Arith.thy arith_defs
clasohm@0
    21
    "[| a:N;  b:N |] ==> a #+ b : N"
lcp@354
    22
 (fn prems=> [ (typechk_tac prems) ]);
clasohm@0
    23
clasohm@1294
    24
qed_goalw "add_typingL" Arith.thy arith_defs
clasohm@0
    25
    "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
lcp@354
    26
 (fn prems=> [ (equal_tac prems) ]);
clasohm@0
    27
clasohm@0
    28
clasohm@0
    29
(*computation for add: 0 and successor cases*)
clasohm@0
    30
clasohm@1294
    31
qed_goalw "addC0" Arith.thy arith_defs
clasohm@0
    32
    "b:N ==> 0 #+ b = b : N"
lcp@354
    33
 (fn prems=> [ (rew_tac prems) ]);
clasohm@0
    34
clasohm@1294
    35
qed_goalw "addC_succ" Arith.thy arith_defs
clasohm@0
    36
    "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
lcp@354
    37
 (fn prems=> [ (rew_tac prems) ]); 
clasohm@0
    38
clasohm@0
    39
clasohm@0
    40
(** Multiplication *)
clasohm@0
    41
clasohm@0
    42
(*typing of mult: short and long versions*)
clasohm@0
    43
clasohm@1294
    44
qed_goalw "mult_typing" Arith.thy arith_defs
clasohm@0
    45
    "[| a:N;  b:N |] ==> a #* b : N"
clasohm@0
    46
 (fn prems=>
lcp@354
    47
  [ (typechk_tac([add_typing]@prems)) ]);
clasohm@0
    48
clasohm@1294
    49
qed_goalw "mult_typingL" Arith.thy arith_defs
clasohm@0
    50
    "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
clasohm@0
    51
 (fn prems=>
lcp@354
    52
  [ (equal_tac (prems@[add_typingL])) ]);
clasohm@0
    53
clasohm@0
    54
(*computation for mult: 0 and successor cases*)
clasohm@0
    55
clasohm@1294
    56
qed_goalw "multC0" Arith.thy arith_defs
clasohm@0
    57
    "b:N ==> 0 #* b = 0 : N"
lcp@354
    58
 (fn prems=> [ (rew_tac prems) ]);
clasohm@0
    59
clasohm@1294
    60
qed_goalw "multC_succ" Arith.thy arith_defs
clasohm@0
    61
    "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
lcp@354
    62
 (fn prems=> [ (rew_tac prems) ]);
clasohm@0
    63
clasohm@0
    64
clasohm@0
    65
(** Difference *)
clasohm@0
    66
clasohm@0
    67
(*typing of difference*)
clasohm@0
    68
clasohm@1294
    69
qed_goalw "diff_typing" Arith.thy arith_defs
clasohm@0
    70
    "[| a:N;  b:N |] ==> a - b : N"
lcp@354
    71
 (fn prems=> [ (typechk_tac prems) ]);
clasohm@0
    72
clasohm@1294
    73
qed_goalw "diff_typingL" Arith.thy arith_defs
clasohm@0
    74
    "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
lcp@354
    75
 (fn prems=> [ (equal_tac prems) ]);
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
clasohm@0
    79
(*computation for difference: 0 and successor cases*)
clasohm@0
    80
clasohm@1294
    81
qed_goalw "diffC0" Arith.thy arith_defs
clasohm@0
    82
    "a:N ==> a - 0 = a : N"
lcp@354
    83
 (fn prems=> [ (rew_tac prems) ]);
clasohm@0
    84
clasohm@0
    85
(*Note: rec(a, 0, %z w.z) is pred(a). *)
clasohm@0
    86
clasohm@1294
    87
qed_goalw "diff_0_eq_0" Arith.thy arith_defs
clasohm@0
    88
    "b:N ==> 0 - b = 0 : N"
clasohm@0
    89
 (fn prems=>
clasohm@0
    90
  [ (NE_tac "b" 1),
clasohm@0
    91
    (hyp_rew_tac prems) ]);
clasohm@0
    92
clasohm@0
    93
clasohm@0
    94
(*Essential to simplify FIRST!!  (Else we get a critical pair)
clasohm@0
    95
  succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
clasohm@1294
    96
qed_goalw "diff_succ_succ" Arith.thy arith_defs
clasohm@0
    97
    "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
clasohm@0
    98
 (fn prems=>
lcp@354
    99
  [ (hyp_rew_tac prems),
clasohm@0
   100
    (NE_tac "b" 1),
clasohm@0
   101
    (hyp_rew_tac prems) ]);
clasohm@0
   102
clasohm@0
   103
clasohm@0
   104
clasohm@0
   105
(*** Simplification *)
clasohm@0
   106
clasohm@0
   107
val arith_typing_rls =
clasohm@0
   108
  [add_typing, mult_typing, diff_typing];
clasohm@0
   109
clasohm@0
   110
val arith_congr_rls =
clasohm@0
   111
  [add_typingL, mult_typingL, diff_typingL];
clasohm@0
   112
clasohm@0
   113
val congr_rls = arith_congr_rls@standard_congr_rls;
clasohm@0
   114
clasohm@0
   115
val arithC_rls =
clasohm@0
   116
  [addC0, addC_succ,
clasohm@0
   117
   multC0, multC_succ,
clasohm@0
   118
   diffC0, diff_0_eq_0, diff_succ_succ];
clasohm@0
   119
clasohm@0
   120
clasohm@0
   121
structure Arith_simp_data: TSIMP_DATA =
clasohm@0
   122
  struct
clasohm@1459
   123
  val refl              = refl_elem
clasohm@1459
   124
  val sym               = sym_elem
clasohm@1459
   125
  val trans             = trans_elem
clasohm@1459
   126
  val refl_red          = refl_red
clasohm@1459
   127
  val trans_red         = trans_red
clasohm@1459
   128
  val red_if_equal      = red_if_equal
clasohm@1459
   129
  val default_rls       = arithC_rls @ comp_rls
clasohm@1459
   130
  val routine_tac       = routine_tac (arith_typing_rls @ routine_rls)
clasohm@0
   131
  end;
clasohm@0
   132
clasohm@0
   133
structure Arith_simp = TSimpFun (Arith_simp_data);
clasohm@0
   134
clasohm@0
   135
fun arith_rew_tac prems = make_rew_tac
clasohm@0
   136
    (Arith_simp.norm_tac(congr_rls, prems));
clasohm@0
   137
clasohm@0
   138
fun hyp_arith_rew_tac prems = make_rew_tac
clasohm@0
   139
    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));
clasohm@0
   140
clasohm@0
   141
clasohm@0
   142
(**********
clasohm@0
   143
  Addition
clasohm@0
   144
 **********)
clasohm@0
   145
clasohm@0
   146
(*Associative law for addition*)
clasohm@1294
   147
qed_goal "add_assoc" Arith.thy 
clasohm@0
   148
    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
clasohm@0
   149
 (fn prems=>
clasohm@0
   150
  [ (NE_tac "a" 1),
clasohm@0
   151
    (hyp_arith_rew_tac prems) ]);
clasohm@0
   152
clasohm@0
   153
clasohm@0
   154
(*Commutative law for addition.  Can be proved using three inductions.
clasohm@0
   155
  Must simplify after first induction!  Orientation of rewrites is delicate*)  
clasohm@1294
   156
qed_goal "add_commute" Arith.thy 
clasohm@0
   157
    "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
clasohm@0
   158
 (fn prems=>
clasohm@0
   159
  [ (NE_tac "a" 1),
clasohm@0
   160
    (hyp_arith_rew_tac prems),
clasohm@0
   161
    (NE_tac "b" 2),
clasohm@1459
   162
    (rtac sym_elem 1),
clasohm@0
   163
    (NE_tac "b" 1),
clasohm@0
   164
    (hyp_arith_rew_tac prems) ]);
clasohm@0
   165
clasohm@0
   166
clasohm@0
   167
(****************
clasohm@0
   168
  Multiplication
clasohm@0
   169
 ****************)
clasohm@0
   170
clasohm@0
   171
(*Commutative law for multiplication
clasohm@1294
   172
qed_goal "mult_commute" Arith.thy 
clasohm@0
   173
    "[| a:N;  b:N |] ==> a #* b = b #* a : N"
clasohm@0
   174
 (fn prems=>
clasohm@0
   175
  [ (NE_tac "a" 1),
clasohm@0
   176
    (hyp_arith_rew_tac prems),
clasohm@0
   177
    (NE_tac "b" 2),
clasohm@1459
   178
    (rtac sym_elem 1),
clasohm@0
   179
    (NE_tac "b" 1),
clasohm@0
   180
    (hyp_arith_rew_tac prems) ]);   NEEDS COMMUTATIVE MATCHING
clasohm@0
   181
***************)
clasohm@0
   182
clasohm@0
   183
(*right annihilation in product*)
clasohm@1294
   184
qed_goal "mult_0_right" Arith.thy 
clasohm@0
   185
    "a:N ==> a #* 0 = 0 : N"
clasohm@0
   186
 (fn prems=>
clasohm@0
   187
  [ (NE_tac "a" 1),
clasohm@0
   188
    (hyp_arith_rew_tac prems) ]);
clasohm@0
   189
clasohm@0
   190
(*right successor law for multiplication*)
clasohm@1294
   191
qed_goal "mult_succ_right" Arith.thy 
clasohm@0
   192
    "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
clasohm@0
   193
 (fn prems=>
clasohm@0
   194
  [ (NE_tac "a" 1),
clasohm@0
   195
(*swap round the associative law of addition*)
clasohm@0
   196
    (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])),  
clasohm@0
   197
(*leaves a goal involving a commutative law*)
clasohm@0
   198
    (REPEAT (assume_tac 1  ORELSE  
clasohm@0
   199
            resolve_tac
clasohm@0
   200
             (prems@[add_commute,mult_typingL,add_typingL]@
clasohm@1459
   201
               intrL_rls@[refl_elem])   1)) ]);
clasohm@0
   202
clasohm@0
   203
(*Commutative law for multiplication*)
clasohm@1294
   204
qed_goal "mult_commute" Arith.thy 
clasohm@0
   205
    "[| a:N;  b:N |] ==> a #* b = b #* a : N"
clasohm@0
   206
 (fn prems=>
clasohm@0
   207
  [ (NE_tac "a" 1),
clasohm@0
   208
    (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]);
clasohm@0
   209
clasohm@0
   210
(*addition distributes over multiplication*)
clasohm@1294
   211
qed_goal "add_mult_distrib" Arith.thy 
clasohm@0
   212
    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
clasohm@0
   213
 (fn prems=>
clasohm@0
   214
  [ (NE_tac "a" 1),
clasohm@0
   215
(*swap round the associative law of addition*)
clasohm@0
   216
    (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ]);
clasohm@0
   217
clasohm@0
   218
clasohm@0
   219
(*Associative law for multiplication*)
clasohm@1294
   220
qed_goal "mult_assoc" Arith.thy 
clasohm@0
   221
    "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
clasohm@0
   222
 (fn prems=>
clasohm@0
   223
  [ (NE_tac "a" 1),
clasohm@0
   224
    (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ]);
clasohm@0
   225
clasohm@0
   226
clasohm@0
   227
(************
clasohm@0
   228
  Difference
clasohm@0
   229
 ************
clasohm@0
   230
clasohm@0
   231
Difference on natural numbers, without negative numbers
clasohm@0
   232
  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
clasohm@0
   233
clasohm@1294
   234
qed_goal "diff_self_eq_0" Arith.thy 
clasohm@0
   235
    "a:N ==> a - a = 0 : N"
clasohm@0
   236
 (fn prems=>
clasohm@0
   237
  [ (NE_tac "a" 1),
clasohm@0
   238
    (hyp_arith_rew_tac prems) ]);
clasohm@0
   239
clasohm@0
   240
clasohm@0
   241
(*  [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N  *)
clasohm@0
   242
val add_0_right = addC0 RSN (3, add_commute RS trans_elem);
clasohm@0
   243
clasohm@0
   244
(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
clasohm@0
   245
  An example of induction over a quantified formula (a product).
clasohm@0
   246
  Uses rewriting with a quantified, implicative inductive hypothesis.*)
clasohm@0
   247
val prems =
clasohm@0
   248
goal Arith.thy 
clasohm@0
   249
    "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
clasohm@0
   250
by (NE_tac "b" 1);
clasohm@0
   251
(*strip one "universal quantifier" but not the "implication"*)
clasohm@0
   252
by (resolve_tac intr_rls 3);  
clasohm@0
   253
(*case analysis on x in
clasohm@0
   254
    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
clasohm@0
   255
by (NE_tac "x" 4 THEN assume_tac 4); 
clasohm@0
   256
(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
clasohm@1459
   257
by (rtac replace_type 5);
clasohm@1459
   258
by (rtac replace_type 4);
clasohm@0
   259
by (arith_rew_tac prems); 
clasohm@0
   260
(*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
clasohm@0
   261
  Both follow by rewriting, (2) using quantified induction hyp*)
clasohm@0
   262
by (intr_tac[]);  (*strips remaining PRODs*)
clasohm@0
   263
by (hyp_arith_rew_tac (prems@[add_0_right]));  
clasohm@0
   264
by (assume_tac 1);
clasohm@1294
   265
qed "add_diff_inverse_lemma";
clasohm@0
   266
clasohm@0
   267
clasohm@0
   268
(*Version of above with premise   b-a=0   i.e.    a >= b.
clasohm@0
   269
  Using ProdE does not work -- for ?B(?a) is ambiguous.
clasohm@0
   270
  Instead, add_diff_inverse_lemma states the desired induction scheme;
clasohm@0
   271
    the use of RS below instantiates Vars in ProdE automatically. *)
clasohm@0
   272
val prems =
clasohm@0
   273
goal Arith.thy "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
clasohm@1459
   274
by (rtac EqE 1);
clasohm@0
   275
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
clasohm@0
   276
by (REPEAT (resolve_tac (prems@[EqI]) 1));
clasohm@1294
   277
qed "add_diff_inverse";
clasohm@0
   278
clasohm@0
   279
clasohm@0
   280
(********************
clasohm@0
   281
  Absolute difference
clasohm@0
   282
 ********************)
clasohm@0
   283
clasohm@0
   284
(*typing of absolute difference: short and long versions*)
clasohm@0
   285
clasohm@1294
   286
qed_goalw "absdiff_typing" Arith.thy arith_defs
clasohm@0
   287
    "[| a:N;  b:N |] ==> a |-| b : N"
lcp@354
   288
 (fn prems=> [ (typechk_tac prems) ]);
clasohm@0
   289
clasohm@1294
   290
qed_goalw "absdiff_typingL" Arith.thy arith_defs
clasohm@0
   291
    "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
lcp@354
   292
 (fn prems=> [ (equal_tac prems) ]);
clasohm@0
   293
clasohm@1294
   294
qed_goalw "absdiff_self_eq_0" Arith.thy [absdiff_def]
clasohm@0
   295
    "a:N ==> a |-| a = 0 : N"
clasohm@0
   296
 (fn prems=>
lcp@354
   297
  [ (arith_rew_tac (prems@[diff_self_eq_0])) ]);
clasohm@0
   298
clasohm@1294
   299
qed_goalw "absdiffC0" Arith.thy [absdiff_def]
clasohm@0
   300
    "a:N ==> 0 |-| a = a : N"
clasohm@0
   301
 (fn prems=>
lcp@354
   302
  [ (hyp_arith_rew_tac prems) ]);
clasohm@0
   303
clasohm@0
   304
clasohm@1294
   305
qed_goalw "absdiff_succ_succ" Arith.thy [absdiff_def]
clasohm@0
   306
    "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
clasohm@0
   307
 (fn prems=>
lcp@354
   308
  [ (hyp_arith_rew_tac prems) ]);
clasohm@0
   309
clasohm@0
   310
(*Note how easy using commutative laws can be?  ...not always... *)
lcp@354
   311
val prems = goalw Arith.thy [absdiff_def]
lcp@354
   312
    "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
clasohm@1459
   313
by (rtac add_commute 1);
clasohm@0
   314
by (typechk_tac ([diff_typing]@prems));
clasohm@1294
   315
qed "absdiff_commute";
clasohm@0
   316
clasohm@0
   317
(*If a+b=0 then a=0.   Surprisingly tedious*)
clasohm@0
   318
val prems =
clasohm@0
   319
goal Arith.thy "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
clasohm@0
   320
by (NE_tac "a" 1);
clasohm@1459
   321
by (rtac replace_type 3);
clasohm@0
   322
by (arith_rew_tac prems);
clasohm@0
   323
by (intr_tac[]);  (*strips remaining PRODs*)
clasohm@0
   324
by (resolve_tac [ zero_ne_succ RS FE ] 2);
clasohm@0
   325
by (etac (EqE RS sym_elem) 3);
clasohm@0
   326
by (typechk_tac ([add_typing] @prems));
clasohm@1294
   327
qed "add_eq0_lemma";
clasohm@0
   328
clasohm@0
   329
(*Version of above with the premise  a+b=0.
clasohm@0
   330
  Again, resolution instantiates variables in ProdE *)
clasohm@0
   331
val prems =
clasohm@0
   332
goal Arith.thy "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
clasohm@1459
   333
by (rtac EqE 1);
clasohm@0
   334
by (resolve_tac [add_eq0_lemma RS ProdE] 1);
clasohm@1459
   335
by (rtac EqI 3);
clasohm@0
   336
by (ALLGOALS (resolve_tac prems));
clasohm@1294
   337
qed "add_eq0";
clasohm@0
   338
clasohm@0
   339
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
lcp@354
   340
val prems = goalw Arith.thy [absdiff_def]
clasohm@0
   341
    "[| a:N;  b:N;  a |-| b = 0 : N |] ==> \
clasohm@0
   342
\    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
clasohm@0
   343
by (intr_tac[]);
clasohm@0
   344
by eqintr_tac;
clasohm@1459
   345
by (rtac add_eq0 2);
clasohm@1459
   346
by (rtac add_eq0 1);
clasohm@0
   347
by (resolve_tac [add_commute RS trans_elem] 6);
lcp@354
   348
by (typechk_tac (diff_typing::prems));
clasohm@1294
   349
qed "absdiff_eq0_lem";
clasohm@0
   350
clasohm@0
   351
(*if  a |-| b = 0  then  a = b  
clasohm@0
   352
  proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
clasohm@0
   353
val prems =
clasohm@0
   354
goal Arith.thy "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
clasohm@1459
   355
by (rtac EqE 1);
clasohm@0
   356
by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
clasohm@0
   357
by (TRYALL (resolve_tac prems));
clasohm@0
   358
by eqintr_tac;
clasohm@0
   359
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
clasohm@1459
   360
by (rtac EqE 3  THEN  assume_tac 3);
clasohm@0
   361
by (hyp_arith_rew_tac (prems@[add_0_right]));
clasohm@1294
   362
qed "absdiff_eq0";
clasohm@0
   363
clasohm@0
   364
(***********************
clasohm@0
   365
  Remainder and Quotient
clasohm@0
   366
 ***********************)
clasohm@0
   367
clasohm@0
   368
(*typing of remainder: short and long versions*)
clasohm@0
   369
clasohm@1294
   370
qed_goalw "mod_typing" Arith.thy [mod_def]
clasohm@0
   371
    "[| a:N;  b:N |] ==> a mod b : N"
clasohm@0
   372
 (fn prems=>
lcp@354
   373
  [ (typechk_tac (absdiff_typing::prems)) ]);
clasohm@0
   374
 
clasohm@1294
   375
qed_goalw "mod_typingL" Arith.thy [mod_def]
clasohm@0
   376
    "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
clasohm@0
   377
 (fn prems=>
lcp@354
   378
  [ (equal_tac (prems@[absdiff_typingL])) ]);
clasohm@0
   379
 
clasohm@0
   380
clasohm@0
   381
(*computation for  mod : 0 and successor cases*)
clasohm@0
   382
clasohm@1294
   383
qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
clasohm@0
   384
 (fn prems=>
lcp@354
   385
  [ (rew_tac(absdiff_typing::prems)) ]);
clasohm@0
   386
clasohm@1294
   387
qed_goalw "modC_succ" Arith.thy [mod_def] 
clasohm@0
   388
"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
clasohm@0
   389
 (fn prems=>
lcp@354
   390
  [ (rew_tac(absdiff_typing::prems)) ]);
clasohm@0
   391
clasohm@0
   392
clasohm@0
   393
(*typing of quotient: short and long versions*)
clasohm@0
   394
clasohm@1294
   395
qed_goalw "div_typing" Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
clasohm@0
   396
 (fn prems=>
lcp@354
   397
  [ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
clasohm@0
   398
clasohm@1294
   399
qed_goalw "div_typingL" Arith.thy [div_def]
clasohm@0
   400
   "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
clasohm@0
   401
 (fn prems=>
lcp@354
   402
  [ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
clasohm@0
   403
clasohm@0
   404
val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
clasohm@0
   405
clasohm@0
   406
clasohm@0
   407
(*computation for quotient: 0 and successor cases*)
clasohm@0
   408
clasohm@1294
   409
qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
clasohm@0
   410
 (fn prems=>
lcp@354
   411
  [ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
clasohm@0
   412
clasohm@0
   413
val divC_succ =
lcp@354
   414
prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> succ(a) div b = \
clasohm@0
   415
\    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
clasohm@0
   416
 (fn prems=>
lcp@354
   417
  [ (rew_tac([mod_typing]@prems)) ]);
clasohm@0
   418
clasohm@0
   419
clasohm@0
   420
(*Version of above with same condition as the  mod  one*)
clasohm@1294
   421
qed_goal "divC_succ2" Arith.thy
clasohm@0
   422
    "[| a:N;  b:N |] ==> \
clasohm@0
   423
\    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
clasohm@0
   424
 (fn prems=>
clasohm@0
   425
  [ (resolve_tac [ divC_succ RS trans_elem ] 1),
clasohm@0
   426
    (rew_tac(div_typing_rls @ prems @ [modC_succ])),
clasohm@0
   427
    (NE_tac "succ(a mod b)|-|b" 1),
clasohm@0
   428
    (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);
clasohm@0
   429
clasohm@0
   430
(*for case analysis on whether a number is 0 or a successor*)
clasohm@1294
   431
qed_goal "iszero_decidable" Arith.thy
clasohm@0
   432
    "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
clasohm@1459
   433
\                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
clasohm@0
   434
 (fn prems=>
clasohm@0
   435
  [ (NE_tac "a" 1),
clasohm@1459
   436
    (rtac PlusI_inr 3),
clasohm@1459
   437
    (rtac PlusI_inl 2),
clasohm@0
   438
    eqintr_tac,
clasohm@0
   439
    (equal_tac prems) ]);
clasohm@0
   440
clasohm@0
   441
(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
clasohm@0
   442
val prems =
clasohm@0
   443
goal Arith.thy "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
clasohm@0
   444
by (NE_tac "a" 1);
clasohm@0
   445
by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); 
clasohm@1459
   446
by (rtac EqE 1);
clasohm@0
   447
(*case analysis on   succ(u mod b)|-|b  *)
clasohm@0
   448
by (res_inst_tac [("a1", "succ(u mod b) |-| b")] 
clasohm@0
   449
                 (iszero_decidable RS PlusE) 1);
clasohm@0
   450
by (etac SumE 3);
clasohm@0
   451
by (hyp_arith_rew_tac (prems @ div_typing_rls @
clasohm@1459
   452
        [modC0,modC_succ, divC0, divC_succ2])); 
clasohm@0
   453
(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
clasohm@0
   454
by (resolve_tac [ add_typingL RS trans_elem ] 1);
clasohm@0
   455
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
clasohm@1459
   456
by (rtac refl_elem 3);
clasohm@0
   457
by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
clasohm@1294
   458
qed "mod_div_equality";
clasohm@0
   459
clasohm@0
   460
writeln"Reached end of file.";