Theory utp_pred_laws

section ‹ Predicate Calculus Laws ›

theory utp_pred_laws
  imports utp_pred
begin
  
subsection ‹ Propositional Logic ›
  
text ‹ Showing that predicates form a Boolean Algebra (under the predicate operators as opposed to
  the lattice operators) gives us many useful laws. ›

interpretation boolean_algebra diff_upred not_upred conj_upred "(≤)" "(<)"
  disj_upred false_upred true_upred
  by (unfold_locales; pred_auto)

lemma taut_true [simp]: "`true`"
  by (pred_auto)

lemma taut_false [simp]: "`false` = False"
  by (pred_auto)

lemma taut_conj: "`A ∧ B` = (`A` ∧ `B`)"
  by (rel_auto)

lemma taut_conj_elim [elim!]:
  "⟦ `A ∧ B`; ⟦ `A`; `B` ⟧ ⟹ P ⟧ ⟹ P"
  by (rel_auto)

lemma taut_refine_impl: "⟦ Q ⊑ P; `P` ⟧ ⟹ `Q`"
  by (rel_auto)

lemma taut_shEx_elim: 
  "⟦ `(❙∃ x ∙ P x)`; ⋀ x. Σ ♯ P x; ⋀ x. `P x` ⟹ Q  ⟧ ⟹ Q"
  by (rel_blast)

text ‹ Linking refinement and HOL implication ›

lemma refine_prop_intro:
  assumes "Σ ♯ P" "Σ ♯ Q" "`Q` ⟹ `P`"
  shows "P ⊑ Q"
  using assms
  by (pred_auto)

lemma taut_not: "Σ ♯ P ⟹ (¬ `P`) = `¬ P`"
  by (rel_auto)

lemma taut_shAll_intro:
  "∀ x. `P x` ⟹ `❙∀ x ∙ P x`"
  by (rel_auto)

lemma taut_shAll_intro_2:
  "∀ x y. `P x y` ⟹ `❙∀ (x, y) ∙ P x y`"
  by (rel_auto)

lemma taut_impl_intro:
  "⟦ Σ ♯ P; `P` ⟹ `Q` ⟧ ⟹ `P ⇒ Q`"
  by (rel_auto)

lemma upred_eval_taut:
  "`P⟦«b»/&❙v⟧` = ⟦P⟧⇩eb"
  by (pred_auto)
    
lemma refBy_order: "P ⊑ Q = `Q ⇒ P`"
  by (pred_auto)

lemma conj_idem [simp]: "((P::'α upred) ∧ P) = P"
  by (pred_auto)

lemma disj_idem [simp]: "((P::'α upred) ∨ P) = P"
  by (pred_auto)

lemma conj_comm: "((P::'α upred) ∧ Q) = (Q ∧ P)"
  by (pred_auto)

lemma disj_comm: "((P::'α upred) ∨ Q) = (Q ∨ P)"
  by (pred_auto)

lemma conj_subst: "P = R ⟹ ((P::'α upred) ∧ Q) = (R ∧ Q)"
  by (pred_auto)

lemma disj_subst: "P = R ⟹ ((P::'α upred) ∨ Q) = (R ∨ Q)"
  by (pred_auto)

lemma conj_assoc:"(((P::'α upred) ∧ Q) ∧ S) = (P ∧ (Q ∧ S))"
  by (pred_auto)

lemma disj_assoc:"(((P::'α upred) ∨ Q) ∨ S) = (P ∨ (Q ∨ S))"
  by (pred_auto)

lemma conj_disj_abs:"((P::'α upred) ∧ (P ∨ Q)) = P"
  by (pred_auto)

lemma disj_conj_abs:"((P::'α upred) ∨ (P ∧ Q)) = P"
  by (pred_auto)

lemma conj_disj_distr:"((P::'α upred) ∧ (Q ∨ R)) = ((P ∧ Q) ∨ (P ∧ R))"
  by (pred_auto)

lemma disj_conj_distr:"((P::'α upred) ∨ (Q ∧ R)) = ((P ∨ Q) ∧ (P ∨ R))"
  by (pred_auto)

lemma true_disj_zero [simp]:
  "(P ∨ true) = true" "(true ∨ P) = true"
  by (pred_auto)+

lemma true_conj_zero [simp]:
  "(P ∧ false) = false" "(false ∧ P) = false"
  by (pred_auto)+

lemma false_sup [simp]: "false ⊓ P = P" "P ⊓ false = P"
  by (pred_auto)+

lemma true_inf [simp]: "true ⊔ P = P" "P ⊔ true = P"
  by (pred_auto)+

lemma imp_vacuous [simp]: "(false ⇒ u) = true"
  by (pred_auto)

lemma imp_true [simp]: "(p ⇒ true) = true"
  by (pred_auto)

lemma true_imp [simp]: "(true ⇒ p) = p"
  by (pred_auto)

lemma impl_mp1 [simp]: "(P ∧ (P ⇒ Q)) = (P ∧ Q)"
  by (pred_auto)

lemma impl_mp2 [simp]: "((P ⇒ Q) ∧ P) = (Q ∧ P)"
  by (pred_auto)

lemma impl_adjoin: "((P ⇒ Q) ∧ R) = ((P ∧ R ⇒ Q ∧ R) ∧ R)"
  by (pred_auto)

lemma impl_refine_intro:
  "⟦ Q⇩1 ⊑ P⇩1; P⇩2 ⊑ (P⇩1 ∧ Q⇩2) ⟧ ⟹ (P⇩1 ⇒ P⇩2) ⊑ (Q⇩1 ⇒ Q⇩2)"
  by (pred_auto)

lemma spec_refine:
  "Q ⊑ (P ∧ R) ⟹ (P ⇒ Q) ⊑ R"
  by (rel_auto)
    
