section ‹ Fixed-points and Recursion ›

theory utp_recursion
  imports 
    utp_pred_laws
    utp_rel
begin

subsection ‹ Fixed-point Laws ›
  
lemma mu_id: "(μ X ∙ X) = true"
  by (simp add: antisym gfp_upperbound)

lemma mu_const: "(μ X ∙ P) = P"
  by (simp add: gfp_const)

lemma nu_id: "(ν X ∙ X) = false"                                                            
  by (meson lfp_lowerbound utp_pred_laws.bot.extremum_unique)

lemma nu_const: "(ν X ∙ P) = P"
  by (simp add: lfp_const)

lemma mu_refine_intro:
  assumes "(C → S) ⊑ F(C → S)" "(C ∧ μ F) = (C ∧ ν F)"
  shows "(C → S) ⊑ μ F"
proof -
  from assms have "(C → S) ⊑ ν F"
    by (simp add: lfp_lowerbound)
  with assms show ?thesis
    by (pred_auto)
qed

subsection ‹ Obtaining Unique Fixed-points ›
    
text ‹ Obtaining termination proofs via approximation chains. Theorems and proofs adapted
 from Chapter 2, page 63 of the UTP book~cite‹"Hoare&98"›. ›

type_synonym 'a chain = "nat → 'a upred"

definition chain :: "'a chain → bool" where
  "chain Y = ((Y 0 = false) ∧ (∀ i. Y (Suc i) ⊑ Y i))"

lemma chain0 [simp]: "chain Y ==> Y 0 = false"
  by (simp add:chain_def)

lemma chainI:
  assumes "Y 0 = false" "∧ i. Y (Suc i) ⊑ Y i"
  shows "chain Y"
  using assms by (auto simp add: chain_def)

lemma chainE:
  assumes "chain Y" "∧ i. [ Y 0 = false; Y (Suc i) ⊑ Y i ] ==> P"
  shows "P"
  using assms by (simp add: chain_def)

lemma L274:
  assumes "∀ n. ((E n ∧_p X) = (E n ∧ Y))"
  shows "(⊓ (range E) ∧ X) = (⊓ (range E) ∧ Y)"
  using assms by (pred_auto)

text ‹ Constructive chains ›

definition constr ::
  "('a upred → 'a upred) → 'a chain → bool" where
"constr F E ⟷ chain E ∧ (∀ X n. ((F(X) ∧ E(n + 1)) = (F(X ∧ E(n)) ∧ E (n + 1))))"

lemma constrI:
  assumes "chain E" "∧ X n. ((F(X) ∧ E(n + 1)) = (F(X ∧ E(n)) ∧ E (n + 1)))"
  shows "constr F E"
  using assms by (auto simp add: constr_def)

text ‹ This lemma gives a way of showing that there is a unique fixed-point when
 the predicate function can be built using a constructive function F
 over an approximation chain E ›

lemma chain_pred_terminates:
  assumes "constr F E" "mono F"
  shows "(⊓ (range E) ∧ μ F) = (⊓ (range E) ∧ ν F)"
proof -
  from assms have "∀ n. (E n ∧ μ F) = (E n ∧ ν F)"
  proof (rule_tac allI)
    fix n
    from assms show "(E n ∧ μ F) = (E n ∧ ν F)"
    proof (induct n)
      case 0 thus ?case by (simp add: constr_def)
    next
      case (Suc n)
      note hyp = this
      thus ?case
      proof -
        have "(E (n + 1) ∧ μ F) = (E (n + 1) ∧ F (μ F))"
          using gfp_unfold[OF hyp(3), THEN sym] by (simp add: constr_def)
        also from hyp have "... = (E (n + 1) ∧ F (E n ∧ μ F))"
          by (metis conj_comm constr_def)
        also from hyp have "... = (E (n + 1) ∧ F (E n ∧ ν F))"
          by simp
        also from hyp have "... = (E (n + 1) ∧ ν F)"
          by (metis (no_types, lifting) conj_comm constr_def lfp_unfold)
        ultimately show ?thesis
          by simp
      qed
    qed
  qed
  thus ?thesis
    by (auto intro: L274)
qed

theorem constr_fp_uniq:
  assumes "constr F E" "mono F" "⊓ (range E) = C"
  shows "(C ∧ μ F) = (C ∧ ν F)"
  using assms(1) assms(2) assms(3) chain_pred_terminates by blast
    
subsection ‹ Noetherian Induction Instantiation›
      
text ‹ Contribution from Yakoub Nemouchi.The following generalization was used by Tobias Nipkow
 and Peter Lammich in \emph{Refine\_Monadic} ›

