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