--- a/thys/Hoare_gen.thy Thu Mar 13 20:06:29 2014 +0000
+++ b/thys/Hoare_gen.thy Wed Mar 19 00:00:28 2014 +0000
@@ -7,17 +7,25 @@
"../Separation_Algebra/Sep_Tactics"
begin
-definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)
+definition
+ pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71)
where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
-lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
- by(simp add: sep_conj_ac)
+
+(* smae as sep.mult.left_commute *)
+lemma sep_conj_cond1:
+ "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
+ by (rule sep.mult.left_commute)
-lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)"
- by(simp add: sep_conj_ac)
+(* same as sep.mult.commute *)
+lemma sep_conj_cond2:
+ "(p \<and>* <cond>) = (<cond> \<and>* p)"
+ by(rule sep.mult.commute)
-lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
- by (metis sep.mult_assoc)
+(* same as sep.mult_assoc *)
+lemma sep_conj_cond3:
+ "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
+ by (rule sep.mult_assoc)
lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
@@ -33,7 +41,7 @@
lemma cond_true_eq2: "(p \<and>* <True>) = p"
by simp
-lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s"
+lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s"
by (unfold sep_conj_def pasrt_def, auto)
locale sep_exec =
@@ -44,73 +52,60 @@
definition "run n = step ^^ n"
lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
- apply (unfold run_def)
- by (metis funpow_add o_apply)
+ unfolding run_def
+ by (simp add: funpow_add)
+(* separation Hoare tripple *)
definition
- Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
- ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+ Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
where
- "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> \<equiv>
- (\<forall> s r. (p**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))"
+ "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv>
+ (\<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s)))))"
lemma HoareI [case_names Pre]:
- assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))"
- shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
+ assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s))))"
+ shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
using h
- by (unfold Hoare_gen_def, auto)
+ unfolding Hoare_gen_def
+ by simp
lemma frame_rule:
- assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
- shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>"
-proof(induct rule: HoareI)
- case (Pre r' s')
- hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
- from h[unfolded Hoare_gen_def, rule_format, OF this]
- show ?case
- by (metis sep_conj_assoc sep_conj_left_commute)
-qed
+ assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+ shows "\<lbrace>p \<and>* r\<rbrace> c \<lbrace>q \<and>* r\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_assoc sep_conj_left_commute)
lemma sequencing:
assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"
shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
+proof(induct rule: HoareI)
case (Pre r' s')
- from h1[unfolded Hoare_gen_def, rule_format, OF Pre]
+ have "(p \<and>* c \<and>* r') (recse s')" by fact
+ with h1[unfolded Hoare_gen_def]
obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto
- from h2[unfolded Hoare_gen_def, rule_format, OF this]
+ with h2[unfolded Hoare_gen_def]
obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto
- thus ?case
- apply (rule_tac x = "Suc (k1 + k2)" in exI)
- by (metis add_Suc_right nat_add_commute sep_exec.run_add)
+ thus "\<exists>k. (r \<and>* c \<and>* r') (recse (run (Suc k) s'))"
+ by (auto simp add: run_add[symmetric])
qed
lemma pre_stren:
assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
- and h2: "\<And>s. r s \<Longrightarrow> p s"
+ and h2: "\<And>s. r s \<Longrightarrow> p s"
shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
-proof(induct rule:HoareI)
- case (Pre r' s')
- with h2
- have "(p \<and>* c \<and>* r') (recse s')"
- by (metis sep_conj_impl1)
- from h1[unfolded Hoare_gen_def, rule_format, OF this]
- show ?case .
-qed
+using assms
+unfolding Hoare_gen_def
+by (metis sep_globalise)
lemma post_weaken:
assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
and h2: "\<And> s. q s \<Longrightarrow> r s"
shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
- case (Pre r' s')
- from h1[unfolded Hoare_gen_def, rule_format, OF this]
- obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast
- with h2
- show ?case
- by (metis sep_conj_impl1)
-qed
+using assms
+unfolding Hoare_gen_def
+by (metis sep_globalise)
lemma hoare_adjust:
assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"
@@ -118,65 +113,55 @@
and h3: "\<And>s. q1 s \<Longrightarrow> q s"
shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
using h1 h2 h3 post_weaken pre_stren
- by (metis)
+ by (blast)
lemma code_exI:
assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"
shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"
-proof(unfold pred_ex_def, induct rule:HoareI)
+unfolding pred_ex_def
+proof(induct rule:HoareI)
case (Pre r' s')
then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"
- by (auto elim!:sep_conjE intro!:sep_conjI)
+ by (auto elim!: sep_conjE intro!: sep_conjI)
from h[unfolded Hoare_gen_def, rule_format, OF this]
- show ?case
- by (auto elim!:sep_conjE intro!:sep_conjI)
+ show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))"
+ by (auto elim!: sep_conjE intro!: sep_conjI)
qed
lemma code_extension:
- assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
- shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>"
-proof(induct rule:HoareI)
- case (Pre r' s')
- hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
- from h[unfolded Hoare_gen_def, rule_format, OF this]
- show ?case
- by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
-qed
+ assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+ shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_assoc)
lemma code_extension1:
- assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
- shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>"
- by (metis code_extension h sep.mult_commute)
+ assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+ shows "\<lbrace>p\<rbrace> e \<and>* c \<lbrace>q\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_commute sep_conj_left_commute)
lemma composition:
assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"
and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"
- shows "\<lbrace>p\<rbrace> c1 ** c2 \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
- case (Pre r' s')
- hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
- from h1[unfolded Hoare_gen_def, rule_format, OF this]
- obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))"
- by (auto simp:sep_conj_ac)
- from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add]
- show ?case
- by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
-qed
+ shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>"
+using assms
+by (auto intro: sequencing code_extension code_extension1)
definition
- IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>
- ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
- ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+ IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
+ ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
where
"I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c
- \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
+ \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
lemma IHoareI [case_names IPre]:
assumes h: "\<And>s' s r cnf . (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow>
(\<exists>k t. (<Q t> \<and>* <(t ## s')> \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))"
shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
- unfolding IHoare_def
+unfolding IHoare_def
proof
fix s'
show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace> c