--- a/CONTRIBUTORS Sat Dec 05 19:09:39 2020 +0100
+++ b/CONTRIBUTORS Sat Dec 05 19:30:37 2020 +0100
@@ -5,6 +5,9 @@
Contributions to this Isabelle version
--------------------------------------
+* December 2020 Walter Guttmann
+ Extension of session HOL/Hoare with total correctness proof system
+
* November 2020: Stepan Holub
Removed preconditions from lemma comm_append_are_replicate
--- a/NEWS Sat Dec 05 19:09:39 2020 +0100
+++ b/NEWS Sat Dec 05 19:30:37 2020 +0100
@@ -87,6 +87,8 @@
*** HOL ***
+* Session "Hoare" now provides a total correctness logic as well.
+
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
--- a/src/Doc/Isar_Ref/Spec.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Dec 05 19:30:37 2020 +0100
@@ -512,15 +512,12 @@
subsection \<open>Locale declarations\<close>
text \<open>
- \begin{tabular}{rcll}
+ \begin{tabular}{rcl}
@{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
@{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
@{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
- @{method_def intro_locales} & : & \<open>method\<close> \\
- @{method_def unfold_locales} & : & \<open>method\<close> \\
- @{attribute_def trace_locales} & : & \<open>attribute\<close> & default \<open>false\<close> \\
\end{tabular}
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
@@ -546,11 +543,10 @@
@'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
\<close>
- \<^descr> \<^theory_text>\<open>locale loc = import bundles + body\<close> defines a new locale \<open>loc\<close> as a context
- consisting of a certain view of existing locales (\<open>import\<close>) plus some
- additional elements (\<open>body\<close>); given \<open>bundles\<close> take effect in the surface
- context within both \<open>import\<close> and \<open>body\<close> and the potentially following
- \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block. Each part is optional; the
+ \<^descr> \<^theory_text>\<open>locale loc = import opening bundles + body\<close> defines a new locale \<open>loc\<close>
+ as a context consisting of a certain view of existing locales (\<open>import\<close>) plus some
+ additional elements (\<open>body\<close>) with declaration \<open>bundles\<close> enriching the context
+ of the command itself. All \<open>import\<close>, \<open>bundles\<close> and \<open>body\<close> are optional; the
degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be
useful to collect declarations of facts later on. Type-inference on locale
expressions automatically takes care of the most general typing that the
@@ -565,7 +561,11 @@
and provides a notational convenience for the inheritance of parameters in
locale declarations.
- The \<open>body\<close> consists of context elements.
+ Declarations from \<open>bundles\<close>, see \secref{sec:bundle}, are effective in the
+ entire command including a subsequent \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block, but they do
+ not contribute to the declarations stored in the locale.
+
+ The \<open>body\<close> consists of context elements:
\<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close>
and mixfix annotation \<open>mx\<close> (both are optional). The special syntax
@@ -619,7 +619,7 @@
Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided
as well.
- \<^descr> \<^theory_text>\<open>experiment exprs begin\<close> opens an anonymous locale context with private
+ \<^descr> \<^theory_text>\<open>experiment body begin\<close> opens an anonymous locale context with private
naming policy. Specifications in its body are inaccessible from outside.
This is useful to perform experiments, without polluting the name space.
@@ -632,20 +632,6 @@
\<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse
diagram. This includes locales defined as type classes (\secref{sec:class}).
-
- \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all
- introduction rules of locale predicates of the theory. While @{method
- intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore
- does not descend to assumptions, @{method unfold_locales} is more aggressive
- and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale
- specifications entailed by the context, both from target statements, and
- from interpretations (see below). New goals that are entailed by the current
- context are discharged automatically.
-
- \<^descr> @{attribute trace_locales}, when set to
- \<open>true\<close>, prints the locale instances activated during
- roundup. Useful for understanding local theories created by complex
- locale hierarchies.
\<close>
@@ -658,6 +644,9 @@
@{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
@{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
@{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
+ @{method_def intro_locales} & : & \<open>method\<close> \\
+ @{method_def unfold_locales} & : & \<open>method\<close> \\
+ @{attribute_def trace_locales} & : & \mbox{\<open>attribute\<close> \quad default \<open>false\<close>} \\
\end{matharray}
Locales may be instantiated, and the resulting instantiated declarations
@@ -733,7 +722,7 @@
proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
universally quantified.
- \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>
+ \<^descr> \<^theory_text>\<open>global_interpretation expr defines defs\<close> interprets \<open>expr\<close>
into a global theory.
When adding declarations to locales, interpreted versions of these
@@ -775,6 +764,26 @@
\<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
declarations.
+ \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all
+ introduction rules of locale predicates of the theory. While @{method
+ intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore
+ does not descend to assumptions, @{method unfold_locales} is more aggressive
+ and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale
+ specifications entailed by the context, both from target statements, and
+ from interpretations (see below). New goals that are entailed by the current
+ context are discharged automatically.
+
+ While @{method unfold_locales} is part of the default method for \<^theory_text>\<open>proof\<close>
+ and often invoked ``behind the scenes'', @{method intro_locales} helps
+ understand which proof obligations originated from which locale instances.
+ The latter method is useful while developing proofs but rare in finished
+ developments.
+
+ \<^descr> @{attribute trace_locales}, when set to \<open>true\<close>, prints the locale
+ instances activated during roundup. Use this when locale commands yield
+ obscure errors or for understanding local theories created by complex locale
+ hierarchies.
+
\begin{warn}
If a global theory inherits declarations (body elements) for a locale from
one parent and an interpretation of that locale from another parent, the
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Sat Dec 05 19:30:37 2020 +0100
@@ -59,33 +59,25 @@
subsubsection \<open>Invariants\<close>
-text \<open>Binomial invariant\<close>
+text \<open>Binomial tree\<close>
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
"invar_btree (Node r x ts) \<longleftrightarrow>
(\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
-definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
-"invar_bheap ts
- \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (<) (map rank ts))"
-
text \<open>Ordering (heap) invariant\<close>
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
"invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
-definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
-"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
+definition "invar_tree t \<longleftrightarrow> invar_btree t \<and> invar_otree t"
-definition invar :: "'a::linorder heap \<Rightarrow> bool" where
-"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
+text \<open>Binomial Heap invariant\<close>
+definition "invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_tree t) \<and> (sorted_wrt (<) (map rank ts))"
+
text \<open>The children of a node are a valid heap\<close>
-lemma invar_oheap_children:
- "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"
-by (auto simp: invar_oheap_def)
-
-lemma invar_bheap_children:
- "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
-by (auto simp: invar_bheap_def rev_map[symmetric])
+lemma invar_children:
+ "invar_tree (Node r v ts) \<Longrightarrow> invar (rev ts)"
+ by (auto simp: invar_tree_def invar_def rev_map[symmetric])
subsection \<open>Operations and Their Functional Correctness\<close>
@@ -102,19 +94,12 @@
end
-lemma invar_btree_link:
- assumes "invar_btree t\<^sub>1"
- assumes "invar_btree t\<^sub>2"
+lemma invar_link:
+ assumes "invar_tree t\<^sub>1"
+ assumes "invar_tree t\<^sub>2"
assumes "rank t\<^sub>1 = rank t\<^sub>2"
- shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
-using assms
-by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
-
-lemma invar_otree_link:
- assumes "invar_otree t\<^sub>1"
- assumes "invar_otree t\<^sub>2"
- shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
-using assms
+ shows "invar_tree (link t\<^sub>1 t\<^sub>2)"
+using assms unfolding invar_tree_def
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
@@ -130,29 +115,21 @@
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
(if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
-lemma invar_bheap_Cons[simp]:
- "invar_bheap (t#ts)
- \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
-by (auto simp: invar_bheap_def)
+lemma invar_tree0[simp]: "invar_tree (Node 0 x [])"
+unfolding invar_tree_def by auto
-lemma invar_btree_ins_tree:
- assumes "invar_btree t"
- assumes "invar_bheap ts"
+lemma invar_Cons[simp]:
+ "invar (t#ts)
+ \<longleftrightarrow> invar_tree t \<and> invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
+by (auto simp: invar_def)
+
+lemma invar_ins_tree:
+ assumes "invar_tree t"
+ assumes "invar ts"
assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
- shows "invar_bheap (ins_tree t ts)"
+ shows "invar (ins_tree t ts)"
using assms
-by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
-
-lemma invar_oheap_Cons[simp]:
- "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"
-by (auto simp: invar_oheap_def)
-
-lemma invar_oheap_ins_tree:
- assumes "invar_otree t"
- assumes "invar_oheap ts"
- shows "invar_oheap (ins_tree t ts)"
-using assms
-by (induction t ts rule: ins_tree.induct) (auto simp: invar_otree_link)
+by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric])
lemma mset_heap_ins_tree[simp]:
"mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
@@ -174,7 +151,7 @@
"insert x ts = ins_tree (Node 0 x []) ts"
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
-by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)
+by (auto intro!: invar_ins_tree simp: insert_def)
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
by(auto simp: insert_def)
@@ -208,54 +185,79 @@
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
(auto split: if_splits simp: ins_tree_rank_bound)
-lemma invar_bheap_merge:
- assumes "invar_bheap ts\<^sub>1"
- assumes "invar_bheap ts\<^sub>2"
- shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
+lemma invar_merge[simp]:
+ assumes "invar ts\<^sub>1"
+ assumes "invar ts\<^sub>2"
+ shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
+using assms
+by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
+ (auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound)
+
+
+text \<open>Longer, more explicit proof of @{thm [source] invar_merge},
+ to illustrate the application of the @{thm [source] merge_rank_bound} lemma.\<close>
+lemma
+ assumes "invar ts\<^sub>1"
+ assumes "invar ts\<^sub>2"
+ shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
using assms
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
-
- from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"
+ \<comment> \<open>Invariants of the parts can be shown automatically\<close>
+ from "3.prems" have [simp]:
+ "invar_tree t\<^sub>1" "invar_tree t\<^sub>2"
+ (*"invar (merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2)"
+ "invar (merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2))"
+ "invar (merge ts\<^sub>1 ts\<^sub>2)"*)
by auto
+ \<comment> \<open>These are the three cases of the @{const merge} function\<close>
consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
| (GT) "rank t\<^sub>1 > rank t\<^sub>2"
| (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
using antisym_conv3 by blast
then show ?case proof cases
- case LT
- then show ?thesis using 3
- by (force elim!: merge_rank_bound)
+ case LT
+ \<comment> \<open>@{const merge} takes the first tree from the left heap\<close>
+ then have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)" by simp
+ also have "invar \<dots>" proof (simp, intro conjI)
+ \<comment> \<open>Invariant follows from induction hypothesis\<close>
+ show "invar (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2))"
+ using LT "3.IH" "3.prems" by simp
+
+ \<comment> \<open>It remains to show that \<open>t\<^sub>1\<close> has smallest rank.\<close>
+ show "\<forall>t'\<in>set (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)). rank t\<^sub>1 < rank t'"
+ \<comment> \<open>Which is done by auxiliary lemma @{thm [source] merge_rank_bound}\<close>
+ using LT "3.prems" by (force elim!: merge_rank_bound)
+ qed
+ finally show ?thesis .
next
- case GT
- then show ?thesis using 3
- by (force elim!: merge_rank_bound)
+ \<comment> \<open>@{const merge} takes the first tree from the right heap\<close>
+ case GT
+ \<comment> \<open>The proof is anaologous to the \<open>LT\<close> case\<close>
+ then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound)
next
case [simp]: EQ
-
- from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
- by auto
+ \<comment> \<open>@{const merge} links both first trees, and inserts them into the merged remaining heaps\<close>
+ have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)" by simp
+ also have "invar \<dots>" proof (intro invar_ins_tree invar_link)
+ \<comment> \<open>Invariant of merged remaining heaps follows by IH\<close>
+ show "invar (merge ts\<^sub>1 ts\<^sub>2)"
+ using EQ "3.prems" "3.IH" by auto
- have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
- using that
- apply (rule merge_rank_bound)
- using "3.prems" by auto
- with EQ show ?thesis
- by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link)
+ \<comment> \<open>For insertion, we have to show that the rank of the linked tree is \<open>\<le>\<close> the
+ ranks in the merged remaining heaps\<close>
+ show "\<forall>t'\<in>set (merge ts\<^sub>1 ts\<^sub>2). rank (link t\<^sub>1 t\<^sub>2) \<le> rank t'"
+ proof -
+ \<comment> \<open>Which is, again, done with the help of @{thm [source] merge_rank_bound}\<close>
+ have "rank (link t\<^sub>1 t\<^sub>2) = Suc (rank t\<^sub>2)" by simp
+ thus ?thesis using "3.prems" by (auto simp: Suc_le_eq elim!: merge_rank_bound)
+ qed
+ qed simp_all
+ finally show ?thesis .
qed
-qed simp_all
+qed auto
-lemma invar_oheap_merge:
- assumes "invar_oheap ts\<^sub>1"
- assumes "invar_oheap ts\<^sub>2"
- shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
-using assms
-by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
- (auto simp: invar_oheap_ins_tree invar_otree_link)
-
-lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
-by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
lemma mset_heap_merge[simp]:
"mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
@@ -267,32 +269,25 @@
"get_min [t] = root t"
| "get_min (t#ts) = min (root t) (get_min ts)"
-lemma invar_otree_root_min:
- assumes "invar_otree t"
+lemma invar_tree_root_min:
+ assumes "invar_tree t"
assumes "x \<in># mset_tree t"
shows "root t \<le> x"
-using assms
+using assms unfolding invar_tree_def
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
-lemma get_min_mset_aux:
- assumes "ts\<noteq>[]"
- assumes "invar_oheap ts"
- assumes "x \<in># mset_heap ts"
- shows "get_min ts \<le> x"
- using assms
-apply (induction ts arbitrary: x rule: get_min.induct)
-apply (auto
- simp: invar_otree_root_min min_def intro: order_trans;
- meson linear order_trans invar_otree_root_min
- )+
-done
-
lemma get_min_mset:
assumes "ts\<noteq>[]"
assumes "invar ts"
assumes "x \<in># mset_heap ts"
shows "get_min ts \<le> x"
-using assms by (auto simp: invar_def get_min_mset_aux)
+ using assms
+apply (induction ts arbitrary: x rule: get_min.induct)
+apply (auto
+ simp: invar_tree_root_min min_def intro: order_trans;
+ meson linear order_trans invar_tree_root_min
+ )+
+done
lemma get_min_member:
"ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
@@ -333,13 +328,13 @@
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
by auto
-lemma invar_bheap_get_min_rest:
+lemma invar_get_min_rest:
assumes "get_min_rest ts = (t',ts')"
assumes "ts\<noteq>[]"
- assumes "invar_bheap ts"
- shows "invar_btree t'" and "invar_bheap ts'"
+ assumes "invar ts"
+ shows "invar_tree t'" and "invar ts'"
proof -
- have "invar_btree t' \<and> invar_bheap ts'"
+ have "invar_tree t' \<and> invar ts'"
using assms
proof (induction ts arbitrary: t' ts' rule: get_min.induct)
case (2 t v va)
@@ -348,17 +343,9 @@
apply (drule set_get_min_rest; fastforce)
done
qed auto
- thus "invar_btree t'" and "invar_bheap ts'" by auto
+ thus "invar_tree t'" and "invar ts'" by auto
qed
-lemma invar_oheap_get_min_rest:
- assumes "get_min_rest ts = (t',ts')"
- assumes "ts\<noteq>[]"
- assumes "invar_oheap ts"
- shows "invar_otree t'" and "invar_oheap ts'"
-using assms
-by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
-
subsubsection \<open>\<open>del_min\<close>\<close>
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
@@ -370,12 +357,11 @@
assumes "invar ts"
shows "invar (del_min ts)"
using assms
-unfolding invar_def del_min_def
+unfolding del_min_def
by (auto
split: prod.split tree.split
- intro!: invar_bheap_merge invar_oheap_merge
- dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
- intro!: invar_oheap_children invar_bheap_children
+ intro!: invar_merge invar_children
+ dest: invar_get_min_rest
)
lemma mset_heap_del_min:
@@ -412,7 +398,7 @@
next
case (5 q) thus ?case using get_min[of q] by auto
next
- case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
+ case 6 thus ?case by (auto simp add: invar_def)
next
case 7 thus ?case by simp
next
@@ -453,15 +439,21 @@
by (simp)
qed
+lemma size_mset_tree:
+ assumes "invar_tree t"
+ shows "size (mset_tree t) = 2^rank t"
+using assms unfolding invar_tree_def
+by (simp add: size_mset_btree)
+
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
-lemma size_mset_bheap:
- assumes "invar_bheap ts"
+lemma size_mset_heap:
+ assumes "invar ts"
shows "2^length ts \<le> size (mset_heap ts) + 1"
proof -
- from \<open>invar_bheap ts\<close> have
+ from \<open>invar ts\<close> have
ASC: "sorted_wrt (<) (map rank ts)" and
- TINV: "\<forall>t\<in>set ts. invar_btree t"
- unfolding invar_bheap_def by auto
+ TINV: "\<forall>t\<in>set ts. invar_tree t"
+ unfolding invar_def by auto
have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
by (simp add: sum_power2)
@@ -470,7 +462,7 @@
using power_increasing[where a="2::nat"]
by (auto simp: o_def)
also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
- by (auto cong: map_cong simp: size_mset_btree)
+ by (auto cong: map_cong simp: size_mset_tree)
also have "\<dots> = size (mset_heap ts) + 1"
unfolding mset_heap_def by (induction ts) auto
finally show ?thesis .
@@ -509,7 +501,7 @@
unfolding T_insert_def by (rule T_ins_tree_simple_bound)
also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
proof -
- from size_mset_bheap[of ts] assms
+ from size_mset_heap[of ts] assms
have "2 ^ length ts \<le> size (mset_heap ts) + 1"
unfolding invar_def by auto
hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
@@ -553,7 +545,7 @@
fixes ts\<^sub>1 ts\<^sub>2
defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
- assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
+ assumes BINVARS: "invar ts\<^sub>1" "invar ts\<^sub>2"
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
proof -
define n where "n = n\<^sub>1 + n\<^sub>2"
@@ -564,8 +556,8 @@
by (rule power_increasing) auto
also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
by (auto simp: algebra_simps power_add power_mult)
- also note BINVARS(1)[THEN size_mset_bheap]
- also note BINVARS(2)[THEN size_mset_bheap]
+ also note BINVARS(1)[THEN size_mset_heap]
+ also note BINVARS(2)[THEN size_mset_heap]
finally have "2 ^ T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
from le_log2_of_power[OF this] have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
@@ -608,7 +600,7 @@
have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
proof -
- from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
unfolding invar_def by auto
thus ?thesis using le_log2_of_power by blast
qed
@@ -625,14 +617,14 @@
by (induction ts rule: T_get_min_rest.induct) auto
lemma T_get_min_rest_bound_aux:
- assumes "invar_bheap ts"
+ assumes "invar ts"
assumes "ts\<noteq>[]"
shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
proof -
have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
proof -
- from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
by auto
thus ?thesis using le_log2_of_power by blast
qed
@@ -659,12 +651,12 @@
lemma T_rev_ts1_bound_aux:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
- assumes BINVAR: "invar_bheap (rev ts)"
+ assumes BINVAR: "invar (rev ts)"
shows "T_rev ts \<le> 1 + log 2 (n+1)"
proof -
have "T_rev ts = length ts + 1" by (auto simp: T_rev_def)
hence "2^T_rev ts = 2*2^length ts" by auto
- also have "\<dots> \<le> 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def)
+ also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def)
finally have "2 ^ T_rev ts \<le> 2 * n + 2" .
from le_log2_of_power[OF this] have "T_rev ts \<le> log 2 (2 * (n + 1))"
by auto
@@ -676,15 +668,15 @@
lemma T_del_min_bound_aux:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
- assumes BINVAR: "invar_bheap ts"
+ assumes BINVAR: "invar ts"
assumes "ts\<noteq>[]"
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
proof -
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
by (metis surj_pair tree.exhaust_sel)
- note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
- hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
+ note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+ hence BINVAR1: "invar (rev ts\<^sub>1)" by (blast intro: invar_children)
define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
@@ -706,7 +698,7 @@
also have "\<dots> \<le> 2*log 2 (n+1) + T_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
using T_rev_ts1_bound by auto
also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
- using T_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
+ using T_merge_bound_aux[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>]
by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
also have "n\<^sub>1 + n\<^sub>2 \<le> n"
unfolding n\<^sub>1_def n\<^sub>2_def n_def
--- a/src/HOL/Data_Structures/Tree23_Map.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Sat Dec 05 19:30:37 2020 +0100
@@ -98,14 +98,14 @@
subsection \<open>Balancedness\<close>
-lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
+lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> hI(upd x y t) = height t"
by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *)
corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
by (simp add: update_def complete_upd)
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
by(induction x t rule: del.induct)
(auto simp add: heights max_def height_split_min split: prod.split)
--- a/src/HOL/Data_Structures/Tree23_Set.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Sat Dec 05 19:30:37 2020 +0100
@@ -45,7 +45,7 @@
(case ins x l of
TI l' => TI (Node2 l' a r) |
OF l1 b l2 => TI (Node3 l1 b l2 a r)) |
- EQ \<Rightarrow> TI (Node2 l x r) |
+ EQ \<Rightarrow> TI (Node2 l a r) |
GT \<Rightarrow>
(case ins x r of
TI r' => TI (Node2 l a r') |
@@ -210,18 +210,11 @@
text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
-instantiation upI :: (type)height
-begin
+fun hI :: "'a upI \<Rightarrow> nat" where
+"hI (TI t) = height t" |
+"hI (OF l a r) = height l"
-fun height_upI :: "'a upI \<Rightarrow> nat" where
-"height (TI t) = height t" |
-"height (OF l a r) = height l"
-
-instance ..
-
-end
-
-lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> height(ins a t) = height t"
+lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> hI(ins a t) = height t"
by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
@@ -290,37 +283,30 @@
subsection "Proofs for delete"
-instantiation upD :: (type)height
-begin
-
-fun height_upD :: "'a upD \<Rightarrow> nat" where
-"height (TD t) = height t" |
-"height (UF t) = height t + 1"
-
-instance ..
-
-end
+fun hD :: "'a upD \<Rightarrow> nat" where
+"hD (TD t) = height t" |
+"hD (UF t) = height t + 1"
lemma complete_treeD_node21:
- "\<lbrakk>complete r; complete (treeD l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
+ "\<lbrakk>complete r; complete (treeD l'); height r = hD l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
by(induct l' a r rule: node21.induct) auto
lemma complete_treeD_node22:
- "\<lbrakk>complete(treeD r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
+ "\<lbrakk>complete(treeD r'); complete l; hD r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
by(induct l a r' rule: node22.induct) auto
lemma complete_treeD_node31:
- "\<lbrakk> complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
+ "\<lbrakk> complete (treeD l'); complete m; complete r; hD l' = height r; height m = height r \<rbrakk>
\<Longrightarrow> complete (treeD (node31 l' a m b r))"
by(induct l' a m b r rule: node31.induct) auto
lemma complete_treeD_node32:
- "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \<rbrakk>
+ "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; hD m' = height r \<rbrakk>
\<Longrightarrow> complete (treeD (node32 l a m' b r))"
by(induct l a m' b r rule: node32.induct) auto
lemma complete_treeD_node33:
- "\<lbrakk> complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \<rbrakk>
+ "\<lbrakk> complete l; complete m; complete(treeD r'); height l = hD r'; height m = hD r' \<rbrakk>
\<Longrightarrow> complete (treeD (node33 l a m b r'))"
by(induct l a m b r' rule: node33.induct) auto
@@ -328,37 +314,37 @@
complete_treeD_node31 complete_treeD_node32 complete_treeD_node33
lemma height'_node21:
- "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
+ "height r > 0 \<Longrightarrow> hD(node21 l' a r) = max (hD l') (height r) + 1"
by(induct l' a r rule: node21.induct)(simp_all)
lemma height'_node22:
- "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
+ "height l > 0 \<Longrightarrow> hD(node22 l a r') = max (height l) (hD r') + 1"
by(induct l a r' rule: node22.induct)(simp_all)
lemma height'_node31:
- "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
- max (height l) (max (height m) (height r)) + 1"
+ "height m > 0 \<Longrightarrow> hD(node31 l a m b r) =
+ max (hD l) (max (height m) (height r)) + 1"
by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
lemma height'_node32:
- "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
- max (height l) (max (height m) (height r)) + 1"
+ "height r > 0 \<Longrightarrow> hD(node32 l a m b r) =
+ max (height l) (max (hD m) (height r)) + 1"
by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
lemma height'_node33:
- "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
- max (height l) (max (height m) (height r)) + 1"
+ "height m > 0 \<Longrightarrow> hD(node33 l a m b r) =
+ max (height l) (max (height m) (hD r)) + 1"
by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
lemmas heights = height'_node21 height'_node22
height'_node31 height'_node32 height'_node33
lemma height_split_min:
- "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
+ "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> hD t' = height t"
by(induct t arbitrary: x t' rule: split_min.induct)
(auto simp: heights split: prod.splits)
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
by(induction x t rule: del.induct)
(auto simp: heights max_def height_split_min split: prod.splits)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ExamplesTC.thy Sat Dec 05 19:30:37 2020 +0100
@@ -0,0 +1,118 @@
+(* Title: Examples using Hoare Logic for Total Correctness
+ Author: Walter Guttmann
+*)
+
+section \<open>Examples using Hoare Logic for Total Correctness\<close>
+
+theory ExamplesTC
+
+imports Hoare_Logic
+
+begin
+
+text \<open>
+This theory demonstrates a few simple partial- and total-correctness proofs.
+The first example is taken from HOL/Hoare/Examples.thy written by N. Galm.
+We have added the invariant \<open>m \<le> a\<close>.
+\<close>
+
+lemma multiply_by_add: "VARS m s a b
+ {a=A \<and> b=B}
+ m := 0; s := 0;
+ WHILE m\<noteq>a
+ INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
+ DO s := s+b; m := m+(1::nat) OD
+ {s = A*B}"
+ by vcg_simp
+
+text \<open>
+Here is the total-correctness proof for the same program.
+It needs the additional invariant \<open>m \<le> a\<close>.
+\<close>
+
+lemma multiply_by_add_tc: "VARS m s a b
+ [a=A \<and> b=B]
+ m := 0; s := 0;
+ WHILE m\<noteq>a
+ INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
+ VAR {a-m}
+ DO s := s+b; m := m+(1::nat) OD
+ [s = A*B]"
+ apply vcg_tc_simp
+ by auto
+
+text \<open>
+Next, we prove partial correctness of a program that computes powers.
+\<close>
+
+lemma power: "VARS (p::int) i
+ { True }
+ p := 1;
+ i := 0;
+ WHILE i < n
+ INV { p = x^i \<and> i \<le> n }
+ DO p := p * x;
+ i := i + 1
+ OD
+ { p = x^n }"
+ apply vcg_simp
+ by auto
+
+text \<open>
+Here is its total-correctness proof.
+\<close>
+
+lemma power_tc: "VARS (p::int) i
+ [ True ]
+ p := 1;
+ i := 0;
+ WHILE i < n
+ INV { p = x^i \<and> i \<le> n }
+ VAR { n - i }
+ DO p := p * x;
+ i := i + 1
+ OD
+ [ p = x^n ]"
+ apply vcg_tc
+ by auto
+
+text \<open>
+The last example is again taken from HOL/Hoare/Examples.thy.
+We have modified it to integers so it requires precondition \<open>0 \<le> x\<close>.
+\<close>
+
+lemma sqrt_tc: "VARS r
+ [0 \<le> (x::int)]
+ r := 0;
+ WHILE (r+1)*(r+1) <= x
+ INV {r*r \<le> x}
+ VAR {nat (x-r)}
+ DO r := r+1 OD
+ [r*r \<le> x \<and> x < (r+1)*(r+1)]"
+ apply vcg_tc_simp
+ by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left)
+
+text \<open>
+A total-correctness proof allows us to extract a function for further use.
+For every input satisfying the precondition the function returns an output satisfying the postcondition.
+\<close>
+
+lemma sqrt_exists:
+ "0 \<le> (x::int) \<Longrightarrow> \<exists>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
+ using tc_extract_function sqrt_tc by blast
+
+definition "sqrt (x::int) \<equiv> (SOME r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1))"
+
+lemma sqrt_function:
+ assumes "0 \<le> (x::int)"
+ and "r' = sqrt x"
+ shows "r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
+proof -
+ let ?P = "\<lambda>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
+ have "?P (SOME z . ?P z)"
+ by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp)
+ thus ?thesis
+ using assms(2) sqrt_def by auto
+qed
+
+end
--- a/src/HOL/Hoare/Hoare.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/Hoare.thy Sat Dec 05 19:30:37 2020 +0100
@@ -3,7 +3,7 @@
*)
theory Hoare
-imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
+imports Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
begin
end
--- a/src/HOL/Hoare/Hoare_Logic.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Sat Dec 05 19:30:37 2020 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Hoare/Hoare_Logic.thy
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 1998 TUM
+ Author: Walter Guttmann (extension to total-correctness proofs)
Sugared semantic embedding of Hoare logic.
Strictly speaking a shallow embedding (as implemented by Norbert Galm
@@ -14,12 +15,19 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
+type_synonym 'a var = "'a \<Rightarrow> nat"
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+
+syntax (xsymbols)
+ "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+
+translations
+ "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -31,17 +39,38 @@
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
-| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
-| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
- Sem (While b x c) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
+ Sem (While b x y c) s s'"
inductive_cases [elim!]:
"Sem (Basic f) s s'" "Sem (c1;c2) s s'"
"Sem (IF b THEN c1 ELSE c2 FI) s s'"
+lemma Sem_deterministic:
+ assumes "Sem c s s1"
+ and "Sem c s s2"
+ shows "s1 = s2"
+proof -
+ have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
+ by (induct rule: Sem.induct) (subst Sem.simps, blast)+
+ thus ?thesis
+ using assms by simp
+qed
+
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "Valid p c q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q)"
+ where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
+
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c s t \<and> t \<in> q)"
+lemma tc_implies_pc:
+ "ValidTC p c q \<Longrightarrow> Valid p c q"
+ by (metis Sem_deterministic Valid_def ValidTC_def)
+
+lemma tc_extract_function:
+ "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
+ by (metis ValidTC_def)
syntax
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
@@ -57,6 +86,16 @@
parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
+syntax
+ "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+ ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare_tc" :: "['a assn,'a com,'a assn] => bool"
+ ("[_] // _ // [_]" [0,55,0] 50)
+
+parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close>
+
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
@@ -73,14 +112,14 @@
by (auto simp:Valid_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+ assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
using assms
- by (induct "WHILE b INV {i} DO c OD" s s') auto
+ by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
apply assumption
@@ -88,8 +127,73 @@
apply blast
done
+lemma SkipRuleTC:
+ assumes "p \<subseteq> q"
+ shows "ValidTC p (Basic id) q"
+ by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
-lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
+lemma BasicRuleTC:
+ assumes "p \<subseteq> {s. f s \<in> q}"
+ shows "ValidTC p (Basic f) q"
+ by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
+
+lemma SeqRuleTC:
+ assumes "ValidTC p c1 q"
+ and "ValidTC q c2 r"
+ shows "ValidTC p (c1;c2) r"
+ by (meson assms Sem.intros(2) ValidTC_def)
+
+lemma CondRuleTC:
+ assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
+ and "ValidTC w c1 q"
+ and "ValidTC w' c2 q"
+ shows "ValidTC p (Cond b c1 c2) q"
+proof (unfold ValidTC_def, rule allI)
+ fix s
+ show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) s t \<and> t \<in> q)"
+ apply (cases "s \<in> b")
+ apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
+ by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
+qed
+
+lemma WhileRuleTC:
+ assumes "p \<subseteq> i"
+ and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
+ and "i \<inter> uminus b \<subseteq> q"
+ shows "ValidTC p (While b i v c) q"
+proof -
+ {
+ fix s n
+ have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
+ proof (induction "n" arbitrary: s rule: less_induct)
+ fix n :: nat
+ fix s :: 'a
+ assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
+ show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
+ proof (rule impI, cases "s \<in> b")
+ assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
+ hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
+ using assms(1) by auto
+ hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
+ by (metis assms(2) ValidTC_def)
+ from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
+ by auto
+ hence "\<exists>u . Sem (While b i v c) t u \<and> u \<in> q"
+ using 1 by auto
+ thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
+ using 2 3 Sem.intros(6) by force
+ next
+ assume "s \<notin> b" and "s \<in> i \<and> v s = n"
+ thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
+ using Sem.intros(5) assms(3) by fastforce
+ qed
+ qed
+ }
+ thus ?thesis
+ using assms(1) ValidTC_def by force
+qed
+
+lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
by blast
lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
@@ -104,4 +208,13 @@
SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
+method_setup vcg_tc = \<open>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+ "verification condition generator"
+
+method_setup vcg_tc_simp = \<open>
+ Scan.succeed (fn ctxt =>
+ SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ "verification condition generator plus simplification"
+
end
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Sat Dec 05 19:30:37 2020 +0100
@@ -1,8 +1,9 @@
(* Title: HOL/Hoare/Hoare_Logic_Abort.thy
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 2003 TUM
+ Author: Walter Guttmann (extension to total-correctness proofs)
-Like Hoare.thy, but with an Abort statement for modelling run time errors.
+Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors.
*)
theory Hoare_Logic_Abort
@@ -11,13 +12,20 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
+type_synonym 'a var = "'a \<Rightarrow> nat"
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Abort
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+
+syntax (xsymbols)
+ "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+
+translations
+ "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -32,18 +40,39 @@
| "Sem (IF b THEN c1 ELSE c2 FI) None None"
| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
-| "Sem (While b x c) None None"
-| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
-| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
- Sem (While b x c) (Some s) s'"
+| "Sem (While b x y c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
+ Sem (While b x y c) (Some s) s'"
inductive_cases [elim!]:
"Sem (Basic f) s s'" "Sem (c1;c2) s s'"
"Sem (IF b THEN c1 ELSE c2 FI) s s'"
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
- "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
+lemma Sem_deterministic:
+ assumes "Sem c s s1"
+ and "Sem c s s2"
+ shows "s1 = s2"
+proof -
+ have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
+ by (induct rule: Sem.induct) (subst Sem.simps, blast)+
+ thus ?thesis
+ using assms by simp
+qed
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
+
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)"
+
+lemma tc_implies_pc:
+ "ValidTC p c q \<Longrightarrow> Valid p c q"
+ by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
+
+lemma tc_extract_function:
+ "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
+ by (meson ValidTC_def)
syntax
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
@@ -57,11 +86,19 @@
ML_file \<open>hoare_syntax.ML\<close>
parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation
- \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
+syntax
+ "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+ ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare_abort_tc" :: "['a assn,'a com,'a assn] => bool"
+ ("[_] // _ // [_]" [0,55,0] 50)
-section \<open>The proof rules\<close>
+parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
+print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>
+
+text \<open>The proof rules for partial correctness\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
@@ -78,17 +115,15 @@
by (fastforce simp:Valid_def image_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+ assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
using assms
- by (induct "WHILE b INV {i} DO c OD" s s') auto
+ by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
-apply(simp add:Valid_def)
-apply(simp (no_asm) add:image_def)
-apply clarify
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
+apply (clarsimp simp:Valid_def)
apply(drule While_aux)
apply assumption
apply blast
@@ -98,6 +133,74 @@
lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
by(auto simp:Valid_def)
+text \<open>The proof rules for total correctness\<close>
+
+lemma SkipRuleTC:
+ assumes "p \<subseteq> q"
+ shows "ValidTC p (Basic id) q"
+ by (metis Sem.intros(2) ValidTC_def assms id_def subsetD)
+
+lemma BasicRuleTC:
+ assumes "p \<subseteq> {s. f s \<in> q}"
+ shows "ValidTC p (Basic f) q"
+ by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)
+
+lemma SeqRuleTC:
+ assumes "ValidTC p c1 q"
+ and "ValidTC q c2 r"
+ shows "ValidTC p (c1;c2) r"
+ by (meson assms Sem.intros(4) ValidTC_def)
+
+lemma CondRuleTC:
+ assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
+ and "ValidTC w c1 q"
+ and "ValidTC w' c2 q"
+ shows "ValidTC p (Cond b c1 c2) q"
+proof (unfold ValidTC_def, rule allI)
+ fix s
+ show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) (Some s) (Some t) \<and> t \<in> q)"
+ apply (cases "s \<in> b")
+ apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
+ by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
+qed
+
+lemma WhileRuleTC:
+ assumes "p \<subseteq> i"
+ and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
+ and "i \<inter> uminus b \<subseteq> q"
+ shows "ValidTC p (While b i v c) q"
+proof -
+ {
+ fix s n
+ have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
+ proof (induction "n" arbitrary: s rule: less_induct)
+ fix n :: nat
+ fix s :: 'a
+ assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
+ show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
+ proof (rule impI, cases "s \<in> b")
+ assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
+ hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
+ using assms(1) by auto
+ hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
+ by (metis assms(2) ValidTC_def)
+ from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
+ by auto
+ hence "\<exists>u . Sem (While b i v c) (Some t) (Some u) \<and> u \<in> q"
+ using 1 by auto
+ thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
+ using 2 3 Sem.intros(10) by force
+ next
+ assume "s \<notin> b" and "s \<in> i \<and> v s = n"
+ thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
+ using Sem.intros(9) assms(3) by fastforce
+ qed
+ qed
+ }
+ thus ?thesis
+ using assms(1) ValidTC_def by force
+qed
+
subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
@@ -115,6 +218,15 @@
SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
+method_setup vcg_tc = \<open>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+ "verification condition generator"
+
+method_setup vcg_tc_simp = \<open>
+ Scan.succeed (fn ctxt =>
+ SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+ "verification condition generator plus simplification"
+
\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
syntax
"_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
--- a/src/HOL/Hoare/README.html Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/README.html Sat Dec 05 19:30:37 2020 +0100
@@ -62,6 +62,32 @@
This is a logic of partial correctness. You can only prove that your program
does the right thing <i>if</i> it terminates, but not <i>that</i> it
terminates.
+A logic of total correctness is also provided and described below.
+
+<H3>Total correctness</H3>
+
+To prove termination, each WHILE-loop must be annotated with a variant:
+<UL>
+<LI> <kbd>WHILE _ INV {_} VAR {_} DO _ OD</kbd>
+</UL>
+A variant is an expression with type <kbd>nat</kbd>, which may use program
+variables and normal variables.
+<P>
+
+A total-correctness goal has the form
+<PRE>
+VARS x y ... [P] prog [Q]
+</PRE>
+enclosing the pre- and postcondition in square brackets.
+<P>
+
+Methods <kbd>vcg_tc</kbd> and <kbd>vcg_tc_simp</kbd> can be used to derive
+verification conditions.
+<P>
+
+From a total-correctness proof, a function can be extracted which
+for every input satisfying the precondition returns an output
+satisfying the postcondition.
<H3>Notes on the implementation</H3>
--- a/src/HOL/Hoare/SchorrWaite.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/SchorrWaite.thy Sat Dec 05 19:30:37 2020 +0100
@@ -222,7 +222,7 @@
(is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
proof (vcg)
let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
- {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
+ {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ ?body" = ?c3
{
fix c m l r t p q root
--- a/src/HOL/Hoare/hoare_syntax.ML Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML Sat Dec 05 19:30:37 2020 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Hoare/hoare_syntax.ML
Author: Leonor Prensa Nieto & Tobias Nipkow
+ Author: Walter Guttmann (extension to total-correctness proofs)
Syntax translations for Hoare logic.
*)
@@ -7,6 +8,7 @@
signature HOARE_SYNTAX =
sig
val hoare_vars_tr: term list -> term
+ val hoare_tc_vars_tr: term list -> term
val spec_tr': string -> term list -> term
end;
@@ -47,6 +49,8 @@
fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r;
+fun var_tr v xs = mk_abstuple xs v;
+
(* com_tr *)
@@ -57,8 +61,8 @@
Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs
| com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs =
Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ c) xs =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+ | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ V $ c) xs =
+ Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs
| com_tr t _ = t;
fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
@@ -73,6 +77,13 @@
end
| hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+fun hoare_tc_vars_tr [vars, pre, prg, post] =
+ let val xs = vars_tr vars
+ in Syntax.const \<^const_syntax>\<open>ValidTC\<close> $
+ assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+ end
+ | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts);
+
end;
@@ -122,6 +133,9 @@
fun bexp_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
| bexp_tr' t = t;
+fun var_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
+ | var_tr' t = t;
+
(* com_tr' *)
@@ -142,8 +156,8 @@
Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2
| com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) =
Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ c) =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ com_tr' c
+ | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ V $ c) =
+ Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c
| com_tr' t = t;
in
--- a/src/HOL/Hoare/hoare_tac.ML Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Sat Dec 05 19:30:37 2020 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Hoare/hoare_tac.ML
Author: Leonor Prensa Nieto & Tobias Nipkow
+ Author: Walter Guttmann (extension to total-correctness proofs)
Derivation of the proof rules and, most importantly, the VCG tactic.
*)
@@ -9,6 +10,7 @@
val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
int -> tactic
val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
+ val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic
end;
structure Hoare: HOARE =
@@ -195,5 +197,39 @@
fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
+
+(* total correctness rules *)
+
+fun hoare_tc_rule_tac ctxt (vars, Mlem) tac =
+ let
+ val var_names = map (fst o dest_Free) vars;
+ fun wlp_tac i =
+ resolve_tac ctxt @{thms SeqRuleTC} i THEN rule_tac false (i + 1)
+ and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
+ ((wlp_tac i THEN rule_tac pre_cond i)
+ ORELSE
+ (FIRST [
+ resolve_tac ctxt @{thms SkipRuleTC} i,
+ EVERY [
+ resolve_tac ctxt @{thms BasicRuleTC} i,
+ resolve_tac ctxt [Mlem] i,
+ split_simp_tac ctxt i],
+ EVERY [
+ resolve_tac ctxt @{thms CondRuleTC} i,
+ rule_tac false (i + 2),
+ rule_tac false (i + 1)],
+ EVERY [
+ resolve_tac ctxt @{thms WhileRuleTC} i,
+ basic_simp_tac ctxt var_names tac (i + 2),
+ rule_tac true (i + 1)]]
+ THEN (
+ if pre_cond then basic_simp_tac ctxt var_names tac i
+ else resolve_tac ctxt [subset_refl] i)));
+ in rule_tac end;
+
+
+fun hoare_tc_tac ctxt tac = SUBGOAL (fn (goal, i) =>
+ SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
+
end;
--- a/src/HOL/Isar_Examples/Hoare.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sat Dec 05 19:30:37 2020 +0100
@@ -21,12 +21,13 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
+type_synonym 'a var = "'a \<Rightarrow> nat"
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60)
| Cond "'a bexp" "'a com" "'a com"
- | While "'a bexp" "'a assn" "'a com"
+ | While "'a bexp" "'a assn" "'a var" "'a com"
abbreviation Skip ("SKIP")
where "SKIP \<equiv> Basic id"
@@ -43,7 +44,7 @@
"Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
| "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
- | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
+ | "Sem (While b x y c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
@@ -147,10 +148,10 @@
theorem while:
assumes body: "\<turnstile> (P \<inter> b) c P"
- shows "\<turnstile> P (While b X c) (P \<inter> -b)"
+ shows "\<turnstile> P (While b X Y c) (P \<inter> -b)"
proof
fix s s' assume s: "s \<in> P"
- assume "Sem (While b X c) s s'"
+ assume "Sem (While b X Y c) s s'"
then obtain n where "iter n b (Sem c) s s'" by auto
from this and s show "s' \<in> P \<inter> -b"
proof (induct n arbitrary: s)
@@ -207,7 +208,7 @@
"B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
"\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
- "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+ "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i (\<lambda>_. 0) c"
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
parse_translation \<open>
@@ -335,10 +336,10 @@
text \<open>While statements --- with optional invariant.\<close>
-lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P V c) (P \<inter> -b)"
by (rule while)
-lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined V c) (P \<inter> -b)"
by (rule while)
@@ -387,7 +388,7 @@
by (induct n) auto
lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
apply (clarsimp simp: Valid_def)
apply (drule iter_aux)
prefer 2
@@ -400,6 +401,11 @@
by blast
lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close>
+lemmas SeqRuleTC = SkipRule \<comment> \<open>dummy version\<close>
+lemmas SkipRuleTC = SkipRule \<comment> \<open>dummy version\<close>
+lemmas BasicRuleTC = SkipRule \<comment> \<open>dummy version\<close>
+lemmas CondRuleTC = SkipRule \<comment> \<open>dummy version\<close>
+lemmas WhileRuleTC = SkipRule \<comment> \<open>dummy version\<close>
ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Sat Dec 05 19:09:39 2020 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Sat Dec 05 19:30:37 2020 +0100
@@ -280,7 +280,7 @@
"timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
| "timeit (c1; c2) = (timeit c1; timeit c2)"
| "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
- | "timeit (While b iv c) = While b iv (timeit c)"
+ | "timeit (While b iv v c) = While b iv v (timeit c)"
record tvars = tstate +
I :: nat