equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Hoare_Examples imports Hoare begin |
3 theory Hoare_Examples imports Hoare begin |
|
4 |
|
5 text{* The following lemmas improve proof automation and should be included |
|
6 (globally?) when dealing with negative numerals. *} |
|
7 |
|
8 lemma add_neg1R[simp]: |
|
9 "x + -1 = x - (1 :: 'a :: neg_numeral)" |
|
10 unfolding minus_one[symmetric] by (rule diff_minus[symmetric]) |
|
11 lemma add_neg1L[simp]: |
|
12 "-1 + x = x - (1 :: 'a :: {neg_numeral, ab_group_add})" |
|
13 unfolding minus_one[symmetric] by simp |
|
14 |
|
15 lemma add_neg_numeralL[simp]: |
|
16 "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)" |
|
17 by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral) |
|
18 lemma add_neg_numeralR[simp]: |
|
19 "neg_numeral n + x = (x::'a::{neg_numeral,ab_group_add}) - numeral(n)" |
|
20 by simp |
|
21 |
4 |
22 |
5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
23 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
6 |
24 |
7 fun sum :: "int \<Rightarrow> int" where |
25 fun sum :: "int \<Rightarrow> int" where |
8 "sum i = (if i <= 0 then 0 else sum (i - 1) + i)" |
26 "sum i = (if i <= 0 then 0 else sum (i - 1) + i)" |
55 apply(rule Seq) |
73 apply(rule Seq) |
56 prefer 2 |
74 prefer 2 |
57 apply(rule Assign) |
75 apply(rule Assign) |
58 apply(rule Assign') |
76 apply(rule Assign') |
59 apply simp |
77 apply simp |
60 apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps) |
|
61 apply(simp) |
78 apply(simp) |
62 apply(rule Assign') |
79 apply(rule Assign') |
63 apply simp |
80 apply simp |
64 done |
81 done |
65 |
82 |