Theory Examples

Up to index of Isabelle/HOL/IMP

theory Examples
imports Natural
begin

(*  Title:      HOL/IMP/Examples.thy
    ID:         $Id: Examples.thy,v 1.3 2005/06/17 14:13:07 haftmann Exp $
    Author:     David von Oheimb, TUM
    Copyright   2000 TUM
*)

header "Examples"

theory Examples imports Natural begin

constdefs  
  factorial :: "loc => loc => com"
  "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 [rule_format (no_asm)]: 
  "[| !x. P x --> Q x; ⟨w,s⟩ -->c t |] ==>
  !c. w = While P c --> ⟨While Q c,t⟩ -->c u --> ⟨While Q c,s⟩ -->c u"
apply (erule evalc.induct)
apply auto
done


lemma lemma2 [rule_format (no_asm)]: 
  "[| !x. P x --> Q x; ⟨w,s⟩ -->c u |] ==>  
  !c. w = While Q c --> ⟨While P c; While Q c,s⟩ -->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 --> Q x ==>  
  (⟨While P c; While Q c, s⟩ -->c t) = (⟨While Q c, s⟩ -->c t)"
  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])


subsection "Factorial"

lemma factorial_3: "a~=b ==>  
  ⟨factorial a b, Mem(a:=3)⟩ -->c Mem(b:=6, a:=0)"
apply (unfold factorial_def)
apply simp
done

text {* the same in single step mode: *}
lemmas [simp del] = evalc_cases
lemma  "a~=b ==> ⟨factorial a b, Mem(a:=3)⟩ -->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

An example due to Tony Hoare

lemma lemma1:

  [| ∀x. P x --> Q x; ⟨w,s⟩ -->c t; w = WHILE P DO c; ⟨WHILE Q DO c,t⟩ -->c u |]
  ==> ⟨WHILE Q DO c,s⟩ -->c u

lemma lemma2:

  [| ∀x. P x --> Q x; ⟨w,s⟩ -->c u; w = WHILE Q DO c |]
  ==> ⟨WHILE P DO c; WHILE Q DO c,s⟩ -->c u

lemma Hoare_example:

x. P x --> Q x
  ==> ⟨WHILE P DO c; WHILE Q DO c,s⟩ -->c t = ⟨WHILE Q DO c,s⟩ -->c t

Factorial

lemma factorial_3:

  ab ==> ⟨factorial a b,Mem(a := 3)⟩ -->c Mem(b := 6, a := 0)

lemmas

  ⟨SKIP,s⟩ -->c s' = (s' = s)
x :== a ,s⟩ -->c s' = (s' = s[x ::= a s])
  b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c0.0,s⟩ -->c s'
  ¬ b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c1.0,s⟩ -->c s'
  ¬ b s ==> ⟨WHILE b DO c,s⟩ -->c s' = (s' = s)
c0.0; c1.0,s⟩ -->c s' = (∃s''. ⟨c0.0,s⟩ -->c s'' ∧ ⟨c1.0,s''⟩ -->c s')
  b s ==> ⟨WHILE b DO c,s⟩ -->c s' =
          (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨WHILE b DO c,s''⟩ -->c s')

lemmas

  ⟨SKIP,s⟩ -->c s' = (s' = s)
x :== a ,s⟩ -->c s' = (s' = s[x ::= a s])
  b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c0.0,s⟩ -->c s'
  ¬ b s ==> ⟨IF b THEN c0.0 ELSE c1.0,s⟩ -->c s' = ⟨c1.0,s⟩ -->c s'
  ¬ b s ==> ⟨WHILE b DO c,s⟩ -->c s' = (s' = s)
c0.0; c1.0,s⟩ -->c s' = (∃s''. ⟨c0.0,s⟩ -->c s'' ∧ ⟨c1.0,s''⟩ -->c s')
  b s ==> ⟨WHILE b DO c,s⟩ -->c s' =
          (∃s''. ⟨c,s⟩ -->c s'' ∧ ⟨WHILE b DO c,s''⟩ -->c s')

lemma

  ab ==> ⟨factorial a b,Mem(a := 3)⟩ -->c Mem(b := 6, a := 0)