avoid slow proofs due to simp rules from 960509bfd47e;
authorwenzelm
Sat Oct 28 16:12:29 2017 +0200 (18 months ago)
changeset 66930d4f7c6f14fa2
parent 66929 c19b17b72777
child 66931 4ff031d249b2
avoid slow proofs due to simp rules from 960509bfd47e;
src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
     1.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Fri Oct 27 17:06:30 2017 +0200
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Oct 28 16:12:29 2017 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4    from this[OF x_lower x_upper x_lower' x_upper' \<open>0 <= 0\<close> \<open>0 <= 79\<close>]
     1.5      \<open>0 \<le> ca\<close> \<open>0 \<le> ce\<close> x_lower x_lower'
     1.6    show ?thesis unfolding returns(1) returns(2) unfolding returns
     1.7 -    by simp
     1.8 +    by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)
     1.9  qed
    1.10  
    1.11  spark_vc procedure_round_62
    1.12 @@ -415,7 +415,8 @@
    1.13      \<open>0 \<le> cla\<close> \<open>0 \<le> cle\<close> \<open>0 \<le> cra\<close> \<open>0 \<le> cre\<close> x_lower x_lower'
    1.14    show ?thesis unfolding \<open>loop__1__j + 1 + 1 = loop__1__j + 2\<close>
    1.15      unfolding returns(1) returns(2) unfolding returns
    1.16 -    by simp
    1.17 +    by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)
    1.18 +
    1.19  qed
    1.20  
    1.21  spark_vc procedure_round_76