29 |
29 |
30 (** An example due to Tony Hoare **) |
30 (** An example due to Tony Hoare **) |
31 |
31 |
32 Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \ |
32 Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \ |
33 \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u"; |
33 \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u"; |
34 be evalc.induct 1; |
34 by (etac evalc.induct 1); |
35 by(Auto_tac); |
35 by (Auto_tac); |
36 val lemma1 = result() RS spec RS mp RS mp; |
36 val lemma1 = result() RS spec RS mp RS mp; |
37 |
37 |
38 Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \ |
38 Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \ |
39 \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u"; |
39 \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u"; |
40 be evalc.induct 1; |
40 by (etac evalc.induct 1); |
41 by(ALLGOALS Asm_simp_tac); |
41 by (ALLGOALS Asm_simp_tac); |
42 by(Blast_tac 1); |
42 by (Blast_tac 1); |
43 by(case_tac "P s" 1); |
43 by (case_tac "P s" 1); |
44 by(Auto_tac); |
44 by (Auto_tac); |
45 val lemma2 = result() RS spec RS mp; |
45 val lemma2 = result() RS spec RS mp; |
46 |
46 |
47 Goal "!x. P x --> Q x ==> \ |
47 Goal "!x. P x --> Q x ==> \ |
48 \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)"; |
48 \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)"; |
49 by(blast_tac (claset() addIs [lemma1,lemma2]) 1); |
49 by (blast_tac (claset() addIs [lemma1,lemma2]) 1); |
50 qed "Hoare_example"; |
50 qed "Hoare_example"; |