--- a/CONTRIBUTORS Fri Dec 04 17:20:41 2020 +0000
+++ b/CONTRIBUTORS Fri Dec 04 17:21:09 2020 +0000
@@ -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/src/HOL/Data_Structures/Tree23_Map.thy Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/README.html Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/SchorrWaite.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Hoare/hoare_tac.ML Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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 Fri Dec 04 17:20:41 2020 +0000
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Fri Dec 04 17:21:09 2020 +0000
@@ -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