src/HOL/IMP/Examples.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 27362 a6dc1769fdda
child 41589 bbd861837ebc
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:      HOL/IMP/Examples.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb, TUM
     4     Copyright   2000 TUM
     5 *)
     6 
     7 header "Examples"
     8 
     9 theory Examples imports Natural begin
    10 
    11 definition
    12   factorial :: "loc => loc => com" where
    13   "factorial a b = (b :== (%s. 1);
    14                     \<WHILE> (%s. s a ~= 0) \<DO>
    15                     (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
    16 
    17 declare update_def [simp]
    18 
    19 subsection "An example due to Tony Hoare"
    20 
    21 lemma lemma1:
    22   assumes 1: "!x. P x \<longrightarrow> Q x"
    23     and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
    24   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"
    25   using 2 apply induct
    26   using 1 apply auto
    27   done
    28 
    29 lemma lemma2 [rule_format (no_asm)]:
    30   "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
    31   !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    32 apply (erule evalc.induct)
    33 apply (simp_all (no_asm_simp))
    34 apply blast
    35 apply (case_tac "P s")
    36 apply auto
    37 done
    38 
    39 lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
    40   (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    41   by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    42 
    43 
    44 subsection "Factorial"
    45 
    46 lemma factorial_3: "a~=b ==>
    47     \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    48   by (simp add: factorial_def)
    49 
    50 text {* the same in single step mode: *}
    51 lemmas [simp del] = evalc_cases
    52 lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    53 apply (unfold factorial_def)
    54 apply (frule not_sym)
    55 apply (rule evalc.intros)
    56 apply  (rule evalc.intros)
    57 apply simp
    58 apply (rule evalc.intros)
    59 apply   simp
    60 apply  (rule evalc.intros)
    61 apply   (rule evalc.intros)
    62 apply  simp
    63 apply  (rule evalc.intros)
    64 apply simp
    65 apply (rule evalc.intros)
    66 apply   simp
    67 apply  (rule evalc.intros)
    68 apply   (rule evalc.intros)
    69 apply  simp
    70 apply  (rule evalc.intros)
    71 apply simp
    72 apply (rule evalc.intros)
    73 apply   simp
    74 apply  (rule evalc.intros)
    75 apply   (rule evalc.intros)
    76 apply  simp
    77 apply  (rule evalc.intros)
    78 apply simp
    79 apply (rule evalc.intros)
    80 apply simp
    81 done
    82 
    83 end