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