1 (* Title: HOL/IMP/Examples.ML
3 Author: David von Oheimb, TUM
9 section "An example due to Tony Hoare";
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);
15 val lemma1 = result() RS spec RS mp RS mp;
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);
22 by (case_tac "P s" 1);
24 val lemma2 = result() RS spec RS mp;
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);
34 val step = resolve_tac evalc.intrs 1;
35 val simp = Asm_simp_tac 1;
36 Goalw [factorial_def] "a~=b ==> \
37 \ <factorial a b, Mem(a:=3)> -c-> Mem(b:=6,a:=Numeral0)";