author  paulson 
Fri, 14 Jun 1996 12:25:02 +0200  
changeset 1798  c055505f36d1 
parent 1465  5d7a7e439cec 
child 1875  54c0462f8fb2 
permissions  rwrr 
1465  1 
(* Title: HOL/Hoare/Examples.thy 
1335  2 
ID: $Id$ 
1465  3 
Author: Norbert Galm 
1335  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:=ba \ 

31 
\ ELSE \ 

32 
\ a:=ab \ 

33 
\ END \ 

34 
\ END \ 

35 
\ {a = gcd A B}"; 

36 

37 
by (hoare_tac 1); 

38 

39 
by (safe_tac HOL_cs); 

40 

1465  41 
by (etac less_imp_diff_positive 1); 
42 
by (etac gcd_diff_r 1); 

1335  43 

44 
by (cut_facts_tac [less_linear] 1); 

45 
by (cut_facts_tac [less_linear] 2); 

1465  46 
by (rtac less_imp_diff_positive 1); 
47 
by (rtac gcd_diff_l 2); 

1335  48 

1465  49 
by (dtac gcd_nnn 3); 
1335  50 

51 
by (ALLGOALS (fast_tac HOL_cs)); 

52 

53 
qed "Euclid_GCD"; 

54 

55 

56 
(*** Power by interated squaring and multiplication ***) 

57 

58 
goal thy 

59 
" {a=A & b=B} \ 

60 
\ c:=1; \ 

61 
\ WHILE b~=0 \ 

62 
\ DO {A pow B = c * a pow b} \ 

63 
\ WHILE b mod 2=0 \ 

64 
\ DO {A pow B = c * a pow b} \ 

65 
\ a:=a*a; \ 

66 
\ b:=b div 2 \ 

67 
\ END; \ 

68 
\ c:=c*a; \ 

69 
\ b:=b1 \ 

70 
\ END \ 

71 
\ {c = A pow B}"; 

72 

73 
by (hoare_tac 1); 

74 

75 
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3); 

76 

77 
by (safe_tac HOL_cs); 

78 

79 
by (subgoal_tac "a*a=a pow 2" 1); 

80 
by (Asm_simp_tac 1); 

1465  81 
by (rtac (pow_pow_reduce RS ssubst) 1); 
1335  82 

83 
by (subgoal_tac "(b div 2)*2=b" 1); 

84 
by (subgoal_tac "0<2" 2); 

85 
by (dres_inst_tac [("m","b")] mod_div_equality 2); 

86 

87 
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); 

88 

89 
by (subgoal_tac "b~=0" 1); 

90 
by (res_inst_tac [("n","b")] natE 1); 

91 
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3); 

1465  92 
by (assume_tac 4); 
1335  93 

94 
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); 

1465  95 
by (rtac mod_less 1); 
1335  96 
by (Simp_tac 1); 
97 

98 
qed "power_by_mult"; 

99 

100 
(*** factorial ***) 

101 

102 
goal thy 

103 
" {a=A} \ 

104 
\ b:=1; \ 

105 
\ WHILE a~=0 \ 

106 
\ DO {fac A = b*fac a} \ 

107 
\ b:=b*a; \ 

108 
\ a:=a1 \ 

109 
\ END \ 

110 
\ {b = fac A}"; 

111 

112 
by (hoare_tac 1); 

113 
by (safe_tac HOL_cs); 

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  118 
by (fast_tac HOL_cs 1); 
119 

120 
qed"factorial"; 