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