author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37604  1840dc0265da 
child 51717  9e7d1c139569 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/Equivalence.thy 
2 
Author: David von Oheimb 

3 
Copyright 2001 Technische Universitaet Muenchen 

4 
*) 

5 

6 
header "Equivalence of Operational and Axiomatic Semantics" 

7 

16417  8 
theory Equivalence imports OpSem AxSem begin 
11376  9 

10 
subsection "Validity" 

11 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

12 
definition valid :: "[assn,stmt, assn] => bool" ("= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where 
23755  13 
"= {P} c {Q} \<equiv> \<forall>s t. P s > (\<exists>n. s c n\<rightarrow> t) > Q t" 
11476  14 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

15 
definition evalid :: "[assn,expr,vassn] => bool" ("=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where 
23755  16 
"=e {P} e {Q} \<equiv> \<forall>s v t. P s > (\<exists>n. s e\<succ>vn\<rightarrow> t) > Q v t" 
11476  17 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

18 
definition nvalid :: "[nat, triple ] => bool" ("=_: _" [61,61] 60) where 
23755  19 
"=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s c n\<rightarrow> t > P s > Q t" 
11376  20 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

21 
definition envalid :: "[nat,etriple ] => bool" ("=_:e _" [61,61] 60) where 
23755  22 
"=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s e\<succ>vn\<rightarrow> t > P s > Q v t" 
11476  23 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

24 
definition nvalids :: "[nat, triple set] => bool" ("=_: _" [61,61] 60) where 
11376  25 
"=n: T \<equiv> \<forall>t\<in>T. =n: t" 
26 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

27 
definition cnvalids :: "[triple set,triple set] => bool" ("_ =/ _" [61,61] 60) where 
11476  28 
"A = C \<equiv> \<forall>n. =n: A > =n: C" 
29 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

30 
definition cenvalid :: "[triple set,etriple ] => bool" ("_ =e/ _" [61,61] 60) where 
11476  31 
"A =e t \<equiv> \<forall>n. =n: A > =n:e t" 
11376  32 

35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

33 
notation (xsymbols) 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

34 
valid ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

35 
evalid ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

36 
nvalid ("\<Turnstile>_: _" [61,61] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

37 
envalid ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

38 
nvalids ("\<Turnstile>_: _" [61,61] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

39 
cnvalids ("_ \<Turnstile>/ _" [61,61] 60) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

40 
cenvalid ("_ \<Turnstile>\<^sub>e/ _"[61,61] 60) 
11376  41 

42 

11476  43 
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t" 
11376  44 
by (simp add: nvalid_def Let_def) 
45 

11476  46 
lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))" 
47 
apply (simp add: valid_def nvalid_def2) 

11376  48 
apply blast 
49 
done 

50 

11486  51 
lemma envalid_def2: "\<Turnstile>n:\<^sub>e (P,e,Q) \<equiv> \<forall>s v t. s e\<succ>vn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t" 
11476  52 
by (simp add: envalid_def Let_def) 
53 

11486  54 
lemma evalid_def2: "\<Turnstile>\<^sub>e {P} e {Q} = (\<forall>n. \<Turnstile>n:\<^sub>e (P,e,Q))" 
11476  55 
apply (simp add: evalid_def envalid_def2) 
56 
apply blast 

57 
done 

58 

59 
lemma cenvalid_def2: 

11486  60 
"A\<Turnstile>\<^sub>e (P,e,Q) = (\<forall>n. \<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s e\<succ>vn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))" 
11476  61 
by(simp add: cenvalid_def envalid_def2) 
62 

11376  63 

64 
subsection "Soundness" 

65 

11476  66 
declare exec_elim_cases [elim!] eval_elim_cases [elim!] 
11376  67 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

68 
lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)" 
11476  69 
by (clarsimp simp add: nvalid_def2) 
11376  70 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

71 
lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl M,Q)" 
11476  72 
by (clarsimp simp add: nvalid_def2) 
11376  73 

74 
lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t" 

11476  75 
by (force simp add: split_paired_all nvalid_def2 intro: exec_mono) 
11376  76 

77 
lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow> Ball A (nvalid n)" 

78 
by (fast intro: nvalid_SucD) 

79 

80 
lemma Loop_sound_lemma [rule_format (no_asm)]: 

11476  81 
"\<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
82 
(s c0n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)" 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
12934
diff
changeset

83 
apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1]) 
11376  84 
apply clarsimp+ 
85 
done 

86 

87 
lemma Impl_sound_lemma: 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

88 
"\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
12742  89 
Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)" 
11376  90 
by blast 
91 

11476  92 
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" 
93 
by fast 

94 

95 
lemma all3_conjunct2: 

96 
"\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l" 

97 
by fast 

98 

99 
lemma cnvalid1_eq: 

100 
"A \<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. \<Turnstile>n: A \<longrightarrow> (\<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" 

101 
by(simp add: cnvalids_def nvalids_def nvalid_def2) 

102 

