src/HOL/Induct/Com.thy

 
 subsection {* Commands *}
 
 text{* Execution of commands *}
 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
-       "@exec"  :: "((exp*state) * (nat*state)) set => 
+syntax "@exec"  :: "((exp*state) * (nat*state)) set =>
                     [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
 
 translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
 
-syntax  eval'   :: "[exp*state,nat*state] => 
-		    ((exp*state) * (nat*state)) set => bool"
-					   ("_/ -|[_]-> _" [50,0,50] 50)
+syntax  eval'   :: "[exp*state,nat*state] =>
+                    ((exp*state) * (nat*state)) set => bool"
+                                           ("_/ -|[_]-> _" [50,0,50] 50)
 
 translations
     "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
 
 text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}

   intros
     Skip:    "(SKIP,s) -[eval]-> s"
 
     Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
 
-    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
+    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
              ==> (c0 ;; c1, s) -[eval]-> s1"
 
-    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
+    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
+    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) 
+    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
                  ==> (WHILE e DO c, s) -[eval]-> s1"
 
     WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
-                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
+                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
                  ==> (WHILE e DO c, s) -[eval]-> s3"
 
 declare exec.intros [intro]
 
 
 inductive_cases
-	[elim!]: "(SKIP,s) -[eval]-> t"
+        [elim!]: "(SKIP,s) -[eval]-> t"
     and [elim!]: "(x:=a,s) -[eval]-> t"
-    and	[elim!]: "(c1;;c2, s) -[eval]-> t"
-    and	[elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
-    and	exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
+    and [elim!]: "(c1;;c2, s) -[eval]-> t"
+    and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
+    and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
 
 
 text{*Justifies using "exec" in the inductive definition of "eval"*}
 lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
 apply (unfold exec.defs )

 *}
 
 text{*Command execution is functional (deterministic) provided evaluation is*}
 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
 apply (simp add: single_valued_def)
-apply (intro allI) 
+apply (intro allI)
 apply (rule impI)
 apply (erule exec.induct)
 apply (blast elim: exec_WHILE_case)+
 done
 

        "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
 
 translations
     "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
     "esig -|-> ns"    == "(esig,ns ) \<in> eval"
-  
+
 inductive eval
-  intros 
+  intros
     N [intro!]: "(N(n),s) -|-> (n,s)"
 
     X [intro!]: "(X(x),s) -|-> (s(x),s)"
 
-    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
+    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
 
-    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
+    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
 
   monos exec_mono
 
 
 inductive_cases
-	[elim!]: "(N(n),sigma) -|-> (n',s')"
+        [elim!]: "(N(n),sigma) -|-> (n',s')"
     and [elim!]: "(X(x),sigma) -|-> (n,s')"
-    and	[elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
-    and	[elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
+    and [elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
+    and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
 
 
 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
 by (rule fun_upd_same [THEN subst], fast)
 

 lemma split_lemma:
      "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
 by auto
 
 text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
-lemma eval_induct:
-  "[| (e,s) -|-> (n,s');                                          
-      !!n s. P (N n) s n s;                                       
-      !!s x. P (X x) s (s x) s;                                   
-      !!e0 e1 f n0 n1 s s0 s1.                                    
-         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                    
-            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                   
-         |] ==> P (Op f e0 e1) s (f n0 n1) s1;                    
-      !!c e n s s0 s1.                                            
-         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;  
-            (c,s) -[eval]-> s0;                                   
-            (e,s0) -|-> (n,s1); P e s0 n s1 |]                    
-         ==> P (VALOF c RESULTIS e) s n s1                        
+lemma eval_induct
+  [case_names N X Op valOf, consumes 1, induct set: eval]:
+  "[| (e,s) -|-> (n,s');
+      !!n s. P (N n) s n s;
+      !!s x. P (X x) s (s x) s;
+      !!e0 e1 f n0 n1 s s0 s1.
+         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
+            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
+         |] ==> P (Op f e0 e1) s (f n0 n1) s1;
+      !!c e n s s0 s1.
+         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
+            (c,s) -[eval]-> s0;
+            (e,s0) -|-> (n,s1); P e s0 n s1 |]
+         ==> P (VALOF c RESULTIS e) s n s1
    |] ==> P e s n s'"
-apply (erule eval.induct, blast) 
-apply blast 
-apply blast 
+apply (induct set: eval)
+apply blast
+apply blast
+apply blast
 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
 apply (auto simp add: split_lemma)
 done
 
 
 text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
   using eval restricted to its functional part.  Note that the execution
-  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
+  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that
   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   functional on the argument (c,s).
 *}
 lemma com_Unique:
- "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1  
+ "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
-apply (erule exec.induct, simp_all)
+apply (induct set: exec)
+      apply simp_all
       apply blast
      apply force
     apply blast
    apply blast
   apply blast
  apply (blast elim: exec_WHILE_case)
 apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
 apply clarify
