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

antiframe is continues!

This commit is contained in:
yakoub 2019-03-21 15:38:53 +00:00
parent d3265eb492
commit d297000259
1 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
C-verifier/src/Midend-IVL/Isabelle-UTP-Extended/AlgebraicLaws/algebraic_laws_prog.thy
View File

@ -1952,6 +1952,28 @@ lemma antiframe_prog_refinedBy_while_lfp_scp_prog:
order_refl order_trans seq_prog_monoI)
done
lemma " (x = y) = (x\<sqsubseteq>y \<and> y\<sqsubseteq>x)"
using antisym by blast
find_theorems "\<Sqinter>\<^sub>p_ \<in> _"
lemma "vwb_lens G \<Longrightarrow> G:[\<Sqinter>\<^sub>pA] \<in> pantiframe_prog G ` A \<Longrightarrow>
pantiframe_prog G (\<Sqinter>\<^sub>p A) = \<Sqinter>\<^sub>p (image (pantiframe_prog G) A)"
proof (rule antisym, goal_cases)
case 1
then show ?case
apply (subst inf_prog_lower)
apply simp_all
done
next
case 2
then show ?case
apply (subst inf_prog_greatest)
apply (metis antiframe_prog_monoI imageE inf_prog_lower)
apply simp
done
qed
lemma antiframe_prog_modifies_while_lfp_scp_prog:
assumes vwb_lens: "vwb_lens G"
assumes modifies: "G:[body] = body"