--- a/src/HOL/Hoare/ExamplesTC.thy Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/ExamplesTC.thy Tue Oct 12 20:57:43 2021 +0200
@@ -27,7 +27,7 @@
Here is the total-correctness proof for the same program.
It needs the additional invariant \<open>m \<le> a\<close>.
\<close>
-
+ML \<open>\<^const_syntax>\<open>HOL.eq\<close>\<close>
lemma multiply_by_add_tc: "VARS m s a b
[a=A \<and> b=B]
m := 0; s := 0;
@@ -84,7 +84,7 @@
r := 0;
WHILE (r+1)*(r+1) <= x
INV {r*r \<le> x}
- VAR {nat (x-r)}
+ VAR { nat (x-r)}
DO r := r+1 OD
[r*r \<le> x \<and> x < (r+1)*(r+1)]"
apply vcg_tc_simp
@@ -113,4 +113,21 @@
using assms(2) sqrt_def by auto
qed
+text \<open>Nested loops!\<close>
+
+lemma "VARS (i::nat) j
+ [ True ]
+ WHILE 0 < i
+ INV { True }
+ VAR { z = i }
+ DO i := i - 1; j := i;
+ WHILE 0 < j
+ INV { z = i+1 }
+ VAR { j }
+ DO j := j - 1 OD
+ OD
+ [ i \<le> 0 ]"
+ apply vcg_tc
+ by auto
+
end
--- a/src/HOL/Hoare/Hoare_Logic.thy Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Oct 12 20:57:43 2021 +0200
@@ -20,13 +20,12 @@
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"
| Cond "'a bexp" "'a com" "'a com"
-| While "'a bexp" "'a assn" "'a var" "'a com"
+| While "'a bexp" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -38,15 +37,15 @@
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) 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'"
+| "s \<notin> b \<Longrightarrow> Sem (While b c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b c) s'' s' \<Longrightarrow>
+ Sem (While b c) 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> p \<longrightarrow> s' \<in> q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c a 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)"
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c a q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
inductive_cases [elim!]:
"Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
@@ -64,37 +63,37 @@
qed
lemma tc_implies_pc:
- "ValidTC p c q \<Longrightarrow> Valid p c q"
+ "ValidTC p c a q \<Longrightarrow> Valid p c a 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"
+ "ValidTC p c a q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (metis ValidTC_def)
-lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) a q"
by (auto simp:Valid_def)
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) a q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
+lemma SeqRule: "Valid P c1 a1 Q \<Longrightarrow> Valid Q c2 a2 R \<Longrightarrow> Valid P (Seq c1 c2) (Aseq a1 a2) R"
by (auto simp:Valid_def)
lemma CondRule:
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
- \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+ \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
by (auto simp:Valid_def)
lemma While_aux:
- assumes "Sem (While b i v c) s s'"
+ assumes "Sem (While b c) 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 i v c" s s') auto
+ by (induct "While b c" 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 v c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
apply assumption
@@ -104,25 +103,25 @@
lemma SkipRuleTC:
assumes "p \<subseteq> q"
- shows "ValidTC p (Basic id) q"
+ shows "ValidTC p (Basic id) a q"
by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
lemma BasicRuleTC:
assumes "p \<subseteq> {s. f s \<in> q}"
- shows "ValidTC p (Basic f) q"
+ shows "ValidTC p (Basic f) a 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 (Seq c1 c2) r"
+ assumes "ValidTC p c1 a1 q"
+ and "ValidTC q c2 a2 r"
+ shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) 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"
+ and "ValidTC w c1 a1 q"
+ and "ValidTC w' c2 a2 q"
+ shows "ValidTC p (Cond b c1 c2) (Acond a1 a2) 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)"
@@ -133,18 +132,18 @@
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 "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
and "i \<inter> uminus b \<subseteq> q"
- shows "ValidTC p (While b i v c) q"
+ shows "ValidTC p (While b c) (Awhile i v A) 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)"
+ have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b 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)"
+ assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
+ show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b 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}"
@@ -153,13 +152,13 @@
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"
+ hence "\<exists>u . Sem (While b 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"
+ thus "\<exists>t . Sem (While b 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"
+ thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
using Sem.intros(5) assms(3) by fastforce
qed
qed
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Oct 12 20:57:43 2021 +0200
@@ -19,7 +19,7 @@
| Abort
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
-| While "'a bexp" "'a assn" "'a var" "'a com"
+| While "'a bexp" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -34,10 +34,10 @@
| "Sem (Cond b c1 c2) None None"
| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (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'"
+| "Sem (While b c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b c) s'' s' \<Longrightarrow>
+ Sem (While b c) (Some s) s'"
inductive_cases [elim!]:
"Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
@@ -54,45 +54,45 @@
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 Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c a 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)"
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c a 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"
+ "ValidTC p c a q \<Longrightarrow> Valid p c a q"
by (smt (verit) 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"
+ "ValidTC p c a q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (meson ValidTC_def)
text \<open>The proof rules for partial correctness\<close>
-lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) a q"
by (auto simp:Valid_def)
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) a q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
+lemma SeqRule: "Valid P c1 a1 Q \<Longrightarrow> Valid Q c2 a2 R \<Longrightarrow> Valid P (Seq c1 c2) (Aseq a1 a2) R"
by (auto simp:Valid_def)
lemma CondRule:
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
- \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+ \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
by (fastforce simp:Valid_def image_def)
lemma While_aux:
- assumes "Sem (While b i v c) s s'"
+ assumes "Sem (While b c) 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 i v c" s s') auto
+ by (induct "While b c" 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 v c) q"
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
apply assumption
@@ -100,32 +100,32 @@
apply blast
done
-lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
+lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort a 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"
+ shows "ValidTC p (Basic id) a 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"
+ shows "ValidTC p (Basic f) a 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 (Seq c1 c2) r"
+ assumes "ValidTC p c1 a1 q"
+ and "ValidTC q c2 a2 r"
+ shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) 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"
+ and "ValidTC w c1 a1 q"
+ and "ValidTC w' c2 a2 q"
+ shows "ValidTC p (Cond b c1 c2) (Acons a1 a2) 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)"
@@ -136,18 +136,18 @@
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 "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
and "i \<inter> uminus b \<subseteq> q"
- shows "ValidTC p (While b i v c) q"
+ shows "ValidTC p (While b c) (Awhile i v A) 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)"
+ have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b 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)"
+ assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
+ show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b 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}"
@@ -156,13 +156,13 @@
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"
+ hence "\<exists>u . Sem (While b 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"
+ thus "\<exists>t . Sem (While b 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"
+ thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
using Sem.intros(9) assms(3) by fastforce
qed
qed
--- a/src/HOL/Hoare/Hoare_Syntax.thy Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Syntax.thy Tue Oct 12 20:57:43 2021 +0200
@@ -15,10 +15,18 @@
"_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
"_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+text \<open>The \<open>VAR {_}\<close> syntax supports two variants:
+\<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression,
+ the variant, and \<open>x\<close> a variable that can be referred to from inner annotations.
+ The \<open>x\<close> can be necessary for nested loops, e.g. to prove that the inner loops do not mess with \<open>t\<close>.
+\<^item> \<open>VAR {t}\<close> where the variable is omitted because it is not needed.
+\<close>
+
syntax
"_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-translations
- "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+
+text \<open>The \<open>_While0\<close> syntax is translated into the \<open>_While\<close> syntax with the trivial variant 0.
+This is ok because partial correctness proofs do not make use of the variant.\<close>
syntax
"_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
@@ -27,6 +35,18 @@
"_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50)
"_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50)
+text \<open>Completeness requires(?) the ability to refer to an outer variant in an inner invariant.
+Thus we need to abstract over a variable equated with the variant, the \<open>x\<close> in \<open>VAR {x = t}\<close>.
+But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<open>hoare_syntax.ML\<close>
+separate the program from its annotations and only the latter are abstracted over over \<open>x\<close>.
+(Thus \<open>x\<close> can also occur in inner variants, but that neither helps nor hurts.)\<close>
+
+datatype 'a anno =
+ Abasic |
+ Aseq "'a anno" "'a anno" |
+ Acond "'a anno" "'a anno" |
+ Awhile "'a set" "'a \<Rightarrow> nat" "nat \<Rightarrow> 'a anno"
+
ML_file \<open>hoare_syntax.ML\<close>
end
--- a/src/HOL/Hoare/SchorrWaite.thy Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Tue Oct 12 20:57:43 2021 +0200
@@ -219,10 +219,11 @@
ELSE q := p; p := t; t := t^.l; p^.l := q; \<comment> \<open>\<open>push\<close>\<close>
p^.m := True; p^.c := False FI OD
{(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
- (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
+ (is "Valid
+ {(c, m, l, r, t, p, q, root). ?Pre c m l r root}
+ (Seq _ (Seq _ (While {(c, m, l, r, t, p, q, root). ?whileB m t p} _)))
+ (Aseq _ (Aseq _ (Awhile {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ _))) _")
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
{
fix c m l r t p q root
@@ -252,8 +253,8 @@
let "?ifB1" = "(t = Null \<or> t^.m)"
let "?ifB2" = "p^.c"
- assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
- then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
+ assume "(\<exists>stack.?Inv stack) \<and> ?whileB m t p"
+ then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+
--- a/src/HOL/Hoare/hoare_syntax.ML Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Tue Oct 12 20:57:43 2021 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Hoare/hoare_syntax.ML
Author: Leonor Prensa Nieto & Tobias Nipkow
- Author: Walter Guttmann (extension to total-correctness proofs)
+ Author: Walter Guttmann (initial extension to total-correctness proofs)
+ Author: Tobias Nipkow (complete version of total correctness with separate anno type)
Syntax translations for Hoare logic.
*)
@@ -84,14 +85,34 @@
fun com_tr ctxt =
let
fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
- syntax_const ctxt #Basic $ mk_fexp x e xs
+ (syntax_const ctxt #Basic $ mk_fexp x e xs, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
| tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
- syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs
+ let val (c1',a1) = tr c1 xs;
+ val (c2',a2) = tr c2 xs
+ in (syntax_const ctxt #Seq $ c1' $ c2', Syntax.const \<^const_syntax>\<open>Aseq\<close> $ a1 $ a2) end
| tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
- syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs
- | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ I $ V $ c) xs =
- syntax_const ctxt #While $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ tr c xs
- | tr t _ = t;
+ let val (c1',a1) = tr c1 xs;
+ val (c2',a2) = tr c2 xs
+ in (syntax_const ctxt #Cond $ bexp_tr b xs $ c1' $ c2',
+ Syntax.const \<^const_syntax>\<open>Acond\<close> $ a1 $ a2)
+ end
+ | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ i $ v $ c) xs =
+ let val (c',a) = tr c xs
+ val (v',A) = case v of
+ Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
+ t => (t, absdummy dummyT a)
+ in (syntax_const ctxt #While $ bexp_tr b xs $ c',
+ Syntax.const \<^const_syntax>\<open>Awhile\<close>
+ $ assn_tr i xs $ var_tr v' xs $ A)
+ end
+ | tr (Const (\<^syntax_const>\<open>_While0\<close>,_) $ b $ I $ c) xs =
+ let val (c',a) = tr c xs
+ in (syntax_const ctxt #While $ bexp_tr b xs $ c',
+ Syntax.const \<^const_syntax>\<open>Awhile\<close>
+ $ assn_tr I xs $ var_tr (Syntax.const \<^const_syntax>\<open>zero_class.zero\<close>) xs
+ $ absdummy dummyT a)
+ end
+ | tr t _ = (t, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
in tr end;
fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
@@ -101,12 +122,14 @@
fun hoare_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in syntax_const ctxt #Valid $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ val (c',a) = com_tr ctxt prg xs
+ in syntax_const ctxt #Valid $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
| hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);
fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in syntax_const ctxt #ValidTC $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ val (c',a) = com_tr ctxt prg xs
+ in syntax_const ctxt #ValidTC $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
| hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);
end;
@@ -158,8 +181,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;
+fun var_tr' xo T =
+ let val n = dest_abstuple T
+ in case xo of NONE => n | SOME x => Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Syntax.free x $ n end
(* com_tr' *)
@@ -174,32 +198,40 @@
else syntax_const ctxt #Skip
end;
-fun com_tr' ctxt t =
+fun com_tr' ctxt (t,a) =
let
val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
fun arg k = nth args (k - 1);
val n = length args;
+ val (_, args_a) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb a);
+ fun arg_a k = nth args_a (k - 1)
in
- (case head of
+ case head of
NONE => t
| SOME c =>
if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
mk_assign ctxt (arg 1)
else if c = const_syntax ctxt #Seq andalso n = 2 then
- Syntax.const \<^syntax_const>\<open>_Seq\<close> $ com_tr' ctxt (arg 1) $ com_tr' ctxt (arg 2)
+ Syntax.const \<^syntax_const>\<open>_Seq\<close>
+ $ com_tr' ctxt (arg 1, arg_a 1) $ com_tr' ctxt (arg 2, arg_a 2)
else if c = const_syntax ctxt #Cond andalso n = 3 then
Syntax.const \<^syntax_const>\<open>_Cond\<close> $
- bexp_tr' (arg 1) $ com_tr' ctxt (arg 2) $ com_tr' ctxt (arg 3)
- else if c = const_syntax ctxt #While andalso n = 4 then
- Syntax.const \<^syntax_const>\<open>_While\<close> $
- bexp_tr' (arg 1) $ assn_tr' (arg 2) $ var_tr' (arg 3) $ com_tr' ctxt (arg 4)
- else t)
+ bexp_tr' (arg 1) $ com_tr' ctxt (arg 2, arg_a 1) $ com_tr' ctxt (arg 3, arg_a 2)
+ else if c = const_syntax ctxt #While andalso n = 2 then
+ let val (xo,a') = case arg_a 3 of
+ Abs(x,_,a) => (if loose_bvar1(a,0) then SOME x else NONE,
+ subst_bound (Syntax.free x, a)) |
+ t => (NONE,t)
+ in Syntax.const \<^syntax_const>\<open>_While\<close>
+ $ bexp_tr' (arg 1) $ assn_tr' (arg_a 1) $ var_tr' xo (arg_a 2) $ com_tr' ctxt (arg 2, a')
+ end
+ else t
end;
in
-fun spec_tr' syn ctxt [p, c, q] =
- Syntax.const syn $ assn_tr' p $ com_tr' ctxt c $ assn_tr' q;
+fun spec_tr' syn ctxt [p, c, a, q] =
+ Syntax.const syn $ assn_tr' p $ com_tr' ctxt (c,a) $ assn_tr' q;
end;
--- a/src/HOL/Hoare/hoare_tac.ML Mon Oct 11 21:55:21 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Tue Oct 12 20:57:43 2021 +0200
@@ -71,7 +71,7 @@
fun get_vars c =
let
val d = Logic.strip_assums_concl c;
- val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
+ val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d;
in mk_vars pre end;
fun mk_CollectC tm =