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