src/HOL/Hoare/Examples.ML
author nipkow
Fri, 17 Nov 1995 09:04:10 +0100
changeset 1335 5e1c0540f285
child 1465 5d7a7e439cec
permissions -rw-r--r--
New directory. Hoare logic according to Mike Gordon.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/Hoare/Examples.thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     3
    Author: 	Norbert Galm
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
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    41
be less_imp_diff_positive 1;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    42
be gcd_diff_r 1;
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);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    46
br less_imp_diff_positive 1;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    47
br gcd_diff_l 2;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    48
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    49
bd gcd_nnn 3;
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);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    81
br (pow_pow_reduce RS ssubst) 1;
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);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    92
ba 4;
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])));
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    95
br mod_less 1;
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
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   114
by (safe_tac HOL_cs);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   115
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   116
by (res_inst_tac [("n","a")] natE 1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   117
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc])));
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";