lemma impl_disjI: "⟦ `P ⇒ R`; `Q ⇒ R` ⟧ ⟹ `(P ∨ Q) ⇒ R`"
  by (rel_auto)

lemma conditional_iff:
  "(P ⇒ Q) = (P ⇒ R) ⟷ `P ⇒ (Q ⇔ R)`"
  by (pred_auto)

lemma p_and_not_p [simp]: "(P ∧ ¬ P) = false"
  by (pred_auto)

lemma p_or_not_p [simp]: "(P ∨ ¬ P) = true"
  by (pred_auto)

lemma p_imp_p [simp]: "(P ⇒ P) = true"
  by (pred_auto)

lemma p_iff_p [simp]: "(P ⇔ P) = true"
  by (pred_auto)

lemma p_imp_false [simp]: "(P ⇒ false) = (¬ P)"
  by (pred_auto)

lemma not_conj_deMorgans [simp]: "(¬ ((P::'α upred) ∧ Q)) = ((¬ P) ∨ (¬ Q))"
  by (pred_auto)

lemma not_disj_deMorgans [simp]: "(¬ ((P::'α upred) ∨ Q)) = ((¬ P) ∧ (¬ Q))"
  by (pred_auto)

lemma conj_disj_not_abs [simp]: "((P::'α upred) ∧ ((¬P) ∨ Q)) = (P ∧ Q)"
  by (pred_auto)

lemma subsumption1:
  "`P ⇒ Q` ⟹ (P ∨ Q) = Q"
  by (pred_auto)

lemma subsumption2:
  "`Q ⇒ P` ⟹ (P ∨ Q) = P"
  by (pred_auto)

lemma neg_conj_cancel1: "(¬ P ∧ (P ∨ Q)) = (¬ P ∧ Q :: 'α upred)"
  by (pred_auto)

lemma neg_conj_cancel2: "(¬ Q ∧ (P ∨ Q)) = (¬ Q ∧ P :: 'α upred)"
  by (pred_auto)

lemma double_negation [simp]: "(¬ ¬ (P::'α upred)) = P"
  by (pred_auto)

lemma true_not_false [simp]: "true ≠ false" "false ≠ true"
  by (pred_auto)+

lemma closure_conj_distr: "([P]⇩u ∧ [Q]⇩u) = [P ∧ Q]⇩u"
  by (pred_auto)

lemma closure_imp_distr: "`[P ⇒ Q]⇩u ⇒ [P]⇩u ⇒ [Q]⇩u`"
  by (pred_auto)

lemma true_iff [simp]: "(P ⇔ true) = P"
  by (pred_auto)

lemma taut_iff_eq:
  "`P ⇔ Q` ⟷ (P = Q)"
  by (pred_auto)
    
lemma impl_alt_def: "(P ⇒ Q) = (¬ P ∨ Q)"
  by (pred_auto)
    
subsection ‹ Lattice laws ›
    
lemma uinf_or:
  fixes P Q :: "'α upred"
  shows "(P ⊓ Q) = (P ∨ Q)"
  by (pred_auto)

lemma usup_and:
  fixes P Q :: "'α upred"
  shows "(P ⊔ Q) = (P ∧ Q)"
  by (pred_auto)

lemma UINF_alt_def:
  "(⨅ i | A(i) ∙ P(i)) = (⨅ i ∙ A(i) ∧ P(i))"
  by (rel_auto)
    
lemma USUP_true [simp]: "(⨆ P | F(P) ∙ true) = true"
  by (pred_auto)

lemma UINF_mem_UNIV [simp]: "(⨅ x∈UNIV ∙ P(x)) = (⨅ x ∙ P(x))"
  by (pred_auto)

lemma USUP_mem_UNIV [simp]: "(⨆ x∈UNIV ∙ P(x)) = (⨆ x ∙ P(x))"
  by (pred_auto)

lemma USUP_false [simp]: "(⨆ i ∙ false) = false"
  by (pred_simp)

lemma USUP_mem_false [simp]: "I ≠ {} ⟹ (⨆ i∈I ∙ false) = false"
  by (rel_simp)

lemma USUP_where_false [simp]: "(⨆ i | false ∙ P(i)) = true"
  by (rel_auto)

lemma UINF_true [simp]: "(⨅ i ∙ true) = true"
  by (pred_simp)

lemma UINF_ind_const [simp]: 
  "(⨅ i ∙ P) = P"
  by (rel_auto)
    
lemma UINF_mem_true [simp]: "A ≠ {} ⟹ (⨅ i∈A ∙ true) = true"
  by (pred_auto)

lemma UINF_false [simp]: "(⨅ i | P(i) ∙ false) = false"
  by (pred_auto)

lemma UINF_where_false [simp]: "(⨅ i | false ∙ P(i)) = false"
  by (rel_auto)

lemma UINF_cong_eq:
  "⟦ ⋀ x. P⇩1(x) = P⇩2(x); ⋀ x. `P⇩1(x) ⇒ Q⇩1(x) =⇩u Q⇩2(x)` ⟧ ⟹
        (⨅ x | P⇩1(x) ∙ Q⇩1(x)) = (⨅ x | P⇩2(x) ∙ Q⇩2(x))"
 by (unfold UINF_def, pred_simp, metis)

lemma UINF_as_Sup: "(⨅ P ∈ 𝒫 ∙ P) = ⨅ 𝒫"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Sup_uexpr_def)
  apply (pred_simp)
  apply (rule cong[of "Sup"])
   apply (auto)
  done

lemma UINF_as_Sup_collect: "(⨅P∈A ∙ f(P)) = (⨅P∈A. f(P))"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Sup_uexpr_def)
  apply (pred_simp)
  apply (simp add: Setcompr_eq_image)
  done

lemma UINF_as_Sup_collect': "(⨅P ∙ f(P)) = (⨅P. f(P))"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Sup_uexpr_def)
  apply (pred_simp)
  apply (simp add: full_SetCompr_eq)
  done

