--- a/src/HOL/IMP/AExp.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AExp.thy Tue Sep 20 05:48:23 2011 +0200
@@ -62,7 +62,7 @@
theorem aval_asimp_const[simp]:
"aval (asimp_const a) s = aval a s"
-apply(induct a)
+apply(induction a)
apply (auto split: aexp.split)
done
@@ -77,7 +77,7 @@
lemma aval_plus[simp]:
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
-apply(induct a1 a2 rule: plus.induct)
+apply(induction a1 a2 rule: plus.induct)
apply simp_all (* just for a change from auto *)
done
@@ -94,7 +94,7 @@
theorem aval_asimp[simp]:
"aval (asimp a) s = aval a s"
-apply(induct a)
+apply(induction a)
apply simp_all
done
--- a/src/HOL/IMP/ASM.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/ASM.thy Tue Sep 20 05:48:23 2011 +0200
@@ -29,7 +29,7 @@
lemma aexec_append[simp]:
"aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
-apply(induct is1 arbitrary: stk)
+apply(induction is1 arbitrary: stk)
apply (auto)
done
@@ -44,7 +44,7 @@
value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
-apply(induct a arbitrary: stk)
+apply(induction a arbitrary: stk)
apply (auto)
done
--- a/src/HOL/IMP/AbsInt0.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy Tue Sep 20 05:48:23 2011 +0200
@@ -38,7 +38,7 @@
"AI (WHILE b DO c) S = pfp (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induct c arbitrary: s t S0)
+proof(induction c arbitrary: s t S0)
case SKIP thus ?case by fastforce
next
case Assign thus ?case
@@ -52,10 +52,10 @@
case (While b c)
let ?P = "pfp (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
- proof(induct "WHILE b DO c" s t rule: big_step_induct)
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
next
- case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
+ case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
qed
}
with astate_in_rep_le[OF `s <: S0` above]
--- a/src/HOL/IMP/AbsInt0_fun.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy Tue Sep 20 05:48:23 2011 +0200
@@ -36,7 +36,7 @@
"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
apply (simp)
apply (simp)
done
@@ -52,7 +52,7 @@
point does @{const iter} yield? *}
lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
-apply(induct n arbitrary: x)
+apply(induction n arbitrary: x)
apply simp
apply (auto)
apply(metis funpow.simps(1) id_def)
@@ -69,7 +69,7 @@
using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
moreover
{ fix n have "(f^^n) x0 \<sqsubseteq> p"
- proof(induct n)
+ proof(induction n)
case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
next
case (Suc n) thus ?case
@@ -155,7 +155,7 @@
"AI (WHILE b DO c) S = pfp (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induct c arbitrary: s t S0)
+proof(induction c arbitrary: s t S0)
case SKIP thus ?case by fastforce
next
case Assign thus ?case by (auto simp: aval'_sound)
@@ -167,10 +167,10 @@
case (While b c)
let ?P = "pfp (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
- proof(induct "WHILE b DO c" s t rule: big_step_induct)
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
next
- case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
+ case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
qed
}
with fun_in_rep_le[OF `s <: S0` above]
--- a/src/HOL/IMP/AbsInt1.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy Tue Sep 20 05:48:23 2011 +0200
@@ -141,7 +141,7 @@
in afilter e1 res1 (afilter e2 res2 S))"
lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
-proof(induct e arbitrary: a S)
+proof(induction e arbitrary: a S)
case N thus ?case by simp
next
case (V x)
@@ -158,7 +158,7 @@
qed
lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
-proof(induct b arbitrary: S bv)
+proof(induction b arbitrary: S bv)
case B thus ?case by simp
next
case (Not b) thus ?case by simp
@@ -181,7 +181,7 @@
bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
-proof(induct c arbitrary: s t S)
+proof(induction c arbitrary: s t S)
case SKIP thus ?case by fastforce
next
case Assign thus ?case
@@ -196,12 +196,12 @@
{ fix s t
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
t <:: bfilter b False ?P"
- proof(induct "WHILE b DO c" s t rule: big_step_induct)
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by(metis bfilter_sound)
next
case WhileTrue show ?case
by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
- rule While.hyps[OF WhileTrue(2)],
+ rule While.IH[OF WhileTrue(2)],
rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
qed
}
--- a/src/HOL/IMP/AbsInt2.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy Tue Sep 20 05:48:23 2011 +0200
@@ -24,7 +24,7 @@
(let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
apply (simp)
apply (simp add: Let_def)
done
@@ -35,7 +35,7 @@
(let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
apply (simp)
apply (simp add: Let_def)
done
--- a/src/HOL/IMP/BExp.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/BExp.thy Tue Sep 20 05:48:23 2011 +0200
@@ -23,7 +23,7 @@
"less a1 a2 = Less a1 a2"
lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
-apply(induct a1 a2 rule: less.induct)
+apply(induction a1 a2 rule: less.induct)
apply simp_all
done
@@ -35,7 +35,7 @@
"and b1 b2 = And b1 b2"
lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
-apply(induct b1 b2 rule: and.induct)
+apply(induction b1 b2 rule: and.induct)
apply simp_all
done
@@ -45,7 +45,7 @@
"not b = Not b"
lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
-apply(induct b rule: not.induct)
+apply(induction b rule: not.induct)
apply simp_all
done
@@ -62,7 +62,7 @@
value "bsimp (And (Less (N 1) (N 0)) (B True))"
theorem "bval (bsimp b) s = bval b s"
-apply(induct b)
+apply(induction b)
apply simp_all
done
--- a/src/HOL/IMP/Big_Step.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy Tue Sep 20 05:48:23 2011 +0200
@@ -215,7 +215,7 @@
text {* This proof is automatic. *}
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
-apply (induct arbitrary: u rule: big_step.induct)
+apply (induction arbitrary: u rule: big_step.induct)
apply blast+
done
@@ -225,7 +225,7 @@
*}
theorem
"(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t"
-proof (induct arbitrary: t' rule: big_step.induct)
+proof (induction arbitrary: t' rule: big_step.induct)
-- "the only interesting case, @{text WhileTrue}:"
fix b c s s1 t t'
-- "The assumptions of the rule:"
--- a/src/HOL/IMP/Comp_Rev.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy Tue Sep 20 05:48:23 2011 +0200
@@ -196,13 +196,13 @@
"0 \<le> i \<Longrightarrow>
succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
\<union> {n + i + isize (bcomp b c i)}"
-proof (induct b arbitrary: c i n)
+proof (induction b arbitrary: c i n)
case (And b1 b2)
from And.prems
show ?case
by (cases c)
- (auto dest: And.hyps(1) [THEN subsetD, rotated]
- And.hyps(2) [THEN subsetD, rotated])
+ (auto dest: And.IH(1) [THEN subsetD, rotated]
+ And.IH(2) [THEN subsetD, rotated])
qed auto
lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
@@ -219,7 +219,7 @@
lemma ccomp_succs:
"succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
-proof (induct c arbitrary: n)
+proof (induction c arbitrary: n)
case SKIP thus ?case by simp
next
case Assign thus ?case by simp
@@ -227,16 +227,16 @@
case (Semi c1 c2)
from Semi.prems
show ?case
- by (fastforce dest: Semi.hyps [THEN subsetD])
+ by (fastforce dest: Semi.IH [THEN subsetD])
next
case (If b c1 c2)
from If.prems
show ?case
- by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)
+ by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
next
case (While b c)
from While.prems
- show ?case by (auto dest!: While.hyps [THEN subsetD])
+ show ?case by (auto dest!: While.IH [THEN subsetD])
qed
lemma ccomp_exits:
@@ -264,7 +264,7 @@
i' \<in> exits c \<and>
P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
n = k + m"
-using assms proof (induct n arbitrary: i j s)
+using assms proof (induction n arbitrary: i j s)
case 0
thus ?case by simp
next
@@ -289,7 +289,7 @@
{ assume "j0 \<in> {0 ..< isize c}"
with j0 j rest c
have ?case
- by (fastforce dest!: Suc.hyps intro!: exec_Suc)
+ by (fastforce dest!: Suc.IH intro!: exec_Suc)
} moreover {
assume "j0 \<notin> {0 ..< isize c}"
moreover
@@ -338,7 +338,7 @@
assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
"isize P \<le> i" "exits P' \<subseteq> {0..}"
shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
-using assms proof (induct k arbitrary: i s stk)
+using assms proof (induction k arbitrary: i s stk)
case 0 thus ?case by simp
next
case (Suc k)
@@ -357,7 +357,7 @@
have "isize P \<le> i'" by (auto simp: exits_def)
from rest this `exits P' \<subseteq> {0..}`
have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
- by (rule Suc.hyps)
+ by (rule Suc.IH)
finally
show ?case .
qed
@@ -411,7 +411,7 @@
lemma acomp_exec_n [dest!]:
"acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow>
s' = s \<and> stk' = aval a s#stk"
-proof (induct a arbitrary: n s' stk stk')
+proof (induction a arbitrary: n s' stk stk')
case (Plus a1 a2)
let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
from Plus.prems
@@ -424,7 +424,7 @@
"[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
by (auto dest!: exec_n_split_full)
- thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
+ thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
qed (auto simp: exec_n_simps)
lemma bcomp_split:
@@ -442,13 +442,13 @@
"isize (bcomp b c j) \<le> i" "0 \<le> j"
shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
s' = s \<and> stk' = stk"
-using assms proof (induct b arbitrary: c j i n s' stk')
+using assms proof (induction b arbitrary: c j i n s' stk')
case B thus ?case
by (simp split: split_if_asm add: exec_n_simps)
next
case (Not b)
from Not.prems show ?case
- by (fastforce dest!: Not.hyps)
+ by (fastforce dest!: Not.IH)
next
case (And b1 b2)
@@ -466,10 +466,10 @@
by (auto dest!: bcomp_split dest: exec_n_drop_left)
from b1 j
have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
- by (auto dest!: And.hyps)
+ by (auto dest!: And.IH)
with b2 j
show ?case
- by (fastforce dest!: And.hyps simp: exec_n_end split: split_if_asm)
+ by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
next
case Less
thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *)
@@ -484,7 +484,7 @@
lemma ccomp_exec_n:
"ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
\<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
-proof (induct c arbitrary: s t stk stk' n)
+proof (induction c arbitrary: s t stk stk' n)
case SKIP
thus ?case by auto
next
@@ -496,7 +496,7 @@
thus ?case by (fastforce dest!: exec_n_split_full)
next
case (If b c1 c2)
- note If.hyps [dest!]
+ note If.IH [dest!]
let ?if = "IF b THEN c1 ELSE c2"
let ?cs = "ccomp ?if"
@@ -538,7 +538,7 @@
from While.prems
show ?case
- proof (induct n arbitrary: s rule: nat_less_induct)
+ proof (induction n arbitrary: s rule: nat_less_induct)
case (1 n)
{ assume "\<not> bval b s"
@@ -568,7 +568,7 @@
"?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
"m < n"
by (auto simp: exec_n_step [where k=k])
- with "1.hyps"
+ with "1.IH"
show ?case by blast
next
assume "ccomp c \<noteq> []"
@@ -581,14 +581,14 @@
by (auto dest: exec_n_split [where i=0, simplified])
from c
have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
- by (auto dest!: While.hyps)
+ by (auto dest!: While.IH)
moreover
from rest m k stk
obtain k' where
"?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
"k' < n"
by (auto simp: exec_n_step [where k=m])
- with "1.hyps"
+ with "1.IH"
have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
ultimately
show ?case using b by blast
--- a/src/HOL/IMP/Compiler.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Tue Sep 20 05:48:23 2011 +0200
@@ -222,7 +222,7 @@
"0 \<le> n \<Longrightarrow>
bcomp b c n \<turnstile>
(0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
-proof(induct b arbitrary: c n m)
+proof(induction b arbitrary: c n m)
case Not
from Not(1)[where c="~c"] Not(2) show ?case by fastforce
next
@@ -256,17 +256,17 @@
lemma ccomp_bigstep:
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
-proof(induct arbitrary: stk rule: big_step_induct)
+proof(induction arbitrary: stk rule: big_step_induct)
case (Assign x a s)
show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
case (Semi c1 s1 s2 c2 s3)
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
- using Semi.hyps(2) by fastforce
+ using Semi.IH(1) by fastforce
moreover
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
- using Semi.hyps(4) by fastforce
+ using Semi.IH(2) by fastforce
ultimately show ?case by simp (blast intro: exec_trans)
next
case (WhileTrue b s1 c s2 s3)
@@ -274,12 +274,12 @@
let ?cb = "bcomp b False (isize ?cc + 1)"
let ?cw = "ccomp(WHILE b DO c)"
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
- using WhileTrue(1,3) by fastforce
+ using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
moreover
have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
by fastforce
moreover
- have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
+ have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
ultimately show ?case by(blast intro: exec_trans)
qed fastforce+
--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:48:23 2011 +0200
@@ -12,7 +12,7 @@
theorem Sound:
"\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk>
\<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
-proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
+proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
case AssignNone thus ?case
by auto (metis aval_Some option.simps(3) subset_trans)
next
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy Tue Sep 20 05:48:23 2011 +0200
@@ -7,7 +7,7 @@
theorem progress:
"D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
-proof (induct c arbitrary: s A')
+proof (induction c arbitrary: s A')
case Assign thus ?case by auto (metis aval_Some small_step.Assign)
next
case (If b c1 c2)
@@ -17,13 +17,13 @@
qed (fastforce intro: small_step.intros)+
lemma D_mono: "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
-proof (induct c arbitrary: A A' M)
+proof (induction c arbitrary: A A' M)
case Semi thus ?case by auto (metis D.intros(3))
next
case (If b c1 c2)
then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
by auto
- with If.hyps `A \<subseteq> A'` obtain M1' M2'
+ with If.IH `A \<subseteq> A'` obtain M1' M2'
where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
@@ -34,7 +34,7 @@
theorem D_preservation:
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
-proof (induct arbitrary: A rule: small_step_induct)
+proof (induction arbitrary: A rule: small_step_induct)
case (While b c s)
then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
moreover
@@ -49,7 +49,7 @@
theorem D_sound:
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
-apply(induct arbitrary: A' rule:star_induct)
+apply(induction arbitrary: A' rule:star_induct)
apply (metis progress)
by (metis D_preservation)
--- a/src/HOL/IMP/Denotation.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy Tue Sep 20 05:48:23 2011 +0200
@@ -32,7 +32,7 @@
text{* Equivalence of denotational and big-step semantics: *}
lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-apply (induct rule: big_step_induct)
+apply (induction rule: big_step_induct)
apply auto
(* while *)
apply (unfold Gamma_def)
@@ -43,7 +43,7 @@
done
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
-apply (induct c arbitrary: s t)
+apply (induction c arbitrary: s t)
apply auto
apply blast
(* while *)
--- a/src/HOL/IMP/Fold.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Fold.thy Tue Sep 20 05:48:23 2011 +0200
@@ -81,7 +81,7 @@
lemma defs_restrict:
"defs c t |` (- lnames c) = t |` (- lnames c)"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
case (Semi c1 c2)
hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
by simp
@@ -114,7 +114,7 @@
lemma big_step_pres_approx:
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
case Skip thus ?case by simp
next
case Assign
@@ -122,8 +122,8 @@
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
next
case (Semi c1 s1 s2 c2 s3)
- have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
- hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
+ have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
+ hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
thus ?case by simp
next
case (IfTrue b s c1 s')
@@ -151,7 +151,7 @@
lemma big_step_pres_approx_restrict:
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
case Assign
thus ?case by (clarsimp simp: approx_def)
next
@@ -190,7 +190,7 @@
lemma approx_eq:
"approx t \<Turnstile> c \<sim> fold c t"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
case SKIP show ?case by simp
next
case Assign
@@ -292,7 +292,7 @@
lemma bdefs_restrict:
"bdefs c t |` (- lnames c) = t |` (- lnames c)"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
case (Semi c1 c2)
hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
by simp
@@ -327,7 +327,7 @@
lemma big_step_pres_approx_b:
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
case Skip thus ?case by simp
next
case Assign
@@ -335,8 +335,8 @@
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
next
case (Semi c1 s1 s2 c2 s3)
- have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
- hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
+ have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
+ hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
thus ?case by simp
next
case (IfTrue b s c1 s')
@@ -371,7 +371,7 @@
lemma bfold_equiv:
"approx t \<Turnstile> c \<sim> bfold c t"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
case SKIP show ?case by simp
next
case Assign
--- a/src/HOL/IMP/HoareT.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy Tue Sep 20 05:48:23 2011 +0200
@@ -88,7 +88,7 @@
proof
fix s
show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
- proof(induct "f s" arbitrary: s rule: less_induct)
+ proof(induction "f s" arbitrary: s rule: less_induct)
case (less n)
thus ?case by (metis While(2) WhileFalse WhileTrue)
qed
@@ -137,7 +137,7 @@
text{* The relation is in fact a function: *}
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
-proof(induct arbitrary: n' rule:Its.induct)
+proof(induction arbitrary: n' rule:Its.induct)
(* new release:
case Its_0 thus ?case by(metis Its.cases)
next
@@ -160,7 +160,7 @@
text{* For all terminating loops, @{const Its} yields a result: *}
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
-proof(induct "WHILE b DO c" s t rule: big_step_induct)
+proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by (metis Its_0)
next
case WhileTrue thus ?case by (metis Its_Suc)
@@ -179,7 +179,7 @@
by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
-proof (induct c arbitrary: Q)
+proof (induction c arbitrary: Q)
case SKIP show ?case by simp (blast intro:hoaret.Skip)
next
case Assign show ?case by simp (blast intro:hoaret.Assign)
--- a/src/HOL/IMP/Hoare_Examples.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Tue Sep 20 05:48:23 2011 +0200
@@ -25,7 +25,7 @@
lemma while_sum:
"(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
-apply(induct "w n" s t rule: big_step_induct)
+apply(induction "w n" s t rule: big_step_induct)
apply(auto simp add: setsum_head_plus_1)
done
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Tue Sep 20 05:48:23 2011 +0200
@@ -9,11 +9,11 @@
"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}"
-proof(induct rule: hoare.induct)
+proof(induction rule: hoare.induct)
case (While P b c)
{ fix s t
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<longrightarrow> P t \<and> \<not> bval b t"
- proof(induct "WHILE b DO c" s t rule: big_step_induct)
+ proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by blast
next
case WhileTrue thus ?case
@@ -59,7 +59,7 @@
subsection "Completeness"
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
+proof(induction c arbitrary: Q)
case Semi thus ?case by(auto intro: Semi)
next
case (If b c1 c2)
--- a/src/HOL/IMP/Live.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Live.thy Tue Sep 20 05:48:23 2011 +0200
@@ -44,17 +44,17 @@
theorem L_sound:
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct arbitrary: X t rule: big_step_induct)
+proof (induction arbitrary: X t rule: big_step_induct)
case Skip then show ?case by auto
next
case Assign then show ?case
by (auto simp: ball_Un)
next
case (Semi c1 s1 s2 c2 s3 X t1)
- from Semi(2,5) obtain t2 where
+ from Semi.IH(1) Semi.prems obtain t2 where
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
by simp blast
- from Semi(4)[OF s2t2] obtain t3 where
+ from Semi.IH(2)[OF s2t2] obtain t3 where
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using t12 t23 s3t3 by auto
@@ -83,9 +83,9 @@
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
have "s1 = t1 on L c (L ?w X)" using L_While_subset WhileTrue.prems
by (blast)
- from WhileTrue(3)[OF this] obtain t2 where
+ from WhileTrue.IH(1)[OF this] obtain t2 where
"(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
- from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
+ from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
by auto
with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
qed
@@ -108,17 +108,17 @@
theorem bury_sound:
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
\<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct arbitrary: X t rule: big_step_induct)
+proof (induction arbitrary: X t rule: big_step_induct)
case Skip then show ?case by auto
next
case Assign then show ?case
by (auto simp: ball_Un)
next
case (Semi c1 s1 s2 c2 s3 X t1)
- from Semi(2,5) obtain t2 where
+ from Semi.IH(1) Semi.prems obtain t2 where
t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
by simp blast
- from Semi(4)[OF s2t2] obtain t3 where
+ from Semi.IH(2)[OF s2t2] obtain t3 where
t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using t12 t23 s3t3 by auto
@@ -147,9 +147,9 @@
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
have "s1 = t1 on L c (L ?w X)"
using L_While_subset WhileTrue.prems by blast
- from WhileTrue(3)[OF this] obtain t2 where
+ from WhileTrue.IH(1)[OF this] obtain t2 where
"(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
- from WhileTrue(5)[OF this(2)] obtain t3
+ from WhileTrue.IH(2)[OF this(2)] obtain t3
where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
by auto
with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
@@ -184,7 +184,7 @@
theorem bury_sound2:
"(bury c X,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
+proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
case Skip then show ?case by auto
next
case Assign then show ?case
@@ -193,9 +193,10 @@
case (Semi bc1 s1 s2 bc2 s3 c X t1)
then obtain c1 c2 where c: "c = c1;c2"
and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
- from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
+ note IH = Semi.hyps(2,4)
+ from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
- from Semi(4)[OF bc2 s2t2] obtain t3 where
+ from IH(2)[OF bc2 s2t2] obtain t3 where
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using c t12 t23 s3t3 by auto
@@ -205,7 +206,8 @@
and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
- from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
+ note IH = IfTrue.hyps(3)
+ from IH[OF bc1 `s = t on L c1 X`] obtain t' where
"(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
thus ?case using c `bval b t` by auto
next
@@ -214,7 +216,8 @@
and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
- from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
+ note IH = IfFalse.hyps(3)
+ from IH[OF bc2 `s = t on L c2 X`] obtain t' where
"(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
thus ?case using c `~bval b t` by auto
next
@@ -228,11 +231,12 @@
let ?w = "WHILE b DO c'"
from `bval b s1` WhileTrue.prems c have "bval b t1"
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+ note IH = WhileTrue.hyps(3,5)
have "s1 = t1 on L c' (L ?w X)"
using L_While_subset WhileTrue.prems c by blast
- with WhileTrue(3)[OF bc', of t1] obtain t2 where
+ with IH(1)[OF bc', of t1] obtain t2 where
"(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
- from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
+ from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
by auto
with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
--- a/src/HOL/IMP/Poly_Types.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy Tue Sep 20 05:48:23 2011 +0200
@@ -45,12 +45,12 @@
subsection{* Typing is Preserved by Substitution *}
lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
-apply(induct rule: atyping.induct)
+apply(induction rule: atyping.induct)
apply(auto intro: atyping.intros)
done
lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
-apply(induct rule: btyping.induct)
+apply(induction rule: btyping.induct)
apply(auto intro: btyping.intros)
apply(drule subst_atyping[where S=S])
apply(drule subst_atyping[where S=S])
@@ -58,7 +58,7 @@
done
lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
-apply(induct rule: ctyping.induct)
+apply(induction rule: ctyping.induct)
apply(auto intro: ctyping.intros)
apply(drule subst_atyping[where S=S])
apply(simp add: o_def ctyping.intros)
--- a/src/HOL/IMP/Sec_Typing.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy Tue Sep 20 05:48:23 2011 +0200
@@ -30,7 +30,7 @@
text{* An important property: anti-monotonicity. *}
lemma anti_mono: "\<lbrakk> l \<turnstile> c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
-apply(induct arbitrary: l' rule: sec_type.induct)
+apply(induction arbitrary: l' rule: sec_type.induct)
apply (metis sec_type.intros(1))
apply (metis le_trans sec_type.intros(2))
apply (metis sec_type.intros(3))
@@ -39,7 +39,7 @@
done
lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t; l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
-proof(induct rule: big_step_induct)
+proof(induction rule: big_step_induct)
case Skip thus ?case by simp
next
case Assign thus ?case by auto
@@ -49,12 +49,12 @@
case (IfTrue b s c1)
hence "max (sec_bexp b) l \<turnstile> c1" by auto
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
- thus ?case using IfTrue.hyps by metis
+ thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
hence "max (sec_bexp b) l \<turnstile> c2" by auto
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
- thus ?case using IfFalse.hyps by metis
+ thus ?case using IfFalse.IH by metis
next
case WhileFalse thus ?case by auto
next
@@ -68,7 +68,7 @@
theorem noninterference:
"\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t'; 0 \<turnstile> c; s = t (\<le> l) \<rbrakk>
\<Longrightarrow> s' = t' (\<le> l)"
-proof(induct arbitrary: t t' rule: big_step_induct)
+proof(induction arbitrary: t t' rule: big_step_induct)
case Skip thus ?case by auto
next
case (Assign x a s)
@@ -94,7 +94,7 @@
assume "sec_bexp b \<le> l"
hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
- with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1` anti_mono
+ with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1` anti_mono
show ?thesis by auto
next
assume "\<not> sec_bexp b \<le> l"
@@ -115,7 +115,7 @@
assume "sec_bexp b \<le> l"
hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
- with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
+ with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
show ?thesis by auto
next
assume "\<not> sec_bexp b \<le> l"
@@ -157,14 +157,14 @@
using `bval b s1` by(simp add: bval_eq_if_eq_le)
then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
using `(?w,t1) \<Rightarrow> t3` by auto
- from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
- WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
+ from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
+ WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
`s1 = t1 (\<le> l)`]]
show ?thesis by simp
next
assume "\<not> sec_bexp b \<le> l"
have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
- from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
have "s1 = s3 (\<le> l)" by auto
moreover
from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
@@ -196,7 +196,7 @@
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type.induct)
+apply(induction rule: sec_type.induct)
apply (metis Skip')
apply (metis Assign')
apply (metis Semi')
@@ -205,7 +205,7 @@
lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
apply (metis Skip)
apply (metis Assign)
apply (metis Semi)
@@ -230,7 +230,7 @@
lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type2.induct)
+apply(induction rule: sec_type2.induct)
apply (metis Skip')
apply (metis Assign' eq_imp_le)
apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
@@ -238,7 +238,7 @@
by (metis While')
lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
apply (metis Skip2 le_refl)
apply (metis Assign2)
apply (metis Semi2 min_max.inf_greatest)
--- a/src/HOL/IMP/Sec_TypingT.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy Tue Sep 20 05:48:23 2011 +0200
@@ -23,7 +23,7 @@
lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
-apply(induct arbitrary: l' rule: sec_type.induct)
+apply(induction arbitrary: l' rule: sec_type.induct)
apply (metis sec_type.intros(1))
apply (metis le_trans sec_type.intros(2))
apply (metis sec_type.intros(3))
@@ -32,7 +32,7 @@
lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
-proof(induct rule: big_step_induct)
+proof(induction rule: big_step_induct)
case Skip thus ?case by simp
next
case Assign thus ?case by auto
@@ -42,12 +42,12 @@
case (IfTrue b s c1)
hence "max (sec_bexp b) l \<turnstile> c1" by auto
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
- thus ?case using IfTrue.hyps by metis
+ thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
hence "max (sec_bexp b) l \<turnstile> c2" by auto
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
- thus ?case using IfFalse.hyps by metis
+ thus ?case using IfFalse.IH by metis
next
case WhileFalse thus ?case by auto
next
@@ -57,7 +57,7 @@
qed
lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
-apply(induct arbitrary: s rule: sec_type.induct)
+apply(induction arbitrary: s rule: sec_type.induct)
apply (metis big_step.Skip)
apply (metis big_step.Assign)
apply (metis big_step.Semi)
@@ -67,7 +67,7 @@
theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> s = t (\<le> l)
\<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
-proof(induct arbitrary: t rule: big_step_induct)
+proof(induction arbitrary: t rule: big_step_induct)
case Skip thus ?case by auto
next
case (Assign x a s)
@@ -152,9 +152,9 @@
let ?w = "WHILE b DO c"
from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
- from WhileTrue(3)[OF this WhileTrue.prems(2)]
+ from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
- from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
+ from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
from `bval b s` have "bval b t"
using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
@@ -185,7 +185,7 @@
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type.induct)
+apply(induction rule: sec_type.induct)
apply (metis Skip')
apply (metis Assign')
apply (metis Semi')
@@ -194,7 +194,7 @@
lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
apply (metis Skip)
apply (metis Assign)
apply (metis Semi)
--- a/src/HOL/IMP/Sem_Equiv.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Tue Sep 20 05:48:23 2011 +0200
@@ -83,10 +83,9 @@
P s \<Longrightarrow>
d = WHILE b DO c \<Longrightarrow>
(WHILE b' DO c', s) \<Rightarrow> s'"
-proof (induct rule: big_step_induct)
+proof (induction rule: big_step_induct)
case (WhileTrue b s1 c s2 s3)
- note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
-
+ note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
from WhileTrue.prems
have "P \<Turnstile> b <\<sim>> b'" by simp
with `bval b s1` `P s1`
--- a/src/HOL/IMP/Small_Step.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy Tue Sep 20 05:48:23 2011 +0200
@@ -71,7 +71,7 @@
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
@@ -79,7 +79,7 @@
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
@@ -98,7 +98,7 @@
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
@@ -140,7 +140,7 @@
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
@@ -161,13 +161,13 @@
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
@@ -188,7 +188,7 @@
lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
apply(simp add: final_def)
-apply(induct c)
+apply(induction c)
apply blast+
done
--- a/src/HOL/IMP/Star.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Star.thy Tue Sep 20 05:48:23 2011 +0200
@@ -9,7 +9,7 @@
lemma star_trans:
"star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-proof(induct rule: star.induct)
+proof(induction rule: star.induct)
case refl thus ?case .
next
case step thus ?case by (metis star.step)
--- a/src/HOL/IMP/Types.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Types.thy Tue Sep 20 05:48:23 2011 +0200
@@ -119,28 +119,28 @@
lemma apreservation:
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
-apply(induct arbitrary: v rule: atyping.induct)
+apply(induction arbitrary: v rule: atyping.induct)
apply (fastforce simp: styping_def)+
done
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
-proof(induct rule: atyping.induct)
+proof(induction rule: atyping.induct)
case (Plus_ty \<Gamma> a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
show ?case
proof (cases v1)
case Iv
- with Plus_ty(1,3,5) v show ?thesis
+ with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(4) dest!: apreservation)
next
case Rv
- with Plus_ty(1,3,5) v show ?thesis
+ with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(5) dest!: apreservation)
qed
qed (auto intro: taval.intros)
lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
-proof(induct rule: btyping.induct)
+proof(induction rule: btyping.induct)
case (Less_ty \<Gamma> a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
by (metis aprogress)
@@ -158,7 +158,7 @@
theorem progress:
"\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
-proof(induct rule: ctyping.induct)
+proof(induction rule: ctyping.induct)
case Skip_ty thus ?case by simp
next
case Assign_ty
@@ -182,7 +182,7 @@
theorem styping_preservation:
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
-proof(induct rule: small_step_induct)
+proof(induction rule: small_step_induct)
case Assign thus ?case
by (auto simp: styping_def) (metis Assign(1,3) apreservation)
qed auto
@@ -197,7 +197,7 @@
theorem type_sound:
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
-apply(induct rule:star_induct)
+apply(induction rule:star_induct)
apply (metis progress)
by (metis styping_preservation ctyping_preservation)
--- a/src/HOL/IMP/VC.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/VC.thy Tue Sep 20 05:48:23 2011 +0200
@@ -49,14 +49,14 @@
subsection "Soundness"
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
-proof(induct c arbitrary: Q)
+proof(induction c arbitrary: Q)
case (Awhile b I c)
show ?case
proof(simp, rule While')
from `\<forall>s. vc (Awhile b I c) Q s`
have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
- have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
+ have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
by(rule strengthen_pre)
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
@@ -72,20 +72,20 @@
lemma pre_mono:
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
-proof (induct c arbitrary: P P' s)
+proof (induction c arbitrary: P P' s)
case Asemi thus ?case by simp metis
qed simp_all
lemma vc_mono:
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
-proof(induct c arbitrary: P P')
+proof(induction c arbitrary: P P')
case Asemi thus ?case by simp (metis pre_mono)
qed simp_all
lemma vc_complete:
"\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
(is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
-proof (induct rule: hoare.induct)
+proof (induction rule: hoare.induct)
case Skip
show ?case (is "\<exists>ac. ?C ac")
proof show "?C Askip" by simp qed
@@ -95,8 +95,8 @@
proof show "?C(Aassign x a)" by simp qed
next
case (Semi P c1 Q c2 R)
- from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
- from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+ from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+ from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
show ?case (is "\<exists>ac. ?C ac")
proof
show "?C(Asemi ac1 ac2)"
@@ -104,9 +104,9 @@
qed
next
case (If P b c1 Q c2)
- from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
+ from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
by blast
- from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
+ from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
by blast
show ?case (is "\<exists>ac. ?C ac")
proof
@@ -114,7 +114,7 @@
qed
next
case (While P b c)
- from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
+ from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
show ?case (is "\<exists>ac. ?C ac")
proof show "?C(Awhile b P ac)" using ih by simp qed
next
--- a/src/HOL/IMP/Vars.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Vars.thy Tue Sep 20 05:48:23 2011 +0200
@@ -59,13 +59,13 @@
lemma aval_eq_if_eq_on_vars[simp]:
"s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
-apply(induct a)
+apply(induction a)
apply simp_all
done
lemma bval_eq_if_eq_on_vars:
"s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
-proof(induct b)
+proof(induction b)
case (Less a1 a2)
hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all
thus ?case by simp