-
Notifications
You must be signed in to change notification settings - Fork 0
/
Imperative_Loops.thy
129 lines (116 loc) · 3.94 KB
/
Imperative_Loops.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
theory Imperative_Loops
imports
"Refine_Imperative_HOL.Sepref_HOL_Bindings"
"Refine_Imperative_HOL.Pf_Mono_Prover"
"Refine_Imperative_HOL.Pf_Add"
begin
section \<open>Imperative Loops\<close>
text "An auxiliary while rule provided by Peter Lammich."
lemma heap_WHILET_rule:
assumes
"wf R"
"P \<Longrightarrow>\<^sub>A I s"
"\<And>s. <I s * true> bi s <\<lambda>r. I s * \<up>(r \<longleftrightarrow> b s)>\<^sub>t"
"\<And>s. b s \<Longrightarrow> <I s * true> f s <\<lambda>s'. I s' * \<up>((s', s) \<in> R)>\<^sub>t"
"\<And>s. \<not> b s \<Longrightarrow> I s \<Longrightarrow>\<^sub>A Q s"
shows "<P * true> heap_WHILET bi f s <Q>\<^sub>t"
proof -
have "<I s * true> heap_WHILET bi f s <\<lambda>s'. I s' * \<up>(\<not> b s')>\<^sub>t"
using assms(1)
proof (induction arbitrary:)
case (less s)
show ?case
proof (cases "b s")
case True
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3,4) less)
next
case False
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
qed
qed
then show ?thesis
apply (rule cons_rule[rotated 2])
apply (intro ent_star_mono assms(2) ent_refl)
apply clarsimp
apply (intro ent_star_mono assms(5) ent_refl)
.
qed
lemma heap_WHILET_rule':
assumes
"wf R"
"P \<Longrightarrow>\<^sub>A I s si * F"
"\<And>si s. <I s si * F> bi si <\<lambda>r. I s si * F * \<up>(r \<longleftrightarrow> b s)>\<^sub>t"
"\<And>si s. b s \<Longrightarrow> <I s si * F> f si <\<lambda>si'. \<exists>\<^sub>As'. I s' si' * F * \<up>((s', s) \<in> R)>\<^sub>t"
"\<And>si s. \<not> b s \<Longrightarrow> I s si * F \<Longrightarrow>\<^sub>A Q s si"
shows "<P> heap_WHILET bi f si <\<lambda>si. \<exists>\<^sub>As. Q s si>\<^sub>t"
proof -
have "<I s si * F> heap_WHILET bi f si <\<lambda>si'. \<exists>\<^sub>As'. I s' si' * F * \<up>(\<not> b s')>\<^sub>t"
using assms(1)
proof (induction arbitrary: si)
case (less s)
show ?case
proof (cases "b s")
case True
then show ?thesis
apply (subst heap_WHILET_unfold)
apply (sep_auto heap: assms(3,4) less)
done
next
case False
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
qed
qed
then show ?thesis
apply (rule cons_rule[rotated 2])
apply (intro ent_star_mono assms(2) ent_refl)
apply clarsimp
apply (sep_auto )
apply (erule ent_frame_fwd[OF assms(5)])
apply frame_inference
by sep_auto
qed
(* Added by NM, just a technicality since this rule fits our use case better *)
text "I derived my own version,
simply because it was a better fit to my use case."
corollary heap_WHILET_rule'':
assumes
"wf R"
"P \<Longrightarrow>\<^sub>A I s"
"\<And>s. <I s * true> bi s <\<lambda>r. I s * \<up>(r \<longleftrightarrow> b s)>\<^sub>t"
"\<And>s. b s \<Longrightarrow> <I s * true> f s <\<lambda>s'. I s' * \<up>((s', s) \<in> R)>\<^sub>t"
"\<And>s. \<not> b s \<Longrightarrow> I s \<Longrightarrow>\<^sub>A Q s"
shows "<P> heap_WHILET bi f s <Q>\<^sub>t"
supply R = heap_WHILET_rule'[of R P "\<lambda>s si. \<up>(s = si) * I s" s _ true bi b f "\<lambda>s si.\<up>(s = si) * Q s * true"]
thm R
using assms ent_true_drop apply(sep_auto heap: R assms)
done
(*
explicit proof:
proof -
have "<I s * true> heap_WHILET bi f s <\<lambda>s'. I s' * \<up>(\<not> b s')>\<^sub>t"
using assms(1)
proof (induction arbitrary:)
case (less s)
show ?case
proof (cases "b s")
case True
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3,4) less)
next
case False
then show ?thesis
by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
qed
qed
then show ?thesis
apply (rule cons_rule[rotated 2])
apply (intro ent_true_drop assms(2) ent_refl)
apply clarsimp
apply(intro ent_star_mono assms(5) ent_refl)
.
qed
*)
end