lemma UINF_as_Sup_image: "(⨅ P | «P» ∈⇩u «A» ∙ f(P)) = ⨅ (f ` A)"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Sup_uexpr_def)
  apply (pred_simp)
  apply (rule cong[of "Sup"])
   apply (auto)
  done

lemma USUP_as_Inf: "(⨆ P ∈ 𝒫 ∙ P) = ⨆ 𝒫"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Inf_uexpr_def)
  apply (pred_simp)
  apply (rule cong[of "Inf"])
   apply (auto)
  done

lemma USUP_as_Inf_collect: "(⨆P∈A ∙ f(P)) = (⨆P∈A. f(P))"
  apply (pred_simp)
  apply (simp add: Setcompr_eq_image)
  done

lemma USUP_as_Inf_collect': "(⨆P ∙ f(P)) = (⨆P. f(P))"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Sup_uexpr_def)
  apply (pred_simp)
  apply (simp add: full_SetCompr_eq)
  done

lemma USUP_as_Inf_image: "(⨆ P ∈ 𝒫 ∙ f(P)) = ⨆ (f ` 𝒫)"
  apply (simp add: upred_defs bop.rep_eq lit.rep_eq Inf_uexpr_def)
  apply (pred_simp)
  apply (rule cong[of "Inf"])
   apply (auto)
  done

lemma USUP_image_eq [simp]: "USUP (λi. «i» ∈⇩u «f ` A») g = (⨆ i∈A ∙ g(f(i)))"
  by (pred_simp, rule_tac cong[of Inf Inf], auto)

lemma UINF_image_eq [simp]: "UINF (λi. «i» ∈⇩u «f ` A») g = (⨅ i∈A ∙ g(f(i)))"
  by (pred_simp, rule_tac cong[of Sup Sup], auto)

lemma subst_continuous [usubst]: "σ † (⨅ A) = (⨅ {σ † P | P. P ∈ A})"
  by (simp add: UINF_as_Sup[THEN sym] usubst setcompr_eq_image)

lemma not_UINF: "(¬ (⨅ i∈A∙ P(i))) = (⨆ i∈A∙ ¬ P(i))"
  by (pred_auto)

lemma not_USUP: "(¬ (⨆ i∈A∙ P(i))) = (⨅ i∈A∙ ¬ P(i))"
  by (pred_auto)

lemma not_UINF_ind: "(¬ (⨅ i ∙ P(i))) = (⨆ i ∙ ¬ P(i))"
  by (pred_auto)

lemma not_USUP_ind: "(¬ (⨆ i ∙ P(i))) = (⨅ i ∙ ¬ P(i))"
  by (pred_auto)

lemma UINF_empty [simp]: "(⨅ i ∈ {} ∙ P(i)) = false"
  by (pred_auto)

lemma UINF_insert [simp]: "(⨅ i∈insert x xs ∙ P(i)) = (P(x) ⊓ (⨅ i∈xs ∙ P(i)))"
  apply (pred_simp)
  apply (subst Sup_insert[THEN sym])
  apply (rule_tac cong[of Sup Sup])
   apply (auto)
  done
    
lemma UINF_atLeast_first:
  "P(n) ⊓ (⨅ i ∈ {Suc n..} ∙ P(i)) = (⨅ i ∈ {n..} ∙ P(i))"
proof -
  have "insert n {Suc n..} = {n..}"
    by (auto)
  thus ?thesis
    by (metis UINF_insert)
qed  

lemma UINF_atLeast_Suc:
  "(⨅ i ∈ {Suc m..} ∙ P(i)) = (⨅ i ∈ {m..} ∙ P(Suc i))"
  by (rel_simp, metis (full_types) Suc_le_D not_less_eq_eq)

lemma USUP_empty [simp]: "(⨆ i ∈ {} ∙ P(i)) = true"
  by (pred_auto)

lemma USUP_insert [simp]: "(⨆ i∈insert x xs ∙ P(i)) = (P(x) ⊔ (⨆ i∈xs ∙ P(i)))"
  apply (pred_simp)
  apply (subst Inf_insert[THEN sym])
  apply (rule_tac cong[of Inf Inf])
   apply (auto)
  done

lemma USUP_atLeast_first:
  "(P(n) ∧ (⨆ i ∈ {Suc n..} ∙ P(i))) = (⨆ i ∈ {n..} ∙ P(i))"
proof -
  have "insert n {Suc n..} = {n..}"
    by (auto)
  thus ?thesis
    by (metis USUP_insert conj_upred_def)
qed

lemma USUP_atLeast_Suc:
  "(⨆ i ∈ {Suc m..} ∙ P(i)) = (⨆ i ∈ {m..} ∙ P(Suc i))"
  by (rel_simp, metis (full_types) Suc_le_D not_less_eq_eq)

lemma conj_UINF_dist:
  "(P ∧ (⨅ Q∈S ∙ F(Q))) = (⨅ Q∈S ∙ P ∧ F(Q))"
  by (simp add: upred_defs bop.rep_eq lit.rep_eq, pred_auto)

lemma conj_UINF_ind_dist:
  "(P ∧ (⨅ Q ∙ F(Q))) = (⨅ Q ∙ P ∧ F(Q))"
  by pred_auto

lemma disj_UINF_dist:
  "S ≠ {} ⟹ (P ∨ (⨅ Q∈S ∙ F(Q))) = (⨅ Q∈S ∙ P ∨ F(Q))"
  by (simp add: upred_defs bop.rep_eq lit.rep_eq, pred_auto)

lemma UINF_conj_UINF [simp]: 
  "((⨅ i∈I ∙ P(i)) ∨ (⨅ i∈I ∙ Q(i))) = (⨅ i∈I ∙ P(i) ∨ Q(i))"
  by (rel_auto)

