1(*  Title:      HOL/IMPP/Natural.thy
2    Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
3*)
4
5section \<open>Natural semantics of commands\<close>
6
7theory Natural
8imports Com
9begin
10
11(** Execution of commands **)
12
13consts
14  newlocs :: locals
15  setlocs :: "state => locals => state"
16  getlocs :: "state => locals"
17  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
18
19abbreviation
20  loc :: "state => locals"  ("_<_>" [75,0] 75) where
21  "s<X> == getlocs s X"
22
23inductive
24  evalc :: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
25  where
26    Skip:    "<SKIP,s> -c-> s"
27
28  | Assign:  "<X :== a,s> -c-> s[X::=a s]"
29
30  | Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
31              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
32
33  | Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
34              <c0;; c1, s0> -c-> s2"
35
36  | IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
37              <IF b THEN c0 ELSE c1, s> -c-> s1"
38
39  | IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
40              <IF b THEN c0 ELSE c1, s> -c-> s1"
41
42  | WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
43
44  | WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
45                 <WHILE b DO c, s0> -c-> s2"
46
47  | Body:       "<the (body pn), s0> -c-> s1 ==>
48                 <BODY pn, s0> -c-> s1"
49
50  | Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
51                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
52                                          [X::=s1<Res>]"
53
54inductive
55  evaln :: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
56  where
57    Skip:    "<SKIP,s> -n-> s"
58
59  | Assign:  "<X :== a,s> -n-> s[X::=a s]"
60
61  | Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
62              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
63
64  | Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
65              <c0;; c1, s0> -n-> s2"
66
67  | IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
68              <IF b THEN c0 ELSE c1, s> -n-> s1"
69
70  | IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
71              <IF b THEN c0 ELSE c1, s> -n-> s1"
72
73  | WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
74
75  | WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
76                 <WHILE b DO c, s0> -n-> s2"
77
78  | Body:       "<the (body pn), s0> -    n-> s1 ==>
79                 <BODY pn, s0> -Suc n-> s1"
80
81  | Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
82                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
83                                          [X::=s1<Res>]"
84
85
86inductive_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"
90
91inductive_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
96inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
97inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
98
99declare evalc.intros [intro]
100declare evaln.intros [intro]
101
102declare evalc_elim_cases [elim!]
103declare evaln_elim_cases [elim!]
104
105(* evaluation of com is deterministic *)
106lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t \<Longrightarrow> (\<forall>u. <c,s> -c-> u \<longrightarrow> u=t)"
107apply (erule evalc.induct)
108apply (erule_tac [8] V = "<c,s1> -c-> s2" for c in thin_rl)
109apply (blast elim: evalc_WHILE_case)+
110done
111
112lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
113apply (erule evaln.induct)
114apply (tactic \<open>
115  ALLGOALS (resolve_tac \<^context> @{thms evalc.intros} THEN_ALL_NEW assume_tac \<^context>)
116\<close>)
117done
118
119lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
120apply (frule Suc_le_D)
121apply blast
122done
123
124lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t \<Longrightarrow> \<forall>m. n<=m \<longrightarrow> <c,s> -m-> t"
125apply (erule evaln.induct)
126apply (auto elim!: Suc_le_D_lemma)
127done
128
129lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
130apply (erule evaln_nonstrict)
131apply auto
132done
133
134lemma evaln_max2: "[| <c1,s1> -n1-> t1;  <c2,s2> -n2-> t2 |] ==>  
135    \<exists>n. <c1,s1> -n -> t1 \<and> <c2,s2> -n -> t2"
136apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
137apply (blast dest: evaln_nonstrict)
138done
139
140lemma evalc_evaln: "<c,s> -c-> t \<Longrightarrow> \<exists>n. <c,s> -n-> t"
141apply (erule evalc.induct)
142apply (tactic \<open>ALLGOALS (REPEAT o eresolve_tac \<^context> [exE])\<close>)
143apply (tactic \<open>TRYALL (EVERY' [dresolve_tac \<^context> @{thms evaln_max2}, assume_tac \<^context>,
144  REPEAT o eresolve_tac \<^context> [exE, conjE]])\<close>)
145apply (tactic
146  \<open>ALLGOALS (resolve_tac \<^context> [exI] THEN'
147    resolve_tac \<^context> @{thms evaln.intros} THEN_ALL_NEW assume_tac \<^context>)\<close>)
148done
149
150lemma eval_eq: "<c,s> -c-> t = (\<exists>n. <c,s> -n-> t)"
151apply (fast elim: evalc_evaln evaln_evalc)
152done
153
154end
155