src/HOL/Induct/Com.thy
changeset 18260 5597cfcecd49
parent 16417 9bc16273c2d4
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/Induct/Com.thy	Fri Nov 25 20:57:51 2005 +0100
     1.2 +++ b/src/HOL/Induct/Com.thy	Fri Nov 25 21:14:34 2005 +0100
     1.3 @@ -34,14 +34,14 @@
     1.4  
     1.5  text{* Execution of commands *}
     1.6  consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
     1.7 -       "@exec"  :: "((exp*state) * (nat*state)) set => 
     1.8 +syntax "@exec"  :: "((exp*state) * (nat*state)) set =>
     1.9                      [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    1.10  
    1.11  translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
    1.12  
    1.13 -syntax  eval'   :: "[exp*state,nat*state] => 
    1.14 -		    ((exp*state) * (nat*state)) set => bool"
    1.15 -					   ("_/ -|[_]-> _" [50,0,50] 50)
    1.16 +syntax  eval'   :: "[exp*state,nat*state] =>
    1.17 +                    ((exp*state) * (nat*state)) set => bool"
    1.18 +                                           ("_/ -|[_]-> _" [50,0,50] 50)
    1.19  
    1.20  translations
    1.21      "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
    1.22 @@ -53,31 +53,31 @@
    1.23  
    1.24      Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    1.25  
    1.26 -    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    1.27 +    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
    1.28               ==> (c0 ;; c1, s) -[eval]-> s1"
    1.29  
    1.30 -    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
    1.31 +    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
    1.32               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.33  
    1.34 -    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
    1.35 +    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
    1.36                ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.37  
    1.38 -    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) 
    1.39 +    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
    1.40                   ==> (WHILE e DO c, s) -[eval]-> s1"
    1.41  
    1.42      WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    1.43 -                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    1.44 +                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
    1.45                   ==> (WHILE e DO c, s) -[eval]-> s3"
    1.46  
    1.47  declare exec.intros [intro]
    1.48  
    1.49  
    1.50  inductive_cases
    1.51 -	[elim!]: "(SKIP,s) -[eval]-> t"
    1.52 +        [elim!]: "(SKIP,s) -[eval]-> t"
    1.53      and [elim!]: "(x:=a,s) -[eval]-> t"
    1.54 -    and	[elim!]: "(c1;;c2, s) -[eval]-> t"
    1.55 -    and	[elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
    1.56 -    and	exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    1.57 +    and [elim!]: "(c1;;c2, s) -[eval]-> t"
    1.58 +    and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
    1.59 +    and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    1.60  
    1.61  
    1.62  text{*Justifies using "exec" in the inductive definition of "eval"*}
    1.63 @@ -95,7 +95,7 @@
    1.64  text{*Command execution is functional (deterministic) provided evaluation is*}
    1.65  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
    1.66  apply (simp add: single_valued_def)
    1.67 -apply (intro allI) 
    1.68 +apply (intro allI)
    1.69  apply (rule impI)
    1.70  apply (erule exec.induct)
    1.71  apply (blast elim: exec_WHILE_case)+
    1.72 @@ -111,27 +111,27 @@
    1.73  translations
    1.74      "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
    1.75      "esig -|-> ns"    == "(esig,ns ) \<in> eval"
    1.76 -  
    1.77 +
    1.78  inductive eval
    1.79 -  intros 
    1.80 +  intros
    1.81      N [intro!]: "(N(n),s) -|-> (n,s)"
    1.82  
    1.83      X [intro!]: "(X(x),s) -|-> (s(x),s)"
    1.84  
    1.85 -    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
    1.86 +    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
    1.87                   ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
    1.88  
    1.89 -    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
    1.90 +    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
    1.91                      ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
    1.92  
    1.93    monos exec_mono
    1.94  
    1.95  
    1.96  inductive_cases
    1.97 -	[elim!]: "(N(n),sigma) -|-> (n',s')"
    1.98 +        [elim!]: "(N(n),sigma) -|-> (n',s')"
    1.99      and [elim!]: "(X(x),sigma) -|-> (n,s')"
   1.100 -    and	[elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
   1.101 -    and	[elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   1.102 +    and [elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
   1.103 +    and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   1.104  
   1.105  
   1.106  lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
   1.107 @@ -146,23 +146,25 @@
   1.108  by auto
   1.109  
   1.110  text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
   1.111 -lemma eval_induct:
   1.112 -  "[| (e,s) -|-> (n,s');                                          
   1.113 -      !!n s. P (N n) s n s;                                       
   1.114 -      !!s x. P (X x) s (s x) s;                                   
   1.115 -      !!e0 e1 f n0 n1 s s0 s1.                                    
   1.116 -         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                    
   1.117 -            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                   
   1.118 -         |] ==> P (Op f e0 e1) s (f n0 n1) s1;                    
   1.119 -      !!c e n s s0 s1.                                            
   1.120 -         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;  
   1.121 -            (c,s) -[eval]-> s0;                                   
   1.122 -            (e,s0) -|-> (n,s1); P e s0 n s1 |]                    
   1.123 -         ==> P (VALOF c RESULTIS e) s n s1                        
   1.124 +lemma eval_induct
   1.125 +  [case_names N X Op valOf, consumes 1, induct set: eval]:
   1.126 +  "[| (e,s) -|-> (n,s');
   1.127 +      !!n s. P (N n) s n s;
   1.128 +      !!s x. P (X x) s (s x) s;
   1.129 +      !!e0 e1 f n0 n1 s s0 s1.
   1.130 +         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
   1.131 +            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
   1.132 +         |] ==> P (Op f e0 e1) s (f n0 n1) s1;
   1.133 +      !!c e n s s0 s1.
   1.134 +         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
   1.135 +            (c,s) -[eval]-> s0;
   1.136 +            (e,s0) -|-> (n,s1); P e s0 n s1 |]
   1.137 +         ==> P (VALOF c RESULTIS e) s n s1
   1.138     |] ==> P e s n s'"
   1.139 -apply (erule eval.induct, blast) 
   1.140 -apply blast 
   1.141 -apply blast 
   1.142 +apply (induct set: eval)
   1.143 +apply blast
   1.144 +apply blast
   1.145 +apply blast
   1.146  apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
   1.147  apply (auto simp add: split_lemma)
   1.148  done
   1.149 @@ -170,14 +172,15 @@
   1.150  
   1.151  text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
   1.152    using eval restricted to its functional part.  Note that the execution
   1.153 -  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
   1.154 +  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that
   1.155    the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   1.156    functional on the argument (c,s).
   1.157  *}
   1.158  lemma com_Unique:
   1.159 - "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1  
   1.160 + "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
   1.161    ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
   1.162 -apply (erule exec.induct, simp_all)
   1.163 +apply (induct set: exec)
   1.164 +      apply simp_all
   1.165        apply blast
   1.166       apply force
   1.167      apply blast
   1.168 @@ -186,14 +189,14 @@
   1.169   apply (blast elim: exec_WHILE_case)
   1.170  apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
   1.171  apply clarify
   1.172 -apply (erule exec_WHILE_case, blast+) 
   1.173 +apply (erule exec_WHILE_case, blast+)
   1.174  done
   1.175  
   1.176  
   1.177  text{*Expression evaluation is functional, or deterministic*}
   1.178  theorem single_valued_eval: "single_valued eval"
   1.179  apply (unfold single_valued_def)
   1.180 -apply (intro allI, rule impI) 
   1.181 +apply (intro allI, rule impI)
   1.182  apply (simp (no_asm_simp) only: split_tupled_all)
   1.183  apply (erule eval_induct)
   1.184  apply (drule_tac [4] com_Unique)
   1.185 @@ -201,37 +204,33 @@
   1.186  apply blast+
   1.187  done
   1.188  
   1.189 -
   1.190 -lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
   1.191 -by (erule eval_induct, simp_all)
   1.192 -
   1.193 -lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
   1.194 -
   1.195 +lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
   1.196 +  by (induct e == "N n" s v s' set: eval) simp_all
   1.197  
   1.198  text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
   1.199 -lemma while_true_E [rule_format]:
   1.200 -     "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
   1.201 -by (erule exec.induct, auto)
   1.202 +lemma while_true_E:
   1.203 +    "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
   1.204 +  by (induct set: exec) auto
   1.205  
   1.206  
   1.207 -subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  
   1.208 +subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
   1.209         WHILE e DO c *}
   1.210  
   1.211 -lemma while_if1 [rule_format]:
   1.212 -     "(c',s) -[eval]-> t 
   1.213 -      ==> (c' = WHILE e DO c) -->  
   1.214 +lemma while_if1:
   1.215 +     "(c',s) -[eval]-> t
   1.216 +      ==> c' = WHILE e DO c ==>
   1.217            (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
   1.218 -by (erule exec.induct, auto)
   1.219 +  by (induct set: exec) auto
   1.220  
   1.221 -lemma while_if2 [rule_format]:
   1.222 +lemma while_if2:
   1.223       "(c',s) -[eval]-> t
   1.224 -      ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->  
   1.225 +      ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>
   1.226            (WHILE e DO c, s) -[eval]-> t"
   1.227 -by (erule exec.induct, auto)
   1.228 +  by (induct set: exec) auto
   1.229  
   1.230  
   1.231  theorem while_if:
   1.232 -     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =   
   1.233 +     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =
   1.234        ((WHILE e DO c, s) -[eval]-> t)"
   1.235  by (blast intro: while_if1 while_if2)
   1.236  
   1.237 @@ -240,21 +239,21 @@
   1.238  subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
   1.239                           and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
   1.240  
   1.241 -lemma if_semi1 [rule_format]:
   1.242 +lemma if_semi1:
   1.243       "(c',s) -[eval]-> t
   1.244 -      ==> (c' = (IF e THEN c1 ELSE c2);;c) -->  
   1.245 +      ==> c' = (IF e THEN c1 ELSE c2);;c ==>
   1.246            (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
   1.247 -by (erule exec.induct, auto)
   1.248 +  by (induct set: exec) auto
   1.249  
   1.250 -lemma if_semi2 [rule_format]:
   1.251 +lemma if_semi2:
   1.252       "(c',s) -[eval]-> t
   1.253 -      ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->  
   1.254 +      ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>
   1.255            ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
   1.256 -by (erule exec.induct, auto)
   1.257 +  by (induct set: exec) auto
   1.258  
   1.259 -theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =   
   1.260 +theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =
   1.261                    ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
   1.262 -by (blast intro: if_semi1 if_semi2)
   1.263 +  by (blast intro: if_semi1 if_semi2)
   1.264  
   1.265  
   1.266  
   1.267 @@ -262,55 +261,51 @@
   1.268                    and  VALOF c1;;c2 RESULTIS e
   1.269   *}
   1.270  
   1.271 -lemma valof_valof1 [rule_format]:
   1.272 -     "(e',s) -|-> (v,s')  
   1.273 -      ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->  
   1.274 +lemma valof_valof1:
   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 +  by (induct set: eval) auto
   1.280  
   1.281 -
   1.282 -lemma valof_valof2 [rule_format]:
   1.283 +lemma valof_valof2:
   1.284       "(e',s) -|-> (v,s')
   1.285 -      ==> (e' = VALOF c1;;c2 RESULTIS e) -->  
   1.286 +      ==> e' = VALOF c1;;c2 RESULTIS e ==>
   1.287            (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
   1.288 -by (erule eval_induct, auto)
   1.289 +  by (induct set: eval) auto
   1.290  
   1.291  theorem valof_valof:
   1.292 -     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =   
   1.293 +     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =
   1.294        ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
   1.295 -by (blast intro: valof_valof1 valof_valof2)
   1.296 +  by (blast intro: valof_valof1 valof_valof2)
   1.297  
   1.298  
   1.299  subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
   1.300  
   1.301 -lemma valof_skip1 [rule_format]:
   1.302 +lemma valof_skip1:
   1.303       "(e',s) -|-> (v,s')
   1.304 -      ==> (e' = VALOF SKIP RESULTIS e) -->  
   1.305 +      ==> e' = VALOF SKIP RESULTIS e ==>
   1.306            (e, s) -|-> (v,s')"
   1.307 -by (erule eval_induct, auto)
   1.308 +  by (induct set: eval) auto
   1.309  
   1.310  lemma valof_skip2:
   1.311 -     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
   1.312 -by blast
   1.313 +    "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
   1.314 +  by blast
   1.315  
   1.316  theorem valof_skip:
   1.317 -     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
   1.318 -by (blast intro: valof_skip1 valof_skip2)
   1.319 +    "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
   1.320 +  by (blast intro: valof_skip1 valof_skip2)
   1.321  
   1.322  
   1.323  subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
   1.324  
   1.325 -lemma valof_assign1 [rule_format]:
   1.326 +lemma valof_assign1:
   1.327       "(e',s) -|-> (v,s'')
   1.328 -      ==> (e' = VALOF x:=e RESULTIS X x) -->  
   1.329 +      ==> e' = VALOF x:=e RESULTIS X x ==>
   1.330            (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
   1.331 -apply (erule eval_induct)
   1.332 -apply (simp_all del: fun_upd_apply, clarify, auto) 
   1.333 -done
   1.334 +  by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)
   1.335  
   1.336  lemma valof_assign2:
   1.337 -     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
   1.338 -by blast
   1.339 -
   1.340 +    "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
   1.341 +  by blast
   1.342  
   1.343  end