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:
  " P1  P2; Q1  Q2   (P1 ;; Q1)  (P2 ;; Q2)"
  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) = (Ptrue/$x´ ;; Qtrue/$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) = (Pfalse/$x´ ;; Qfalse/$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)) = (Ptrue/$x´ ;; Qtrue/$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)) = (Pfalse/$x´ ;; Qfalse/$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 = (Ptrue/$x´ ;; Qtrue/$x  Pfalse/$x´ ;; Qfalse/$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 = (Ptrue/$x´ ;; Rtrue/$x  Qfalse/$x´ ;; Rfalse/$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 "... = (Ptrue/$x´ ;; Rtrue/$x  Qfalse/$x´ ;; Rfalse/$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) = ( QA. P ;; Q)"
  by (transfer, auto)

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

lemma seq_UINF_distl: "P ;; ( QA  F(Q)) = ( QA  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: "( PA  F(P)) ;; Q = ( PA  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 ;; (iA. Q(i)) = (iA. P ;; Q(i))"
  by (metis image_image seq_Sup_distl)

lemma seq_SUP_distr: "(iA. P(i)) ;; Q = (iA. 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  IIy)"
  by (rel_auto)

lemma skip_res_as_ra:
  " vwb_lens y; x +L y L 1L; x  y   IIαx = IIy"
  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: "(fa ;; ga) = g  fa"
  by (simp add: assigns_r_comp usubst)

lemma assigns_cond: "(fa  b r ga) = f  b s ga"
  by (rel_auto)

lemma assigns_r_conv:
  "bij f  fa- = inv fa"
  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 = Pu</$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)  (be</$x)  (x := e ;; Q))"
  by (rel_auto)

lemma assign_rcond:
  fixes x :: "('a  )"
  shows "(x := e ;; (P  b r Q)) = ((x := e ;; P)  (be/x) r (x := e ;; Q))"
  by (rel_auto)

lemma assign_r_alt_def:
  fixes x :: "('a  )"
  shows "x := v = IIv</$x"
  by (rel_auto)

lemma assigns_r_ufunc: "ufunctional fa"
  by (rel_auto)

lemma assigns_r_uinj: "inj f  uinj fa"
  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' s0)
   apply (subgoal_tac "(s L s' on y) L s0 on x = s0 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' s0)
  apply (subgoal_tac "puty(putxs (getx(putxs0 (getxs')))) (gety(putys (getys0))) 
                      = putxs0 (getxs')")
   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 = 1L   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' s0)
   apply (rule_tac x="putas s0" 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 aa"
  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. gety(putxb a) = getyb")
    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. getx(putyb c) = getxb")
   apply (subgoal_tac "b a. gety(putxb a) = getyb")
    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) = IIx"
  by (rel_auto, meson vwb_lens_wb wb_lens.get_put)
    
lemma nameset_skip_ra: "vwb_lens x  (ns x  IIx) = IIx"
  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 ;; trueh = 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 = falseh 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 ^ ie = (λ b. b  ({p. Pe 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 ida (;;) P ie = (λb. b  ({p. Pe 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) = (iinsert (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: "fa ^ n = f ^^ na"
  by (induct n, rel_auto+)

subsection ‹ Kleene Star ›

definition ustar :: " hrel   hrel" ("_" [999] 999) where
"P = (i{0..}  P^i)"

lemma ustar_rep_eq:
  "Pe = (λb. b  ({p. Pe 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