src/HOL/IMPP/Misc.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 58963 26bf09b95dda
child 62145 5b946c81dfbf
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/IMPP/Misc.thy
     2     Author:     David von Oheimb, TUM
     3 *)
     4 
     5 section {* Several examples for Hoare logic *}
     6 
     7 theory Misc
     8 imports Hoare
     9 begin
    10 
    11 defs
    12   newlocs_def: "newlocs       == %x. undefined"
    13   setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    14   getlocs_def: "getlocs s     == case s of st g l => l"
    15    update_def: "update s vn v == case vn of
    16                                Glb gn => (case s of st g l => st (g(gn:=v)) l)
    17                              | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    18 
    19 
    20 subsection "state access"
    21 
    22 lemma getlocs_def2: "getlocs (st g l) = l"
    23 apply (unfold getlocs_def)
    24 apply simp
    25 done
    26 
    27 lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s"
    28 apply (unfold update_def)
    29 apply (induct_tac s)
    30 apply (simp add: getlocs_def2)
    31 done
    32 
    33 lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]"
    34 apply (unfold update_def)
    35 apply (induct_tac X)
    36 apply  auto
    37 apply  (induct_tac [!] s)
    38 apply  auto
    39 done
    40 
    41 lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)"
    42 apply (unfold update_def)
    43 apply (induct_tac s)
    44 apply (simp add: getlocs_def2)
    45 done
    46 
    47 lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s"
    48 apply (unfold update_def)
    49 apply (induct_tac s)
    50 apply (simp add: getlocs_def2)
    51 done
    52 
    53 lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l"
    54 apply (unfold setlocs_def)
    55 apply (induct_tac s)
    56 apply auto
    57 apply (simp add: getlocs_def2)
    58 done
    59 
    60 lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])"
    61 apply (induct_tac Y)
    62 apply (rule_tac [2] ext)
    63 apply auto
    64 done
    65 
    66 (*unused*)
    67 lemma classic_Local_valid: 
    68 "!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.  
    69   c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}"
    70 apply (unfold hoare_valids_def)
    71 apply (simp (no_asm_use) add: triple_valid_def2)
    72 apply clarsimp
    73 apply (drule_tac x = "s<Y>" in spec)
    74 apply (tactic "smp_tac @{context} 1 1")
    75 apply (drule spec)
    76 apply (drule_tac x = "s[Loc Y::=a s]" in spec)
    77 apply (simp (no_asm_use))
    78 apply (erule (1) notE impE)
    79 apply (tactic "smp_tac @{context} 1 1")
    80 apply simp
    81 done
    82 
    83 lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.  
    84   c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}"
    85 apply (rule export_s)
    86 apply (rule hoare_derivs.Local [THEN conseq1])
    87 apply (erule spec)
    88 apply force
    89 done
    90 
    91 lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
    92   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
    93 apply (rule classic_Local)
    94 apply clarsimp
    95 apply (erule conseq12)
    96 apply clarsimp
    97 apply (drule sym)
    98 apply simp
    99 done
   100 
   101 lemma Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
   102   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
   103 apply (rule export_s)
   104 apply (rule hoare_derivs.Local)
   105 apply clarsimp
   106 done
   107 
   108 lemma weak_Local_indep: "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
   109   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
   110 apply (rule weak_Local)
   111 apply auto
   112 done
   113 
   114 
   115 lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
   116 apply (rule export_s)
   117 apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12)
   118 prefer 2
   119 apply  clarsimp
   120 apply (rule hoare_derivs.Local)
   121 apply clarsimp
   122 apply (rule trueI)
   123 done
   124 
   125 lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
   126 apply (rule classic_Local)
   127 apply clarsimp
   128 apply (rule trueI [THEN conseq12])
   129 apply clarsimp
   130 done
   131 
   132 lemma Call_invariant: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==>  
   133   G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}.  
   134   X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}"
   135 apply (rule_tac s'1 = "s'" and
   136   Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in
   137   hoare_derivs.Call [THEN conseq12])
   138 apply  (simp (no_asm_simp) add: getlocs_setlocs_lemma)
   139 apply force
   140 done
   141 
   142 end