src/HOL/IMPP/EvenOdd.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27362 a6dc1769fdda
child 41589 bbd861837ebc
permissions -rw-r--r--
moved global ML bindings to global place;
oheimb@8177
     1
(*  Title:      HOL/IMPP/EvenOdd.thy
oheimb@8177
     2
    ID:         $Id$
oheimb@8177
     3
    Author:     David von Oheimb
oheimb@8177
     4
    Copyright   1999 TUM
oheimb@8177
     5
*)
oheimb@8177
     6
wenzelm@17477
     7
header {* Example of mutually recursive procedures verified with Hoare logic *}
oheimb@8177
     8
wenzelm@17477
     9
theory EvenOdd
wenzelm@17477
    10
imports Misc
wenzelm@17477
    11
begin
wenzelm@17477
    12
wenzelm@27362
    13
definition
wenzelm@27362
    14
  even :: "nat => bool" where
wenzelm@27362
    15
  "even n = (2 dvd n)"
oheimb@8177
    16
wenzelm@27362
    17
axiomatization
wenzelm@27362
    18
  Even :: pname and
wenzelm@17477
    19
  Odd :: pname
wenzelm@27362
    20
where
wenzelm@27362
    21
  Even_neq_Odd: "Even ~= Odd" and
wenzelm@17477
    22
  Arg_neq_Res:  "Arg  ~= Res"
oheimb@8177
    23
wenzelm@27362
    24
definition
wenzelm@27362
    25
  evn :: com where
wenzelm@27362
    26
 "evn = (IF (%s. s<Arg> = 0)
oheimb@8177
    27
         THEN Loc Res:==(%s. 0)
oheimb@8177
    28
         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
oheimb@8177
    29
              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
wenzelm@27362
    30
              Loc Res:==(%s. s<Res> * s<Arg>)))"
wenzelm@27362
    31
wenzelm@27362
    32
definition
wenzelm@27362
    33
  odd :: com where
wenzelm@27362
    34
 "odd = (IF (%s. s<Arg> = 0)
oheimb@8177
    35
         THEN Loc Res:==(%s. 1)
wenzelm@27362
    36
         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
oheimb@8177
    37
oheimb@8177
    38
defs
wenzelm@17477
    39
  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
wenzelm@17477
    40
wenzelm@27362
    41
definition
wenzelm@27362
    42
  Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
wenzelm@27362
    43
  "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
wenzelm@27362
    44
wenzelm@27362
    45
definition
wenzelm@27362
    46
  Res_ok :: "nat assn" where
wenzelm@27362
    47
  "Res_ok = (%Z s. even Z = (s<Res> = 0))"
wenzelm@17477
    48
wenzelm@19803
    49
wenzelm@19803
    50
subsection "even"
wenzelm@19803
    51
wenzelm@19803
    52
lemma even_0 [simp]: "even 0"
wenzelm@19803
    53
apply (unfold even_def)
wenzelm@19803
    54
apply simp
wenzelm@19803
    55
done
wenzelm@19803
    56
wenzelm@19803
    57
lemma not_even_1 [simp]: "even (Suc 0) = False"
wenzelm@19803
    58
apply (unfold even_def)
wenzelm@19803
    59
apply simp
wenzelm@19803
    60
done
wenzelm@19803
    61
wenzelm@19803
    62
lemma even_step [simp]: "even (Suc (Suc n)) = even n"
wenzelm@19803
    63
apply (unfold even_def)
wenzelm@19803
    64
apply (subgoal_tac "Suc (Suc n) = n+2")
wenzelm@19803
    65
prefer 2
wenzelm@19803
    66
apply  simp
wenzelm@19803
    67
apply (erule ssubst)
wenzelm@19803
    68
apply (rule dvd_reduce)
wenzelm@19803
    69
done
wenzelm@19803
    70
wenzelm@19803
    71
wenzelm@19803
    72
subsection "Arg, Res"
wenzelm@19803
    73
wenzelm@19803
    74
declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
wenzelm@19803
    75
declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
wenzelm@19803
    76
wenzelm@19803
    77
lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
wenzelm@19803
    78
apply (unfold Z_eq_Arg_plus_def)
wenzelm@19803
    79
apply (rule refl)
wenzelm@19803
    80
done
wenzelm@19803
    81
wenzelm@19803
    82
lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
wenzelm@19803
    83
