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