equal
deleted
inserted
replaced
92 but not list h (h a) [] (because h is cyclic) |
92 but not list h (h a) [] (because h is cyclic) |
93 *) |
93 *) |
94 |
94 |
95 section"Hoare logic" |
95 section"Hoare logic" |
96 |
96 |
97 consts fac :: "nat \<Rightarrow> nat" |
|
98 primrec |
|
99 "fac 0 = 1" |
|
100 "fac (Suc n) = Suc n * fac n" |
|
101 |
|
102 lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i" |
|
103 by(induct i, simp_all) |
|
104 |
|
105 lemma "|- VARS i f. |
|
106 {True} |
|
107 i := (1::nat); f := 1; |
|
108 WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1} |
|
109 DO f := f*i; i := i+1 OD |
|
110 {f = fac n}" |
|
111 apply vcg_simp |
|
112 apply(subgoal_tac "i = Suc n") |
|
113 apply simp |
|
114 apply arith |
|
115 done |
|
116 |
|
117 |
|
118 |
|
119 subsection"List reversal" |
97 subsection"List reversal" |
120 |
98 |
121 lemma "|- VARS tl p q r. |
99 lemma "|- VARS tl p q r. |
122 {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}} |
100 {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}} |
123 WHILE p ~= None |
101 WHILE p ~= None |