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