src/HOL/IMP/Examples.thy
changeset 12431 07ec657249e5
parent 9243 22b460a0b676
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/IMP/Examples.thy	Sun Dec 09 14:35:11 2001 +0100
     1.2 +++ b/src/HOL/IMP/Examples.thy	Sun Dec 09 14:35:36 2001 +0100
     1.3 @@ -4,17 +4,83 @@
     1.4      Copyright   2000 TUM
     1.5  *)
     1.6  
     1.7 -Examples = Natural +
     1.8 +header "Examples"
     1.9 +
    1.10 +theory Examples = Natural:
    1.11 +
    1.12 +constdefs  
    1.13 +  factorial :: "loc => loc => com"
    1.14 +  "factorial a b == b :== (%s. 1);
    1.15 +                    \<WHILE> (%s. s a ~= 0) \<DO>
    1.16 +                    (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    1.17 +
    1.18 +declare update_def [simp]
    1.19 +
    1.20 +subsection "An example due to Tony Hoare"
    1.21  
    1.22 -defs (* bring up the deferred definition for update *)
    1.23 +lemma lemma1 [rule_format (no_asm)]: 
    1.24 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
    1.25 +  !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"
    1.26 +apply (erule evalc.induct)
    1.27 +apply auto
    1.28 +done
    1.29 +
    1.30  
    1.31 - update_def "update == fun_upd"
    1.32 +lemma lemma2 [rule_format (no_asm)]: 
    1.33 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>  
    1.34 +  !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    1.35 +apply (erule evalc.induct)
    1.36 +apply (simp_all (no_asm_simp))
    1.37 +apply blast
    1.38 +apply (case_tac "P s")
    1.39 +apply auto
    1.40 +done
    1.41 +
    1.42 +
    1.43 +lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
    1.44 +  (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    1.45 +  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    1.46 +
    1.47  
    1.48 -constdefs
    1.49 -  
    1.50 -  factorial :: loc => loc => com
    1.51 - "factorial a b == b :== (%s. 1);
    1.52 -               WHILE (%s. s a ~= 0) DO
    1.53 -                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    1.54 +subsection "Factorial"
    1.55 +
    1.56 +lemma factorial_3: "a~=b ==>  
    1.57 +  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    1.58 +apply (unfold factorial_def)
    1.59 +apply simp
    1.60 +done
    1.61 +
    1.62 +text {* the same in single step mode: *}
    1.63 +lemmas [simp del] = evalc_cases
    1.64 +lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    1.65 +apply (unfold factorial_def)
    1.66 +apply (frule not_sym)
    1.67 +apply (rule evalc.intros)
    1.68 +apply  (rule evalc.intros)
    1.69 +apply simp
    1.70 +apply (rule evalc.intros)
    1.71 +apply   simp
    1.72 +apply  (rule evalc.intros)
    1.73 +apply   (rule evalc.intros)
    1.74 +apply  simp
    1.75 +apply  (rule evalc.intros)
    1.76 +apply simp
    1.77 +apply (rule evalc.intros)
    1.78 +apply   simp
    1.79 +apply  (rule evalc.intros)
    1.80 +apply   (rule evalc.intros)
    1.81 +apply  simp
    1.82 +apply  (rule evalc.intros)
    1.83 +apply simp
    1.84 +apply (rule evalc.intros)
    1.85 +apply   simp
    1.86 +apply  (rule evalc.intros)
    1.87 +apply   (rule evalc.intros)
    1.88 +apply  simp
    1.89 +apply  (rule evalc.intros)
    1.90 +apply simp
    1.91 +apply (rule evalc.intros)
    1.92 +apply simp
    1.93 +done
    1.94    
    1.95  end