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.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