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