src/HOL/IMP/Examples.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 12431 07ec657249e5
child 18372 2bffdf62fe7f
permissions -rw-r--r--
migrated theory headers to new format
     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 constdefs  
    12   factorial :: "loc => loc => com"
    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 [rule_format (no_asm)]: 
    22   "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
    23   !c. 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"
    24 apply (erule evalc.induct)
    25 apply auto
    26 done
    27 
    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 
    40 lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
    41   (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    42   by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    43 
    44 
    45 subsection "Factorial"
    46 
    47 lemma factorial_3: "a~=b ==>  
    48   \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    49 apply (unfold factorial_def)
    50 apply simp
    51 done
    52 
    53 text {* the same in single step mode: *}
    54 lemmas [simp del] = evalc_cases
    55 lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    56 apply (unfold factorial_def)
    57 apply (frule not_sym)
    58 apply (rule evalc.intros)
    59 apply  (rule evalc.intros)
    60 apply simp
    61 apply (rule evalc.intros)
    62 apply   simp
    63 apply  (rule evalc.intros)
    64 apply   (rule evalc.intros)
    65 apply  simp
    66 apply  (rule evalc.intros)
    67 apply simp
    68 apply (rule evalc.intros)
    69 apply   simp
    70 apply  (rule evalc.intros)
    71 apply   (rule evalc.intros)
    72 apply  simp
    73 apply  (rule evalc.intros)
    74 apply simp
    75 apply (rule evalc.intros)
    76 apply   simp
    77 apply  (rule evalc.intros)
    78 apply   (rule evalc.intros)
    79 apply  simp
    80 apply  (rule evalc.intros)
    81 apply simp
    82 apply (rule evalc.intros)
    83 apply simp
    84 done
    85   
    86 end