(* 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