src/HOL/IMP/Examples.thy
changeset 18372 2bffdf62fe7f
parent 16417 9bc16273c2d4
child 27362 a6dc1769fdda
     1.1 --- a/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:41 2005 +0100
     1.2 +++ b/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:50 2005 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  theory Examples imports Natural begin
     1.6  
     1.7 -constdefs  
     1.8 +constdefs
     1.9    factorial :: "loc => loc => com"
    1.10    "factorial a b == b :== (%s. 1);
    1.11                      \<WHILE> (%s. s a ~= 0) \<DO>
    1.12 @@ -18,16 +18,16 @@
    1.13  
    1.14  subsection "An example due to Tony Hoare"
    1.15  
    1.16 -lemma lemma1 [rule_format (no_asm)]: 
    1.17 -  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
    1.18 -  !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.19 -apply (erule evalc.induct)
    1.20 -apply auto
    1.21 -done
    1.22 +lemma lemma1:
    1.23 +  assumes 1: "!x. P x \<longrightarrow> Q x"
    1.24 +    and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.25 +  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"
    1.26 +  using 2 apply induct
    1.27 +  using 1 apply auto
    1.28 +  done
    1.29  
    1.30 -
    1.31 -lemma lemma2 [rule_format (no_asm)]: 
    1.32 -  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>  
    1.33 +lemma lemma2 [rule_format (no_asm)]:
    1.34 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
    1.35    !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    1.36  apply (erule evalc.induct)
    1.37  apply (simp_all (no_asm_simp))
    1.38 @@ -36,19 +36,16 @@
    1.39  apply auto
    1.40  done
    1.41  
    1.42 -
    1.43 -lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
    1.44 +lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
    1.45    (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    1.46    by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    1.47  
    1.48  
    1.49  subsection "Factorial"
    1.50  
    1.51 -lemma factorial_3: "a~=b ==>  
    1.52 -  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    1.53 -apply (unfold factorial_def)
    1.54 -apply simp
    1.55 -done
    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 +  by (simp add: factorial_def)
    1.59  
    1.60  text {* the same in single step mode: *}
    1.61  lemmas [simp del] = evalc_cases
    1.62 @@ -82,5 +79,5 @@
    1.63  apply (rule evalc.intros)
    1.64  apply simp
    1.65  done
    1.66 -  
    1.67 +
    1.68  end