Theory utp_rel_laws

section ‹ Relational Calculus Laws ›

theory utp_rel_laws
  imports 
    utp_rel
    utp_recursion
begin

subsection ‹ Conditional Laws ›
  
lemma comp_cond_left_distr:
  "((P ◃ b ▹⇩r Q) ;; R) = ((P ;; R) ◃ b ▹⇩r (Q ;; R))"
  by (rel_auto)

lemma cond_seq_left_distr:
  "outα ♯ b ⟹ ((P ◃ b ▹ Q) ;; R) = ((P ;; R) ◃ b ▹ (Q ;; R))"
  by (rel_auto)

lemma cond_seq_right_distr:
  "inα ♯ b ⟹ (P ;; (Q ◃ b ▹ R)) = ((P ;; Q) ◃ b ▹ (P ;; R))"
  by (rel_auto)

text ‹ Alternative expression of conditional using assumptions and choice ›

lemma rcond_rassume_expand: "P ◃ b ▹⇩r Q = ([b]⇧⊤ ;; P) ⊓ ([(¬ b)]⇧⊤ ;; Q)"
  by (rel_auto)

subsection ‹ Precondition and Postcondition Laws ›
  
theorem precond_equiv:
  "P = (P ;; true) ⟷ (outα ♯ P)"
  by (rel_auto)

theorem postcond_equiv:
  "P = (true ;; P) ⟷ (inα ♯ P)"
  by (rel_auto)

lemma precond_right_unit: "outα ♯ p ⟹ (p ;; true) = p"
  by (metis precond_equiv)

lemma postcond_left_unit: "inα ♯ p ⟹ (true ;; p) = p"
  by (metis postcond_equiv)

theorem precond_left_zero:
  assumes "outα ♯ p" "p ≠ false"
  shows "(true ;; p) = true"
  using assms by (rel_auto)

theorem feasibile_iff_true_right_zero:
  "P ;; true = true ⟷ `∃ outα ∙ P`"
  by (rel_auto)
    
subsection ‹ Sequential Composition Laws ›
    
lemma seqr_assoc: "(P ;; Q) ;; R = P ;; (Q ;; R)"
  by (rel_auto)

lemma seqr_left_unit [simp]:
  "II ;; P = P"
  by (rel_auto)

lemma seqr_right_unit [simp]:
  "P ;; II = P"
  by (rel_auto)

lemma seqr_left_zero [simp]:
  "false ;; P = false"
  by pred_auto

lemma seqr_right_zero [simp]:
  "P ;; false = false"
  by pred_auto

lemma impl_seqr_mono: "⟦ `P ⇒ Q`; `R ⇒ S` ⟧ ⟹ `(P ;; R) ⇒ (Q ;; S)`"
  by (pred_blast)

lemma seqr_mono:
  "⟦ P⇩1 ⊑ P⇩2; Q⇩1 ⊑ Q⇩2 ⟧ ⟹ (P⇩1 ;; Q⇩1) ⊑ (P⇩2 ;; Q⇩2)"
  by (rel_blast)
    
lemma seqr_monotonic:
  "⟦ mono P; mono Q ⟧ ⟹ mono (λ X. P X ;; Q X)"
  by (simp add: mono_def, rel_blast)
    
lemma Monotonic_seqr_tail [closure]:
  assumes "Monotonic F"
  shows "Monotonic (λ X. P ;; F(X))"
  by (simp add: assms monoD monoI seqr_mono)
    
lemma seqr_exists_left:
  "((∃ $x ∙ P) ;; Q) = (∃ $x ∙ (P ;; Q))"
  by (rel_auto)

lemma seqr_exists_right:
  "(P ;; (∃ $x´ ∙ Q)) = (∃ $x´ ∙ (P ;; Q))"
  by (rel_auto)

lemma seqr_or_distl:
  "((P ∨ Q) ;; R) = ((P ;; R) ∨ (Q ;; R))"
  by (rel_auto)

lemma seqr_or_distr:
  "(P ;; (Q ∨ R)) = ((P ;; Q) ∨ (P ;; R))"
  by (rel_auto)

lemma seqr_inf_distl:
  "((P ⊓ Q) ;; R) = ((P ;; R) ⊓ (Q ;; R))"
  by (rel_auto)

lemma seqr_inf_distr:
  "(P ;; (Q ⊓ R)) = ((P ;; Q) ⊓ (P ;; R))"
  by (rel_auto)

lemma seqr_and_distr_ufunc:
  "ufunctional P ⟹ (P ;; (Q ∧ R)) = ((P ;; Q) ∧ (P ;; R))"
  by (rel_auto)

lemma seqr_and_distl_uinj:
  "uinj R ⟹ ((P ∧ Q) ;; R) = ((P ;; R) ∧ (Q ;; R))"
  by (rel_auto)

lemma seqr_unfold:
  "(P ;; Q) = (❙∃ v ∙ P⟦«v»/$❙v´⟧ ∧ Q⟦«v»/$❙v⟧)"
  by (rel_auto)

lemma seqr_middle:
  assumes "vwb_lens x"
  shows "(P ;; Q) = (❙∃ v ∙ P⟦«v»/$x´⟧ ;; Q⟦«v»/$x⟧)"
  using assms
  by (rel_auto', metis vwb_lens_wb wb_lens.source_stability)

lemma seqr_left_one_point:
  assumes "vwb_lens x"
  shows "((P ∧ $x´ =⇩u «v») ;; Q) = (P⟦«v»/$x´⟧ ;; Q⟦«v»/$x⟧)"
  using assms
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put)

lemma seqr_right_one_point:
  assumes "vwb_lens x"
  shows "(P ;; ($x =⇩u «v» ∧ Q)) = (P⟦«v»/$x´⟧ ;; Q⟦«v»/$x⟧)"
  using assms
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put)

