1.1 --- a/src/HOL/Induct/Com.thy Tue Apr 02 13:47:01 2002 +0200
1.2 +++ b/src/HOL/Induct/Com.thy Tue Apr 02 14:28:28 2002 +0200
1.3 @@ -6,11 +6,12 @@
1.4 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
1.5 *)
1.6
1.7 -Com = Main +
1.8 +theory Com = Main:
1.9
1.10 -types loc
1.11 - state = "loc => nat"
1.12 - n2n2n = "nat => nat => nat"
1.13 +typedecl loc
1.14 +
1.15 +types state = "loc => nat"
1.16 + n2n2n = "nat => nat => nat"
1.17
1.18 arities loc :: type
1.19
1.20 @@ -26,38 +27,285 @@
1.21 | Cond exp com com ("IF _ THEN _ ELSE _" 60)
1.22 | While exp com ("WHILE _ DO _" 60)
1.23
1.24 -(** Execution of commands **)
1.25 +text{* Execution of commands *}
1.26 consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
1.27 "@exec" :: "((exp*state) * (nat*state)) set =>
1.28 [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
1.29
1.30 -translations "csig -[eval]-> s" == "(csig,s) : exec eval"
1.31 +translations "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
1.32
1.33 syntax eval' :: "[exp*state,nat*state] =>
1.34 ((exp*state) * (nat*state)) set => bool"
1.35 - ("_/ -|[_]-> _" [50,0,50] 50)
1.36 -translations
1.37 - "esig -|[eval]-> ns" => "(esig,ns) : eval"
1.38 + ("_/ -|[_]-> _" [50,0,50] 50)
1.39
1.40 -(*Command execution. Natural numbers represent Booleans: 0=True, 1=False*)
1.41 -inductive "exec eval"
1.42 - intrs
1.43 - Skip "(SKIP,s) -[eval]-> s"
1.44 +translations
1.45 + "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
1.46
1.47 - Assign "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
1.48 -
1.49 - Semi "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
1.50 - ==> (c0 ;; c1, s) -[eval]-> s1"
1.51 +text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
1.52 +inductive "exec eval"
1.53 + intros
1.54 + Skip: "(SKIP,s) -[eval]-> s"
1.55
1.56 - IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |]
1.57 - ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
1.58 + Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
1.59
1.60 - IfFalse "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |]
1.61 + Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
1.62 + ==> (c0 ;; c1, s) -[eval]-> s1"
1.63 +
1.64 + IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |]
1.65 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
1.66
1.67 - WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1"
1.68 + IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |]
1.69 + ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
1.70 +
1.71 + WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
1.72 + ==> (WHILE e DO c, s) -[eval]-> s1"
1.73 +
1.74 + WhileTrue: "[| (e,s) -|[eval]-> (0,s1);
1.75 + (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
1.76 + ==> (WHILE e DO c, s) -[eval]-> s3"
1.77 +
1.78 +declare exec.intros [intro]
1.79 +
1.80 +
1.81 +inductive_cases
1.82 + [elim!]: "(SKIP,s) -[eval]-> t"
1.83 + and [elim!]: "(x:=a,s) -[eval]-> t"
1.84 + and [elim!]: "(c1;;c2, s) -[eval]-> t"
1.85 + and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
1.86 + and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
1.87 +
1.88 +
1.89 +text{*Justifies using "exec" in the inductive definition of "eval"*}
1.90 +lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
1.91 +apply (unfold exec.defs )
1.92 +apply (rule lfp_mono)
1.93 +apply (assumption | rule basic_monos)+
1.94 +done
1.95 +
1.96 +ML {*
1.97 +Unify.trace_bound := 30;
1.98 +Unify.search_bound := 60;
1.99 +*}
1.100 +
1.101 +text{*Command execution is functional (deterministic) provided evaluation is*}
1.102 +theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
1.103 +apply (simp add: single_valued_def)
1.104 +apply (intro allI)
1.105 +apply (rule impI)
1.106 +apply (erule exec.induct)
1.107 +apply (blast elim: exec_WHILE_case)+
1.108 +done
1.109 +
1.110 +
1.111 +section {* Expressions *}
1.112 +
1.113 +text{* Evaluation of arithmetic expressions *}
1.114 +consts eval :: "((exp*state) * (nat*state)) set"
1.115 + "-|->" :: "[exp*state,nat*state] => bool" (infixl 50)
1.116 +
1.117 +translations
1.118 + "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
1.119 + "esig -|-> ns" == "(esig,ns ) \<in> eval"
1.120 +
1.121 +inductive eval
1.122 + intros
1.123 + N [intro!]: "(N(n),s) -|-> (n,s)"
1.124 +
1.125 + X [intro!]: "(X(x),s) -|-> (s(x),s)"
1.126 +
1.127 + Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |]
1.128 + ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
1.129 +
1.130 + valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |]
1.131 + ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
1.132 +
1.133 + monos exec_mono
1.134 +
1.135 +
1.136 +inductive_cases
1.137 + [elim!]: "(N(n),sigma) -|-> (n',s')"
1.138 + and [elim!]: "(X(x),sigma) -|-> (n,s')"
1.139 + and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')"
1.140 + and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
1.141 +
1.142 +
1.143 +lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
1.144 +by (rule fun_upd_same [THEN subst], fast)
1.145 +
1.146 +
1.147 +text{* Make the induction rule look nicer -- though eta_contract makes the new
1.148 + version look worse than it is...*}
1.149 +
1.150 +lemma split_lemma:
1.151 + "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
1.152 +by auto
1.153 +
1.154 +text{*New induction rule. Note the form of the VALOF induction hypothesis*}
1.155 +lemma eval_induct:
1.156 + "[| (e,s) -|-> (n,s');
1.157 + !!n s. P (N n) s n s;
1.158 + !!s x. P (X x) s (s x) s;
1.159 + !!e0 e1 f n0 n1 s s0 s1.
1.160 + [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
1.161 + (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
1.162 + |] ==> P (Op f e0 e1) s (f n0 n1) s1;
1.163 + !!c e n s s0 s1.
1.164 + [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
1.165 + (c,s) -[eval]-> s0;
1.166 + (e,s0) -|-> (n,s1); P e s0 n s1 |]
1.167 + ==> P (VALOF c RESULTIS e) s n s1
1.168 + |] ==> P e s n s'"
1.169 +apply (erule eval.induct, blast)
1.170 +apply blast
1.171 +apply blast
1.172 +apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
1.173 +apply (auto simp add: split_lemma)
1.174 +done
1.175 +
1.176
1.177 - WhileTrue "[| (e,s) -|[eval]-> (0,s1);
1.178 - (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
1.179 - ==> (WHILE e DO c, s) -[eval]-> s3"
1.180 +text{*Lemma for Function_eval. The major premise is that (c,s) executes to s1
1.181 + using eval restricted to its functional part. Note that the execution
1.182 + (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that
1.183 + the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
1.184 + functional on the argument (c,s).
1.185 +*}
1.186 +lemma com_Unique:
1.187 + "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
1.188 + ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
1.189 +apply (erule exec.induct, simp_all)
1.190 + apply blast
1.191 + apply force
1.192 + apply blast
1.193 + apply blast
1.194 + apply blast
1.195 + apply (blast elim: exec_WHILE_case)
1.196 +apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
1.197 +apply clarify
1.198 +apply (erule exec_WHILE_case, blast+)
1.199 +done
1.200 +
1.201 +
1.202 +text{*Expression evaluation is functional, or deterministic*}
1.203 +theorem single_valued_eval: "single_valued eval"
1.204 +apply (unfold single_valued_def)
1.205 +apply (intro allI, rule impI)
1.206 +apply (simp (no_asm_simp) only: split_tupled_all)
1.207 +apply (erule eval_induct)
1.208 +apply (drule_tac [4] com_Unique)
1.209 +apply (simp_all (no_asm_use))
1.210 +apply blast+
1.211 +done
1.212 +
1.213 +
1.214 +lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
1.215 +by (erule eval_induct, simp_all)
1.216 +
1.217 +lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
1.218 +
1.219 +
1.220 +text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
1.221 +lemma while_true_E [rule_format]:
1.222 + "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
1.223 +by (erule exec.induct, auto)
1.224 +
1.225 +
1.226 +subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
1.227 + WHILE e DO c *}
1.228 +
1.229 +lemma while_if1 [rule_format]:
1.230 + "(c',s) -[eval]-> t
1.231 + ==> (c' = WHILE e DO c) -->
1.232 + (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
1.233 +by (erule exec.induct, auto)
1.234 +
1.235 +lemma while_if2 [rule_format]:
1.236 + "(c',s) -[eval]-> t
1.237 + ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->
1.238 + (WHILE e DO c, s) -[eval]-> t"
1.239 +by (erule exec.induct, auto)
1.240 +
1.241 +
1.242 +theorem while_if:
1.243 + "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) =
1.244 + ((WHILE e DO c, s) -[eval]-> t)"
1.245 +by (blast intro: while_if1 while_if2)
1.246 +
1.247 +
1.248 +
1.249 +subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c
1.250 + and IF e THEN (c1;;c) ELSE (c2;;c) *}
1.251 +
1.252 +lemma if_semi1 [rule_format]:
1.253 + "(c',s) -[eval]-> t
1.254 + ==> (c' = (IF e THEN c1 ELSE c2);;c) -->
1.255 + (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
1.256 +by (erule exec.induct, auto)
1.257 +
1.258 +lemma if_semi2 [rule_format]:
1.259 + "(c',s) -[eval]-> t
1.260 + ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->
1.261 + ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
1.262 +by (erule exec.induct, auto)
1.263 +
1.264 +theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) =
1.265 + ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
1.266 +by (blast intro: if_semi1 if_semi2)
1.267 +
1.268 +
1.269 +
1.270 +subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
1.271 + and VALOF c1;;c2 RESULTIS e
1.272 + *}
1.273 +
1.274 +lemma valof_valof1 [rule_format]:
1.275 + "(e',s) -|-> (v,s')
1.276 + ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->
1.277 + (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
1.278 +by (erule eval_induct, auto)
1.279 +
1.280 +
1.281 +lemma valof_valof2 [rule_format]:
1.282 + "(e',s) -|-> (v,s')
1.283 + ==> (e' = VALOF c1;;c2 RESULTIS e) -->
1.284 + (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
1.285 +by (erule eval_induct, auto)
1.286 +
1.287 +theorem valof_valof:
1.288 + "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) =
1.289 + ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
1.290 +by (blast intro: valof_valof1 valof_valof2)
1.291 +
1.292 +
1.293 +subsection{* Equivalence of VALOF SKIP RESULTIS e and e *}
1.294 +
1.295 +lemma valof_skip1 [rule_format]:
1.296 + "(e',s) -|-> (v,s')
1.297 + ==> (e' = VALOF SKIP RESULTIS e) -->
1.298 + (e, s) -|-> (v,s')"
1.299 +by (erule eval_induct, auto)
1.300 +
1.301 +lemma valof_skip2:
1.302 + "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
1.303 +by blast
1.304 +
1.305 +theorem valof_skip:
1.306 + "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))"
1.307 +by (blast intro: valof_skip1 valof_skip2)
1.308 +
1.309 +
1.310 +subsection{* Equivalence of VALOF x:=e RESULTIS x and e *}
1.311 +
1.312 +lemma valof_assign1 [rule_format]:
1.313 + "(e',s) -|-> (v,s'')
1.314 + ==> (e' = VALOF x:=e RESULTIS X x) -->
1.315 + (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
1.316 +apply (erule eval_induct)
1.317 +apply (simp_all del: fun_upd_apply, clarify, auto)
1.318 +done
1.319 +
1.320 +lemma valof_assign2:
1.321 + "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
1.322 +by blast
1.323 +
1.324 +
1.325 end