| author | huffman |
| Tue, 15 Nov 2011 12:49:05 +0100 | |
| changeset 45504 | cad35ed6effa |
| parent 41589 | bbd861837ebc |
| child 46459 | 73823dbbecc4 |
| permissions | -rw-r--r-- |
| 8177 | 1 |
(* Title: HOL/IMPP/Natural.thy |
2 |
Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM |
|
3 |
*) |
|
4 |
||
| 17477 | 5 |
header {* Natural semantics of commands *}
|
6 |
||
7 |
theory Natural |
|
8 |
imports Com |
|
9 |
begin |
|
| 8177 | 10 |
|
11 |
(** Execution of commands **) |
|
12 |
||
13 |
consts |
|
14 |
newlocs :: locals |
|
| 17477 | 15 |
setlocs :: "state => locals => state" |
16 |
getlocs :: "state => locals" |
|
17 |
update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)
|
|
| 27362 | 18 |
|
19 |
abbreviation |
|
20 |
loc :: "state => locals" ("_<_>" [75,0] 75) where
|
|
21 |
"s<X> == getlocs s X" |
|
| 8177 | 22 |
|
| 23746 | 23 |
inductive |
24 |
evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51)
|
|
25 |
where |
|
| 17477 | 26 |
Skip: "<SKIP,s> -c-> s" |
| 8177 | 27 |
|
| 23746 | 28 |
| Assign: "<X :== a,s> -c-> s[X::=a s]" |
| 8177 | 29 |
|
| 23746 | 30 |
| Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==> |
| 17477 | 31 |
<LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]" |
| 8177 | 32 |
|
| 23746 | 33 |
| Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==> |
| 17477 | 34 |
<c0;; c1, s0> -c-> s2" |
| 8177 | 35 |
|
| 23746 | 36 |
| IfTrue: "[| b s; <c0,s> -c-> s1 |] ==> |
| 17477 | 37 |
<IF b THEN c0 ELSE c1, s> -c-> s1" |
| 8177 | 38 |
|
| 23746 | 39 |
| IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==> |
| 17477 | 40 |
<IF b THEN c0 ELSE c1, s> -c-> s1" |
| 8177 | 41 |
|
| 23746 | 42 |
| WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s" |
| 8177 | 43 |
|
| 23746 | 44 |
| WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==> |
| 17477 | 45 |
<WHILE b DO c, s0> -c-> s2" |
| 8177 | 46 |
|
| 23746 | 47 |
| Body: "<the (body pn), s0> -c-> s1 ==> |
| 17477 | 48 |
<BODY pn, s0> -c-> s1" |
| 8177 | 49 |
|
| 23746 | 50 |
| Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==> |
| 17477 | 51 |
<X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0)) |
52 |
[X::=s1<Res>]" |
|
| 8177 | 53 |
|
| 23746 | 54 |
inductive |
55 |
evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51)
|
|
56 |
where |
|
| 17477 | 57 |
Skip: "<SKIP,s> -n-> s" |
58 |
||
| 23746 | 59 |
| Assign: "<X :== a,s> -n-> s[X::=a s]" |
| 8177 | 60 |
|
| 23746 | 61 |
| Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==> |
| 17477 | 62 |
<LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]" |
63 |
||
| 23746 | 64 |
| Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==> |
| 17477 | 65 |
<c0;; c1, s0> -n-> s2" |
| 8177 | 66 |
|
| 23746 | 67 |
| IfTrue: "[| b s; <c0,s> -n-> s1 |] ==> |
| 17477 | 68 |
<IF b THEN c0 ELSE c1, s> -n-> s1" |
| 8177 | 69 |
|
| 23746 | 70 |
| IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==> |
| 17477 | 71 |
<IF b THEN c0 ELSE c1, s> -n-> s1" |
| 8177 | 72 |
|
| 23746 | 73 |
| WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s" |
| 17477 | 74 |
|
| 23746 | 75 |
| WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==> |
| 17477 | 76 |
<WHILE b DO c, s0> -n-> s2" |
| 8177 | 77 |
|
| 23746 | 78 |
| Body: "<the (body pn), s0> - n-> s1 ==> |
| 17477 | 79 |
<BODY pn, s0> -Suc n-> s1" |
| 8177 | 80 |
|
| 23746 | 81 |
| Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==> |
| 17477 | 82 |
<X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0)) |
83 |
[X::=s1<Res>]" |
|
| 8177 | 84 |
|
85 |
||
| 17477 | 86 |
inductive_cases evalc_elim_cases: |
87 |
"<SKIP,s> -c-> t" "<X:==a,s> -c-> t" "<LOCAL Y:=a IN c,s> -c-> t" |
|
88 |
"<c1;;c2,s> -c-> t" "<IF b THEN c1 ELSE c2,s> -c-> t" |
|
89 |
"<BODY P,s> -c-> s1" "<X:=CALL P(a),s> -c-> s1" |
|
| 8177 | 90 |
|
| 17477 | 91 |
inductive_cases evaln_elim_cases: |
92 |
"<SKIP,s> -n-> t" "<X:==a,s> -n-> t" "<LOCAL Y:=a IN c,s> -n-> t" |
|
93 |
"<c1;;c2,s> -n-> t" "<IF b THEN c1 ELSE c2,s> -n-> t" |
|
94 |
"<BODY P,s> -n-> s1" "<X:=CALL P(a),s> -n-> s1" |
|
95 |
||
96 |
inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t" |
|
97 |
inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t" |
|
98 |
||
| 19803 | 99 |
declare evalc.intros [intro] |
100 |
declare evaln.intros [intro] |
|
101 |
||
102 |
declare evalc_elim_cases [elim!] |
|
103 |
declare evaln_elim_cases [elim!] |
|
104 |
||
105 |
(* evaluation of com is deterministic *) |
|
106 |
lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)" |
|
107 |
apply (erule evalc.induct) |
|
108 |
apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl) |
|
|
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23746
diff
changeset
|
109 |
(*blast needs unify_search_bound = 40*) |
| 19803 | 110 |
apply (best elim: evalc_WHILE_case)+ |
111 |
done |
|
112 |
||
113 |
lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t" |
|
114 |
apply (erule evaln.induct) |
|
| 39159 | 115 |
apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *})
|
| 19803 | 116 |
done |
117 |
||
118 |
lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'" |
|
119 |
apply (frule Suc_le_D) |
|
120 |
apply blast |
|
121 |
done |
|
122 |
||
123 |
lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t" |
|
124 |
apply (erule evaln.induct) |
|
| 39159 | 125 |
apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *})
|
126 |
apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
|
|
| 19803 | 127 |
done |
128 |
||
129 |
lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'" |
|
130 |
apply (erule evaln_nonstrict) |
|
131 |
apply auto |
|
132 |
done |
|
133 |
||
134 |
lemma evaln_max2: "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==> |
|
135 |
? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2" |
|
136 |
apply (cut_tac m = "n1" and n = "n2" in nat_le_linear) |
|
137 |
apply (blast dest: evaln_nonstrict) |
|
138 |
done |
|
139 |
||
140 |
lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t" |
|
141 |
apply (erule evalc.induct) |
|
142 |
apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
|
|
| 39159 | 143 |
apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
|
144 |
apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
|
|
| 19803 | 145 |
done |
146 |
||
147 |
lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)" |
|
148 |
apply (fast elim: evalc_evaln evaln_evalc) |
|
149 |
done |
|
| 17477 | 150 |
|
| 8177 | 151 |
end |