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