# 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 \ 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