This commit is contained in:
nemouchi 2019-02-24 20:18:04 +01:00
parent 79185f1ac4
commit add6534da2
1 changed files with 21 additions and 11 deletions

View File

@ -140,22 +140,27 @@ lemma
"(\<sigma> s\<^sub>0, t) \<in> P \<and> t = \<sigma> s\<^sub>0 \<longrightarrow> (t, t) \<in> P"
by auto
term "\<lbrace> & x =\<^sub>u 2 \<rbrace> x :== ( & x + 1 ) \<lbrace> & x =\<^sub>u 3 \<rbrace>\<^sub>P"
lemma
"\<lbrace>P\<lbrakk>e/x\<rbrakk>\<rbrace>x :== e\<lbrace>P\<rbrace>\<^sub>P"
" \<lbrace> P\<lbrakk>e/x\<rbrakk> \<rbrace>x :== e\<lbrace>P\<rbrace>\<^sub>P "
apply (simp add: prog_rep_eq )
apply rel_simp
done
lemma assigns_prog_floyd[hoare_sp_rules]:
assumes "vwb_lens x"
shows \<open>\<lbrace>P\<rbrace>x :== e\<lbrace>\<^bold>\<exists>v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/x\<rbrakk> \<and> &x =\<^sub>u e\<lbrakk>\<guillemotleft>v\<guillemotright>/x\<rbrakk>\<rbrace>\<^sub>P\<close>
shows \<open> \<lbrace>P\<rbrace>x :== e
\<lbrace>\<^bold>\<exists>v \<bullet> P\<lbrakk>\<guillemotleft>v\<guillemotright>/x\<rbrakk> \<and> &x =\<^sub>u e\<lbrakk>\<guillemotleft>v\<guillemotright>/x\<rbrakk>\<rbrace>\<^sub>P \<close>
using assms
by (simp add: assms prog_rep_eq hoare_des)
lemma
shows \<open>\<lbrace>P\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>p\<lbrace>\<^bold>\<exists>v \<bullet> ((subst_upd \<sigma> (1\<^sub>L) \<guillemotleft>v\<guillemotright>) \<dagger> P)\<rbrace>\<^sub>P\<close>
shows \<open>\<lbrace>P\<rbrace>
\<langle>\<sigma>\<rangle>\<^sub>p
\<lbrace>\<^bold>\<exists>v \<bullet> ((subst_upd id (1\<^sub>L) \<guillemotleft>v\<guillemotright>) \<dagger> P) \<and> &\<Sigma> =\<^sub>u ((subst_upd id (1\<^sub>L) \<guillemotleft>v\<guillemotright>) \<dagger> (usubst_lookup \<sigma> 1\<^sub>L) )\<rbrace>\<^sub>P\<close>
apply (simp add: prog_rep_eq )
apply rel_simp
apply auto
done
section \<open>Hoare Logic for Sequential Composition\<close>
@ -178,9 +183,11 @@ lemma seq_prog_hoare_stronger_pre_2:
apply rel_blast
done
lemma seq_prog_hoare[hoare_wp_rules, hoare_sp_rules]:
assumes"\<lbrace>p\<rbrace>C\<^sub>1\<lbrace>s\<rbrace>\<^sub>P" and "\<lbrace>s\<rbrace>C\<^sub>2\<lbrace>r\<rbrace>\<^sub>P"
shows"\<lbrace>p\<rbrace>C\<^sub>1 ; C\<^sub>2\<lbrace>r\<rbrace>\<^sub>P"
lemma seq_prog_hoare[hoare_wp_rules, hoare_sp_rules]:
assumes"\<lbrace>P\<rbrace>PROG\<^sub>1\<lbrace>R\<rbrace>\<^sub>P" and "\<lbrace>R\<rbrace>PROG\<^sub>2\<lbrace>Q\<rbrace>\<^sub>P"
shows"\<lbrace>P\<rbrace>PROG\<^sub>1 ; PROG\<^sub>2\<lbrace>Q\<rbrace>\<^sub>P"
using assms
by (simp add: prog_rep_eq hoare_des)
@ -193,16 +200,19 @@ lemma cond_prog_hoare_basic:
by (simp add: prog_rep_eq hoare_des)
lemma cond_prog_hoare_wp[hoare_wp_rules]:
assumes "\<lbrace>p'\<rbrace>C\<^sub>1\<lbrace>q\<rbrace>\<^sub>P" and "\<lbrace>p''\<rbrace>C\<^sub>2\<lbrace>q\<rbrace>\<^sub>P"
shows "\<lbrace>(b \<and> p')\<or> (\<not>b \<and> p'')\<rbrace>IF b THEN C\<^sub>1 ELSE C\<^sub>2 FI\<lbrace>q\<rbrace>\<^sub>P"
assumes "\<lbrace>P'\<rbrace>PROG\<^sub>1\<lbrace>Q\<rbrace>\<^sub>P" and "\<lbrace>P''\<rbrace>PROG\<^sub>2\<lbrace>Q\<rbrace>\<^sub>P"
shows "\<lbrace>(b \<and> P')\<or> (\<not>b \<and> P'')\<rbrace>
IF b THEN PROG\<^sub>1 ELSE PROG\<^sub>2 FI
\<lbrace>Q\<rbrace>\<^sub>P"
using assms
apply (simp add: prog_rep_eq )
apply pred_simp
done
lemma cond_prog_hoare_sp[hoare_sp_rules]:
assumes \<open>\<lbrace>b \<and> p\<rbrace>C\<^sub>1\<lbrace>q\<rbrace>\<^sub>P\<close> and \<open>\<lbrace>\<not>b \<and> p\<rbrace>C\<^sub>2\<lbrace>s\<rbrace>\<^sub>P\<close>
shows \<open>\<lbrace>p\<rbrace>IF b THEN C\<^sub>1 ELSE C\<^sub>2 FI\<lbrace>q \<or> s\<rbrace>\<^sub>P\<close>
assumes \<open>\<lbrace>b \<and> P\<rbrace>PROG\<^sub>1\<lbrace>Q\<rbrace>\<^sub>P\<close> and \<open>\<lbrace>\<not>b \<and> P\<rbrace>PROG\<^sub>2\<lbrace>R\<rbrace>\<^sub>P\<close>
shows \<open>\<lbrace>P\<rbrace>IF b THEN PROG\<^sub>1 ELSE PROG\<^sub>2 FI\<lbrace>Q \<or> R\<rbrace>\<^sub>P\<close>
using assms
by (simp add: prog_rep_eq hoare_des)