lemma conj_USUP_dist:
  "S ≠ {} ⟹ (P ∧ (⨆ Q∈S ∙ F(Q))) = (⨆ Q∈S ∙ P ∧ F(Q))"
  by (subst uexpr_eq_iff, auto simp add: conj_upred_def USUP.rep_eq inf_uexpr.rep_eq bop.rep_eq lit.rep_eq)

lemma USUP_conj_USUP [simp]: "((⨆ P ∈ A ∙ F(P)) ∧ (⨆ P ∈ A ∙ G(P))) = (⨆ P ∈ A ∙ F(P) ∧ G(P))"
  by (simp add: upred_defs bop.rep_eq lit.rep_eq, pred_auto)

lemma UINF_all_cong [cong]:
  assumes "⋀ P. F(P) = G(P)"
  shows "(⨅ P ∙ F(P)) = (⨅ P ∙ G(P))"
  by (simp add: UINF_as_Sup_collect assms)

lemma UINF_cong:
  assumes "⋀ P. P ∈ A ⟹ F(P) = G(P)"
  shows "(⨅ P∈A ∙ F(P)) = (⨅ P∈A ∙ G(P))"
  by (simp add: UINF_as_Sup_collect assms)

lemma USUP_all_cong:
  assumes "⋀ P. F(P) = G(P)"
  shows "(⨆ P ∙ F(P)) = (⨆ P ∙ G(P))"
  by (simp add: assms)
    
lemma USUP_cong:
  assumes "⋀ P. P ∈ A ⟹ F(P) = G(P)"
  shows "(⨆ P∈A ∙ F(P)) = (⨆ P∈A ∙ G(P))"
  by (simp add: USUP_as_Inf_collect assms)

lemma UINF_subset_mono: "A ⊆ B ⟹ (⨅ P∈B ∙ F(P)) ⊑ (⨅ P∈A ∙ F(P))"
  by (simp add: SUP_subset_mono UINF_as_Sup_collect)

lemma USUP_subset_mono: "A ⊆ B ⟹ (⨆ P∈A ∙ F(P)) ⊑ (⨆ P∈B ∙ F(P))"
  by (simp add: INF_superset_mono USUP_as_Inf_collect)

lemma UINF_impl: "(⨅ P∈A ∙ F(P) ⇒ G(P)) = ((⨆ P∈A ∙ F(P)) ⇒ (⨅ P∈A ∙ G(P)))"
  by (pred_auto)

lemma USUP_is_forall: "(⨆ x ∙ P(x)) = (❙∀ x ∙ P(x))"
  by (pred_simp)

lemma USUP_ind_is_forall: "(⨆ x∈A ∙ P(x)) = (❙∀ x∈«A» ∙ P(x))"
  by (pred_auto)

lemma UINF_is_exists: "(⨅ x ∙ P(x)) = (❙∃ x ∙ P(x))"
  by (pred_simp)

lemma UINF_all_nats [simp]:
  fixes P :: "nat ⇒ 'α upred"
  shows "(⨅ n ∙ ⨅ i∈{0..n} ∙ P(i)) = (⨅ n ∙ P(n))"
  by (pred_auto)

lemma USUP_all_nats [simp]:
  fixes P :: "nat ⇒ 'α upred"
  shows "(⨆ n ∙ ⨆ i∈{0..n} ∙ P(i)) = (⨆ n ∙ P(n))"
  by (pred_auto)

lemma UINF_upto_expand_first:
  "m < n ⟹ (⨅ i ∈ {m..<n} ∙ P(i)) = ((P(m) :: 'α upred) ∨ (⨅ i ∈ {Suc m..<n} ∙ P(i)))"
  apply (rel_auto) using Suc_leI le_eq_less_or_eq by auto

lemma UINF_upto_expand_last:
  "(⨅ i ∈ {0..<Suc(n)} ∙ P(i)) = ((⨅ i ∈ {0..<n} ∙ P(i)) ∨ P(n))"
  apply (rel_auto)
  using less_SucE by blast
    
lemma UINF_Suc_shift: "(⨅ i ∈ {Suc 0..<Suc n} ∙ P(i)) = (⨅ i ∈ {0..<n} ∙ P(Suc i))"
  apply (rel_simp)
  apply (rule cong[of Sup], auto)
  using less_Suc_eq_0_disj by auto

lemma USUP_upto_expand_first:
  "(⨆ i ∈ {0..<Suc(n)} ∙ P(i)) = (P(0) ∧ (⨆ i ∈ {1..<Suc(n)} ∙ P(i)))"
  apply (rel_auto)
  using not_less by auto

lemma USUP_Suc_shift: "(⨆ i ∈ {Suc 0..<Suc n} ∙ P(i)) = (⨆ i ∈ {0..<n} ∙ P(Suc i))"
  apply (rel_simp)
  apply (rule cong[of Inf], auto)
  using less_Suc_eq_0_disj by auto
    
lemma UINF_list_conv:
  "(⨅ i ∈ {0..<length(xs)} ∙ f (xs ! i)) = foldr (∨) (map f xs) false"    
  apply (induct xs)
   apply (rel_auto)
  apply (simp add: UINF_upto_expand_first UINF_Suc_shift)
  done

lemma USUP_list_conv:
  "(⨆ i ∈ {0..<length(xs)} ∙ f (xs ! i)) = foldr (∧) (map f xs) true"    
  apply (induct xs)
   apply (rel_auto)
  apply (simp_all add: USUP_upto_expand_first USUP_Suc_shift)
  done

lemma UINF_refines:
  "⟦ ⋀ i. i∈I ⟹ P ⊑ Q i ⟧ ⟹ P ⊑ (⨅ i∈I ∙ Q i)"
  by (simp add: UINF_as_Sup_collect, metis SUP_least)

