1 (* Title: HOL/IMPP/Natural.thy
3 Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
7 header {* Natural semantics of commands *}
13 (** Execution of commands **)
17 setlocs :: "state => locals => state"
18 getlocs :: "state => locals"
19 update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)
22 loc :: "state => locals" ("_<_>" [75,0] 75) where
26 evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51)
28 Skip: "<SKIP,s> -c-> s"
30 | Assign: "<X :== a,s> -c-> s[X::=a s]"
32 | Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
33 <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
35 | Semi: "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
36 <c0;; c1, s0> -c-> s2"
38 | IfTrue: "[| b s; <c0,s> -c-> s1 |] ==>
39 <IF b THEN c0 ELSE c1, s> -c-> s1"
41 | IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
42 <IF b THEN c0 ELSE c1, s> -c-> s1"
44 | WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
46 | WhileTrue: "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==>
47 <WHILE b DO c, s0> -c-> s2"
49 | Body: "<the (body pn), s0> -c-> s1 ==>
50 <BODY pn, s0> -c-> s1"
52 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
53 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
57 evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51)
59 Skip: "<SKIP,s> -n-> s"
61 | Assign: "<X :== a,s> -n-> s[X::=a s]"
63 | Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
64 <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
66 | Semi: "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
67 <c0;; c1, s0> -n-> s2"
69 | IfTrue: "[| b s; <c0,s> -n-> s1 |] ==>
70 <IF b THEN c0 ELSE c1, s> -n-> s1"
72 | IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
73 <IF b THEN c0 ELSE c1, s> -n-> s1"
75 | WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
77 | WhileTrue: "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==>
78 <WHILE b DO c, s0> -n-> s2"
80 | Body: "<the (body pn), s0> - n-> s1 ==>
81 <BODY pn, s0> -Suc n-> s1"
83 | Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
84 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
88 inductive_cases evalc_elim_cases:
89 "<SKIP,s> -c-> t" "<X:==a,s> -c-> t" "<LOCAL Y:=a IN c,s> -c-> t"
90 "<c1;;c2,s> -c-> t" "<IF b THEN c1 ELSE c2,s> -c-> t"
91 "<BODY P,s> -c-> s1" "<X:=CALL P(a),s> -c-> s1"
93 inductive_cases evaln_elim_cases:
94 "<SKIP,s> -n-> t" "<X:==a,s> -n-> t" "<LOCAL Y:=a IN c,s> -n-> t"
95 "<c1;;c2,s> -n-> t" "<IF b THEN c1 ELSE c2,s> -n-> t"
96 "<BODY P,s> -n-> s1" "<X:=CALL P(a),s> -n-> s1"
98 inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
99 inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
101 declare evalc.intros [intro]
102 declare evaln.intros [intro]
104 declare evalc_elim_cases [elim!]
105 declare evaln_elim_cases [elim!]
107 (* evaluation of com is deterministic *)
108 lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
109 apply (erule evalc.induct)
110 apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
111 (*blast needs unify_search_bound = 40*)
112 apply (best elim: evalc_WHILE_case)+
115 lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
116 apply (erule evaln.induct)
117 apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
120 lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
121 apply (frule Suc_le_D)
125 lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
126 apply (erule evaln.induct)
127 apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
128 apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
131 lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
132 apply (erule evaln_nonstrict)
136 lemma evaln_max2: "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==>
137 ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"
138 apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
139 apply (blast dest: evaln_nonstrict)
142 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
143 apply (erule evalc.induct)
144 apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
145 apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
146 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
149 lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
150 apply (fast elim: evalc_evaln evaln_evalc)