Quelle  utp_rel_laws.thy

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]^\<top> ;; P) ⊓ ([(¬ b)]^\<top> ;; 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₁ ⊑ P₂; Q₁ ⊑ Q₂ ] ==> (P₁ ;; Q₁) ⊑ (P₂ ;; Q₂)"
  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) = (\<exists> v ∙ P[«v¬/$v🍋] ∧ Q[«v¬/$v])"
  by (rel_auto)

lemma seqr_middle:
  assumes "vwb_lens x"
  shows "(P ;; Q) = (\<exists> 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]:
  "((\<exists> x ∙ P x) ;; Q) = (\<exists> x ∙ (P x ;; Q))"
  by rel_auto

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

lemma shEx_lift_seq_2 [uquant_lift]:
  "(P ;; (\<exists> x ∙ Q x)) = (\<exists> x ∙ (P ;; Q x))"
  by rel_auto

lemma shEx_mem_lift_seq_2 [uquant_lift]:
  assumes "inα ♯ A"
  shows "(P ;; (\<exists> x ∈ A ∙ Q x)) = (\<exists> 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🛇_\<alpha>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_;y = ($x🍋 =_u $x ∧ II)"
  by (rel_auto)

lemma skip_res_as_ra:
  "[ vwb_lens y; x +_L y ≈_L 1_L; x ⋈ y ] ==> II🛇_\<alpha>x = II"
  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 «S¬)]^\<top> ;; (x := &x) = [(&v ∈_u «S¬)]^\<top>"
  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🛇_\<alpha>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]^\<top> = false"
  by (rel_auto)
  
lemma assume_true: "[true]^\<top> = II"
  by (rel_auto)
    
lemma assume_seq: "[b]^\<top> ;; [c]^\<top> = [(b ∧ c)]^\<top>"
  by (rel_auto)

lemma assert_false: "{false}_\<bottom> = true"
  by (rel_auto)

lemma assert_true: "{true}_\<bottom> = II"
  by (rel_auto)
    
lemma assert_seq: "{b}_\<bottom> ;; {c}_\<bottom> = {(b ∧ c)}_\<bottom>"
  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₀)
   apply (subgoal_tac "(s ⊕_L s' on y) ⊕_L s₀ on x = s₀ ⊕_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₀)
  apply (subgoal_tac "put (put s (get (put s₀ (get s')))) (get (put s (get s₀)))
                      = put s₀ (get 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₀)
   apply (rule_tac x="put s s₀" 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 (put b a) = get 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 (put b c) = get b")
   apply (subgoal_tac "∧b a. get (put b a) = get 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"
  by (rel_auto, meson vwb_lens_wb wb_lens.get_put)
    
lemma nameset_skip_ra: "vwb_lens x ==> (ns x ∙ II) = II"
  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_\<bottom> b do P od = ((P ;; while_\<bottom> 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_\<bottom> 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_\<bottom> b do P od) ◃ b ▹_r II)"
    by (simp add: while_bot_def)
  finally show ?thesis .
qed

theorem while_bot_false: "while_\<bottom> false do P od = II"
  by (simp add: while_bot_def mu_const alpha)

theorem while_bot_true: "while_\<bottom> 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_\<bottom> 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^\<star> = (⊓i∈{0..} ∙ P^i)"

lemma ustar_rep_eq:
  "[P^\<star>]_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 (‹(‹notation=‹postfix +››_⁺)› [1000] 999)

definition uplus :: "'α hrel ==> 'α hrel" (‹_⁺› [999] 999) where
[upred_defs]: "P⁺ = P ;; P^\<star>"

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^\<omega> = (μ 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^\<star> = (⊓ i ∙ P ^ i)"
  by (simp add: ustar_def)

theorem ustar_sub_unfoldl: "P^\<star> ⊑ II ⊓ (P;;P^\<star>)"
  by (rel_simp, simp add: rtrancl_into_trancl2 trancl_into_rtrancl)
    
theorem ustar_inductl:
  assumes "Q ⊑ R" "Q ⊑ P ;; Q"
  shows "Q ⊑ P^\<star> ;; R"
proof -
  have "P^\<star> ;; 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^\<star>"
proof -
  have "R ;; P^\<star> = (⊓ 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^\<star>"
  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^\<star> = (ν X ∙ (P ;; X) ⊓ II)"
proof (rule antisym)
  show "(ν X ∙ (P ;; X) ⊓ II) ⊑ P^\<star>"
    by (simp add: ustar_refines_nu)
  show "P^\<star> ⊑ (ν X ∙ (P ;; X) ⊓ II)"
    by (metis lfp_lowerbound upred_semiring.add_commute ustar_sub_unfoldl)
qed

lemma ustar_unfoldl: "P^\<star> = II ⊓ (P ;; P^\<star>)"
  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)^\<star> ;; [(¬b)]^\<top>"
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)]^\<top>)"
    by (rel_auto)
  also have "... = (P ◃ b ▹_r II)^\<star> ;; [(¬b)]^\<top>"
    by (metis seq_UINF_distr ustar_def)
  finally show ?thesis .
qed
  
subsection ‹ Omega Algebra Laws ›

lemma uomega_induct:
  "P ;; P^\<omega> ⊑ P^\<omega>"
  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]^\<top>) = b"
  by (rel_auto)
    
lemma Dom_seq:
  "Dom(P ;; Q) = Dom(P ;; [Dom(Q)]^\<top>)"
  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)]^\<top> ;; P = P"
  by (rel_auto)

end