# HG changeset patch
# User haftmann
# Date 1527146309 -7200
# Node ID 61188c781cddb7326825aa92d1310542a066859f
# Parent  80df7c90e3151ada2005bd9c8e7ad25ad3555fff
avoid overaggressive classical rule

diff -r 80df7c90e315 -r 61188c781cdd NEWS
--- a/NEWS	Thu May 24 07:59:41 2018 +0200
+++ b/NEWS	Thu May 24 09:18:29 2018 +0200
@@ -347,6 +347,11 @@
 
 INCOMPATIBILITY.
 
+* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
+longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
+adding "elim!: dvd" to classical proof methods in most situations
+restores broken proofs.
+
 
 *** ML ***
 
diff -r 80df7c90e315 -r 61188c781cdd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu May 24 07:59:41 2018 +0200
+++ b/src/HOL/Divides.thy	Thu May 24 09:18:29 2018 +0200
@@ -1298,7 +1298,7 @@
   "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
 
-lemma mod_eq_0D [dest!]:
+lemma mod_eq_0D:
   "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
   using that by (auto simp add: mod_eq_0_iff_dvd elim: dvdE)
 
diff -r 80df7c90e315 -r 61188c781cdd src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu May 24 07:59:41 2018 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu May 24 09:18:29 2018 +0200
@@ -276,8 +276,9 @@
 apply(rule While)
     apply force
    apply force
-  apply force
- apply(rule_tac pre'="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
+    apply force
+  apply (erule dvdE)
+ apply(rule_tac pre'="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * k \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
      apply force
     apply(rule subset_refl)+
  apply(rule Cond)
@@ -326,7 +327,8 @@
     apply force
    apply force
   apply force
- apply(rule_tac pre'="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
+  apply (erule dvdE)
+ apply(rule_tac pre'="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * k \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
      apply force
     apply(rule subset_refl)+
  apply(rule Cond)
diff -r 80df7c90e315 -r 61188c781cdd src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Thu May 24 07:59:41 2018 +0200
+++ b/src/HOL/Library/Stream.thy	Thu May 24 09:18:29 2018 +0200
@@ -328,11 +328,13 @@
 
 lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
    stake n (cycle u) = concat (replicate (n div length u) u)"
-  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
+  by (induct "n div length u" arbitrary: n u)
+    (auto simp: stake_add [symmetric] mod_eq_0_iff_dvd elim!: dvdE)
 
 lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
    sdrop n (cycle u) = cycle u"
-  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
+  by (induct "n div length u" arbitrary: n u)
+    (auto simp: sdrop_add [symmetric] mod_eq_0_iff_dvd elim!: dvdE)
 
 lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
    stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
diff -r 80df7c90e315 -r 61188c781cdd src/HOL/ex/Parallel_Example.thy
--- a/src/HOL/ex/Parallel_Example.thy	Thu May 24 07:59:41 2018 +0200
+++ b/src/HOL/ex/Parallel_Example.thy	Thu May 24 09:18:29 2018 +0200
@@ -68,13 +68,11 @@
 by pat_completeness auto
 
 termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
-term measure
-apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
-apply (auto simp add: prod_eq_iff)
-apply (case_tac "k \<le> 2 * q")
-apply (rule diff_less_mono)
-apply auto
-done
+  apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
+    apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
+  apply (case_tac "k \<le> ka * 2")
+   apply (auto intro: diff_less_mono)
+  done
 
 definition factorise :: "nat \<Rightarrow> nat list" where
   "factorise n = factorise_from 2 n"