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
```