11486  103 
lemma hoare_sound_main:"\<And>t. (A \<turnstile> C \<longrightarrow> A \<Turnstile> C) \<and> (A \<turnstile>\<^sub>e t \<longrightarrow> A \<Turnstile>\<^sub>e t)" 
11476  104 
apply (tactic "split_all_tac 1", rename_tac P e Q) 
105 
apply (rule hoare_ehoare.induct) 

12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

106 
(*18*) 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23755
diff
changeset

107 
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *}) 
27239  108 
apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *}) 
109 
apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) 

11476  110 
apply (simp_all only: cnvalid1_eq cenvalid_def2) 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

111 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

112 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

113 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

114 
apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

115 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

116 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

117 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

118 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

119 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

120 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

121 
apply (clarsimp del: Meth_elim_cases) (* Call *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

122 
apply (force del: Impl_elim_cases) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

123 
defer 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

124 
prefer 4 apply blast (* Conseq *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

125 
prefer 4 apply blast (* eConseq *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

126 
apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

127 
apply blast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

128 
apply blast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

129 
apply blast 
11376  130 
apply (rule allI) 
11565  131 
apply (rule_tac x=Z in spec) 
11376  132 
apply (induct_tac "n") 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

133 
apply (clarify intro!: Impl_nvalid_0) 
11376  134 
apply (clarify intro!: Impl_nvalid_Suc) 
135 
apply (drule nvalids_SucD) 

37604  136 
apply (simp only: HOL.all_simps) 
11376  137 
apply (erule (1) impE) 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

138 
apply (drule (2) Impl_sound_lemma) 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

139 
apply blast 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

140 
apply assumption 
11376  141 
done 
142 

143 
theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" 

144 
apply (simp only: valid_def2) 

11476  145 
apply (drule hoare_sound_main [THEN conjunct1, rule_format]) 
11376  146 
apply (unfold cnvalids_def nvalids_def) 
147 
apply fast 

148 
done 

149 

11486  150 
theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}" 
11476  151 
apply (simp only: evalid_def2) 
152 
apply (drule hoare_sound_main [THEN conjunct2, rule_format]) 

153 
apply (unfold cenvalid_def nvalids_def) 

154 
apply fast 

155 
done 

156 

11376  157 

158 
subsection "(Relative) Completeness" 

159 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

160 
definition MGT :: "stmt => state => triple" where 
23755  161 
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z c n\<rightarrow> t)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

162 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

163 
definition MGTe :: "expr => state => etriple" where 
23755  164 
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z e\<succ>vn\<rightarrow> t)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27239
diff
changeset

165 

35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

166 
notation (xsymbols) 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

167 
MGTe ("MGT\<^sub>e") 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

168 
notation (HTML output) 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
27239
diff
changeset

169 
MGTe ("MGT\<^sub>e") 
11376  170 

171 
lemma MGF_implies_complete: 

11565  172 
"\<forall>Z. {} \<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" 
11376  173 
apply (simp only: valid_def2) 
174 
apply (unfold MGT_def) 

11476  175 
apply (erule hoare_ehoare.Conseq) 
176 
apply (clarsimp simp add: nvalid_def2) 

11376  177 
done 
178 

11476  179 
lemma eMGF_implies_complete: 
11565  180 
"\<forall>Z. {} \<turnstile>\<^sub>e MGT\<^sub>e e Z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}" 
11476  181 
apply (simp only: evalid_def2) 
11486  182 
apply (unfold MGTe_def) 
11476  183 
apply (erule hoare_ehoare.eConseq) 
184 
apply (clarsimp simp add: envalid_def2) 

185 
done 

11376  186 

11476  187 
declare exec_eval.intros[intro!] 
11376  188 

11565  189 
lemma MGF_Loop: "\<forall>Z. A \<turnstile> {op = Z} c {\<lambda>t. \<exists>n. Z cn\<rightarrow> t} \<Longrightarrow> 
190 
A \<turnstile> {op = Z} While (x) c {\<lambda>t. \<exists>n. Z While (x) cn\<rightarrow> t}" 

191 
apply (rule_tac P' = "\<lambda>Z s. (Z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s cn\<rightarrow> t})^*" 

11476  192 
in hoare_ehoare.Conseq) 
11376  193 
apply (rule allI) 
11476  194 
apply (rule hoare_ehoare.Loop) 
195 
apply (erule hoare_ehoare.Conseq) 

11376  196 
apply clarsimp 
197 
apply (blast intro:rtrancl_into_rtrancl) 

198 
apply (erule thin_rl) 

199 
apply clarsimp 

11565  200 
apply (erule_tac x = Z in allE) 
11376  201 
apply clarsimp 
202 
apply (erule converse_rtrancl_induct) 

203 
apply blast 

204 
apply clarsimp 

11476  205 
apply (drule (1) exec_exec_max) 
11376  206 
apply (blast del: exec_elim_cases) 
207 
done 

208 

11565  209 
lemma MGF_lemma: "\<forall>M Z. A \<turnstile> {MGT (Impl M) Z} \<Longrightarrow> 
210 
(\<forall>Z. A \<turnstile> {MGT c Z}) \<and> (\<forall>Z. A \<turnstile>\<^sub>e MGT\<^sub>e e Z)" 

