--- 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 ***
--- 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)
--- 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)
--- 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"
--- 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"