author nipkow Fri, 05 Jul 2013 16:45:31 +0200 changeset 52529 48b52b039150 parent 52528 b6a224676c04 child 52538 64206b5b243c
improved proof automation for numerals
 src/HOL/IMP/Hoare_Examples.thy file | annotate | diff | comparison | revisions src/HOL/IMP/Hoare_Total.thy file | annotate | diff | comparison | revisions
```--- 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. *}
+
+  "x + -1 = x - (1 :: 'a :: neg_numeral)"
+unfolding minus_one[symmetric] by (rule diff_minus[symmetric])
+  "-1 + x = x - (1 :: 'a :: {neg_numeral, ab_group_add})"
+unfolding minus_one[symmetric] by simp
+
+  "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
+  "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```
```--- 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```