(*  Title:      HOL/IMP/Examples.thy

    ID:         $Id$

    Author:     David von Oheimb, TUM

    Copyright   2000 TUM

*)

header "Examples"

theory Examples imports Natural begin

definition

  factorial :: "loc => loc => com" where

  "factorial a b = (b :== (%s. 1);

                    \<WHILE> (%s. s a ~= 0) \<DO>

                    (b :== (%s. s b * s a); a :== (%s. s a - 1)))"

declare update_def [simp]

subsection "An example due to Tony Hoare"

lemma lemma1:

  assumes 1: "!x. P x \<longrightarrow> Q x"

    and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"

  shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"

  using 2 apply induct

  using 1 apply auto

  done

lemma lemma2 [rule_format (no_asm)]:

  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>

  !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"

apply (erule evalc.induct)

apply (simp_all (no_asm_simp))

apply blast

apply (case_tac "P s")

apply auto

done

lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>

  (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"

  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])

subsection "Factorial"

lemma factorial_3: "a~=b ==>

    \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"

  by (simp add: factorial_def)

text {* the same in single step mode: *}

lemmas [simp del] = evalc_cases

lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"

apply (unfold factorial_def)

apply (frule not_sym)

apply (rule evalc.intros)

apply  (rule evalc.intros)

apply simp

apply (rule evalc.intros)

apply   simp

apply  (rule evalc.intros)

apply   (rule evalc.intros)

apply  simp

apply  (rule evalc.intros)

apply simp

apply (rule evalc.intros)

apply   simp

apply  (rule evalc.intros)

apply   (rule evalc.intros)

apply  simp

apply  (rule evalc.intros)

apply simp

apply (rule evalc.intros)

apply   simp

apply  (rule evalc.intros)

apply   (rule evalc.intros)

apply  simp

apply  (rule evalc.intros)

apply simp

apply (rule evalc.intros)

apply simp

done

end