# HG changeset patch
# User nipkow
# Date 1373035531 -7200
# Node ID 48b52b03915076bc7c39dbf7e48d74b955df9f1e
# Parent  b6a224676c04e957d112d53305824b92248cdf57
improved proof automation for numerals

diff -r b6a224676c04 -r 48b52b039150 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Fri Jul 05 16:45:31 2013 +0200
@@ -2,6 +2,24 @@
 
 theory Hoare_Examples imports Hoare begin
 
+text{* The following lemmas improve proof automation and should be included
+(globally?) when dealing with negative numerals. *}
+
+lemma add_neg1R[simp]:
+  "x + -1 = x - (1 :: 'a :: neg_numeral)"
+unfolding minus_one[symmetric] by (rule diff_minus[symmetric])
+lemma add_neg1L[simp]:
+  "-1 + x = x - (1 :: 'a :: {neg_numeral, ab_group_add})"
+unfolding minus_one[symmetric] by simp
+
+lemma add_neg_numeralL[simp]:
+  "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
+by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral)
+lemma add_neg_numeralR[simp]:
+  "neg_numeral n + x = (x::'a::{neg_numeral,ab_group_add}) - numeral(n)"
+by simp
+
+
 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
 
 fun sum :: "int \<Rightarrow> int" where
@@ -57,7 +75,6 @@
    apply(rule Assign)
   apply(rule Assign')
   apply simp
-  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
  apply(simp)
 apply(rule Assign')
 apply simp
diff -r b6a224676c04 -r 48b52b039150 src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/HOL/IMP/Hoare_Total.thy	Fri Jul 05 16:45:31 2013 +0200
@@ -80,7 +80,6 @@
    apply(rule Assign)
   apply(rule Assign')
   apply simp
-  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
  apply(simp)
 apply(rule Assign')
 apply simp