lemma  wf_fixp_uinduct_pure_ueq_gen:     
  assumes fixp_unfold: "fp B = B (fp B)"
  and              WF: "wf R"
  and     induct_step:
          "∧f st. [∧st'. (st',st) ∈ R ==> (((Pre ∧ ⌈e⌉_< =_u «st'¬) → Post) ⊑ f)]
               ==> fp B = f ==>((Pre ∧ ⌈e⌉_< =_u «st¬) → Post) ⊑ (B f)"
        shows "((Pre → Post) ⊑ fp B)"  
proof -  
  { fix st
    have "((Pre ∧ ⌈e⌉_< =_u «st¬) → Post) ⊑ (fp B)" 
    using WF proof (induction rule: wf_induct_rule)
      case (less x)
      hence "(Pre ∧ ⌈e⌉_< =_u «x¬ → Post) ⊑ B (fp B)"
        by (rule induct_step, rel_blast, simp)
      then show ?case
        using fixp_unfold by auto
    qed
  }
  thus ?thesis 
  by pred_simp  
qed
  
text ‹ The next lemma shows that using substitution also work. However it is not that generic
 nor practical for proof automation ... ›

lemma refine_usubst_to_ueq:
  "vwb_lens E ==> (Pre → Post)[«st'¬/$E] ⊑ f[«st'¬/$E] = (((Pre ∧ $E =_u «st'¬) → Post) ⊑ f)"
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put)  

text ‹ By instantiation of @{thm wf_fixp_uinduct_pure_ueq_gen} with @{term μ} and lifting of the
 well-founded relation we have ... ›
  
lemma mu_rec_total_pure_rule: 
  assumes WF: "wf R"
  and     M: "mono B"  
  and     induct_step:
          "∧ f st. [(Pre ∧ (⌈e⌉_<,«st¬)_u ∈_u «R¬ → Post) ⊑ f]
               ==> μ B = f ==>(Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ (B f)"
        shows "(Pre → Post) ⊑ μ B"  
proof (rule wf_fixp_uinduct_pure_ueq_gen[where fp=μ and Pre=Pre and B=B and R=R and e=e])
  show "μ B = B (μ B)"
    by (simp add: M def_gfp_unfold)
  show "wf R"
    by (fact WF)
  show "∧f st. (∧st'. (st', st) ∈ R ==> (Pre ∧ ⌈e⌉_< =_u «st'¬ → Post) ⊑ f) ==>
                μ B = f ==>
                (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ B f"
    by (rule induct_step, rel_simp, simp)
qed

lemma nu_rec_total_pure_rule: 
  assumes WF: "wf R"
  and     M: "mono B"  
  and     induct_step:
          "∧ f st. [(Pre ∧ (⌈e⌉_<,«st¬)_u ∈_u «R¬ → Post) ⊑ f]
               ==> ν B = f ==>(Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ (B f)"
        shows "(Pre → Post) ⊑ ν B"  
proof (rule wf_fixp_uinduct_pure_ueq_gen[where fp=ν and Pre=Pre and B=B and R=R and e=e])
  show "ν B = B (ν B)"
    by (simp add: M def_lfp_unfold)
  show "wf R"
    by (fact WF)
  show "∧f st. (∧st'. (st', st) ∈ R ==> (Pre ∧ ⌈e⌉_< =_u «st'¬ → Post) ⊑ f) ==>
                ν B = f ==>
                (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ B f"
    by (rule induct_step, rel_simp, simp)
qed

text ‹Since @{term "B ((Pre ∧ (⌈E⌉_<,«st¬)_u∈_u«R¬ → Post)) ⊑ B (μ B)"} and
 @{term "mono B"}, thus, @{thm mu_rec_total_pure_rule} can be expressed as follows›
  
lemma mu_rec_total_utp_rule: 
  assumes WF: "wf R"
    and     M: "mono B"  
    and     induct_step:
    "∧st. (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ (B ((Pre ∧ (⌈e⌉_<,«st¬)_u ∈_u «R¬ → Post)))"
  shows "(Pre → Post) ⊑ μ B"  
proof (rule mu_rec_total_pure_rule[where R=R and e=e], simp_all add: assms)
  show "∧f st. (Pre ∧ (⌈e⌉_<, «st¬)_u ∈_u «R¬ → Post) ⊑ f ==> μ B = f ==> (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ B f"
    by (simp add: M induct_step monoD order_subst2)
qed

lemma nu_rec_total_utp_rule: 
  assumes WF: "wf R"
    and     M: "mono B"  
    and     induct_step:
    "∧st. (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ (B ((Pre ∧ (⌈e⌉_<,«st¬)_u ∈_u «R¬ → Post)))"
  shows "(Pre → Post) ⊑ ν B"  
proof (rule nu_rec_total_pure_rule[where R=R and e=e], simp_all add: assms)
  show "∧f st. (Pre ∧ (⌈e⌉_<, «st¬)_u ∈_u «R¬ → Post) ⊑ f ==> ν B = f ==> (Pre ∧ ⌈e⌉_< =_u «st¬ → Post) ⊑ B f"
    by (simp add: M induct_step monoD order_subst2)
qed

end