src/HOL/Hoare/Examples.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4356 0dfd34f0d33d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
clasohm@1465
     1
(*  Title:      HOL/Hoare/Examples.thy
nipkow@1335
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Norbert Galm
nipkow@1335
     4
    Copyright   1995 TUM
nipkow@1335
     5
nipkow@1335
     6
Various arithmetic examples.
nipkow@1335
     7
*)
nipkow@1335
     8
nipkow@1335
     9
open Examples;
nipkow@1335
    10
nipkow@1335
    11
(*** multiplication by successive addition ***)
nipkow@1335
    12
nipkow@1335
    13
goal thy
nipkow@1335
    14
 "{m=0 & s=0} \
nipkow@1335
    15
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
nipkow@1335
    16
\ {s = a*b}";
paulson@2031
    17
by (hoare_tac 1);
wenzelm@4089
    18
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
nipkow@1335
    19
qed "multiply_by_add";
nipkow@1335
    20
nipkow@1335
    21
nipkow@1335
    22
(*** Euclid's algorithm for GCD ***)
nipkow@1335
    23
nipkow@1335
    24
goal thy
nipkow@1335
    25
" {0<A & 0<B & a=A & b=B}   \
nipkow@1335
    26
\ WHILE a ~= b  \
nipkow@1335
    27
\ DO  {0<a & 0<b & gcd A B = gcd a b} \
nipkow@1335
    28
\      IF a<b   \
nipkow@1335
    29
\      THEN   \
nipkow@1335
    30
\           b:=b-a   \
nipkow@1335
    31
\      ELSE   \
nipkow@1335
    32
\           a:=a-b   \
nipkow@1335
    33
\      END   \
nipkow@1335
    34
\ END   \
nipkow@1335
    35
\ {a = gcd A B}";
nipkow@1335
    36
nipkow@1335
    37
by (hoare_tac 1);
paulson@3372
    38
(*Now prove the verification conditions*)
paulson@4153
    39
by Safe_tac;
clasohm@1465
    40
by (etac less_imp_diff_positive 1);
wenzelm@4089
    41
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
wenzelm@4089
    42
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
paulson@3372
    43
by (etac gcd_nnn 2);
wenzelm@4089
    44
by (full_simp_tac (simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 1);
wenzelm@4089
    45
by (blast_tac (claset() addIs [less_imp_diff_positive]) 1);
nipkow@1335
    46
qed "Euclid_GCD";
nipkow@1335
    47
nipkow@1335
    48
nipkow@1335
    49
(*** Power by interated squaring and multiplication ***)
nipkow@1335
    50
nipkow@1335
    51
goal thy
nipkow@1335
    52
" {a=A & b=B}   \
nipkow@1335
    53
\ c:=1;   \
nipkow@1335
    54
\ WHILE b~=0   \
nipkow@1335
    55
\ DO {A pow B = c * a pow b}   \
nipkow@1335
    56
\      WHILE b mod 2=0   \
nipkow@1335
    57
\      DO  {A pow B = c * a pow b}  \
nipkow@1335
    58
\           a:=a*a;   \
nipkow@1335
    59
\           b:=b div 2   \
nipkow@1335
    60
\      END;   \
nipkow@1335
    61
\      c:=c*a;   \
nipkow@1335
    62
\      b:=b-1   \
nipkow@1335
    63
\ END   \
nipkow@1335
    64
\ {c = A pow B}";
nipkow@1335
    65
nipkow@1335
    66
by (hoare_tac 1);
nipkow@1335
    67
wenzelm@4089
    68
by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
nipkow@1335
    69
paulson@4153
    70
by Safe_tac;
nipkow@1335
    71
nipkow@1335
    72
by (subgoal_tac "a*a=a pow 2" 1);
nipkow@1335
    73
by (Asm_simp_tac 1);
paulson@2031
    74
by (stac pow_pow_reduce 1);
nipkow@1335
    75
nipkow@1335
    76
by (subgoal_tac "(b div 2)*2=b" 1);
nipkow@1335
    77
by (subgoal_tac "0<2" 2);
nipkow@1335
    78
by (dres_inst_tac [("m","b")] mod_div_equality 2);
nipkow@1335
    79
wenzelm@4089
    80
by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
nipkow@1335
    81
nipkow@1335
    82
by (subgoal_tac "b~=0" 1);
nipkow@1335
    83
by (res_inst_tac [("n","b")] natE 1);
nipkow@1335
    84
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
clasohm@1465
    85
by (assume_tac 4);
nipkow@1335
    86
wenzelm@4089
    87
by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
clasohm@1465
    88
by (rtac mod_less 1);
nipkow@1335
    89
by (Simp_tac 1);
nipkow@1335
    90
nipkow@1335
    91
qed "power_by_mult";
nipkow@1335
    92
nipkow@1335
    93
(*** factorial ***)
nipkow@1335
    94
nipkow@1335
    95
goal thy
nipkow@1335
    96
" {a=A}   \
nipkow@1335
    97
\ b:=1;   \
nipkow@1335
    98
\ WHILE a~=0    \
nipkow@1335
    99
\ DO  {fac A = b*fac a} \
nipkow@1335
   100
\      b:=b*a;   \
nipkow@1335
   101
\      a:=a-1   \
nipkow@1335
   102
\ END   \
nipkow@1335
   103
\ {b = fac A}";
nipkow@1335
   104
nipkow@1335
   105
by (hoare_tac 1);
paulson@4153
   106
by Safe_tac;
nipkow@1335
   107
by (res_inst_tac [("n","a")] natE 1);
paulson@1798
   108
by (ALLGOALS
paulson@1798
   109
    (asm_simp_tac
wenzelm@4089
   110
     (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
berghofe@1875
   111
by (Fast_tac 1);
nipkow@1335
   112
nipkow@1335
   113
qed"factorial";