|
8177
|
1 |
(* Title: HOL/IMPP/Natural.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb, TUM
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
open Natural;
|
|
|
8 |
|
|
|
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 |
|
|
|
23 |
AddSEs evalc_elim_cases;
|
|
|
24 |
AddSEs evaln_elim_cases;
|
|
|
25 |
|
|
|
26 |
(* evaluation of com is deterministic *)
|
|
|
27 |
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
|
|
|
28 |
be evalc.induct 1;
|
|
|
29 |
by (thin_tac "<?c,s1> -c-> s2" 8);
|
|
|
30 |
(*blast_tac needs Unify.search_bound := 40*)
|
|
|
31 |
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
|
|
|
32 |
qed_spec_mp "com_det";
|
|
|
33 |
|
|
|
34 |
Goal "<c,s> -n-> t ==> <c,s> -c-> t";
|
|
|
35 |
be evaln.induct 1;
|
|
|
36 |
by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
|
|
|
37 |
qed "evaln_evalc";
|
|
|
38 |
|
|
|
39 |
goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)";
|
|
|
40 |
by (induct_tac "m'" 1);
|
|
9442
|
41 |
by (CLASIMPSET auto_tac);
|
|
8177
|
42 |
qed_spec_mp "Suc_le_D";
|
|
|
43 |
|
|
|
44 |
Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
|
|
|
45 |
by (cut_facts_tac (premises()) 1);
|
|
|
46 |
by (ftac Suc_le_D 1);
|
|
|
47 |
by (Clarify_tac 1);
|
|
|
48 |
by (eresolve_tac (premises()) 1);
|
|
|
49 |
qed "Suc_le_D_lemma";
|
|
|
50 |
|
|
|
51 |
Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
|
|
|
52 |
be evaln.induct 1;
|
|
|
53 |
by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
|
|
|
54 |
by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
|
|
|
55 |
qed_spec_mp "evaln_nonstrict";
|
|
|
56 |
|
|
|
57 |
Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
|
|
|
58 |
be evaln_nonstrict 1;
|
|
|
59 |
by Auto_tac;
|
|
|
60 |
qed "evaln_Suc";
|
|
|
61 |
|
|
|
62 |
Goal "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==> \
|
|
|
63 |
\ ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2";
|
|
|
64 |
by (cut_facts_tac [read_instantiate [("m","n1"),("n","n2")] nat_le_linear] 1);
|
|
|
65 |
by (blast_tac (claset() addDs [evaln_nonstrict]) 1);
|
|
|
66 |
qed "evaln_max2";
|
|
|
67 |
|
|
|
68 |
Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t";
|
|
|
69 |
be evalc.induct 1;
|
|
|
70 |
by (ALLGOALS (REPEAT o etac exE));
|
|
|
71 |
by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
|
|
|
72 |
by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
|
|
|
73 |
qed "evalc_evaln";
|
|
|
74 |
|
|
|
75 |
Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
|
|
|
76 |
by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1);
|
|
|
77 |
qed "eval_eq";
|