-apply (erule exec_WHILE_case, blast+) 
+apply (erule exec_WHILE_case, blast+)
 done
 
 
 text{*Expression evaluation is functional, or deterministic*}
 theorem single_valued_eval: "single_valued eval"
 apply (unfold single_valued_def)
-apply (intro allI, rule impI) 
+apply (intro allI, rule impI)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply (erule eval_induct)
 apply (drule_tac [4] com_Unique)
 apply (simp_all (no_asm_use))
 apply blast+
 done
 
-
-lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
-by (erule eval_induct, simp_all)
-
-lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
-
+lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
+  by (induct e == "N n" s v s' set: eval) simp_all
 
 text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
-lemma while_true_E [rule_format]:
-     "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
-by (erule exec.induct, auto)
-
-
-subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  
+lemma while_true_E:
+    "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
+  by (induct set: exec) auto
+
+
+subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
        WHILE e DO c *}
 
-lemma while_if1 [rule_format]:
-     "(c',s) -[eval]-> t 
-      ==> (c' = WHILE e DO c) -->  
+lemma while_if1:
+     "(c',s) -[eval]-> t
+      ==> c' = WHILE e DO c ==>
           (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
-by (erule exec.induct, auto)
-
-lemma while_if2 [rule_format]:
+  by (induct set: exec) auto
+
+lemma while_if2:
      "(c',s) -[eval]-> t
-      ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->  
+      ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>
           (WHILE e DO c, s) -[eval]-> t"
-by (erule exec.induct, auto)
+  by (induct set: exec) auto
 
 
 theorem while_if:
-     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =   
+     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =
       ((WHILE e DO c, s) -[eval]-> t)"
 by (blast intro: while_if1 while_if2)
 
 
 
 subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
                          and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
 
-lemma if_semi1 [rule_format]:
+lemma if_semi1:
      "(c',s) -[eval]-> t
-      ==> (c' = (IF e THEN c1 ELSE c2);;c) -->  
+      ==> c' = (IF e THEN c1 ELSE c2);;c ==>
           (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
-by (erule exec.induct, auto)
-
-lemma if_semi2 [rule_format]:
+  by (induct set: exec) auto
+
+lemma if_semi2:
      "(c',s) -[eval]-> t
-      ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->  
+      ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>
           ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
-by (erule exec.induct, auto)
-
-theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =   
+  by (induct set: exec) auto
+
+theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =
                   ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
-by (blast intro: if_semi1 if_semi2)
+  by (blast intro: if_semi1 if_semi2)
 
 
 
 subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
                   and  VALOF c1;;c2 RESULTIS e
  *}
 
-lemma valof_valof1 [rule_format]:
-     "(e',s) -|-> (v,s')  
-      ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->  
+lemma valof_valof1:
+     "(e',s) -|-> (v,s')
+      ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==>
           (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
-by (erule eval_induct, auto)
-
-
-lemma valof_valof2 [rule_format]:
+  by (induct set: eval) auto
+
+lemma valof_valof2:
      "(e',s) -|-> (v,s')
-      ==> (e' = VALOF c1;;c2 RESULTIS e) -->  
+      ==> e' = VALOF c1;;c2 RESULTIS e ==>
           (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
-by (erule eval_induct, auto)
+  by (induct set: eval) auto
 
 theorem valof_valof:
-     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =   
+     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =
       ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
-by (blast intro: valof_valof1 valof_valof2)
+  by (blast intro: valof_valof1 valof_valof2)
 
 
 subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
 
-lemma valof_skip1 [rule_format]:
+lemma valof_skip1:
      "(e',s) -|-> (v,s')
-      ==> (e' = VALOF SKIP RESULTIS e) -->  
+      ==> e' = VALOF SKIP RESULTIS e ==>
           (e, s) -|-> (v,s')"
-by (erule eval_induct, auto)
+  by (induct set: eval) auto
 
 lemma valof_skip2:
-     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
-by blast
+    "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
+  by blast
 
 theorem valof_skip:
-     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
-by (blast intro: valof_skip1 valof_skip2)
+    "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
+  by (blast intro: valof_skip1 valof_skip2)
 
 
 subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
 
-lemma valof_assign1 [rule_format]:
+lemma valof_assign1:
      "(e',s) -|-> (v,s'')
-      ==> (e' = VALOF x:=e RESULTIS X x) -->  
+      ==> e' = VALOF x:=e RESULTIS X x ==>
           (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
-apply (erule eval_induct)
-apply (simp_all del: fun_upd_apply, clarify, auto) 
-done
+  by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)
 
 lemma valof_assign2:
-     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
-by blast
-
+    "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
+  by blast
 
 end