Theory utp_recursion

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