src/HOL/IMPP/EvenOdd.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 59807 22bc39064290
child 62145 5b946c81dfbf
permissions -rw-r--r--
isabelle update_cartouches;
oheimb@8177
     1
(*  Title:      HOL/IMPP/EvenOdd.thy
wenzelm@41589
     2
    Author:     David von Oheimb, TUM
oheimb@8177
     3
*)
oheimb@8177
     4
wenzelm@58889
     5
section {* Example of mutually recursive procedures verified with Hoare logic *}
oheimb@8177
     6
wenzelm@17477
     7
theory EvenOdd
haftmann@58770
     8
imports Main Misc
wenzelm@17477
     9
begin
wenzelm@17477
    10
wenzelm@27362
    11
axiomatization
wenzelm@27362
    12
  Even :: pname and
wenzelm@17477
    13
  Odd :: pname
wenzelm@27362
    14
where
wenzelm@27362
    15
  Even_neq_Odd: "Even ~= Odd" and
wenzelm@17477
    16
  Arg_neq_Res:  "Arg  ~= Res"
oheimb@8177
    17
wenzelm@27362
    18
definition
wenzelm@27362
    19
  evn :: com where
wenzelm@27362
    20
 "evn = (IF (%s. s<Arg> = 0)
oheimb@8177
    21
         THEN Loc Res:==(%s. 0)
oheimb@8177
    22
         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
oheimb@8177
    23
              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
wenzelm@27362
    24
              Loc Res:==(%s. s<Res> * s<Arg>)))"
wenzelm@27362
    25
wenzelm@27362
    26
definition
wenzelm@27362
    27
  odd :: com where
wenzelm@27362
    28
 "odd = (IF (%s. s<Arg> = 0)
oheimb@8177
    29
         THEN Loc Res:==(%s. 1)
wenzelm@27362
    30
         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
oheimb@8177
    31
oheimb@8177
    32
defs
wenzelm@17477
    33
  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
wenzelm@17477
    34
wenzelm@27362
    35
definition
wenzelm@27362
    36
  Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
wenzelm@27362
    37
  "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
wenzelm@27362
    38
wenzelm@27362
    39
definition
wenzelm@27362
    40
  Res_ok :: "nat assn" where
wenzelm@27362
    41
  "Res_ok = (%Z s. even Z = (s<Res> = 0))"
wenzelm@17477
    42
wenzelm@19803
    43
wenzelm@19803
    44
subsection "Arg, Res"
wenzelm@19803
    45
wenzelm@19803
    46
declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
wenzelm@19803
    47
declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
wenzelm@19803
    48
wenzelm@19803
    49
lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
wenzelm@19803
    50
apply (unfold Z_eq_Arg_plus_def)
wenzelm@19803
    51
apply (rule refl)
wenzelm@19803
    52
done
wenzelm@19803
    53
wenzelm@19803
    54
lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
wenzelm@19803
    55
apply (unfold Res_ok_def)
wenzelm@19803
    56
apply (rule refl)
wenzelm@19803
    57
done
wenzelm@19803
    58
wenzelm@19803
    59
lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
wenzelm@19803
    60
wenzelm@19803
    61
lemma body_Odd [simp]: "body Odd = Some odd"
wenzelm@19803
    62
apply (unfold body_def bodies_def)
wenzelm@19803
    63
apply auto
wenzelm@19803
    64
done
wenzelm@19803
    65
wenzelm@19803
    66
lemma body_Even [simp]: "body Even = Some evn"
wenzelm@19803
    67
apply (unfold body_def bodies_def)
wenzelm@19803
    68
apply auto
wenzelm@19803
    69
done
wenzelm@19803
    70
wenzelm@19803
    71
wenzelm@19803
    72
subsection "verification"
wenzelm@19803
    73
wenzelm@19803
    74
lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
wenzelm@19803
    75
apply (unfold odd_def)
wenzelm@19803
    76
apply (rule hoare_derivs.If)
wenzelm@19803
    77
apply (rule hoare_derivs.Ass [THEN conseq1])
wenzelm@19803
    78
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
    79
apply (rule export_s)
wenzelm@19803
    80
apply (rule hoare_derivs.Call [THEN conseq1])
wenzelm@19803
    81
apply  (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
wenzelm@19803
    82
apply (rule single_asm)
wenzelm@19803
    83
apply (auto simp: Arg_Res_simps)
wenzelm@19803
    84
done
wenzelm@19803
    85
wenzelm@19803
    86
lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
wenzelm@19803
    87
apply (unfold evn_def)
wenzelm@19803
    88
apply (rule hoare_derivs.If)
wenzelm@19803
    89
apply (rule hoare_derivs.Ass [THEN conseq1])
wenzelm@19803
    90
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
    91
apply (rule hoare_derivs.Comp)
wenzelm@19803
    92
apply (rule_tac [2] hoare_derivs.Ass)
wenzelm@19803
    93
apply clarsimp
wenzelm@59807
    94
apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp)
wenzelm@19803
    95
apply (rule export_s)
wenzelm@19803
    96
apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
wenzelm@19803
    97
apply (rule single_asm [THEN conseq2])
wenzelm@19803
    98
apply   (clarsimp simp: Arg_Res_simps)
wenzelm@19803
    99
apply  (force simp: Arg_Res_simps)
wenzelm@19803
   100
apply (rule export_s)
wenzelm@19803
   101
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
   102
apply (rule single_asm [THEN conseq2])
wenzelm@19803
   103
apply  (clarsimp simp: Arg_Res_simps)
wenzelm@19803
   104
apply (force simp: Arg_Res_simps)
wenzelm@19803
   105
done
wenzelm@19803
   106
wenzelm@19803
   107
wenzelm@19803
   108
lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
wenzelm@19803
   109
apply (rule BodyN)
wenzelm@19803
   110
apply (simp (no_asm))
wenzelm@19803
   111
apply (rule Even_lemma [THEN hoare_derivs.cut])
wenzelm@19803
   112
apply (rule BodyN)
wenzelm@19803
   113
apply (simp (no_asm))
wenzelm@19803
   114
apply (rule Odd_lemma [THEN thin])
wenzelm@19803
   115
apply (simp (no_asm))
wenzelm@19803
   116
done
wenzelm@19803
   117
wenzelm@19803
   118
lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
wenzelm@19803
   119
apply (rule conseq1)
wenzelm@19803
   120
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
   121
apply    auto
wenzelm@19803
   122
apply (rule hoare_derivs.insert)
wenzelm@19803
   123
apply (rule Odd_lemma [THEN thin])
wenzelm@19803
   124
apply  (simp (no_asm))
wenzelm@19803
   125
apply (rule Even_lemma [THEN thin])
wenzelm@19803
   126
apply (simp (no_asm))
wenzelm@19803
   127
done
oheimb@8177
   128
oheimb@8177
   129
end