4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 Addsimps[update_def]; |
7 Addsimps[update_def]; |
8 |
8 |
9 section "Examples"; |
9 section "An example due to Tony Hoare"; |
|
10 |
|
11 Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \ |
|
12 \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u"; |
|
13 by (etac evalc.induct 1); |
|
14 by (Auto_tac); |
|
15 val lemma1 = result() RS spec RS mp RS mp; |
|
16 |
|
17 Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \ |
|
18 \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u"; |
|
19 by (etac evalc.induct 1); |
|
20 by (ALLGOALS Asm_simp_tac); |
|
21 by (Blast_tac 1); |
|
22 by (case_tac "P s" 1); |
|
23 by (Auto_tac); |
|
24 val lemma2 = result() RS spec RS mp; |
|
25 |
|
26 Goal "!x. P x --> Q x ==> \ |
|
27 \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)"; |
|
28 by (blast_tac (claset() addIs [lemma1,lemma2]) 1); |
|
29 qed "Hoare_example"; |
|
30 |
|
31 |
|
32 section "Factorial"; |
10 |
33 |
11 val step = resolve_tac evalc.intrs 1; |
34 val step = resolve_tac evalc.intrs 1; |
12 val simp = Asm_simp_tac 1; |
35 val simp = Asm_simp_tac 1; |
13 Goalw [factorial_def] "a~=b ==> \ |
36 Goalw [factorial_def] "a~=b ==> \ |
14 \ <factorial a b, Mem(a:=#3)> -c-> Mem(b:=#6,a:=#0)"; |
37 \ <factorial a b, Mem(a:=#3)> -c-> Mem(b:=#6,a:=#0)"; |
15 by (ftac not_sym 1); |
38 by (ftac not_sym 1); |
16 by step; |
39 by step; |
17 by step; |
40 by step; |
|
41 by simp; |
18 by step; |
42 by step; |
19 by simp; |
43 by simp; |
20 by step; |
44 by step; |
21 by step; |
45 by step; |
|
46 by simp; |
22 by step; |
47 by step; |
23 by simp; |
48 by simp; |
24 by step; |
49 by step; |
25 by simp; |
50 by simp; |
26 by step; |
51 by step; |
27 by step; |
52 by step; |
|
53 by simp; |
28 by step; |
54 by step; |
29 by simp; |
55 by simp; |
30 by step; |
56 by step; |
31 by simp; |
57 by simp; |
32 by step; |
58 by step; |
33 by step; |
59 by step; |
|
60 by simp; |
34 by step; |
61 by step; |
35 by simp; |
62 by simp; |
36 by step; |
63 by step; |
37 by simp; |
64 by simp; |
38 qed "factorial_3"; |
65 qed "factorial_3"; |