# HG changeset patch
# User paulson
# Date 1260523545 0
# Node ID 2858dc25eebcf1e9749f3084533eebcf93ef586d
# Parent  53a8f294d60f246aa10437841f572ebfcdc32c74# Parent  de47dc587da04c7606020c3f5222d7ae501c6342
merged

diff -r 53a8f294d60f -r 2858dc25eebc doc-src/TutorialI/Rules/rules.tex
--- 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
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/IMP/Denotation.thy
--- 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
 
 
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/IMP/Natural.thy
--- 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
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/IMP/Transition.thy
--- 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
 
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/Int.thy
--- 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)
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/ex/MergeSort.thy
--- 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
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/ex/Primrec.thy
--- 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
 
 
diff -r 53a8f294d60f -r 2858dc25eebc src/HOL/ex/set.thy
--- 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