avoid overaggressive classical rule
authorhaftmann
Thu May 24 09:18:29 2018 +0200 (20 months ago ago)
changeset 6826061188c781cdd
parent 68259 80df7c90e315
child 68261 035c78bb0a66
child 68266 bb9a3be6952a
avoid overaggressive classical rule
NEWS
src/HOL/Divides.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Library/Stream.thy
src/HOL/ex/Parallel_Example.thy
     1.1 --- a/NEWS	Thu May 24 07:59:41 2018 +0200
     1.2 +++ b/NEWS	Thu May 24 09:18:29 2018 +0200
     1.3 @@ -347,6 +347,11 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
     1.8 +longer aggresively destroyed to "?q. m = d * q".  INCOMPATIBILITY,
     1.9 +adding "elim!: dvd" to classical proof methods in most situations
    1.10 +restores broken proofs.
    1.11 +
    1.12  
    1.13  *** ML ***
    1.14  
     2.1 --- a/src/HOL/Divides.thy	Thu May 24 07:59:41 2018 +0200
     2.2 +++ b/src/HOL/Divides.thy	Thu May 24 09:18:29 2018 +0200
     2.3 @@ -1298,7 +1298,7 @@
     2.4    "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
     2.5    by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
     2.6  
     2.7 -lemma mod_eq_0D [dest!]:
     2.8 +lemma mod_eq_0D:
     2.9    "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
    2.10    using that by (auto simp add: mod_eq_0_iff_dvd elim: dvdE)
    2.11  
     3.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu May 24 07:59:41 2018 +0200
     3.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu May 24 09:18:29 2018 +0200
     3.3 @@ -276,8 +276,9 @@
     3.4  apply(rule While)
     3.5      apply force
     3.6     apply force
     3.7 -  apply force
     3.8 - 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)
     3.9 +    apply force
    3.10 +  apply (erule dvdE)
    3.11 + 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)
    3.12       apply force
    3.13      apply(rule subset_refl)+
    3.14   apply(rule Cond)
    3.15 @@ -326,7 +327,8 @@
    3.16      apply force
    3.17     apply force
    3.18    apply force
    3.19 - 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)
    3.20 +  apply (erule dvdE)
    3.21 + 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)
    3.22       apply force
    3.23      apply(rule subset_refl)+
    3.24   apply(rule Cond)
     4.1 --- a/src/HOL/Library/Stream.thy	Thu May 24 07:59:41 2018 +0200
     4.2 +++ b/src/HOL/Library/Stream.thy	Thu May 24 09:18:29 2018 +0200
     4.3 @@ -328,11 +328,13 @@
     4.4  
     4.5  lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
     4.6     stake n (cycle u) = concat (replicate (n div length u) u)"
     4.7 -  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
     4.8 +  by (induct "n div length u" arbitrary: n u)
     4.9 +    (auto simp: stake_add [symmetric] mod_eq_0_iff_dvd elim!: dvdE)
    4.10  
    4.11  lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
    4.12     sdrop n (cycle u) = cycle u"
    4.13 -  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
    4.14 +  by (induct "n div length u" arbitrary: n u)
    4.15 +    (auto simp: sdrop_add [symmetric] mod_eq_0_iff_dvd elim!: dvdE)
    4.16  
    4.17  lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
    4.18     stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
     5.1 --- a/src/HOL/ex/Parallel_Example.thy	Thu May 24 07:59:41 2018 +0200
     5.2 +++ b/src/HOL/ex/Parallel_Example.thy	Thu May 24 09:18:29 2018 +0200
     5.3 @@ -68,13 +68,11 @@
     5.4  by pat_completeness auto
     5.5  
     5.6  termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
     5.7 -term measure
     5.8 -apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
     5.9 -apply (auto simp add: prod_eq_iff)
    5.10 -apply (case_tac "k \<le> 2 * q")
    5.11 -apply (rule diff_less_mono)
    5.12 -apply auto
    5.13 -done
    5.14 +  apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
    5.15 +    apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
    5.16 +  apply (case_tac "k \<le> ka * 2")
    5.17 +   apply (auto intro: diff_less_mono)
    5.18 +  done
    5.19  
    5.20  definition factorise :: "nat \<Rightarrow> nat list" where
    5.21    "factorise n = factorise_from 2 n"