24 by (etac evalc.induct 1); |
24 by (etac evalc.induct 1); |
25 by (thin_tac "<?c,s2> -c-> s1" 7); |
25 by (thin_tac "<?c,s2> -c-> s1" 7); |
26 (*blast_tac needs Unify.search_bound, trace_bound ::= 40*) |
26 (*blast_tac needs Unify.search_bound, trace_bound ::= 40*) |
27 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
27 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
28 qed_spec_mp "com_det"; |
28 qed_spec_mp "com_det"; |
29 |
|
30 (** An example due to Tony Hoare **) |
|
31 |
|
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"; |
|
34 by (etac evalc.induct 1); |
|
35 by (Auto_tac); |
|
36 val lemma1 = result() RS spec RS mp RS mp; |
|
37 |
|
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"; |
|
40 by (etac evalc.induct 1); |
|
41 by (ALLGOALS Asm_simp_tac); |
|
42 by (Blast_tac 1); |
|
43 by (case_tac "P s" 1); |
|
44 by (Auto_tac); |
|
45 val lemma2 = result() RS spec RS mp; |
|
46 |
|
47 Goal "!x. P x --> Q x ==> \ |
|
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); |
|
50 qed "Hoare_example"; |
|