# 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:

      a ≠ b ==> ⟨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

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