2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb, TUM |
3 Author: David von Oheimb, TUM |
4 Copyright 1999 TUM |
4 Copyright 1999 TUM |
5 *) |
5 *) |
6 |
6 |
7 open Natural; |
7 AddIs evalc.intros; |
8 |
8 AddIs evaln.intros; |
9 AddIs evalc.intrs; |
|
10 AddIs evaln.intrs; |
|
11 |
|
12 val evalc_elim_cases = map evalc.mk_cases |
|
13 ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t", |
|
14 "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t", |
|
15 "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"]; |
|
16 val evaln_elim_cases = map evaln.mk_cases |
|
17 ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t", |
|
18 "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t", |
|
19 "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"]; |
|
20 val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t"; |
|
21 val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t"; |
|
22 |
9 |
23 AddSEs evalc_elim_cases; |
10 AddSEs evalc_elim_cases; |
24 AddSEs evaln_elim_cases; |
11 AddSEs evaln_elim_cases; |
25 |
12 |
26 (* evaluation of com is deterministic *) |
13 (* evaluation of com is deterministic *) |
31 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
18 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
32 qed_spec_mp "com_det"; |
19 qed_spec_mp "com_det"; |
33 |
20 |
34 Goal "<c,s> -n-> t ==> <c,s> -c-> t"; |
21 Goal "<c,s> -n-> t ==> <c,s> -c-> t"; |
35 by (etac evaln.induct 1); |
22 by (etac evaln.induct 1); |
36 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); |
23 by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac)); |
37 qed "evaln_evalc"; |
24 qed "evaln_evalc"; |
38 |
25 |
39 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
26 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
40 by (cut_facts_tac (premises()) 1); |
27 by (cut_facts_tac (premises()) 1); |
41 by (ftac Suc_le_D 1); |
28 by (ftac Suc_le_D 1); |
44 qed "Suc_le_D_lemma"; |
31 qed "Suc_le_D_lemma"; |
45 |
32 |
46 Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"; |
33 Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"; |
47 by (etac evaln.induct 1); |
34 by (etac evaln.induct 1); |
48 by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1])); |
35 by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1])); |
49 by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac)); |
36 by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac)); |
50 qed_spec_mp "evaln_nonstrict"; |
37 qed_spec_mp "evaln_nonstrict"; |
51 |
38 |
52 Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"; |
39 Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"; |
53 by (etac evaln_nonstrict 1); |
40 by (etac evaln_nonstrict 1); |
54 by Auto_tac; |
41 by Auto_tac; |
62 |
49 |
63 Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t"; |
50 Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t"; |
64 by (etac evalc.induct 1); |
51 by (etac evalc.induct 1); |
65 by (ALLGOALS (REPEAT o etac exE)); |
52 by (ALLGOALS (REPEAT o etac exE)); |
66 by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]])); |
53 by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]])); |
67 by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac)); |
54 by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac)); |
68 qed "evalc_evaln"; |
55 qed "evalc_evaln"; |
69 |
56 |
70 Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)"; |
57 Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)"; |
71 by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1); |
58 by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1); |
72 qed "eval_eq"; |
59 qed "eval_eq"; |