1700
|
1 |
(* Title: HOL/IMP/Natural.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Larry Paulson, TUM
|
|
4 |
Copyright 1996 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
open Natural;
|
|
8 |
|
1973
|
9 |
AddIs evalc.intrs;
|
|
10 |
|
1700
|
11 |
val evalc_elim_cases = map (evalc.mk_cases com.simps)
|
|
12 |
["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
|
|
13 |
"<IF b THEN c1 ELSE c2, s> -c-> t"];
|
|
14 |
|
|
15 |
val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
|
|
16 |
|
1973
|
17 |
AddSEs evalc_elim_cases;
|
1700
|
18 |
|
|
19 |
(* evaluation of com is deterministic *)
|
5117
|
20 |
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
|
1730
|
21 |
by (etac evalc.induct 1);
|
1958
|
22 |
by (thin_tac "<?c,s2> -c-> s1" 7);
|
4241
|
23 |
(*blast_tac needs Unify.search_bound, trace_bound := 40*)
|
|
24 |
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
|
1700
|
25 |
qed_spec_mp "com_det";
|
5789
|
26 |
|
|
27 |
(** An example due to Tony Hoare **)
|
|
28 |
|
|
29 |
Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
|
|
30 |
\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
|
|
31 |
be evalc.induct 1;
|
|
32 |
by(Auto_tac);
|
|
33 |
val lemma1 = result() RS spec RS mp RS mp;
|
|
34 |
|
|
35 |
Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
|
|
36 |
\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
|
|
37 |
be evalc.induct 1;
|
|
38 |
by(ALLGOALS Asm_simp_tac);
|
|
39 |
by(Blast_tac 1);
|
|
40 |
by(case_tac "P s" 1);
|
|
41 |
by(Auto_tac);
|
|
42 |
val lemma2 = result() RS spec RS mp;
|
|
43 |
|
|
44 |
Goal "!x. P x --> Q x ==> \
|
|
45 |
\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
|
|
46 |
by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
|
|
47 |
qed "Hoare_example";
|