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