lemma UINF_refines':
  assumes "⋀ i. P ⊑ Q(i)" 
  shows "P ⊑ (⨅ i ∙ Q(i))"
  using assms
  apply (rel_auto) using Sup_le_iff by fastforce

lemma UINF_pred_ueq [simp]: 
  "(⨅ x | «x» =⇩u v ∙ P(x)) = (P x)⟦x→v⟧"
  by (pred_auto)

lemma UINF_pred_lit_eq [simp]: 
  "(⨅ x | «x = v» ∙ P(x)) = (P v)"
  by (pred_auto)

subsection ‹ Equality laws ›

lemma eq_upred_refl [simp]: "(x =⇩u x) = true"
  by (pred_auto)

lemma eq_upred_sym: "(x =⇩u y) = (y =⇩u x)"
  by (pred_auto)

lemma eq_cong_left:
  assumes "vwb_lens x" "$x ♯ Q" "$x´ ♯ Q" "$x ♯ R" "$x´ ♯ R"
  shows "(($x´ =⇩u $x ∧ Q) = ($x´ =⇩u $x ∧ R)) ⟷ (Q = R)"
  using assms
  by (pred_simp, (meson mwb_lens_def vwb_lens_mwb weak_lens_def)+)

lemma conj_eq_in_var_subst:
  fixes x :: "('a ⟹ 'α)"
  assumes "vwb_lens x"
  shows "(P ∧ $x =⇩u v) = (P⟦v/$x⟧ ∧ $x =⇩u v)"
  using assms
  by (pred_simp, (metis vwb_lens_wb wb_lens.get_put)+)

lemma conj_eq_out_var_subst:
  fixes x :: "('a ⟹ 'α)"
  assumes "vwb_lens x"
  shows "(P ∧ $x´ =⇩u v) = (P⟦v/$x´⟧ ∧ $x´ =⇩u v)"
  using assms
  by (pred_simp, (metis vwb_lens_wb wb_lens.get_put)+)

lemma conj_pos_var_subst:
  assumes "vwb_lens x"
  shows "($x ∧ Q) = ($x ∧ Q⟦true/$x⟧)"
  using assms
  by (pred_auto, metis (full_types) vwb_lens_wb wb_lens.get_put, metis (full_types) vwb_lens_wb wb_lens.get_put)

lemma conj_neg_var_subst:
  assumes "vwb_lens x"
  shows "(¬ $x ∧ Q) = (¬ $x ∧ Q⟦false/$x⟧)"
  using assms
  by (pred_auto, metis (full_types) vwb_lens_wb wb_lens.get_put, metis (full_types) vwb_lens_wb wb_lens.get_put)

lemma upred_eq_true [simp]: "(p =⇩u true) = p"
  by (pred_auto)

lemma upred_eq_false [simp]: "(p =⇩u false) = (¬ p)"
  by (pred_auto)

lemma upred_true_eq [simp]: "(true =⇩u p) = p"
  by (pred_auto)

lemma upred_false_eq [simp]: "(false =⇩u p) = (¬ p)"
  by (pred_auto)

lemma conj_var_subst:
  assumes "vwb_lens x"
  shows "(P ∧ var x =⇩u v) = (P⟦v/x⟧ ∧ var x =⇩u v)"
  using assms
  by (pred_simp, (metis (full_types) vwb_lens_def wb_lens.get_put)+)

subsection ‹ HOL Variable Quantifiers ›
    
lemma shEx_unbound [simp]: "(❙∃ x ∙ P) = P"
  by (pred_auto)

lemma shEx_bool [simp]: "shEx P = (P True ∨ P False)"
  by (pred_simp, metis (full_types))

lemma shEx_commute: "(❙∃ x ∙ ❙∃ y ∙ P x y) = (❙∃ y ∙ ❙∃ x ∙ P x y)"
  by (pred_auto)

lemma shEx_cong: "⟦ ⋀ x. P x = Q x ⟧ ⟹ shEx P = shEx Q"
  by (pred_auto)

lemma shEx_insert: "(❙∃ x ∈ insert⇩u y A ∙ P(x)) = (P(x)⟦x→y⟧ ∨ (❙∃ x ∈ A ∙ P(x)))"
  by (pred_auto)

lemma shEx_one_point: "(❙∃ x ∙ «x» =⇩u v ∧ P(x)) = P(x)⟦x→v⟧"
  by (rel_auto)

lemma shAll_unbound [simp]: "(❙∀ x ∙ P) = P"
  by (pred_auto)

lemma shAll_bool [simp]: "shAll P = (P True ∧ P False)"
  by (pred_simp, metis (full_types))

lemma shAll_cong: "⟦ ⋀ x. P x = Q x ⟧ ⟹ shAll P = shAll Q"
  by (pred_auto)
    
text ‹ Quantifier lifting ›

named_theorems uquant_lift

lemma shEx_lift_conj_1 [uquant_lift]:
  "((❙∃ x ∙ P(x)) ∧ Q) = (❙∃ x ∙ P(x) ∧ Q)"
  by (pred_auto)

lemma shEx_lift_conj_2 [uquant_lift]:
  "(P ∧ (❙∃ x ∙ Q(x))) = (❙∃ x ∙ P ∧ Q(x))"
  by (pred_auto)

subsection ‹ Case Splitting ›
  
lemma eq_split_subst:
  assumes "vwb_lens x"
  shows "(P = Q) ⟷ (∀ v. P⟦«v»/x⟧ = Q⟦«v»/x⟧)"
  using assms
  by (pred_auto, metis vwb_lens_wb wb_lens.source_stability)

lemma eq_split_substI:
  assumes "vwb_lens x" "⋀ v. P⟦«v»/x⟧ = Q⟦«v»/x⟧"
  shows "P = Q"
  using assms(1) assms(2) eq_split_subst by blast

