src/HOL/IMP/Small_Step.thy

 
 
 text{* A simple property: *}
 lemma deterministic:
   "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
-apply(induct arbitrary: cs'' rule: small_step.induct)
+apply(induction arbitrary: cs'' rule: small_step.induct)
 apply blast+
 done
 
 
 subsection "Equivalence with big-step semantics"
 
 lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
-proof(induct rule: star_induct)
+proof(induction rule: star_induct)
   case refl thus ?case by simp
 next
   case step
   thus ?case by (metis Semi2 star.step)
 qed

 also/finally proof steps do: they compose chains, implicitly using the rules
 declared with attribute [trans] above. *}
 
 lemma big_to_small:
   "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
-proof (induct rule: big_step.induct)
+proof (induction rule: big_step.induct)
   fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
 next
   fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
 next
   fix c1 c2 s1 s2 s3

   finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
 qed
 
 text{* Each case of the induction can be proved automatically: *}
 lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
-proof (induct rule: big_step.induct)
+proof (induction rule: big_step.induct)
   case Skip show ?case by blast
 next
   case Assign show ?case by blast
 next
   case Semi thus ?case by (blast intro: semi_comp)

     by(metis While semi_comp small_step.IfTrue step[of small_step])
 qed
 
 lemma small1_big_continue:
   "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
-apply (induct arbitrary: t rule: small_step.induct)
+apply (induction arbitrary: t rule: small_step.induct)
 apply auto
 done
 
 lemma small_big_continue:
   "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
-apply (induct rule: star.induct)
+apply (induction rule: star.induct)
 apply (auto intro: small1_big_continue)
 done
 
 lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
 by (metis small_big_continue Skip)

 
 definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
 
 lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
 apply(simp add: final_def)
-apply(induct c)
+apply(induction c)
 apply blast+
 done
 
 lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
 by (metis SkipE finalD final_def)