Theory picore_SIMP_lemma

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn, zhaoyongwang@gmail.com)
School of Computer Science & Engineering, Beihang University, China
*)

section ‹Lemmas of Picore-SIMP›

theory picore_SIMP_lemma
imports "picore_SIMP_Syntax" "picore_SIMP"

begin

lemma id_belong[simp]: "Id ⊆⦃ªx= ºx⦄"
  by (simp add: Collect_mono Id_fstsnd_eq)

lemma allpre_eq_pre: "(∀v∈U. ⊢⇩I P sat⇩p [{v}, rely, guar, post]) ⟷ ⊢⇩I P sat⇩p [U, rely, guar, post]"
  apply auto using Allprecond apply blast
  using Conseq[of _ _ rely rely guar guar post post P] by auto

lemma sat_pre_imp_allinpre: " ⊢⇩I P sat⇩p [U, rely, guar, post] ⟹ v∈U ⟹ ⊢⇩I P sat⇩p [{v}, rely, guar, post]"
  using Conseq[of _ _ rely rely guar guar post post P] by auto

lemma stable_int_col2: "stable ⦃s⦄ r ⟹ stable ⦃t⦄ r ⟹ stable ⦃s ∧ t⦄ r"
  by auto

lemma stable_int_col3: "stable ⦃k⦄ r ⟹ stable ⦃s⦄ r ⟹ stable ⦃t⦄ r ⟹ stable ⦃k ∧ s ∧ t⦄ r"
  by auto

lemma stable_int_col4: "stable ⦃m⦄ r ⟹ stable ⦃k⦄ r ⟹ stable ⦃s⦄ r
  ⟹ stable ⦃t⦄ r ⟹ stable ⦃m ∧ k ∧ s ∧ t⦄ r"
  by auto

lemma stable_int_col5: "stable ⦃q⦄ r ⟹ stable ⦃m⦄ r ⟹  stable ⦃k⦄ r
  ⟹ stable ⦃s⦄ r ⟹ stable ⦃t⦄ r ⟹ stable ⦃q ∧ m ∧ k ∧ s ∧ t⦄ r"
  by auto

lemma stable_un2: "stable s r ⟹ stable t r ⟹ stable (s ∪ t) r"
  by (simp add: stable_def)

lemma stable_un_R: "stable s r ⟹ stable s r' ⟹ stable s (r ∪ r')"
  by (meson UnE stable_def)

lemma stable_un_S: "∀t. stable s (P t) ⟹ stable s (⋃t. P t)"
apply(simp add:stable_def) by auto

lemma stable_un_S2: "∀t x. stable s (P t x) ⟹ stable s (⋃t x. P t x)"
apply(simp add:stable_def) by auto

lemma pairv_IntI:
"y ∈ ⦃´(Pair V) ∈ A⦄ ⟹ y ∈ ⦃´(Pair V) ∈ B⦄ ⟹ y ∈ ⦃´(Pair V) ∈ A ∩ B⦄"
by auto

lemma pairv_rId:
"y ∈ ⦃´(Pair V) ∈ A⦄ ⟹ y ∈ ⦃´(Pair V) ∈ A ∪ Id⦄"
by auto

end