11486  211 
apply (simp add: MGT_def MGTe_def) 
11476  212 
apply (rule stmt_expr.induct) 
213 
apply (rule_tac [!] allI) 

11376  214 

11476  215 
apply (rule Conseq1 [OF hoare_ehoare.Skip]) 
11376  216 
apply blast 
217 

11476  218 
apply (rule hoare_ehoare.Comp) 
11376  219 
apply (erule spec) 
11476  220 
apply (erule hoare_ehoare.Conseq) 
11376  221 
apply clarsimp 
11476  222 
apply (drule (1) exec_exec_max) 
11376  223 
apply blast 
224 

11476  225 
apply (erule thin_rl) 
226 
apply (rule hoare_ehoare.Cond) 

227 
apply (erule spec) 

228 
apply (rule allI) 

229 
apply (simp) 

230 
apply (rule conjI) 

231 
apply (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max, 

232 
erule thin_rl, erule thin_rl, force)+ 

11376  233 

234 
apply (erule MGF_Loop) 

235 

11476  236 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss]) 
237 
apply fast 

11376  238 

11476  239 
apply (erule thin_rl) 
11565  240 
apply (rule_tac Q = "\<lambda>a s. \<exists>n. Z expr1\<succ>Addr an\<rightarrow> s" in hoare_ehoare.FAss) 
11476  241 
apply (drule spec) 
242 
apply (erule eConseq2) 

243 
apply fast 

244 
apply (rule allI) 

245 
apply (erule hoare_ehoare.eConseq) 

246 
apply clarsimp 

247 
apply (drule (1) eval_eval_max) 

11376  248 
apply blast 
249 

11507  250 
apply (simp only: split_paired_all) 
11476  251 
apply (rule hoare_ehoare.Meth) 
11376  252 
apply (rule allI) 
11476  253 
apply (drule spec, drule spec, erule hoare_ehoare.Conseq) 
11376  254 
apply blast 
255 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

256 
apply (simp add: split_paired_all) 
11476  257 

258 
apply (rule eConseq1 [OF hoare_ehoare.NewC]) 

259 
apply blast 

260 

261 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast]) 

262 
apply fast 

263 

264 
apply (rule eConseq1 [OF hoare_ehoare.LAcc]) 

265 
apply blast 

266 

267 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc]) 

268 
apply fast 

269 

11565  270 
apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. Z expr1\<succ>an1\<rightarrow> t \<and> t expr2\<succ>vn2\<rightarrow> s" in 
11476  271 
hoare_ehoare.Call) 
272 
apply (erule spec) 

273 
apply (rule allI) 

274 
apply (erule hoare_ehoare.eConseq) 

275 
apply clarsimp 

276 
apply blast 

277 
apply (rule allI)+ 

278 
apply (rule hoare_ehoare.Meth) 

279 
apply (rule allI) 

280 
apply (drule spec, drule spec, erule hoare_ehoare.Conseq) 

281 
apply (erule thin_rl, erule thin_rl) 

282 
apply (clarsimp del: Impl_elim_cases) 

283 
apply (drule (2) eval_eval_exec_max) 

11565  284 
apply (force del: Impl_elim_cases) 
11376  285 
done 
286 

11565  287 
lemma MGF_Impl: "{} \<turnstile> {MGT (Impl M) Z}" 
11376  288 
apply (unfold MGT_def) 
12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

289 
apply (rule Impl1') 
11376  290 
apply (rule_tac [2] UNIV_I) 
291 
apply clarsimp 

11476  292 
apply (rule hoare_ehoare.ConjI) 
11376  293 
apply clarsimp 
294 
apply (rule ssubst [OF Impl_body_eq]) 

295 
apply (fold MGT_def) 

11476  296 
apply (rule MGF_lemma [THEN conjunct1, rule_format]) 
297 
apply (rule hoare_ehoare.Asm) 

11376  298 
apply force 
299 
done 

300 

301 
theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" 

302 
apply (rule MGF_implies_complete) 

303 
apply (erule_tac [2] asm_rl) 

304 
apply (rule allI) 

11476  305 
apply (rule MGF_lemma [THEN conjunct1, rule_format]) 
306 
apply (rule MGF_Impl) 

307 
done 

308 

11486  309 
theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}" 
11476  310 
apply (rule eMGF_implies_complete) 
311 
apply (erule_tac [2] asm_rl) 

312 
apply (rule allI) 

313 
apply (rule MGF_lemma [THEN conjunct2, rule_format]) 

11376  314 
apply (rule MGF_Impl) 
315 
done 

316 

11565  317 
lemma cFalse: "A \<turnstile> {\<lambda>s. False} c {Q}" 
318 
apply (rule cThin) 

319 
apply (rule hoare_relative_complete) 

320 
apply (auto simp add: valid_def) 

321 
done 

322 

323 
lemma eFalse: "A \<turnstile>\<^sub>e {\<lambda>s. False} e {Q}" 

324 
apply (rule eThin) 

325 
apply (rule ehoare_relative_complete) 

326 
apply (auto simp add: evalid_def) 

327 
done 

328 

11376  329 
end 