lemma seqr_left_one_point_true:
  assumes "vwb_lens x"
  shows "((P ∧ $x´) ;; Q) = (P⟦true/$x´⟧ ;; Q⟦true/$x⟧)"
  by (metis assms seqr_left_one_point true_alt_def upred_eq_true)

lemma seqr_left_one_point_false:
  assumes "vwb_lens x"
  shows "((P ∧ ¬$x´) ;; Q) = (P⟦false/$x´⟧ ;; Q⟦false/$x⟧)"
  by (metis assms false_alt_def seqr_left_one_point upred_eq_false)

lemma seqr_right_one_point_true:
  assumes "vwb_lens x"
  shows "(P ;; ($x ∧ Q)) = (P⟦true/$x´⟧ ;; Q⟦true/$x⟧)"
  by (metis assms seqr_right_one_point true_alt_def upred_eq_true)

lemma seqr_right_one_point_false:
  assumes "vwb_lens x"
  shows "(P ;; (¬$x ∧ Q)) = (P⟦false/$x´⟧ ;; Q⟦false/$x⟧)"
  by (metis assms false_alt_def seqr_right_one_point upred_eq_false)

lemma seqr_insert_ident_left:
  assumes "vwb_lens x" "$x´ ♯ P" "$x ♯ Q"
  shows "(($x´ =⇩u $x ∧ P) ;; Q) = (P ;; Q)"
  using assms
  by (rel_simp, meson vwb_lens_wb wb_lens_weak weak_lens.put_get)

lemma seqr_insert_ident_right:
  assumes "vwb_lens x" "$x´ ♯ P" "$x ♯ Q"
  shows "(P ;; ($x´ =⇩u $x ∧ Q)) = (P ;; Q)"
  using assms
  by (rel_simp, metis (no_types, opaque_lifting) vwb_lens_def wb_lens_def weak_lens.put_get)

