src/HOL/Induct/Com.thy
 changeset 13075 d3e1d554cd6d parent 12338 de0f4a63baa5 child 14527 bc9e5587d05a
```     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.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
```