moved fac example
authornipkow
Mon Oct 28 17:56:00 2002 +0100 (2002-10-28)
changeset 1368448bfc2cc0938
parent 13683 47fdf4e8e89c
child 13685 0b8fbcf65d73
moved fac example
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/Pointers.thy
     1.1 --- a/src/HOL/Hoare/Examples.thy	Mon Oct 28 14:30:37 2002 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Mon Oct 28 17:56:00 2002 +0100
     1.3 @@ -94,6 +94,20 @@
     1.4  apply(clarsimp split: nat_diff_split)
     1.5  done
     1.6  
     1.7 +lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
     1.8 +by(induct i, simp_all)
     1.9 +
    1.10 +lemma "|- VARS i f.
    1.11 + {True}
    1.12 + i := (1::nat); f := 1;
    1.13 + WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
    1.14 + DO f := f*i; i := i+1 OD
    1.15 + {f = fac n}"
    1.16 +apply vcg_simp
    1.17 +apply(subgoal_tac "i = Suc n")
    1.18 +apply simp
    1.19 +apply arith
    1.20 +done
    1.21  
    1.22  (** Square root **)
    1.23  
     2.1 --- a/src/HOL/Hoare/Pointers.thy	Mon Oct 28 14:30:37 2002 +0100
     2.2 +++ b/src/HOL/Hoare/Pointers.thy	Mon Oct 28 17:56:00 2002 +0100
     2.3 @@ -94,28 +94,6 @@
     2.4  
     2.5  section"Hoare logic"
     2.6  
     2.7 -consts fac :: "nat \<Rightarrow> nat"
     2.8 -primrec
     2.9 -"fac 0 = 1"
    2.10 -"fac (Suc n) = Suc n * fac n"
    2.11 -
    2.12 -lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
    2.13 -by(induct i, simp_all)
    2.14 -
    2.15 -lemma "|- VARS i f.
    2.16 - {True}
    2.17 - i := (1::nat); f := 1;
    2.18 - WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
    2.19 - DO f := f*i; i := i+1 OD
    2.20 - {f = fac n}"
    2.21 -apply vcg_simp
    2.22 -apply(subgoal_tac "i = Suc n")
    2.23 -apply simp
    2.24 -apply arith
    2.25 -done
    2.26 -
    2.27 -
    2.28 -
    2.29  subsection"List reversal"
    2.30  
    2.31  lemma "|- VARS tl p q r.