--- 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 *}