src/HOL/IMP/Examples.thy
author kleing
Sun Dec 09 14:35:36 2001 +0100 (2001-12-09)
changeset 12431 07ec657249e5
parent 9243 22b460a0b676
child 16417 9bc16273c2d4
permissions -rw-r--r--
converted to Isar
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
kleing@12431
     9
theory Examples = Natural:
kleing@12431
    10
kleing@12431
    11
constdefs  
kleing@12431
    12
  factorial :: "loc => loc => com"
kleing@12431
    13
  "factorial a b == b :== (%s. 1);
kleing@12431
    14
                    \<WHILE> (%s. s a ~= 0) \<DO>
kleing@12431
    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
kleing@12431
    21
lemma lemma1 [rule_format (no_asm)]: 
kleing@12431
    22
  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
kleing@12431
    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"
kleing@12431
    24
apply (erule evalc.induct)
kleing@12431
    25
apply auto
kleing@12431
    26
done
kleing@12431
    27
oheimb@9243
    28
kleing@12431
    29
lemma lemma2 [rule_format (no_asm)]: 
kleing@12431
    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
kleing@12431
    39
kleing@12431
    40
lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
kleing@12431
    41
  (\<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
    42
  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
kleing@12431
    43
oheimb@9243
    44
kleing@12431
    45
subsection "Factorial"
kleing@12431
    46
kleing@12431
    47
lemma factorial_3: "a~=b ==>  
kleing@12431
    48
  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
kleing@12431
    49
apply (unfold factorial_def)
kleing@12431
    50
apply simp
kleing@12431
    51
done
kleing@12431
    52
kleing@12431
    53
text {* the same in single step mode: *}
kleing@12431
    54
lemmas [simp del] = evalc_cases
kleing@12431
    55
lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
kleing@12431
    56
apply (unfold factorial_def)
kleing@12431
    57
apply (frule not_sym)
kleing@12431
    58
apply (rule evalc.intros)
kleing@12431
    59
apply  (rule evalc.intros)
kleing@12431
    60
apply simp
kleing@12431
    61
apply (rule evalc.intros)
kleing@12431
    62
apply   simp
kleing@12431
    63
apply  (rule evalc.intros)
kleing@12431
    64
apply   (rule evalc.intros)
kleing@12431
    65
apply  simp
kleing@12431
    66
apply  (rule evalc.intros)
kleing@12431
    67
apply simp
kleing@12431
    68
apply (rule evalc.intros)
kleing@12431
    69
apply   simp
kleing@12431
    70
apply  (rule evalc.intros)
kleing@12431
    71
apply   (rule evalc.intros)
kleing@12431
    72
apply  simp
kleing@12431
    73
apply  (rule evalc.intros)
kleing@12431
    74
apply simp
kleing@12431
    75
apply (rule evalc.intros)
kleing@12431
    76
apply   simp
kleing@12431
    77
apply  (rule evalc.intros)
kleing@12431
    78
apply   (rule evalc.intros)
kleing@12431
    79
apply  simp
kleing@12431
    80
apply  (rule evalc.intros)
kleing@12431
    81
apply simp
kleing@12431
    82
apply (rule evalc.intros)
kleing@12431
    83
apply simp
kleing@12431
    84
done
oheimb@9243
    85
  
oheimb@9243
    86
end