lemma taut_split_subst:
  assumes "vwb_lens x"
  shows "`P` ⟷ (∀ v. `P⟦«v»/x⟧`)"
  using assms
  by (pred_auto, metis vwb_lens_wb wb_lens.source_stability)

lemma eq_split:
  assumes "`P ⇒ Q`" "`Q ⇒ P`"
  shows "P = Q"
  using assms
  by (pred_auto)

lemma bool_eq_splitI:
  assumes "vwb_lens x" "P⟦true/x⟧ = Q⟦true/x⟧" "P⟦false/x⟧ = Q⟦false/x⟧"
  shows "P = Q"
  by (metis (full_types) assms eq_split_subst false_alt_def true_alt_def)

lemma subst_bool_split:
  assumes "vwb_lens x"
  shows "`P` = `(P⟦false/x⟧ ∧ P⟦true/x⟧)`"
proof -
  from assms have "`P` = (∀ v. `P⟦«v»/x⟧`)"
    by (subst taut_split_subst[of x], auto)
  also have "... = (`P⟦«True»/x⟧` ∧ `P⟦«False»/x⟧`)"
    by (metis (mono_tags, lifting))
  also have "... = `(P⟦false/x⟧ ∧ P⟦true/x⟧)`"
    by (pred_auto)
  finally show ?thesis .
qed

lemma subst_eq_replace:
  fixes x :: "('a ⟹ 'α)"
  shows "(p⟦u/x⟧ ∧ u =⇩u v) = (p⟦v/x⟧ ∧ u =⇩u v)"
  by (pred_auto)

subsection ‹ UTP Quantifiers ›
    
lemma one_point:
  assumes "mwb_lens x" "x ♯ v"
  shows "(∃ x ∙ P ∧ var x =⇩u v) = P⟦v/x⟧"
  using assms
  by (pred_auto)

lemma exists_twice: "mwb_lens x ⟹ (∃ x ∙ ∃ x ∙ P) = (∃ x ∙ P)"
  by (pred_auto)

lemma all_twice: "mwb_lens x ⟹ (∀ x ∙ ∀ x ∙ P) = (∀ x ∙ P)"
  by (pred_auto)

lemma exists_sub: "⟦ mwb_lens y; x ⊆⇩L y ⟧ ⟹ (∃ x ∙ ∃ y ∙ P) = (∃ y ∙ P)"
  by (pred_auto)

lemma all_sub: "⟦ mwb_lens y; x ⊆⇩L y ⟧ ⟹ (∀ x ∙ ∀ y ∙ P) = (∀ y ∙ P)"
  by (pred_auto)

lemma ex_commute:
  assumes "x ⨝ y"
  shows "(∃ x ∙ ∃ y ∙ P) = (∃ y ∙ ∃ x ∙ P)"
  using assms
  apply (pred_auto)
  using lens_indep_comm apply fastforce+
  done

lemma all_commute:
  assumes "x ⨝ y"
  shows "(∀ x ∙ ∀ y ∙ P) = (∀ y ∙ ∀ x ∙ P)"
  using assms
  apply (pred_auto)
  using lens_indep_comm apply fastforce+
  done

lemma ex_equiv:
  assumes "x ≈⇩L y"
  shows "(∃ x ∙ P) = (∃ y ∙ P)"
  using assms
  by (pred_simp, metis (no_types, lifting) lens.select_convs(2))

lemma all_equiv:
  assumes "x ≈⇩L y"
  shows "(∀ x ∙ P) = (∀ y ∙ P)"
  using assms
  by (pred_simp, metis (no_types, lifting) lens.select_convs(2))

lemma ex_zero:
  "(∃ ∅ ∙ P) = P"
  by (pred_auto)

lemma all_zero:
  "(∀ ∅ ∙ P) = P"
  by (pred_auto)

lemma ex_plus:
  "(∃ y;x ∙ P) = (∃ x ∙ ∃ y ∙ P)"
  by (pred_auto)

lemma all_plus:
  "(∀ y;x ∙ P) = (∀ x ∙ ∀ y ∙ P)"
  by (pred_auto)

lemma closure_all:
  "[P]⇩u = (∀ Σ ∙ P)"
  by (pred_auto)

lemma unrest_as_exists:
  "vwb_lens x ⟹ (x ♯ P) ⟷ ((∃ x ∙ P) = P)"
  by (pred_simp, metis vwb_lens.put_eq)

lemma ex_mono: "P ⊑ Q ⟹ (∃ x ∙ P) ⊑ (∃ x ∙ Q)"
  by (pred_auto)

lemma ex_weakens: "wb_lens x ⟹ (∃ x ∙ P) ⊑ P"
  by (pred_simp, metis wb_lens.get_put)

lemma all_mono: "P ⊑ Q ⟹ (∀ x ∙ P) ⊑ (∀ x ∙ Q)"
  by (pred_auto)

lemma all_strengthens: "wb_lens x ⟹ P ⊑ (∀ x ∙ P)"
  by (pred_simp, metis wb_lens.get_put)

lemma ex_unrest: "x ♯ P ⟹ (∃ x ∙ P) = P"
  by (pred_auto)

lemma all_unrest: "x ♯ P ⟹ (∀ x ∙ P) = P"
  by (pred_auto)

lemma not_ex_not: "¬ (∃ x ∙ ¬ P) = (∀ x ∙ P)"
  by (pred_auto)

lemma not_all_not: "¬ (∀ x ∙ ¬ P) = (∃ x ∙ P)"
  by (pred_auto)

lemma ex_conj_contr_left: "x ♯ P ⟹ (∃ x ∙ P ∧ Q) = (P ∧ (∃ x ∙ Q))"
  by (pred_auto)

lemma ex_conj_contr_right: "x ♯ Q ⟹ (∃ x ∙ P ∧ Q) = ((∃ x ∙ P) ∧ Q)"
  by (pred_auto)