apply (unfold Res_ok_def)
wenzelm@19803
    84
apply (rule refl)
wenzelm@19803
    85
done
wenzelm@19803
    86
wenzelm@19803
    87
lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
wenzelm@19803
    88
wenzelm@19803
    89
lemma body_Odd [simp]: "body Odd = Some odd"
wenzelm@19803
    90
apply (unfold body_def bodies_def)
wenzelm@19803
    91
apply auto
wenzelm@19803
    92
done
wenzelm@19803
    93
wenzelm@19803
    94
lemma body_Even [simp]: "body Even = Some evn"
wenzelm@19803
    95
apply (unfold body_def bodies_def)
wenzelm@19803
    96
apply auto
wenzelm@19803
    97
done
wenzelm@19803
    98
wenzelm@19803
    99
wenzelm@19803
   100
subsection "verification"
wenzelm@19803
   101
wenzelm@19803
   102
lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
wenzelm@19803
   103
apply (unfold odd_def)
wenzelm@19803
   104
apply (rule hoare_derivs.If)
wenzelm@19803
   105
apply (rule hoare_derivs.Ass [THEN conseq1])
wenzelm@19803
   106
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
   107
apply (rule export_s)
wenzelm@19803
   108
apply (rule hoare_derivs.Call [THEN conseq1])
wenzelm@19803
   109
apply  (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
wenzelm@19803
   110
apply (rule single_asm)
wenzelm@19803
   111
apply (auto simp: Arg_Res_simps)
wenzelm@19803
   112
done
wenzelm@19803
   113
wenzelm@19803
   114
lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
wenzelm@19803
   115
apply (unfold evn_def)
wenzelm@19803
   116
apply (rule hoare_derivs.If)
wenzelm@19803
   117
apply (rule hoare_derivs.Ass [THEN conseq1])
wenzelm@19803
   118
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
   119
apply (rule hoare_derivs.Comp)
wenzelm@19803
   120
apply (rule_tac [2] hoare_derivs.Ass)
wenzelm@19803
   121
apply clarsimp
wenzelm@19803
   122
apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp)
wenzelm@19803
   123
apply (rule export_s)
wenzelm@19803
   124
apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
wenzelm@19803
   125
apply (rule single_asm [THEN conseq2])
wenzelm@19803
   126
apply   (clarsimp simp: Arg_Res_simps)
wenzelm@19803
   127
apply  (force simp: Arg_Res_simps)
wenzelm@19803
   128
apply (rule export_s)
wenzelm@19803
   129
apply (rule_tac I1 = "%Z l. even Z = (l Res = 0) " and Q1 = "%Z s. even Z = (s<Arg> = 0) " in Call_invariant [THEN conseq12])
wenzelm@19803
   130
apply (rule single_asm [THEN conseq2])
wenzelm@19803
   131
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
   132
apply (force simp: Arg_Res_simps)
wenzelm@19803
   133
done
wenzelm@19803
   134
wenzelm@19803
   135
wenzelm@19803
   136
lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
wenzelm@19803
   137
apply (rule BodyN)
wenzelm@19803
   138
apply (simp (no_asm))
wenzelm@19803
   139
apply (rule Even_lemma [THEN hoare_derivs.cut])
wenzelm@19803
   140
apply (rule BodyN)
wenzelm@19803
   141
apply (simp (no_asm))
wenzelm@19803
   142
apply (rule Odd_lemma [THEN thin])
wenzelm@19803
   143
apply (simp (no_asm))
wenzelm@19803
   144
done
wenzelm@19803
   145
wenzelm@19803
   146
lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
wenzelm@19803
   147
apply (rule conseq1)
wenzelm@19803
   148
apply  (rule_tac Procs = "{Odd, Even}" and pn = "Even" and P = "%pn. Z=Arg+ (if pn = Odd then 1 else 0) " and Q = "%pn. Res_ok" in Body1)
wenzelm@19803
   149
apply    auto
wenzelm@19803
   150
apply (rule hoare_derivs.insert)
wenzelm@19803
   151
apply (rule Odd_lemma [THEN thin])
wenzelm@19803
   152
apply  (simp (no_asm))
wenzelm@19803
   153
apply (rule Even_lemma [THEN thin])
wenzelm@19803
   154
apply (simp (no_asm))
wenzelm@19803
   155
done
oheimb@8177
   156
oheimb@8177
   157
end