--- a/doc-src/TutorialI/Rules/rules.tex Thu Dec 10 22:28:55 2009 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Fri Dec 11 09:25:45 2009 +0000
@@ -1073,7 +1073,7 @@
\index{quantifiers!existential|)}
-\subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
+\subsection{Renaming a Bound Variable: {\tt\slshape rename_tac}}
\index{assumptions!renaming|(}\index{*rename_tac (method)|(}%
When you apply a rule such as \isa{allI}, the quantified variable
--- a/src/HOL/IMP/Denotation.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/IMP/Denotation.thy Fri Dec 11 09:25:45 2009 +0000
@@ -47,22 +47,20 @@
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
apply fast
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
-apply fast
+apply auto
done
(* Denotational Semantics implies Operational Semantics *)
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
apply (induct c arbitrary: s t)
-
-apply simp_all
-apply fast
-apply fast
+apply auto
+apply blast
(* while *)
apply (erule lfp_induct2 [OF _ Gamma_mono])
apply (unfold Gamma_def)
-apply fast
+apply auto
done
--- a/src/HOL/IMP/Natural.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/IMP/Natural.thy Fri Dec 11 09:25:45 2009 +0000
@@ -1,7 +1,7 @@
(* Title: HOL/IMP/Natural.thy
ID: $Id$
Author: Tobias Nipkow & Robert Sandner, TUM
- Isar Version: Gerwin Klein, 2001
+ Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
Copyright 1996 TUM
*)
@@ -55,43 +55,49 @@
meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
*}
-
text {*
The rules of @{text evalc} are syntax directed, i.e.~for each
syntactic category there is always only one rule applicable. That
- means we can use the rules in both directions. The proofs for this
- are all the same: one direction is trivial, the other one is shown
- by using the @{text evalc} rules backwards:
+ means we can use the rules in both directions. This property is called rule inversion.
*}
+inductive_cases skipE [elim!]: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
+inductive_cases semiE [elim!]: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
+inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
+inductive_cases ifE [elim!]: "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
+inductive_cases whileE [elim]: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+
+text {* The next proofs are all trivial by rule inversion.
+*}
+
lemma skip:
"\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
- by (rule, erule evalc.cases) auto
+ by auto
lemma assign:
"\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
- by (rule, erule evalc.cases) auto
+ by auto
lemma semi:
"\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
- by (rule, erule evalc.cases) auto
+ by auto
lemma ifTrue:
"b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
- by (rule, erule evalc.cases) auto
+ by auto
lemma ifFalse:
"\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
- by (rule, erule evalc.cases) auto
+ by auto
lemma whileFalse:
"\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
- by (rule, erule evalc.cases) auto
+ by auto
lemma whileTrue:
"b s \<Longrightarrow>
\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
(\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
- by (rule, erule evalc.cases) auto
+ by auto
text "Again, Isabelle may use these rules in automatic proofs:"
lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
@@ -136,8 +142,8 @@
{ fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
-- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
-- "then both statements do nothing:"
- hence "\<not>b s \<Longrightarrow> s = s'" by simp
- hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ hence "\<not>b s \<Longrightarrow> s = s'" by blast
+ hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
moreover
-- "on the other hand, if @{text b} is @{text True} in state @{text s},"
-- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
@@ -159,8 +165,8 @@
{ fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
-- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
-- "of the @{text \<IF>} is executed, and both statements do nothing:"
- hence "\<not>b s \<Longrightarrow> s = s'" by simp
- hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ hence "\<not>b s \<Longrightarrow> s = s'" by blast
+ hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
moreover
-- "on the other hand, if @{text b} is @{text True} in state @{text s},"
-- {* then this time only the @{text IfTrue} rule can have be used *}
@@ -181,10 +187,81 @@
show ?thesis by blast
qed
+text {*
+ Happily, such lengthy proofs are seldom necessary. Isabelle can prove many such facts automatically.
+*}
+
+lemma
+ "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
+by blast
+
+lemma triv_if:
+ "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c"
+by blast
+
+lemma commute_if:
+ "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2)
+ \<sim>
+ (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))"
+by blast
+
+lemma while_equiv:
+ "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u"
+by (induct rule: evalc.induct) (auto simp add: equiv_c_def)
+
+lemma equiv_while:
+ "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')"
+by (simp add: equiv_c_def) (metis equiv_c_def while_equiv)
+
+
+text {*
+ Program equivalence is an equivalence relation.
+*}
+
+lemma equiv_refl:
+ "c \<sim> c"
+by blast
+
+lemma equiv_sym:
+ "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1"
+by (auto simp add: equiv_c_def)
+
+lemma equiv_trans:
+ "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3"
+by (auto simp add: equiv_c_def)
+
+text {*
+ Program constructions preserve equivalence.
+*}
+
+lemma equiv_semi:
+ "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')"
+by (force simp add: equiv_c_def)
+
+lemma equiv_if:
+ "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')"
+by (force simp add: equiv_c_def)
+
+lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1"
+apply (induct rule: evalc.induct)
+apply auto
+done
+
+lemma equiv_while_True:
+ "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)"
+by (blast dest: while_never)
+
subsection "Execution is deterministic"
text {*
+This proof is automatic.
+*}
+theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t"
+by (induct arbitrary: u rule: evalc.induct) blast+
+
+
+text {*
The following proof presents all the details:
*}
theorem com_det:
@@ -193,10 +270,10 @@
using prems
proof (induct arbitrary: u set: evalc)
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by simp
+ thus "u = s" by blast
next
fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s[x \<mapsto> a s]" by simp
+ thus "u = s[x \<mapsto> a s]" by blast
next
fix c0 c1 s s1 s2 u
assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
@@ -215,19 +292,19 @@
assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
- hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+ hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
with IH show "u = s1" by blast
next
fix b c0 c1 s s1 u
assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
- hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+ hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
with IH show "u = s1" by blast
next
fix b c s u
assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by simp
+ thus "u = s" by blast
next
fix b c s s1 s2 u
assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
@@ -255,7 +332,7 @@
proof (induct arbitrary: u)
-- "the simple @{text \<SKIP>} case for demonstration:"
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by simp
+ thus "u = s" by blast
next
-- "and the only really interesting case, @{text \<WHILE>}:"
fix b c s s1 s2 u
@@ -270,6 +347,6 @@
from c "IH\<^sub>c" have "s' = s2" by blast
with w "IH\<^sub>w" show "u = s1" by blast
-qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
+qed blast+ -- "prove the rest automatically"
end
--- a/src/HOL/IMP/Transition.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/IMP/Transition.thy Fri Dec 11 09:25:45 2009 +0000
@@ -380,7 +380,7 @@
with n IH
have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
with If True
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
}
moreover
{ assume False: "b s = False"
@@ -389,7 +389,7 @@
with n IH
have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
with If False
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
}
ultimately
show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
@@ -468,8 +468,8 @@
apply (fast intro: converse_rtrancl_into_rtrancl)
-- WHILE
-apply fast
-apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
+apply blast
+apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
done
--- a/src/HOL/Int.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/Int.thy Fri Dec 11 09:25:45 2009 +0000
@@ -1791,16 +1791,28 @@
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
by arith
-lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
-apply (cases "\<bar>n\<bar>=1")
-apply (simp add: abs_mult)
-apply (rule ccontr)
-apply (auto simp add: linorder_neq_iff abs_mult)
-apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
- prefer 2 apply arith
-apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp)
-apply (rule mult_mono, auto)
-done
+lemma abs_zmult_eq_1:
+ assumes mn: "\<bar>m * n\<bar> = 1"
+ shows "\<bar>m\<bar> = (1::int)"
+proof -
+ have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
+ by auto
+ have "~ (2 \<le> \<bar>m\<bar>)"
+ proof
+ assume "2 \<le> \<bar>m\<bar>"
+ hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
+ by (simp add: mult_mono 0)
+ also have "... = \<bar>m*n\<bar>"
+ by (simp add: abs_mult)
+ also have "... = 1"
+ by (simp add: mn)
+ finally have "2*\<bar>n\<bar> \<le> 1" .
+ thus "False" using 0
+ by auto
+ qed
+ thus ?thesis using 0
+ by auto
+qed
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
by (insert abs_zmult_eq_1 [of m n], arith)
--- a/src/HOL/ex/MergeSort.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy Fri Dec 11 09:25:45 2009 +0000
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/Merge.thy
+(* Title: HOL/ex/MergeSort.thy
Author: Tobias Nipkow
Copyright 2002 TU Muenchen
*)
@@ -50,9 +50,7 @@
theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
apply (induct xs rule: msort.induct)
apply simp_all
-apply (subst union_commute)
-apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
-apply (simp add: union_ac)
+apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
done
end
--- a/src/HOL/ex/Primrec.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/ex/Primrec.thy Fri Dec 11 09:25:45 2009 +0000
@@ -103,14 +103,15 @@
@{thm [source] ack_1} is now needed first!] *}
lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k"
-apply (induct i k rule: ack.induct)
- apply simp_all
- prefer 2
- apply (blast intro: less_trans ack_less_mono2)
-apply (induct_tac i' n rule: ack.induct)
- apply simp_all
-apply (blast intro: Suc_leI [THEN le_less_trans] ack_less_mono2)
-done
+proof (induct i k rule: ack.induct)
+ case (1 n) show ?case
+ by (simp, metis ack_less_ack_Suc1 less_ack2 less_trans_Suc)
+next
+ case (2 m) thus ?case by simp
+next
+ case (3 m n) thus ?case
+ by (simp, blast intro: less_trans ack_less_mono2)
+qed
lemma ack_less_mono1: "i < j ==> ack i k < ack j k"
apply (drule less_imp_Suc_add)
@@ -258,14 +259,8 @@
\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
==> \<exists>k. \<forall>l. COMP g fs l < ack k (listsum l)"
apply (unfold COMP_def)
- --{*Now, if meson tolerated map, we could finish with
-@{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans)"} *}
-apply (erule COMP_map_aux [THEN exE])
-apply (rule exI)
-apply (rule allI)
-apply (drule spec)+
-apply (erule less_trans)
-apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
+apply (drule COMP_map_aux)
+apply (meson ack_less_mono2 ack_nest_bound less_trans)
done
--- a/src/HOL/ex/set.thy Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/ex/set.thy Fri Dec 11 09:25:45 2009 +0000
@@ -205,10 +205,7 @@
lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
-- {* Example 11: needs a hint. *}
- apply clarify
- apply (drule_tac x = "{x. P x}" in spec)
- apply force
- done
+by(metis Nat.induct)
lemma
"(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
@@ -223,8 +220,7 @@
to require arithmetic reasoning. *}
apply clarify
apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
- apply (case_tac v, auto)
- apply (drule_tac x = "Suc v" and P = "\<lambda>x. ?a x \<noteq> ?b x" in spec, force)
+ apply metis+
done
end