# HG changeset patch
# User nipkow
# Date 1373286276 -7200
# Node ID 19764bef2730cef7584e995545ea4e45bdc55418
# Parent  d5d150d159adfbaedf60c791e23da2a980994b68
tuned proofs

diff -r d5d150d159ad -r 19764bef2730 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Sun Jul 07 22:58:34 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jul 08 14:24:36 2013 +0200
@@ -2,37 +2,33 @@
 
 theory Hoare_Examples imports Hoare begin
 
-text{* The following lemmas improve proof automation and should be included
-(globally?) when dealing with negative numerals. *}
+text{* Improves proof automation for 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
+  "x + -1 = x - (1 :: int)"
+by arith
 
-lemma add_neg_numeralL[simp]:
+lemma add_neg_numeralR[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
-"sum i = (if i <= 0 then 0 else sum (i - 1) + i)"
+"sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"
 
-lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i - 1) + i" "i <= 0 \<Longrightarrow> sum i = 0"
+lemma sum_simps[simp]:
+  "0 < i \<Longrightarrow> sum i = sum (i - 1) + i"
+  "i \<le> 0 \<Longrightarrow> sum i = 0"
 by(simp_all)
 
 declare sum.simps[simp del]
 
 abbreviation "wsum ==
   WHILE Less (N 0) (V ''x'')
-  DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))"
+  DO (''y'' ::= Plus (V ''y'') (V ''x'');;
+      ''x'' ::= Plus (V ''x'') (N -1))"
 
 
 subsubsection{* Proof by Operational Semantics *}