lemma seq_var_ident_lift:
  assumes "vwb_lens x" "$x´ ♯ P" "$x ♯ Q"
  shows "(($x´ =⇩u $x ∧ P) ;; ($x´ =⇩u $x ∧ Q)) = ($x´ =⇩u $x ∧ (P ;; Q))"
  using assms by (rel_auto', metis (no_types, lifting) vwb_lens_wb wb_lens_weak weak_lens.put_get)

lemma seqr_bool_split:
  assumes "vwb_lens x"
  shows "P ;; Q = (P⟦true/$x´⟧ ;; Q⟦true/$x⟧ ∨ P⟦false/$x´⟧ ;; Q⟦false/$x⟧)"
  using assms
  by (subst seqr_middle[of x], simp_all)

lemma cond_inter_var_split:
  assumes "vwb_lens x"
  shows "(P ◃ $x´ ▹ Q) ;; R = (P⟦true/$x´⟧ ;; R⟦true/$x⟧ ∨ Q⟦false/$x´⟧ ;; R⟦false/$x⟧)"
proof -
  have "(P ◃ $x´ ▹ Q) ;; R = (($x´ ∧ P) ;; R ∨ (¬ $x´ ∧ Q) ;; R)"
    by (simp add: cond_def seqr_or_distl)
  also have "... = ((P ∧ $x´) ;; R ∨ (Q ∧ ¬$x´) ;; R)"
    by (rel_auto)
  also have "... = (P⟦true/$x´⟧ ;; R⟦true/$x⟧ ∨ Q⟦false/$x´⟧ ;; R⟦false/$x⟧)"
    by (simp add: seqr_left_one_point_true seqr_left_one_point_false assms)
  finally show ?thesis .
qed

theorem seqr_pre_transfer: "inα ♯ q ⟹ ((P ∧ q) ;; R) = (P ;; (q⇧- ∧ R))"
  by (rel_auto)

theorem seqr_pre_transfer':
  "((P ∧ ⌈q⌉⇩>) ;; R) = (P ;; (⌈q⌉⇩< ∧ R))"
  by (rel_auto)

theorem seqr_post_out: "inα ♯ r ⟹ (P ;; (Q ∧ r)) = ((P ;; Q) ∧ r)"
  by (rel_blast)

lemma seqr_post_var_out:
  fixes x :: "(bool ⟹ 'α)"
  shows "(P ;; (Q ∧ $x´)) = ((P ;; Q) ∧ $x´)"
  by (rel_auto)

theorem seqr_post_transfer: "outα ♯ q ⟹ (P ;; (q ∧ R)) = ((P ∧ q⇧-) ;; R)"
  by (rel_auto)

lemma seqr_pre_out: "outα ♯ p ⟹ ((p ∧ Q) ;; R) = (p ∧ (Q ;; R))"
  by (rel_blast)

lemma seqr_pre_var_out:
  fixes x :: "(bool ⟹ 'α)"
  shows "(($x ∧ P) ;; Q) = ($x ∧ (P ;; Q))"
  by (rel_auto)

lemma seqr_true_lemma:
  "(P = (¬ ((¬ P) ;; true))) = (P = (P ;; true))"
  by (rel_auto)

lemma seqr_to_conj: "⟦ outα ♯ P; inα ♯ Q ⟧ ⟹ (P ;; Q) = (P ∧ Q)"
  by (metis postcond_left_unit seqr_pre_out utp_pred_laws.inf_top.right_neutral)

lemma shEx_lift_seq_1 [uquant_lift]:
  "((❙∃ x ∙ P x) ;; Q) = (❙∃ x ∙ (P x ;; Q))"
  by rel_auto

lemma shEx_mem_lift_seq_1 [uquant_lift]:
  assumes "outα ♯ A"
  shows "((❙∃ x ∈ A ∙ P x) ;; Q) = (❙∃ x ∈ A ∙ (P x ;; Q))"
  using assms by rel_blast

lemma shEx_lift_seq_2 [uquant_lift]:
  "(P ;; (❙∃ x ∙ Q x)) = (❙∃ x ∙ (P ;; Q x))"
  by rel_auto

lemma shEx_mem_lift_seq_2 [uquant_lift]:
  assumes "inα ♯ A"
  shows "(P ;; (❙∃ x ∈ A ∙ Q x)) = (❙∃ x ∈ A ∙ (P ;; Q x))"
  using assms by rel_blast

subsection ‹ Iterated Sequential Composition Laws ›
  
lemma iter_seqr_nil [simp]: "(;; i : [] ∙ P(i)) = II"
  by (simp add: seqr_iter_def)
    
lemma iter_seqr_cons [simp]: "(;; i : (x # xs) ∙ P(i)) = P(x) ;; (;; i : xs ∙ P(i))"
  by (simp add: seqr_iter_def)

subsection ‹ Quantale Laws ›

lemma seq_Sup_distl: "P ;; (⨅ A) = (⨅ Q∈A. P ;; Q)"
  by (transfer, auto)

lemma seq_Sup_distr: "(⨅ A) ;; Q = (⨅ P∈A. P ;; Q)"
  by (transfer, auto)

lemma seq_UINF_distl: "P ;; (⨅ Q∈A ∙ F(Q)) = (⨅ Q∈A ∙ P ;; F(Q))"
  by (simp add: UINF_as_Sup_collect seq_Sup_distl)

lemma seq_UINF_distl': "P ;; (⨅ Q ∙ F(Q)) = (⨅ Q ∙ P ;; F(Q))"
  by (metis UINF_mem_UNIV seq_UINF_distl)

lemma seq_UINF_distr: "(⨅ P∈A ∙ F(P)) ;; Q = (⨅ P∈A ∙ F(P) ;; Q)"
  by (simp add: UINF_as_Sup_collect seq_Sup_distr)

lemma seq_UINF_distr': "(⨅ P ∙ F(P)) ;; Q = (⨅ P ∙ F(P) ;; Q)"
  by (metis UINF_mem_UNIV seq_UINF_distr)

lemma seq_SUP_distl: "P ;; (⨅i∈A. Q(i)) = (⨅i∈A. P ;; Q(i))"
  by (metis image_image seq_Sup_distl)

lemma seq_SUP_distr: "(⨅i∈A. P(i)) ;; Q = (⨅i∈A. P(i) ;; Q)"
  by (simp add: seq_Sup_distr)

subsection ‹ Skip Laws ›
    
lemma cond_skip: "outα ♯ b ⟹ (b ∧ II) = (II ∧ b⇧-)"
  by (rel_auto)

lemma pre_skip_post: "(⌈b⌉⇩< ∧ II) = (II ∧ ⌈b⌉⇩>)"
  by (rel_auto)

lemma skip_var:
  fixes x :: "(bool ⟹ 'α)"
  shows "($x ∧ II) = (II ∧ $x´)"
  by (rel_auto)

lemma skip_r_unfold:
  "vwb_lens x ⟹ II = ($x´ =⇩u $x ∧ II↾⇩αx)"
  by (rel_simp, metis mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put)

lemma skip_r_alpha_eq:
  "II = ($❙v´ =⇩u $❙v)"
  by (rel_auto)

lemma skip_ra_unfold:
  "II⇘x;y⇙ = ($x´ =⇩u $x ∧ II⇘y⇙)"
  by (rel_auto)

lemma skip_res_as_ra:
  "⟦ vwb_lens y; x +⇩L y ≈⇩L 1⇩L; x ⨝ y ⟧ ⟹ II↾⇩αx = II⇘y⇙"
  apply (rel_auto)
   apply (metis (no_types, lifting) lens_indep_def)
  apply (metis vwb_lens.put_eq)
  done

subsection ‹ Assignment Laws ›
  
lemma assigns_subst [usubst]:
  "⌈σ⌉⇩s † ⟨ρ⟩⇩a = ⟨ρ ∘ σ⟩⇩a"
  by (rel_auto)

lemma assigns_r_comp: "(⟨σ⟩⇩a ;; P) = (⌈σ⌉⇩s † P)"
  by (rel_auto)

lemma assigns_r_feasible:
  "(⟨σ⟩⇩a ;; true) = true"
  by (rel_auto)

lemma assign_subst [usubst]:
  "⟦ mwb_lens x; mwb_lens y ⟧ ⟹ [$x ↦⇩s ⌈u⌉⇩<] † (y := v) = (x, y) := (u, [x ↦⇩s u] † v)"
  by (rel_auto)

lemma assign_vacuous_skip:
  assumes "vwb_lens x"
  shows "(x := &x) = II"
  using assms by rel_auto

text ‹ The following law shows the case for the above law when $x$ is only mainly-well behaved. We
  require that the state is one of those in which $x$ is well defined using and assumption. ›

lemma assign_vacuous_assume:
  assumes "mwb_lens x"
  shows "[(&❙v ∈⇩u «𝒮⇘x⇙»)]⇧⊤ ;; (x := &x) = [(&❙v ∈⇩u «𝒮⇘x⇙»)]⇧⊤"
  using assms by rel_auto

lemma assign_simultaneous:
  assumes "vwb_lens y" "x ⨝ y"
  shows "(x,y) := (e, &y) = (x := e)"
  by (simp add: assms usubst_upd_comm usubst_upd_var_id)

lemma assigns_idem: "mwb_lens x ⟹ (x,x) := (u,v) = (x := v)"
  by (simp add: usubst)

lemma assigns_comp: "(⟨f⟩⇩a ;; ⟨g⟩⇩a) = ⟨g ∘ f⟩⇩a"
  by (simp add: assigns_r_comp usubst)

lemma assigns_cond: "(⟨f⟩⇩a ◃ b ▹⇩r ⟨g⟩⇩a) = ⟨f ◃ b ▹⇩s g⟩⇩a"
  by (rel_auto)

lemma assigns_r_conv:
  "bij f ⟹ ⟨f⟩⇩a⇧- = ⟨inv f⟩⇩a"
  by (rel_auto, simp_all add: bij_is_inj bij_is_surj surj_f_inv_f)

lemma assign_pred_transfer:
  fixes x :: "('a ⟹ 'α)"
  assumes "$x ♯ b" "outα ♯ b"
  shows "(b ∧ x := v) = (x := v ∧ b⇧-)"
  using assms by (rel_blast)
    
lemma assign_r_comp: "x := u ;; P = P⟦⌈u⌉⇩</$x⟧"
  by (simp add: assigns_r_comp usubst alpha)
    
lemma assign_test: "mwb_lens x ⟹ (x := «u» ;; x := «v») = (x := «v»)"
  by (simp add: assigns_comp usubst)

lemma assign_twice: "⟦ mwb_lens x; x ♯ f ⟧ ⟹ (x := e ;; x := f) = (x := f)"
  by (simp add: assigns_comp usubst unrest)
 
lemma assign_commute:
  assumes "x ⨝ y" "x ♯ f" "y ♯ e"
  shows "(x := e ;; y := f) = (y := f ;; x := e)"
  using assms
  by (rel_simp, simp_all add: lens_indep_comm)

lemma assign_cond:
  fixes x :: "('a ⟹ 'α)"
  assumes "outα ♯ b"
  shows "(x := e ;; (P ◃ b ▹ Q)) = ((x := e ;; P) ◃ (b⟦⌈e⌉⇩</$x⟧) ▹ (x := e ;; Q))"
  by (rel_auto)

lemma assign_rcond:
  fixes x :: "('a ⟹ 'α)"
  shows "(x := e ;; (P ◃ b ▹⇩r Q)) = ((x := e ;; P) ◃ (b⟦e/x⟧) ▹⇩r (x := e ;; Q))"
  by (rel_auto)

lemma assign_r_alt_def:
  fixes x :: "('a ⟹ 'α)"
  shows "x := v = II⟦⌈v⌉⇩</$x⟧"
  by (rel_auto)

lemma assigns_r_ufunc: "ufunctional ⟨f⟩⇩a"
  by (rel_auto)

lemma assigns_r_uinj: "inj f ⟹ uinj ⟨f⟩⇩a"
  by (rel_simp, simp add: inj_eq)
    
lemma assigns_r_swap_uinj:
  "⟦ vwb_lens x; vwb_lens y; x ⨝ y ⟧ ⟹ uinj ((x,y) := (&y,&x))"
  by (metis assigns_r_uinj pr_var_def swap_usubst_inj)

lemma assign_unfold:
  "vwb_lens x ⟹ (x := v) = ($x´ =⇩u ⌈v⌉⇩< ∧ II↾⇩αx)"
  apply (rel_auto, auto simp add: comp_def)
  using vwb_lens.put_eq by fastforce

subsection ‹ Non-deterministic Assignment Laws ›

lemma nd_assign_comp:
  "x ⨝ y ⟹ x := * ;; y := * = x,y := *"
  apply (rel_auto) using lens_indep_comm by fastforce+

lemma nd_assign_assign:
  "⟦ vwb_lens x; x ♯ e ⟧ ⟹ x := * ;; x := e = x := e"
  by (rel_auto)

subsection ‹ Converse Laws ›

lemma convr_invol [simp]: "p⇧-⇧- = p"
  by pred_auto

lemma lit_convr [simp]: "«v»⇧- = «v»"
  by pred_auto

lemma uivar_convr [simp]:
  fixes x :: "('a ⟹ 'α)"
  shows "($x)⇧- = $x´"
  by pred_auto

lemma uovar_convr [simp]:
  fixes x :: "('a ⟹ 'α)"
  shows "($x´)⇧- = $x"
  by pred_auto

lemma uop_convr [simp]: "(uop f u)⇧- = uop f (u⇧-)"
  by (pred_auto)

lemma bop_convr [simp]: "(bop f u v)⇧- = bop f (u⇧-) (v⇧-)"
  by (pred_auto)

lemma eq_convr [simp]: "(p =⇩u q)⇧- = (p⇧- =⇩u q⇧-)"
  by (pred_auto)

lemma not_convr [simp]: "(¬ p)⇧- = (¬ p⇧-)"
  by (pred_auto)

lemma disj_convr [simp]: "(p ∨ q)⇧- = (q⇧- ∨ p⇧-)"
  by (pred_auto)

lemma conj_convr [simp]: "(p ∧ q)⇧- = (q⇧- ∧ p⇧-)"
  by (pred_auto)

lemma seqr_convr [simp]: "(p ;; q)⇧- = (q⇧- ;; p⇧-)"
  by (rel_auto)

lemma pre_convr [simp]: "⌈p⌉⇩<⇧- = ⌈p⌉⇩>"
  by (rel_auto)

lemma post_convr [simp]: "⌈p⌉⇩>⇧- = ⌈p⌉⇩<"
  by (rel_auto)

subsection ‹ Assertion and Assumption Laws ›

declare sublens_def [lens_defs del]
  
lemma assume_false: "[false]⇧⊤ = false"
  by (rel_auto)
  
lemma assume_true: "[true]⇧⊤ = II"
  by (rel_auto)
    
lemma assume_seq: "[b]⇧⊤ ;; [c]⇧⊤ = [(b ∧ c)]⇧⊤"
  by (rel_auto)

lemma assert_false: "{false}⇩⊥ = true"
  by (rel_auto)

lemma assert_true: "{true}⇩⊥ = II"
  by (rel_auto)
    
lemma assert_seq: "{b}⇩⊥ ;; {c}⇩⊥ = {(b ∧ c)}⇩⊥"
  by (rel_auto)

subsection ‹ Frame and Antiframe Laws ›

named_theorems frame

lemma frame_all [frame]: "Σ:[P] = P"
  by (rel_auto)

lemma frame_none [frame]: 
  "∅:[P] = (P ∧ II)"
  by (rel_auto)

lemma frame_commute:
  assumes "$y ♯ P" "$y´ ♯ P" "$x ♯ Q" "$x´ ♯ Q" "x ⨝ y" 
  shows "x:[P] ;; y:[Q] = y:[Q] ;; x:[P]"
  apply (insert assms)
  apply (rel_auto)
   apply (rename_tac s s' s⇩0)
   apply (subgoal_tac "(s ⊕⇩L s' on y) ⊕⇩L s⇩0 on x = s⇩0 ⊕⇩L s' on y")
    apply (metis lens_indep_get lens_indep_sym lens_override_def)
   apply (simp add: lens_indep.lens_put_comm lens_override_def)
  apply (rename_tac s s' s⇩0)
  apply (subgoal_tac "put⇘y⇙ (put⇘x⇙ s (get⇘x⇙ (put⇘x⇙ s⇩0 (get⇘x⇙ s')))) (get⇘y⇙ (put⇘y⇙ s (get⇘y⇙ s⇩0))) 
                      = put⇘x⇙ s⇩0 (get⇘x⇙ s')")
   apply (metis lens_indep_get lens_indep_sym)
  apply (metis lens_indep.lens_put_comm)
  done

lemma frame_contract_RID:
  assumes "vwb_lens x" "P is RID(x)" "x ⨝ y"
  shows "(x;y):[P] = y:[P]"
proof -
  from assms(1,3) have "(x;y):[RID(x)(P)] = y:[RID(x)(P)]"
    apply (rel_auto)
     apply (simp add: lens_indep.lens_put_comm)
    apply (metis (no_types) vwb_lens_wb wb_lens.get_put)
    done
  thus ?thesis
    by (simp add: Healthy_if assms)
qed
 
lemma frame_miracle [simp]:
  "x:[false] = false"
  by (rel_auto)

lemma frame_skip [simp]:
  "vwb_lens x ⟹ x:[II] = II"
  by (rel_auto)
    
lemma frame_assign_in [frame]:
  "⟦ vwb_lens a; x ⊆⇩L a ⟧ ⟹ a:[x := v] = x := v"
  by (rel_auto, simp_all add: lens_get_put_quasi_commute lens_put_of_quotient)

lemma frame_conj_true [frame]:
  "⟦ {$x,$x´} ♮ P; vwb_lens x ⟧ ⟹ (P ∧ x:[true]) = x:[P]"
  by (rel_auto)
    
lemma frame_is_assign [frame]:
  "vwb_lens x ⟹ x:[$x´ =⇩u ⌈v⌉⇩<] = x := v"
  by (rel_auto)
    
lemma frame_seq [frame]:
  "⟦ vwb_lens x; {$x,$x´} ♮ P; {$x,$x´} ♮ Q ⟧ ⟹ x:[P ;; Q] = x:[P] ;; x:[Q]"
  apply (rel_auto)
   apply (metis mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens_def weak_lens.put_get)
  apply (metis mwb_lens.put_put vwb_lens_mwb)
  done

lemma frame_to_antiframe [frame]:
  "⟦ x ⨝ y; x +⇩L y = 1⇩L ⟧ ⟹ x:[P] = y:⟦P⟧"
  by (rel_auto, metis lens_indep_def, metis lens_indep_def surj_pair)

lemma rel_frext_miracle [frame]: 
  "a:[false]⇧+ = false"
  by (rel_auto)
    
lemma rel_frext_skip [frame]: 
  "vwb_lens a ⟹ a:[II]⇧+ = II"
  by (rel_auto)

lemma rel_frext_seq [frame]:
  "vwb_lens a ⟹ a:[P ;; Q]⇧+ = (a:[P]⇧+ ;; a:[Q]⇧+)"
  apply (rel_auto)
   apply (rename_tac s s' s⇩0)
   apply (rule_tac x="put⇘a⇙ s s⇩0" in exI)
   apply (auto)
  apply (metis mwb_lens.put_put vwb_lens_mwb)
  done

lemma rel_frext_assigns [frame]:
  "vwb_lens a ⟹ a:[⟨σ⟩⇩a]⇧+ = ⟨σ ⊕⇩s a⟩⇩a"
  by (rel_auto)

lemma rel_frext_rcond [frame]:
  "a:[P ◃ b ▹⇩r Q]⇧+ = (a:[P]⇧+ ◃ b ⊕⇩p a ▹⇩r a:[Q]⇧+)"
  by (rel_auto)

lemma rel_frext_commute: 
  "x ⨝ y ⟹ x:[P]⇧+ ;; y:[Q]⇧+ = y:[Q]⇧+ ;; x:[P]⇧+"
  apply (rel_auto)
   apply (rename_tac a c b)
   apply (subgoal_tac "⋀b a. get⇘y⇙ (put⇘x⇙ b a) = get⇘y⇙ b")
    apply (metis (no_types, opaque_lifting) lens_indep_comm lens_indep_get)
   apply (simp add: lens_indep.lens_put_irr2)
  apply (subgoal_tac "⋀b c. get⇘x⇙ (put⇘y⇙ b c) = get⇘x⇙ b")
   apply (subgoal_tac "⋀b a. get⇘y⇙ (put⇘x⇙ b a) = get⇘y⇙ b")
    apply (metis (mono_tags, lifting) lens_indep_comm)
   apply (simp_all add: lens_indep.lens_put_irr2)    
  done
    
lemma antiframe_disj [frame]: "(x:⟦P⟧ ∨ x:⟦Q⟧) = x:⟦P ∨ Q⟧"
  by (rel_auto)

lemma antiframe_seq [frame]:
  "⟦ vwb_lens x; $x´ ♯ P; $x ♯ Q ⟧  ⟹ (x:⟦P⟧ ;; x:⟦Q⟧) = x:⟦P ;; Q⟧"
  apply (rel_auto)
   apply (metis vwb_lens_wb wb_lens_def weak_lens.put_get)
  apply (metis vwb_lens_wb wb_lens.put_twice wb_lens_def weak_lens.put_get)
  done
  
lemma nameset_skip: "vwb_lens x ⟹ (ns x ∙ II) = II⇘x⇙"
  by (rel_auto, meson vwb_lens_wb wb_lens.get_put)
    
lemma nameset_skip_ra: "vwb_lens x ⟹ (ns x ∙ II⇘x⇙) = II⇘x⇙"
  by (rel_auto)
    
declare sublens_def [lens_defs]
    
subsection ‹ While Loop Laws ›

theorem while_unfold:
  "while b do P od = ((P ;; while b do P od) ◃ b ▹⇩r II)"
proof -
  have m:"mono (λX. (P ;; X) ◃ b ▹⇩r II)"
    by (auto intro: monoI seqr_mono cond_mono)
  have "(while b do P od) = (ν X ∙ (P ;; X) ◃ b ▹⇩r II)"
    by (simp add: while_top_def)
  also have "... = ((P ;; (ν X ∙ (P ;; X) ◃ b ▹⇩r II)) ◃ b ▹⇩r II)"
    by (subst lfp_unfold, simp_all add: m)
  also have "... = ((P ;; while b do P od) ◃ b ▹⇩r II)"
    by (simp add: while_top_def)
  finally show ?thesis .
qed

theorem while_false: "while false do P od = II"
  by (subst while_unfold, rel_auto)

theorem while_true: "while true do P od = false"
  apply (simp add: while_top_def alpha)
  apply (rule antisym)
   apply (simp_all)
  apply (rule lfp_lowerbound)
  apply (rel_auto)
  done

theorem while_bot_unfold:
  "while⇩⊥ b do P od = ((P ;; while⇩⊥ b do P od) ◃ b ▹⇩r II)"
proof -
  have m:"mono (λX. (P ;; X) ◃ b ▹⇩r II)"
    by (auto intro: monoI seqr_mono cond_mono)
  have "(while⇩⊥ b do P od) = (μ X ∙ (P ;; X) ◃ b ▹⇩r II)"
    by (simp add: while_bot_def)
  also have "... = ((P ;; (μ X ∙ (P ;; X) ◃ b ▹⇩r II)) ◃ b ▹⇩r II)"
    by (subst gfp_unfold, simp_all add: m)
  also have "... = ((P ;; while⇩⊥ b do P od) ◃ b ▹⇩r II)"
    by (simp add: while_bot_def)
  finally show ?thesis .
qed

theorem while_bot_false: "while⇩⊥ false do P od = II"
  by (simp add: while_bot_def mu_const alpha)

theorem while_bot_true: "while⇩⊥ true do P od = (μ X ∙ P ;; X)"
  by (simp add: while_bot_def alpha)

text ‹ An infinite loop with a feasible body corresponds to a program error (non-termination). ›

theorem while_infinite: "P ;; true⇩h = true ⟹ while⇩⊥ true do P od = true"
  apply (simp add: while_bot_true)
  apply (rule antisym)
   apply (simp)
  apply (rule gfp_upperbound)
  apply (simp)
  done

subsection ‹ Algebraic Properties ›

interpretation upred_semiring: semiring_1
  where times = seqr and one = skip_r and zero = false⇩h and plus = Lattices.sup
  by (unfold_locales, (rel_auto)+)

declare upred_semiring.power_Suc [simp del]

text ‹ We introduce the power syntax derived from semirings ›

abbreviation upower :: "'α hrel ⇒ nat ⇒ 'α hrel" (infixr "❙^" 80) where
"upower P n ≡ upred_semiring.power P n"

translations
  "P ❙^ i" <= "CONST power.power II op ;; P i"
  "P ❙^ i" <= "(CONST power.power II op ;; P) i"

text ‹ Set up transfer tactic for powers ›

lemma upower_rep_eq:
  "⟦P ❙^ i⟧⇩e = (λ b. b ∈ ({p. ⟦P⟧⇩e p} ^^ i))"
proof (induct i arbitrary: P)
  case 0
  then show ?case
    by (auto, rel_auto)
next
  case (Suc i)
  show ?case
    by (simp add: Suc seqr.rep_eq relpow_commute upred_semiring.power_Suc)
qed

lemma upower_rep_eq_alt:
  "⟦power.power ⟨id⟩⇩a (;;) P i⟧⇩e = (λb. b ∈ ({p. ⟦P⟧⇩e p} ^^ i))"
  by (metis skip_r_def upower_rep_eq)

update_uexpr_rep_eq_thms
  
lemma Sup_power_expand:
  fixes P :: "nat ⇒ 'a::complete_lattice"
  shows "P(0) ⊓ (⨅i. P(i+1)) = (⨅i. P(i))"
proof -
  have "UNIV = insert (0::nat) {1..}"
    by auto
  moreover have "(⨅i. P(i)) = ⨅ (P ` UNIV)"
    by (blast)
  moreover have "⨅ (P ` insert 0 {1..}) = P(0) ⊓ ⨅ (P ` {1..})"
    by (simp)
  moreover have "⨅ (P ` {1..}) = (⨅i. P(i+1))"
    by (simp add: atLeast_Suc_greaterThan greaterThan_0)
  ultimately show ?thesis
    by (simp only:)
qed

lemma Sup_upto_Suc: "(⨅i∈{0..Suc n}. P ❙^ i) = (⨅i∈{0..n}. P ❙^ i) ⊓ P ❙^ Suc n"
proof -
  have "(⨅i∈{0..Suc n}. P ❙^ i) = (⨅i∈insert (Suc n) {0..n}. P ❙^ i)"
    by (simp add: atLeast0_atMost_Suc)
  also have "... = P ❙^ Suc n ⊓ (⨅i∈{0..n}. P ❙^ i)"
    by (simp)
  finally show ?thesis
    by (simp add: Lattices.sup_commute)
qed

text ‹ The following two proofs are adapted from the AFP entry 
  \href{https://www.isa-afp.org/entries/Kleene_Algebra.shtml}{Kleene Algebra}. 
  See also~\<^cite>‹"Armstrong2012" and "Armstrong2015"›. ›

lemma upower_inductl: "Q ⊑ ((P ;; Q) ⊓ R) ⟹ Q ⊑ P ❙^ n ;; R"
proof (induct n)
  case 0
  then show ?case by (auto)
next
  case (Suc n)
  then show ?case
    by (auto simp add: upred_semiring.power_Suc, metis (no_types, opaque_lifting) dual_order.trans order_refl seqr_assoc seqr_mono)
qed

lemma upower_inductr:
  assumes "Q ⊑ R ⊓ (Q ;; P)"
  shows "Q ⊑ R ;; (P ❙^ n)"
using assms proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  have "R ;; P ❙^ Suc n = (R ;; P ❙^ n) ;; P"
    by (metis seqr_assoc upred_semiring.power_Suc2)
  also have "Q ;; P ⊑ ..."
    by (meson Suc.hyps assms eq_iff seqr_mono)
  also have "Q ⊑ ..."
    using assms by auto
  finally show ?case .
qed

lemma SUP_atLeastAtMost_first:
  fixes P :: "nat ⇒ 'a::complete_lattice"
  assumes "m ≤ n"
  shows "(⨅i∈{m..n}. P(i)) = P(m) ⊓ (⨅i∈{Suc m..n}. P(i))"
  by (metis SUP_insert assms atLeastAtMost_insertL)
    
lemma upower_seqr_iter: "P ❙^ n = (;; Q : replicate n P ∙ Q)"
  by (induct n, simp_all add: upred_semiring.power_Suc)

lemma assigns_power: "⟨f⟩⇩a ❙^ n = ⟨f ^^ n⟩⇩a"
  by (induct n, rel_auto+)

subsection ‹ Kleene Star ›

definition ustar :: "'α hrel ⇒ 'α hrel" ("_⇧⋆" [999] 999) where
"P⇧⋆ = (⨅i∈{0..} ∙ P❙^i)"

lemma ustar_rep_eq:
  "⟦P⇧⋆⟧⇩e = (λb. b ∈ ({p. ⟦P⟧⇩e p}⇧*))"
  by (simp add: ustar_def, rel_auto, simp_all add: relpow_imp_rtrancl rtrancl_imp_relpow)

update_uexpr_rep_eq_thms

subsection ‹ Kleene Plus ›

purge_notation trancl ("(_⇧+)" [1000] 999)

definition uplus :: "'α hrel ⇒ 'α hrel" ("_⇧+" [999] 999) where
[upred_defs]: "P⇧+ = P ;; P⇧⋆"

lemma uplus_power_def: "P⇧+ = (⨅ i ∙ P ❙^ (Suc i))"
  by (simp add: uplus_def ustar_def seq_UINF_distl' UINF_atLeast_Suc upred_semiring.power_Suc)

subsection ‹ Omega ›

definition uomega :: "'α hrel ⇒ 'α hrel" ("_⇧ω" [999] 999) where
"P⇧ω = (μ X ∙ P ;; X)"

subsection ‹ Relation Algebra Laws ›

theorem RA1: "(P ;; (Q ;; R)) = ((P ;; Q) ;; R)"
  by (simp add: seqr_assoc)

theorem RA2: "(P ;; II) = P" "(II ;; P) = P"
  by simp_all

theorem RA3: "P⇧-⇧- = P"
  by simp

theorem RA4: "(P ;; Q)⇧- = (Q⇧- ;; P⇧-)"
  by simp

theorem RA5: "(P ∨ Q)⇧- = (P⇧- ∨ Q⇧-)"
  by (rel_auto)

theorem RA6: "((P ∨ Q) ;; R) = (P;;R ∨ Q;;R)"
  using seqr_or_distl by blast

theorem RA7: "((P⇧- ;; (¬(P ;; Q))) ∨ (¬Q)) = (¬Q)"
  by (rel_auto)

subsection ‹ Kleene Algebra Laws ›

lemma ustar_alt_def: "P⇧⋆ = (⨅ i ∙ P ❙^ i)"
  by (simp add: ustar_def)

theorem ustar_sub_unfoldl: "P⇧⋆ ⊑ II ⊓ (P;;P⇧⋆)"
  by (rel_simp, simp add: rtrancl_into_trancl2 trancl_into_rtrancl)
    
theorem ustar_inductl:
  assumes "Q ⊑ R" "Q ⊑ P ;; Q"
  shows "Q ⊑ P⇧⋆ ;; R"
proof -
  have "P⇧⋆ ;; R = (⨅ i. P ❙^ i ;; R)"
    by (simp add: ustar_def UINF_as_Sup_collect' seq_SUP_distr)
  also have "Q ⊑ ..."
    by (simp add: SUP_least assms upower_inductl)
  finally show ?thesis .
qed

theorem ustar_inductr:
  assumes "Q ⊑ R" "Q ⊑ Q ;; P"
  shows "Q ⊑ R ;; P⇧⋆"
proof -
  have "R ;; P⇧⋆ = (⨅ i. R ;; P ❙^ i)"
    by (simp add: ustar_def UINF_as_Sup_collect' seq_SUP_distl)
  also have "Q ⊑ ..."
    by (simp add: SUP_least assms upower_inductr)
  finally show ?thesis .
qed

lemma ustar_refines_nu: "(ν X ∙ (P ;; X) ⊓ II) ⊑ P⇧⋆"
  by (metis (no_types, lifting) lfp_greatest semilattice_sup_class.le_sup_iff 
      semilattice_sup_class.sup_idem upred_semiring.mult_2_right 
      upred_semiring.one_add_one ustar_inductl)

lemma ustar_as_nu: "P⇧⋆ = (ν X ∙ (P ;; X) ⊓ II)"
proof (rule antisym)
  show "(ν X ∙ (P ;; X) ⊓ II) ⊑ P⇧⋆"
    by (simp add: ustar_refines_nu)
  show "P⇧⋆ ⊑ (ν X ∙ (P ;; X) ⊓ II)"
    by (metis lfp_lowerbound upred_semiring.add_commute ustar_sub_unfoldl)
qed

lemma ustar_unfoldl: "P⇧⋆ = II ⊓ (P ;; P⇧⋆)"
  apply (simp add: ustar_as_nu)
  apply (subst lfp_unfold)
   apply (rule monoI)
   apply (rel_auto)+
  done

text ‹ While loop can be expressed using Kleene star ›

lemma while_star_form:
  "while b do P od = (P ◃ b ▹⇩r II)⇧⋆ ;; [(¬b)]⇧⊤"
proof -
  have 1: "Continuous (λX. P ;; X ◃ b ▹⇩r II)"
    by (rel_auto)
  have "while b do P od = (⨅i. ((λX. P ;; X ◃ b ▹⇩r II) ^^ i) false)"
    by (simp add: "1" false_upred_def sup_continuous_Continuous sup_continuous_lfp while_top_def)
  also have "... = ((λX. P ;; X ◃ b ▹⇩r II) ^^ 0) false ⊓ (⨅i. ((λX. P ;; X ◃ b ▹⇩r II) ^^ (i+1)) false)"
    by (subst Sup_power_expand, simp)
  also have "... = (⨅i. ((λX. P ;; X ◃ b ▹⇩r II) ^^ (i+1)) false)"
    by (simp)
  also have "... = (⨅i. (P ◃ b ▹⇩r II)❙^i ;; (false ◃ b ▹⇩r II))"
  proof (rule SUP_cong, simp_all)
    fix i
    show "P ;; ((λX. P ;; X ◃ b ▹⇩r II) ^^ i) false ◃ b ▹⇩r II = (P ◃ b ▹⇩r II) ❙^ i ;; (false ◃ b ▹⇩r II)"
    proof (induct i)
      case 0
      then show ?case by simp
    next
      case (Suc i)
      then show ?case
        by (simp add: upred_semiring.power_Suc)
           (metis (no_types, lifting) RA1 comp_cond_left_distr cond_L6 upred_semiring.mult.left_neutral)
    qed
  qed
  also have "... = (⨅i∈{0..} ∙ (P ◃ b ▹⇩r II)❙^i ;; [(¬b)]⇧⊤)"
    by (rel_auto)
  also have "... = (P ◃ b ▹⇩r II)⇧⋆ ;; [(¬b)]⇧⊤"
    by (metis seq_UINF_distr ustar_def)
  finally show ?thesis .
qed
  
subsection ‹ Omega Algebra Laws ›

lemma uomega_induct:
  "P ;; P⇧ω ⊑ P⇧ω"
  by (simp add: uomega_def, metis eq_refl gfp_unfold monoI seqr_mono)

subsection ‹ Refinement Laws ›

lemma skip_r_refine:
  "(p ⇒ p) ⊑ II"
  by pred_blast

lemma conj_refine_left:
  "(Q ⇒ P) ⊑ R ⟹ P ⊑ (Q ∧ R)"
  by (rel_auto)
  
lemma pre_weak_rel:
  assumes "`Pre ⇒ I`"
  and     "(I ⇒ Post) ⊑ P"
  shows "(Pre ⇒ Post) ⊑ P"
  using assms by(rel_auto)
    
lemma cond_refine_rel: 
  assumes "S ⊑ (⌈b⌉⇩< ∧ P)" "S ⊑ (⌈¬b⌉⇩< ∧ Q)"
  shows "S ⊑ P ◃ b ▹⇩r Q"
  by (metis aext_not assms(1) assms(2) cond_def lift_rcond_def utp_pred_laws.le_sup_iff)

lemma seq_refine_pred:
  assumes "(⌈b⌉⇩< ⇒ ⌈s⌉⇩>) ⊑ P" and "(⌈s⌉⇩< ⇒ ⌈c⌉⇩>) ⊑ Q"
  shows "(⌈b⌉⇩< ⇒ ⌈c⌉⇩>) ⊑ (P ;; Q)"
  using assms by rel_auto
    
lemma seq_refine_unrest:
  assumes "outα ♯ b" "inα ♯ c"
  assumes "(b ⇒ ⌈s⌉⇩>) ⊑ P" and "(⌈s⌉⇩< ⇒ c) ⊑ Q"
  shows "(b ⇒ c) ⊑ (P ;; Q)"
  using assms by rel_blast 
    
 subsection ‹ Domain and Range Laws ›
  
lemma Dom_conv_Ran:
  "Dom(P⇧-) = Ran(P)"
  by (rel_auto)

lemma Ran_conv_Dom:
  "Ran(P⇧-) = Dom(P)"
  by (rel_auto)  

lemma Dom_skip:
  "Dom(II) = true"
  by (rel_auto)

lemma Dom_assigns:
  "Dom(⟨σ⟩⇩a) = true"
  by (rel_auto)
   
lemma Dom_miracle:
  "Dom(false) = false"
  by (rel_auto)

lemma Dom_assume:
  "Dom([b]⇧⊤) = b"
  by (rel_auto)
    
lemma Dom_seq:
  "Dom(P ;; Q) = Dom(P ;; [Dom(Q)]⇧⊤)"
  by (rel_auto)
    
lemma Dom_disj:
  "Dom(P ∨ Q) = (Dom(P) ∨ Dom(Q))"
  by (rel_auto)

lemma Dom_inf:
  "Dom(P ⊓ Q) = (Dom(P) ∨ Dom(Q))"
  by (rel_auto)
    
lemma assume_Dom:
  "[Dom(P)]⇧⊤ ;; P = P"
  by (rel_auto)

end