subsection ‹ Variable Restriction ›    
  
lemma var_res_all: 
  "P ↾⇩v Σ = P"
  by (rel_auto)
  
lemma var_res_twice: 
  "mwb_lens x ⟹ P ↾⇩v x ↾⇩v x = P ↾⇩v x"
  by (pred_auto)
    
subsection ‹ Conditional laws ›

lemma cond_def:
  "(P ◃ b ▹ Q) = ((b ∧ P) ∨ ((¬ b) ∧ Q))"
  by (pred_auto)
    
lemma cond_idem [simp]:"(P ◃ b ▹ P) = P" by (pred_auto)

lemma cond_true_false [simp]: "true ◃ b ▹ false = b" by (pred_auto)
    
lemma cond_symm:"(P ◃ b ▹ Q) = (Q ◃ ¬ b ▹ P)" by (pred_auto)

lemma cond_assoc: "((P ◃ b ▹ Q) ◃ c ▹ R) = (P ◃ b ∧ c ▹ (Q ◃ c ▹ R))" by (pred_auto)

lemma cond_distr: "(P ◃ b ▹ (Q ◃ c ▹ R)) = ((P ◃ b ▹ Q) ◃ c ▹ (P ◃ b ▹ R))" by (pred_auto)

lemma cond_unit_T [simp]:"(P ◃ true ▹ Q) = P" by (pred_auto)

lemma cond_unit_F [simp]:"(P ◃ false ▹ Q) = Q" by (pred_auto)

lemma cond_conj_not: "((P ◃ b ▹ Q) ∧ (¬ b)) = (Q ∧ (¬ b))"
  by (rel_auto)
    
lemma cond_and_T_integrate:
  "((P ∧ b) ∨ (Q ◃ b ▹ R)) = ((P ∨ Q) ◃ b ▹ R)"
  by (pred_auto)

lemma cond_L6: "(P ◃ b ▹ (Q ◃ b ▹ R)) = (P ◃ b ▹ R)" by (pred_auto)

lemma cond_L7: "(P ◃ b ▹ (P ◃ c ▹ Q)) = (P ◃ b ∨ c ▹ Q)" by (pred_auto)

lemma cond_and_distr: "((P ∧ Q) ◃ b ▹ (R ∧ S)) = ((P ◃ b ▹ R) ∧ (Q ◃ b ▹ S))" by (pred_auto)

lemma cond_or_distr: "((P ∨ Q) ◃ b ▹ (R ∨ S)) = ((P ◃ b ▹ R) ∨ (Q ◃ b ▹ S))" by (pred_auto)

lemma cond_imp_distr:
"((P ⇒ Q) ◃ b ▹ (R ⇒ S)) = ((P ◃ b ▹ R) ⇒ (Q ◃ b ▹ S))" by (pred_auto)

lemma cond_eq_distr:
"((P ⇔ Q) ◃ b ▹ (R ⇔ S)) = ((P ◃ b ▹ R) ⇔ (Q ◃ b ▹ S))" by (pred_auto)

lemma cond_conj_distr:"(P ∧ (Q ◃ b ▹ S)) = ((P ∧ Q) ◃ b ▹ (P ∧ S))" by (pred_auto)

lemma cond_disj_distr:"(P ∨ (Q ◃ b ▹ S)) = ((P ∨ Q) ◃ b ▹ (P ∨ S))" by (pred_auto)

lemma cond_neg: "¬ (P ◃ b ▹ Q) = ((¬ P) ◃ b ▹ (¬ Q))" by (pred_auto)

lemma cond_conj: "P ◃ b ∧ c ▹ Q = (P ◃ c ▹ Q) ◃ b ▹ Q"
  by (pred_auto)

lemma spec_cond_dist: "(P ⇒ (Q ◃ b ▹ R)) = ((P ⇒ Q) ◃ b ▹ (P ⇒ R))"
  by (pred_auto)

lemma cond_USUP_dist: "(⨆ P∈S ∙ F(P)) ◃ b ▹ (⨆ P∈S ∙ G(P)) = (⨆ P∈S ∙ F(P) ◃ b ▹ G(P))"
  by (pred_auto)

lemma cond_UINF_dist: "(⨅ P∈S ∙ F(P)) ◃ b ▹ (⨅ P∈S ∙ G(P)) = (⨅ P∈S ∙ F(P) ◃ b ▹ G(P))"
  by (pred_auto)

lemma cond_var_subst_left:
  assumes "vwb_lens x"
  shows "(P⟦true/x⟧ ◃ var x ▹ Q) = (P ◃ var x ▹ Q)"
  using assms by (pred_auto, metis (full_types) vwb_lens_wb wb_lens.get_put)

lemma cond_var_subst_right:
  assumes "vwb_lens x"
  shows "(P ◃ var x ▹ Q⟦false/x⟧) = (P ◃ var x ▹ Q)"
  using assms by (pred_auto, metis (full_types) vwb_lens.put_eq)

lemma cond_var_split:
  "vwb_lens x ⟹ (P⟦true/x⟧ ◃ var x ▹ P⟦false/x⟧) = P"
  by (rel_simp, (metis (full_types) vwb_lens.put_eq)+)

lemma cond_assign_subst:
  "vwb_lens x ⟹ (P ◃ utp_expr.var x =⇩u v ▹ Q) = (P⟦v/x⟧ ◃ utp_expr.var x =⇩u v ▹ Q)"
  apply (rel_simp) using vwb_lens.put_eq by force
    
lemma conj_conds: 
  "(P1 ◃ b ▹ Q1 ∧ P2 ◃ b ▹ Q2) = (P1 ∧ P2) ◃ b ▹ (Q1 ∧ Q2)"
  by pred_auto

