--- a/NEWS Tue Sep 20 11:02:41 2011 -0700
+++ b/NEWS Wed Sep 21 06:41:34 2011 -0700
@@ -76,6 +76,11 @@
*** HOL ***
+* New proof method "induction" that gives induction hypotheses the name IH,
+thus distinguishing them from further hypotheses that come from rule
+induction. The latter are still called "hyps". Method "induction" is a thin
+wrapper around "induct" and follows the same syntax.
+
* Class bot and top require underlying partial order rather than
preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
@@ -91,8 +96,7 @@
Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
-UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
-discarded.
+UNION_eq_Union_image, Union_def, UN_eq have been discarded.
More consistent and comprehensive names:
--- a/doc-src/IsarRef/Thy/Proof.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/doc-src/IsarRef/Thy/Proof.thy Wed Sep 21 06:41:34 2011 -0700
@@ -1259,10 +1259,12 @@
\begin{matharray}{rcl}
@{method_def cases} & : & @{text method} \\
@{method_def induct} & : & @{text method} \\
+ @{method_def induction} & : & @{text method} \\
@{method_def coinduct} & : & @{text method} \\
\end{matharray}
- The @{method cases}, @{method induct}, and @{method coinduct}
+ The @{method cases}, @{method induct}, @{method induction},
+ and @{method coinduct}
methods provide a uniform interface to common proof techniques over
datatypes, inductive predicates (or sets), recursive functions etc.
The corresponding rules may be specified and instantiated in a
@@ -1277,11 +1279,15 @@
and parameters separately). This avoids cumbersome encoding of
``strengthened'' inductive statements within the object-logic.
+ Method @{method induction} differs from @{method induct} only in
+ the names of the facts in the local context invoked by the @{command "case"}
+ command.
+
@{rail "
@@{method cases} ('(' 'no_simp' ')')? \\
(@{syntax insts} * @'and') rule?
;
- @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
+ (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
;
@@{method coinduct} @{syntax insts} taking rule?
;
@@ -1325,8 +1331,9 @@
"(no_simp)"} option can be used to disable pre-simplification of
cases (see the description of @{method induct} below for details).
- \item @{method induct}~@{text "insts R"} is analogous to the
- @{method cases} method, but refers to induction rules, which are
+ \item @{method induct}~@{text "insts R"} and
+ @{method induction}~@{text "insts R"} are analogous to the
+ @{method cases} method, but refer to induction rules, which are
determined as follows:
\medskip
@@ -1437,13 +1444,20 @@
and definitions effectively participate in the inductive rephrasing
of the original statement.
- In induction proofs, local assumptions introduced by cases are split
+ In @{method induct} proofs, local assumptions introduced by cases are split
into two different kinds: @{text hyps} stemming from the rule and
@{text prems} from the goal statement. This is reflected in the
extracted cases accordingly, so invoking ``@{command "case"}~@{text
c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
as well as fact @{text c} to hold the all-inclusive list.
+ In @{method induction} proofs, local assumptions introduced by cases are
+ split into three different kinds: @{text IH}, the induction hypotheses,
+ @{text hyps}, the remaining hypotheses stemming from the rule, and
+ @{text prems}, the assumptions from the goal statement. The names are
+ @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
+
+
\medskip Facts presented to either method are consumed according to
the number of ``major premises'' of the rule involved, which is
usually 0 for plain cases and induction rules of datatypes etc.\ and
--- a/doc-src/IsarRef/Thy/document/Proof.tex Tue Sep 20 11:02:41 2011 -0700
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Wed Sep 21 06:41:34 2011 -0700
@@ -1700,10 +1700,12 @@
\begin{matharray}{rcl}
\indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
\indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
+ \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
\indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
\end{matharray}
- The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
+ The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
+ and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
methods provide a uniform interface to common proof techniques over
datatypes, inductive predicates (or sets), recursive functions etc.
The corresponding rules may be specified and instantiated in a
@@ -1718,6 +1720,10 @@
and parameters separately). This avoids cumbersome encoding of
``strengthened'' inductive statements within the object-logic.
+ Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
+ the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
+ command.
+
\begin{railoutput}
\rail@begin{6}{}
\rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
@@ -1742,7 +1748,11 @@
\rail@endbar
\rail@end
\rail@begin{6}{}
+\rail@bar
\rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
+\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
@@ -1872,8 +1882,9 @@
last premise (it is usually the same for all cases). The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of
cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
- \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
- \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
+ \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
+ \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
+ \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
determined as follows:
\medskip
@@ -1979,12 +1990,19 @@
and definitions effectively participate in the inductive rephrasing
of the original statement.
- In induction proofs, local assumptions introduced by cases are split
+ In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
into two different kinds: \isa{hyps} stemming from the rule and
\isa{prems} from the goal statement. This is reflected in the
extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},
as well as fact \isa{c} to hold the all-inclusive list.
+ In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
+ split into three different kinds: \isa{IH}, the induction hypotheses,
+ \isa{hyps}, the remaining hypotheses stemming from the rule, and
+ \isa{prems}, the assumptions from the goal statement. The names are
+ \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
+
+
\medskip Facts presented to either method are consumed according to
the number of ``major premises'' of the rule involved, which is
usually 0 for plain cases and induction rules of datatypes etc.\ and
--- a/src/HOL/Complete_Lattices.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Complete_Lattices.thy Wed Sep 21 06:41:34 2011 -0700
@@ -1012,6 +1012,9 @@
lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
by blast
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+ by blast
+
subsection {* Distributive laws *}
@@ -1131,11 +1134,6 @@
"\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
by auto
-text {* Legacy names *}
-
-lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
- by blast
-
text {* Finally *}
no_notation
--- a/src/HOL/HOL.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/HOL.thy Wed Sep 21 06:41:34 2011 -0700
@@ -26,6 +26,7 @@
("Tools/simpdata.ML")
"~~/src/Tools/atomize_elim.ML"
"~~/src/Tools/induct.ML"
+ ("~~/src/Tools/induction.ML")
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
("Tools/cnf_funcs.ML")
@@ -1490,8 +1491,10 @@
)
*}
+use "~~/src/Tools/induction.ML"
+
setup {*
- Induct.setup #>
+ Induct.setup #> Induction.setup #>
Context.theory_map (Induct.map_simpset (fn ss => ss
setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
map (Simplifier.rewrite_rule (map Thm.symmetric
--- a/src/HOL/IMP/AExp.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AExp.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/ASM.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt0.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt0_fun.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt1.thy Wed Sep 21 06:41:34 2011 -0700
@@ -30,11 +30,11 @@
locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
-fixes inv_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and inv_less' :: "'a \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> 'a * 'a"
-assumes inv_plus': "inv_plus' a1 a2 a = (a1',a2') \<Longrightarrow>
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and inv_less': "inv_less' a1 a2 (n1<n2) = (a1',a2') \<Longrightarrow>
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
datatype 'a up = bot | Up 'a
@@ -117,12 +117,12 @@
let a' = lookup S x \<sqinter> a in
if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
"afilter (Plus e1 e2) a S =
- (let (a1,a2) = inv_plus' (aval' e1 S) (aval' e2 S) a
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
in afilter e1 a1 (afilter e2 a2 S))"
text{* The test for @{const Bot} in the @{const V}-case is important: @{const
Bot} indicates that a variable has no possible values, i.e.\ that the current
-program point is unreachable. But then the abstract state should collaps to
+program point is unreachable. But then the abstract state should collapse to
@{const bot}. Put differently, we maintain the invariant that in an abstract
state all variables are mapped to non-@{const Bot} values. Otherwise the
(pointwise) join of two abstract states, one of which contains @{const Bot}
@@ -137,11 +137,11 @@
(if res then bfilter b1 True (bfilter b2 True S)
else bfilter b1 False S \<squnion> bfilter b2 False S)" |
"bfilter (Less e1 e2) res S =
- (let (res1,res2) = inv_less' (aval' e1 S) (aval' e2 S) res
+ (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
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)
@@ -153,12 +153,12 @@
(metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
next
case (Plus e1 e2) thus ?case
- using inv_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+ using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
by (auto split: prod.split)
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
@@ -167,7 +167,7 @@
next
case (Less e1 e2) thus ?case
by (auto split: prod.split)
- (metis afilter_sound inv_less' aval'_sound Less)
+ (metis afilter_sound filter_less' aval'_sound Less)
qed
fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
@@ -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/AbsInt1_ivl.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt1_ivl.thy Wed Sep 21 06:41:34 2011 -0700
@@ -145,12 +145,13 @@
by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
-definition "inv_plus_ivl i1 i2 i = ((*if is_empty i then empty else*)
+definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
-fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
-"inv_less_ivl (I l1 h1) (I l2 h2) res =
- (if res
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
+ ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
+ if res
then (I l1 (min_option True h1 (h2 - Some 1)),
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
@@ -178,10 +179,10 @@
qed
interpretation
- Val_abs1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl
+ Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
proof
case goal1 thus ?case
- by(auto simp add: inv_plus_ivl_def)
+ by(auto simp add: filter_plus_ivl_def)
(metis rep_minus_ivl add_diff_cancel add_commute)+
next
case goal2 thus ?case
@@ -190,7 +191,7 @@
qed
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3)"
+ Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and AI_ivl is AI
@@ -250,4 +251,10 @@
DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
value [code] "list_up(AI_ivl test4_ivl Top)"
+text{* Nontermination not detected: *}
+definition "test5_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "list_up(AI_ivl test5_ivl Top)"
+
end
--- a/src/HOL/IMP/AbsInt2.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt2.thy Wed Sep 21 06:41:34 2011 -0700
@@ -4,11 +4,41 @@
imports AbsInt1_ivl
begin
+context preord
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
+
+lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
+by(simp add: mono_def)
+
+declare le_trans[trans]
+
+end
+
+
subsection "Widening and Narrowing"
-text{* The assumptions about winden and narrow are merely sanity checks. They
-are only needed in case we want to prove termination of the fixedpoint
-iteration, which we do not --- we limit the number of iterations as before. *}
+text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
+rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
+a trivial widening step. We generalise this idea and complement it with
+narrowing, a process to regain precision.
+
+Class @{text WN} makes some assumptions about the widening and narrowing
+operators. The assumptions serve two purposes. Together with a further
+assumption that certain chains become stationary, they permit to prove
+termination of the fixed point iteration, which we do not --- we limit the
+number of iterations as before. The second purpose of the narrowing
+assumptions is to prove that the narrowing iteration keeps on producing
+post-fixed points and that it goes down. However, this requires the function
+being iterated to be monotone. Unfortunately, abstract interpretation with
+widening is not monotone. Hence the (recursive) abstract interpretation of a
+loop body that again contains a loop may result in a non-monotone
+function. Therefore our narrowing interation needs to check at every step
+that a post-fixed point is maintained, and we cannot prove that the precision
+increases. *}
class WN = SL_top +
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
@@ -24,7 +54,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 +65,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
@@ -50,6 +80,44 @@
using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
by(auto simp add: iter'_def Let_def)
+text{* This is how narrowing works on monotone functions: you just iterate. *}
+
+abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
+
+text{* Narrowing always yields a post-fixed point: *}
+
+lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
+defines "x n == iter_down_mono f n x0"
+shows "f(x n) \<sqsubseteq> x n"
+proof (induction n)
+ case 0 show ?case by (simp add: x_def assms(2))
+next
+ case (Suc n)
+ have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
+ also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
+ also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
+ also have "\<dots> = x(Suc n)" by(simp add: x_def)
+ finally show ?case .
+qed
+
+text{* Narrowing can only increase precision: *}
+
+lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
+defines "x n == iter_down_mono f n x0"
+shows "x n \<sqsubseteq> x0"
+proof (induction n)
+ case 0 show ?case by(simp add: x_def)
+next
+ case (Suc n)
+ have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
+ also have "\<dots> \<sqsubseteq> x n" unfolding x_def
+ by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
+ also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
+ finally show ?case .
+qed
+
+
end
@@ -57,8 +125,7 @@
begin
definition "widen_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 then ivl2 else
- if is_empty ivl2 then ivl1 else*)
+ ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
@@ -75,7 +142,7 @@
end
-instantiation astate :: (WN)WN
+instantiation astate :: (WN) WN
begin
definition "widen_astate F1 F2 =
@@ -98,7 +165,7 @@
end
-instantiation up :: (WN)WN
+instantiation up :: (WN) WN
begin
fun widen_up where
@@ -126,7 +193,7 @@
end
interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)"
+ Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
defines afilter_ivl' is afilter
and bfilter_ivl' is bfilter
and AI_ivl' is AI
@@ -135,5 +202,6 @@
value [code] "list_up(AI_ivl' test3_ivl Top)"
value [code] "list_up(AI_ivl' test4_ivl Top)"
+value [code] "list_up(AI_ivl' test5_ivl Top)"
end
--- a/src/HOL/IMP/BExp.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/BExp.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Big_Step.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Comp_Rev.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Compiler.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Denotation.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Fold.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/HoareT.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Hoare_Examples.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Live.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Poly_Types.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sec_Typing.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sec_TypingT.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sem_Equiv.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Small_Step.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Star.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Types.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/VC.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Vars.thy Wed Sep 21 06:41:34 2011 -0700
@@ -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
--- a/src/HOL/IsaMakefile Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IsaMakefile Wed Sep 21 06:41:34 2011 -0700
@@ -145,6 +145,7 @@
$(SRC)/Tools/eqsubst.ML \
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
+ $(SRC)/Tools/induction.ML \
$(SRC)/Tools/intuitionistic.ML \
$(SRC)/Tools/misc_legacy.ML \
$(SRC)/Tools/nbe.ML \
@@ -514,7 +515,7 @@
$(OUT)/HOL-IMP: $(OUT)/HOL IMP/AbsInt0_fun.thy IMP/Astate.thy \
IMP/AbsInt0.thy IMP/AbsInt0_const.thy IMP/AbsInt1.thy IMP/AbsInt1_ivl.thy \
- IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
+ IMP/AbsInt2.thy IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
--- a/src/HOL/Library/Executable_Set.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Library/Executable_Set.thy Wed Sep 21 06:41:34 2011 -0700
@@ -101,12 +101,12 @@
lemma insert_Set [code]:
"insert x (Set xs) = Set (List.insert x xs)"
"insert x (Coset xs) = Coset (removeAll x xs)"
- by (simp_all add: set_insert)
+ by simp_all
lemma remove_Set [code]:
"remove x (Set xs) = Set (removeAll x xs)"
"remove x (Coset xs) = Coset (List.insert x xs)"
- by (auto simp add: set_insert remove_def)
+ by (auto simp add: remove_def)
lemma image_Set [code]:
"image f (Set xs) = Set (remdups (map f xs))"
@@ -254,12 +254,12 @@
lemma Inf_inf [code]:
"Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
"Inf (Coset []) = (bot :: 'a::complete_lattice)"
- by (simp_all add: Inf_UNIV Inf_set_foldr)
+ by (simp_all add: Inf_set_foldr)
lemma Sup_sup [code]:
"Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
"Sup (Coset []) = (top :: 'a::complete_lattice)"
- by (simp_all add: Sup_UNIV Sup_set_foldr)
+ by (simp_all add: Sup_set_foldr)
lemma Inter_inter [code]:
"Inter (Set xs) = foldr inter xs (Coset [])"
@@ -279,50 +279,40 @@
text {* Initially contributed by Tjark Weber. *}
-lemma bounded_Collect_code [code_unfold]:
- "{x\<in>S. P x} = project P S"
- by (auto simp add: project_def)
-
-lemma Id_on_code [code]:
- "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
- by (auto simp add: Id_on_def)
-
-lemma Domain_fst [code]:
+lemma [code]:
"Domain r = fst ` r"
- by (auto simp add: image_def Bex_def)
+ by (fact Domain_fst)
-lemma Range_snd [code]:
+lemma [code]:
"Range r = snd ` r"
- by (auto simp add: image_def Bex_def)
+ by (fact Range_snd)
-lemma irrefl_code [code]:
- "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
- by (auto simp add: irrefl_def)
+lemma [code]:
+ "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+ by (fact trans_join)
+
+lemma [code]:
+ "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+ by (fact irrefl_distinct)
-lemma trans_def [code]:
- "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
- by (auto simp add: trans_def)
+lemma [code]:
+ "acyclic r \<longleftrightarrow> irrefl (r^+)"
+ by (fact acyclic_irrefl)
-definition "exTimes A B = Sigma A (%_. B)"
-
-lemma [code_unfold]:
- "Sigma A (%_. B) = exTimes A B"
- by (simp add: exTimes_def)
+lemma [code]:
+ "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+ by (unfold Set_def) (fact product_code)
-lemma exTimes_code [code]:
- "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
- by (auto simp add: exTimes_def)
-
-lemma rel_comp_code [code]:
- "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
+lemma [code]:
+ "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
+ by (unfold Set_def) (fact Id_on_set)
-lemma acyclic_code [code]:
- "acyclic r = irrefl (r^+)"
- by (simp add: acyclic_def irrefl_def)
+lemma [code]:
+ "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+ by (unfold Set_def) (fact set_rel_comp)
-lemma wf_code [code]:
+lemma [code]:
"wf (Set xs) = acyclic (Set xs)"
- by (simp add: wf_iff_acyclic_if_finite)
+ by (unfold Set_def) (fact wf_set)
end
--- a/src/HOL/Library/More_Set.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Library/More_Set.thy Wed Sep 21 06:41:34 2011 -0700
@@ -31,7 +31,20 @@
qed
definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "project P A = {a\<in>A. P a}"
+ "project P A = {a \<in> A. P a}"
+
+lemma bounded_Collect_code [code_unfold_post]:
+ "{x \<in> A. P x} = project P A"
+ by (simp add: project_def)
+
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+ "product A B = Sigma A (\<lambda>_. B)"
+
+hide_const (open) product
+
+lemma [code_unfold_post]:
+ "Sigma A (\<lambda>_. B) = More_Set.product A B"
+ by (simp add: product_def)
subsection {* Basic set operations *}
@@ -75,7 +88,7 @@
"set xs \<union> A = foldr Set.insert xs A"
proof -
have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
- by (auto intro: ext)
+ by auto
then show ?thesis by (simp add: union_set foldr_fold)
qed
@@ -92,7 +105,7 @@
"A - set xs = foldr remove xs A"
proof -
have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
- by (auto simp add: remove_def intro: ext)
+ by (auto simp add: remove_def)
then show ?thesis by (simp add: minus_set foldr_fold)
qed
@@ -120,10 +133,22 @@
by (auto simp add: project_def)
-subsection {* Various lemmas *}
+subsection {* Theorems on relations *}
+
+lemma product_code:
+ "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+ by (auto simp add: product_def)
-lemma not_set_compl:
- "Not \<circ> set xs = - set xs"
- by (simp add: fun_Compl_def comp_def fun_eq_iff)
+lemma Id_on_set:
+ "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+ by (auto simp add: Id_on_def)
+
+lemma set_rel_comp:
+ "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+ by (auto simp add: Bex_def)
+
+lemma wf_set:
+ "wf (set xs) = acyclic (set xs)"
+ by (simp add: wf_iff_acyclic_if_finite)
end
--- a/src/HOL/Relation.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Relation.thy Wed Sep 21 06:41:34 2011 -0700
@@ -275,6 +275,10 @@
subsection {* Transitivity *}
+lemma trans_join:
+ "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+ by (auto simp add: trans_def)
+
lemma transI:
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
by (unfold trans_def) iprover
@@ -296,6 +300,10 @@
subsection {* Irreflexivity *}
+lemma irrefl_distinct:
+ "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+ by (auto simp add: irrefl_def)
+
lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
by(simp add:irrefl_def)
@@ -386,6 +394,10 @@
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
by (iprover dest!: iffD1 [OF Domain_iff])
+lemma Domain_fst:
+ "Domain r = fst ` r"
+ by (auto simp add: image_def Bex_def)
+
lemma Domain_empty [simp]: "Domain {} = {}"
by blast
@@ -440,6 +452,10 @@
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
+lemma Range_snd:
+ "Range r = snd ` r"
+ by (auto simp add: image_def Bex_def)
+
lemma Range_empty [simp]: "Range {} = {}"
by blast
--- a/src/HOL/Wellfounded.thy Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Wellfounded.thy Wed Sep 21 06:41:34 2011 -0700
@@ -387,6 +387,10 @@
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r == acyclic {(x, y). r x y}"
+lemma acyclic_irrefl:
+ "acyclic r \<longleftrightarrow> irrefl (r^+)"
+ by (simp add: acyclic_def irrefl_def)
+
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
by (simp add: acyclic_def)
--- a/src/Tools/induct.ML Tue Sep 20 11:02:41 2011 -0700
+++ b/src/Tools/induct.ML Wed Sep 21 06:41:34 2011 -0700
@@ -74,11 +74,21 @@
val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
+ type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
+ val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
+ Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> cases_tactic
val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
thm list -> int -> cases_tactic
+ val gen_induct_setup: binding ->
+ (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> cases_tactic) ->
+ theory -> theory
val setup: theory -> theory
end;
@@ -721,7 +731,9 @@
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
-fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
+type case_data = (((string * string list) * string list) list * int)
+
+fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
let
val thy = Proof_Context.theory_of ctxt;
@@ -734,6 +746,7 @@
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
|> maps (prep_inst ctxt align_right (atomize_term thy))
|> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+ |> mod_cases thy
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
val ruleq =
@@ -791,7 +804,7 @@
THEN_ALL_NEW rulify_tac)
end;
-
+val induct_tac = gen_induct_tac (K I);
(** coinduct method **)
@@ -910,16 +923,18 @@
(cases_tac ctxt (not no_simp) insts opt_rule facts)))))
"case analysis on types or predicates/sets";
-val induct_setup =
- Method.setup @{binding induct}
+fun gen_induct_setup binding itac =
+ Method.setup binding
(Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
Seq.DETERM
- (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+ (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
"induction on types or predicates/sets";
+val induct_setup = gen_induct_setup @{binding induct} induct_tac;
+
val coinduct_setup =
Method.setup @{binding coinduct}
(Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/induction.ML Wed Sep 21 06:41:34 2011 -0700
@@ -0,0 +1,43 @@
+signature INDUCTION =
+sig
+ val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> cases_tactic
+ val setup: theory -> theory
+end
+
+structure Induction: INDUCTION =
+struct
+
+val ind_hypsN = "IH";
+
+fun preds_of t =
+ (case strip_comb t of
+ (p as Var _, _) => [p]
+ | (p as Free _, _) => [p]
+ | (_, ts) => flat(map preds_of ts))
+
+fun name_hyps thy (arg as ((cases,consumes),th)) =
+ if not(forall (null o #2 o #1) cases) then arg
+ else
+ let
+ val (prems, concl) = Logic.strip_horn (prop_of th);
+ val prems' = drop consumes prems;
+ val ps = preds_of concl;
+
+ fun hname_of t =
+ if exists_subterm (member (op =) ps) t
+ then ind_hypsN else Rule_Cases.case_hypsN
+
+ val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
+ val n = Int.min (length hnamess, length cases)
+ val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
+ (take n cases ~~ take n hnamess)
+ in ((cases',consumes),th) end
+
+val induction_tac = Induct.gen_induct_tac name_hyps
+
+val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+
+end
+
--- a/src/Tools/jEdit/etc/settings Tue Sep 20 11:02:41 2011 -0700
+++ b/src/Tools/jEdit/etc/settings Wed Sep 21 06:41:34 2011 -0700
@@ -4,8 +4,8 @@
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"