--- a/src/HOL/Hoare/Examples.thy Mon Oct 28 14:30:37 2002 +0100
+++ b/src/HOL/Hoare/Examples.thy Mon Oct 28 17:56:00 2002 +0100
@@ -94,6 +94,20 @@
apply(clarsimp split: nat_diff_split)
done
+lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
+by(induct i, simp_all)
+
+lemma "|- VARS i f.
+ {True}
+ i := (1::nat); f := 1;
+ WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
+ DO f := f*i; i := i+1 OD
+ {f = fac n}"
+apply vcg_simp
+apply(subgoal_tac "i = Suc n")
+apply simp
+apply arith
+done
(** Square root **)
--- a/src/HOL/Hoare/Pointers.thy Mon Oct 28 14:30:37 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy Mon Oct 28 17:56:00 2002 +0100
@@ -94,28 +94,6 @@
section"Hoare logic"
-consts fac :: "nat \<Rightarrow> nat"
-primrec
-"fac 0 = 1"
-"fac (Suc n) = Suc n * fac n"
-
-lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
-by(induct i, simp_all)
-
-lemma "|- VARS i f.
- {True}
- i := (1::nat); f := 1;
- WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
- DO f := f*i; i := i+1 OD
- {f = fac n}"
-apply vcg_simp
-apply(subgoal_tac "i = Suc n")
-apply simp
-apply arith
-done
-
-
-
subsection"List reversal"
lemma "|- VARS tl p q r.