src/HOL/IMP/Examples.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 18372 2bffdf62fe7f
child 27362 a6dc1769fdda
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     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:
    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