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