lemma disj_conds:
  "(P1 ◃ b ▹ Q1 ∨ P2 ◃ b ▹ Q2) = (P1 ∨ P2) ◃ b ▹ (Q1 ∨ Q2)"
  by pred_auto

lemma cond_mono:
  "⟦ P⇩1 ⊑ P⇩2; Q⇩1 ⊑ Q⇩2 ⟧ ⟹ (P⇩1 ◃ b ▹ Q⇩1) ⊑ (P⇩2 ◃ b ▹ Q⇩2)"
  by (rel_auto)

lemma cond_monotonic:
  "⟦ mono P; mono Q ⟧ ⟹ mono (λ X. P X ◃ b ▹ Q X)"
  by (simp add: mono_def, rel_blast)

subsection ‹ Additional Expression Laws ›

lemma le_pred_refl [simp]:
  fixes x :: "('a::preorder, 'α) uexpr"
  shows "(x ≤⇩u x) = true"
  by (pred_auto)

lemma uzero_le_laws [simp]:
  "(0 :: ('a::{linordered_semidom}, 'α) uexpr) ≤⇩u numeral x = true"
  "(1 :: ('a::{linordered_semidom}, 'α) uexpr) ≤⇩u numeral x = true"
  "(0 :: ('a::{linordered_semidom}, 'α) uexpr) ≤⇩u 1 = true"
  by (pred_simp)+
  
lemma unumeral_le_1 [simp]:
  assumes "(numeral i :: 'a::{numeral,ord}) ≤ numeral j"
  shows "(numeral i :: ('a, 'α) uexpr) ≤⇩u numeral j = true"
  using assms by (pred_auto)

lemma unumeral_le_2 [simp]:
  assumes "(numeral i :: 'a::{numeral,linorder}) > numeral j"
  shows "(numeral i :: ('a, 'α) uexpr) ≤⇩u numeral j = false"
  using assms by (pred_auto)
    
lemma uset_laws [simp]:
  "x ∈⇩u {}⇩u = false"
  "x ∈⇩u {m..n}⇩u = (m ≤⇩u x ∧ x ≤⇩u n)"
  by (pred_auto)+
  
lemma ulit_eq [simp]: "x = y ⟹ («x» =⇩u «y») = true"
  by (rel_auto)
    
lemma ulit_neq [simp]: "x ≠ y ⟹ («x» =⇩u «y») = false"
  by (rel_auto)
    
lemma uset_mems [simp]:
  "x ∈⇩u {y}⇩u = (x =⇩u y)"
  "x ∈⇩u A ∪⇩u B = (x ∈⇩u A ∨ x ∈⇩u B)"
  "x ∈⇩u A ∩⇩u B = (x ∈⇩u A ∧ x ∈⇩u B)"
  by (rel_auto)+
    
subsection ‹ Refinement By Observation ›
    
text ‹ Function to obtain the set of observations of a predicate ›
    
definition obs_upred :: "'α upred ⇒ 'α set" ("⟦_⟧⇩o")
where [upred_defs]: "⟦P⟧⇩o = {b. ⟦P⟧⇩eb}"
    
lemma obs_upred_refine_iff: 
  "P ⊑ Q ⟷ ⟦Q⟧⇩o ⊆ ⟦P⟧⇩o"
  by (pred_auto)
    
text ‹ A refinement can be demonstrated by considering only the observations of the predicates
  which are relevant, i.e. not unrestricted, for them. In other words, if the alphabet can
  be split into two disjoint segments, $x$ and $y$, and neither predicate refers to $y$ then
  only $x$ need be considered when checking for observations. ›
    
lemma refine_by_obs:
  assumes "x ⨝ y" "bij_lens (x +⇩L y)" "y ♯ P" "y ♯ Q" "{v. `P⟦«v»/x⟧`} ⊆ {v. `Q⟦«v»/x⟧`}"
  shows "Q ⊑ P"
  using assms(3-5)
  apply (simp add: obs_upred_refine_iff subset_eq)
  apply (pred_simp)
  apply (rename_tac b)
  apply (drule_tac x="get⇘x⇙b" in spec)
  apply (auto simp add: assms)
   apply (metis assms(1) assms(2) bij_lens.axioms(2) bij_lens_axioms_def lens_override_def lens_override_plus)+
  done
    
subsection ‹ Cylindric Algebra ›

lemma C1: "(∃ x ∙ false) = false"
  by (pred_auto)

lemma C2: "wb_lens x ⟹ `P ⇒ (∃ x ∙ P)`"
  by (pred_simp, metis wb_lens.get_put)

lemma C3: "mwb_lens x ⟹ (∃ x ∙ (P ∧ (∃ x ∙ Q))) = ((∃ x ∙ P) ∧ (∃ x ∙ Q))"
  by (pred_auto)

lemma C4a: "x ≈⇩L y ⟹ (∃ x ∙ ∃ y ∙ P) = (∃ y ∙ ∃ x ∙ P)"
  by (pred_simp, metis (no_types, lifting) lens.select_convs(2))+

lemma C4b: "x ⨝ y ⟹ (∃ x ∙ ∃ y ∙ P) = (∃ y ∙ ∃ x ∙ P)"
  using ex_commute by blast

lemma C5:
  fixes x :: "('a ⟹ 'α)"
  shows "(&x =⇩u &x) = true"
  by (pred_auto)

lemma C6:
  assumes "wb_lens x" "x ⨝ y" "x ⨝ z"
  shows "(&y =⇩u &z) = (∃ x ∙ &y =⇩u &x ∧ &x =⇩u &z)"
  using assms
  by (pred_simp, (metis lens_indep_def)+)

lemma C7:
  assumes "weak_lens x" "x ⨝ y"
  shows "((∃ x ∙ &x =⇩u &y ∧ P) ∧ (∃ x ∙ &x =⇩u &y ∧ ¬ P)) = false"
  using assms
  by (pred_simp, simp add: lens_indep_sym)

end