nemouchi
/
Orca2017
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

More general rules for assignment!

This commit is contained in:
Yakoub Nemouchi 2019-02-22 19:00:03 +00:00
parent c272e56c4e
commit 0167124a74
1 changed files with 37 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
C-verifier/src/Midend-IVL/Isabelle-UTP-Extended/HoareLogic/TotalCorrectness/utp_hoare_ndes_prog.thy
View File

@ -99,7 +99,7 @@ lemma conj_prog_hoare:
section \<open>Hoare Logic for SKIP\<close>
lemma skip_prog_hoare[hoare_sp_rules, hoare_wp_rules]:
"\<lbrace>p\<rbrace>SKIP\<lbrace>p\<rbrace>\<^sub>P"
"\<lbrace>P\<rbrace>SKIP\<lbrace>P\<rbrace>\<^sub>P"
by (simp add: prog_rep_eq hoare_des)
lemma skip_prog_hoare_intro:
@ -113,17 +113,50 @@ lemma assigns_prog_hoare_backward_intro:
shows "\<lbrace>p\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>p\<lbrace>q\<rbrace>\<^sub>P"
using assms
by (simp add: prog_rep_eq hoare_des)
lemma assigns_prog_hoare_backward[hoare_wp_rules]:
"\<lbrace>\<sigma> \<dagger> p\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>p\<lbrace>p\<rbrace>\<^sub>P"
"\<lbrace>\<sigma> \<dagger> P\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>p\<lbrace>P\<rbrace>\<^sub>P"
by (simp add: prog_rep_eq hoare_des)
lemma "((image (\<lambda>st. (t, t)) UNIV) \<inter> {(st, _). t = \<sigma> st }) \<subseteq>
(image (\<lambda>st. (st, t)) UNIV)"
by auto
lemma "((image (\<lambda>st. (s\<^sub>0, t)) P) \<inter> {(_, tt). t = \<sigma> s\<^sub>0 }) \<subseteq>
(image (\<lambda>st. (s\<^sub>0, \<sigma> s\<^sub>0)) P)"
by auto
lemma
"(s\<^sub>0, t) \<in> P \<and> t = \<sigma> s\<^sub>0 \<longrightarrow> (s\<^sub>0, \<sigma> s\<^sub>0) \<in> P"
by auto
lemma
"(\<forall>s\<^sub>0 t. (s\<^sub>0, t) \<in> P \<and> t = \<sigma> s\<^sub>0) \<longrightarrow> (\<forall>s\<^sub>0. \<exists>s. (s\<^sub>0, \<sigma> s) \<in> P)"
by auto
lemma
"(\<sigma> s\<^sub>0, t) \<in> P \<and> t = \<sigma> s\<^sub>0 \<longrightarrow> (t, t) \<in> P"
by auto
lemma
"\<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>
apply (simp add: prog_rep_eq )
apply rel_simp
done
section \<open>Hoare Logic for Sequential Composition\<close>
lemma seq_prog_hoare_invariant: