src/HOL/Hoare/Examples.ML
author berghofe
Tue, 25 Jun 1996 13:11:29 +0200
changeset 1824 44254696843a
parent 1798 c055505f36d1
child 1875 54c0462f8fb2
permissions -rw-r--r--
Changed argument order of nat_rec.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     1
(*  Title:      HOL/Hoare/Examples.thy
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     3
    Author:     Norbert Galm
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
Various arithmetic examples.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
open Examples;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
(*** multiplication by successive addition ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    12
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    13
goal thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    14
 "{m=0 & s=0} \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    15
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    16
\ {s = a*b}";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
by(hoare_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
qed "multiply_by_add";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    21
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    22
(*** Euclid's algorithm for GCD ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    23
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
goal thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    25
" {0<A & 0<B & a=A & b=B}   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
\ WHILE a ~= b  \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
\ DO  {0<a & 0<b & gcd A B = gcd a b} \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    28
\      IF a<b   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
\      THEN   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    30
\           b:=b-a   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    31
\      ELSE   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    32
\           a:=a-b   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    33
\      END   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    34
\ END   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    35
\ {a = gcd A B}";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    36
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    37
by (hoare_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    38
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    39
by (safe_tac HOL_cs);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    40
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    41
by (etac less_imp_diff_positive 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    42
by (etac gcd_diff_r 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    43
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    44
by (cut_facts_tac [less_linear] 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    45
by (cut_facts_tac [less_linear] 2);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    46
by (rtac less_imp_diff_positive 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    47
by (rtac gcd_diff_l 2);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    48
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    49
by (dtac gcd_nnn 3);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    50
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    51
by (ALLGOALS (fast_tac HOL_cs));
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    52
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    53
qed "Euclid_GCD";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    54
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    55
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    56
(*** Power by interated squaring and multiplication ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    57
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    58
goal thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    59
" {a=A & b=B}   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    60
\ c:=1;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    61
\ WHILE b~=0   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    62
\ DO {A pow B = c * a pow b}   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    63
\      WHILE b mod 2=0   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    64
\      DO  {A pow B = c * a pow b}  \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    65
\           a:=a*a;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    66
\           b:=b div 2   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    67
\      END;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    68
\      c:=c*a;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    69
\      b:=b-1   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    70
\ END   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    71
\ {c = A pow B}";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    72
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    73
by (hoare_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    74
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    75
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    76
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    77
by (safe_tac HOL_cs);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    78
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    79
by (subgoal_tac "a*a=a pow 2" 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    80
by (Asm_simp_tac 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    81
by (rtac (pow_pow_reduce RS ssubst) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    82
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    83
by (subgoal_tac "(b div 2)*2=b" 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    84
by (subgoal_tac "0<2" 2);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    85
by (dres_inst_tac [("m","b")] mod_div_equality 2);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    86
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    87
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    88
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    89
by (subgoal_tac "b~=0" 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    90
by (res_inst_tac [("n","b")] natE 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    91
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    92
by (assume_tac 4);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    93
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    94
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    95
by (rtac mod_less 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    96
by (Simp_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    97
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    98
qed "power_by_mult";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    99
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   100
(*** factorial ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   101
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   102
goal thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   103
" {a=A}   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   104
\ b:=1;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   105
\ WHILE a~=0    \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   106
\ DO  {fac A = b*fac a} \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   107
\      b:=b*a;   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   108
\      a:=a-1   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   109
\ END   \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   110
\ {b = fac A}";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   111
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   112
by (hoare_tac 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   113
by (safe_tac HOL_cs);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   114
by (res_inst_tac [("n","a")] natE 1);
1798
c055505f36d1 Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1465
diff changeset
   115
by (ALLGOALS
c055505f36d1 Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1465
diff changeset
   116
    (asm_simp_tac
c055505f36d1 Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1465
diff changeset
   117
     (!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   118
by (fast_tac HOL_cs 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   119
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   120
qed"factorial";