Theory Refine_Monadic.Refine_Leof

section ‹Less-Equal or Fail›
(* TODO: Move to Refinement Framework *)
theory Refine_Leof
imports Refine_Basic
begin
  text ‹A predicate that states refinement or that the LHS fails.›


  definition le_or_fail :: "'a nres ⇒ 'a nres ⇒ bool" (infix "≤⇩n" 50) where
    "m ≤⇩n m' ≡ nofail m ⟶ m ≤ m'"

  lemma leofI[intro?]: 
    assumes "nofail m ⟹ m ≤ m'" shows "m ≤⇩n m'" 
    using assms unfolding le_or_fail_def by auto
  
  lemma leofD:  
    assumes "nofail m"
    assumes "m ≤⇩n m'"
    shows "m ≤ m'"
    using assms unfolding le_or_fail_def by blast

  lemma pw_leof_iff:
    "m ≤⇩n m' ⟷ (nofail m ⟶ (∀x. inres m x ⟶ inres m' x))"
    unfolding le_or_fail_def by (auto simp add: pw_le_iff refine_pw_simps)
      
  lemma le_by_leofI: "⟦ nofail m' ⟹ nofail m; m≤⇩nm' ⟧ ⟹ m ≤ m'"
    by (auto simp: pw_le_iff pw_leof_iff)
      
  lemma inres_leof_mono: "m≤⇩nm' ⟹ nofail m ⟹ inres m x ⟹ inres m' x"
    by (auto simp: pw_leof_iff)

  lemma leof_trans[trans]: "⟦a ≤⇩n RES X; RES X ≤⇩n c⟧ ⟹ a ≤⇩n c"
    by (auto simp: pw_leof_iff)

  lemma leof_trans_nofail: "⟦ a≤⇩nb; nofail b; b≤⇩nc ⟧ ⟹ a ≤⇩n c"  
    by (auto simp: pw_leof_iff)

  lemma leof_refl[simp]: "a ≤⇩n a" 
    by (auto simp: pw_leof_iff)

  lemma leof_RES_UNIV[simp, intro!]: "m ≤⇩n RES UNIV" 
    by (auto simp: pw_leof_iff)

  lemma leof_FAIL[simp, intro!]: "m ≤⇩n FAIL" by (auto simp: pw_leof_iff)
  lemma FAIL_leof[simp, intro!]: "FAIL ≤⇩n m"  
    by (auto simp: le_or_fail_def)
      
  lemma leof_lift:
    "m ≤ F ⟹ m ≤⇩n F"
    by (auto simp add: pw_leof_iff pw_le_iff)

  lemma leof_RETURN_rule[refine_vcg]: 
    "Φ m ⟹ RETURN m ≤⇩n SPEC Φ" by (simp add: pw_leof_iff)
  
  lemma leof_bind_rule[refine_vcg]: 
    "⟦ m ≤⇩n SPEC (λx. f x ≤⇩n SPEC Φ) ⟧ ⟹ m⤜f ≤⇩n SPEC Φ" 
    by (auto simp add: pw_leof_iff refine_pw_simps)
  
  lemma RETURN_leof_RES_iff[simp]: "RETURN x ≤⇩n RES Y ⟷ x∈Y"
    by (auto simp add: pw_leof_iff refine_pw_simps)

  lemma RES_leof_RES_iff[simp]: "RES X ≤⇩n RES Y ⟷ X ⊆ Y"
    by (auto simp add: pw_leof_iff refine_pw_simps)
   
  lemma leof_Let_rule[refine_vcg]: "f x ≤⇩n SPEC Φ ⟹ Let x f ≤⇩n SPEC Φ" 
    by simp

  lemma leof_If_rule[refine_vcg]: 
    "⟦c ⟹ t ≤⇩n SPEC Φ; ¬c ⟹ e ≤⇩n SPEC Φ⟧ ⟹ If c t e ≤⇩n SPEC Φ" 
    by simp

  lemma leof_RES_rule[refine_vcg]:
    "⟦⋀x. Ψ x ⟹ Φ x⟧ ⟹ SPEC Ψ ≤⇩n SPEC Φ"
    "⟦⋀x. x∈X ⟹ Φ x⟧ ⟹ RES X ≤⇩n SPEC Φ"
    by auto

  lemma leof_True_rule: "⟦⋀x. Φ x⟧ ⟹ m ≤⇩n SPEC Φ"
    by (auto simp add: pw_leof_iff refine_pw_simps)

  lemma sup_leof_iff: "(sup a b ≤⇩n m) ⟷ (nofail a ∧ nofail b ⟶ a≤⇩nm ∧ b≤⇩nm)"  
    by (auto simp: pw_leof_iff refine_pw_simps)

  lemma sup_leof_rule[refine_vcg]:
    assumes "⟦nofail a; nofail b⟧ ⟹ a≤⇩nm"
    assumes "⟦nofail a; nofail b⟧ ⟹ b≤⇩nm"
    shows "sup a b ≤⇩n m"
    using assms by (auto simp: pw_leof_iff refine_pw_simps)
      
  lemma leof_option_rule[refine_vcg]: 
  "⟦v = None ⟹ S1 ≤⇩n SPEC Φ; ⋀x. v = Some x ⟹ f2 x ≤⇩n SPEC Φ⟧
    ⟹ (case v of None ⇒ S1 | Some x ⇒ f2 x) ≤⇩n SPEC Φ"
    by (cases v) auto

  lemma ASSERT_leof_rule[refine_vcg]:
    assumes "Φ ⟹ m ≤⇩n m'"
    shows "do {ASSERT Φ; m} ≤⇩n m'"
    using assms
    by (cases Φ, auto simp: pw_leof_iff)

  lemma leof_ASSERT_rule[refine_vcg]: "⟦Φ ⟹ m ≤⇩n m'⟧ ⟹ m ≤⇩n ASSERT Φ ⪢ m'"  
    by (auto simp: pw_leof_iff refine_pw_simps)

  lemma leof_ASSERT_refine_rule[refine]: "⟦Φ ⟹ m ≤⇩n ⇓R m'⟧ ⟹ m ≤⇩n ⇓R (ASSERT Φ ⪢ m')"  
    by (auto simp: pw_leof_iff refine_pw_simps)

  lemma ASSUME_leof_iff: "(ASSUME Φ ≤⇩n SPEC Ψ) ⟷ (Φ ⟶ Ψ ())"  
    by (auto simp: pw_leof_iff)

  lemma ASSUME_leof_rule[refine_vcg]: 
    assumes "Φ ⟹ Ψ ()" 
    shows "ASSUME Φ ≤⇩n SPEC Ψ"
    using assms
    by (auto simp: ASSUME_leof_iff)
      
      
  lemma SPEC_rule_conj_leofI1:
    assumes "m ≤ SPEC Φ"
    assumes "m ≤⇩n SPEC Ψ"
    shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
    using assms by (auto simp: pw_le_iff pw_leof_iff)

  lemma SPEC_rule_conj_leofI2:
    assumes "m ≤⇩n SPEC Φ"
    assumes "m ≤ SPEC Ψ"
    shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
    using assms by (auto simp: pw_le_iff pw_leof_iff)

  lemma SPEC_rule_leof_conjI: 
    assumes "m ≤⇩n SPEC Φ" "m ≤⇩n SPEC Ψ"
    shows "m ≤⇩n SPEC (λx. Φ x ∧ Ψ x)"
    using assms by (auto simp: pw_leof_iff)

  lemma leof_use_spec_rule:
    assumes "m ≤⇩n SPEC Ψ"
    assumes "m ≤⇩n SPEC (λs. Ψ s ⟶ Φ s)"
    shows "m ≤⇩n SPEC Φ"
    using assms by (auto simp: pw_leof_iff refine_pw_simps)
  
  lemma use_spec_leof_rule:
    assumes "m ≤⇩n SPEC Ψ"
    assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
    shows "m ≤ SPEC Φ"
    using assms by (auto simp: pw_leof_iff pw_le_iff refine_pw_simps)

  lemma leof_strengthen_SPEC: 
    "m ≤⇩n SPEC Φ ⟹ m ≤⇩n SPEC (λx. inres m x ∧ Φ x)"
    by (auto simp: pw_leof_iff)

  lemma build_rel_SPEC_leof: 
    assumes "m ≤⇩n SPEC (λx. I x ∧ Φ (α x))"  
    shows "m ≤⇩n ⇓(br α I) (SPEC Φ)"
    using assms by (auto simp: build_rel_SPEC_conv)
      
  lemma RETURN_as_SPEC_refine_leof[refine2]:
    assumes "M ≤⇩n SPEC (λc. (c,a)∈R)"
    shows "M ≤⇩n ⇓R (RETURN a)"
    using assms
    by (simp add: pw_leof_iff refine_pw_simps)

  lemma ASSERT_leof_defI:
    assumes "c ≡ do { ASSERT Φ; m'}"
    assumes "Φ ⟹ m' ≤⇩n m"
    shows "c ≤⇩n m"
    using assms by (auto simp: pw_leof_iff refine_pw_simps)
  
  lemma leof_fun_conv_le: 
    "(f x ≤⇩n M x) ⟷ (f x ≤ (if nofail (f x) then M x else FAIL))"
    by (auto simp: pw_le_iff pw_leof_iff)
    
  lemma leof_add_nofailI: "⟦ nofail m ⟹ m≤⇩nm' ⟧ ⟹ m≤⇩nm'"
    by (auto simp: pw_le_iff pw_leof_iff)

  lemma leof_cons_rule[refine_vcg_cons]: 
    assumes "m ≤⇩n SPEC Q"
    assumes "⋀x. Q x ⟹ P x"  
    shows "m ≤⇩n SPEC P"
    using assms  
    by (auto simp: pw_le_iff pw_leof_iff)
      
      
lemma RECT_rule_leof:
  assumes WF: "wf (V::('x×'x) set)"
  assumes I0: "pre (x::'x)"
  assumes IS: "⋀f x. ⟦ ⋀x'. ⟦pre x'; (x',x)∈V⟧ ⟹ f x' ≤⇩n M x'; pre x; 
                        RECT body = f
    ⟧ ⟹ body f x ≤⇩n M x"
  shows "RECT body x ≤⇩n M x"
    apply (cases "¬trimono body")
    apply (simp add: RECT_def)
    using assms
    unfolding leof_fun_conv_le
    apply -
    apply (rule RECT_rule[where pre=pre and V=V])
       apply clarsimp_all
proof -
  fix xa :: 'x
  assume a1: "⋀x'. ⟦pre x'; (x', xa) ∈ V⟧ ⟹ REC⇩T body x' ≤ (if nofail (REC⇩T body x') then M x' else FAIL)"
  assume a2: "⋀x f. ⟦⋀x'. ⟦pre x'; (x', x) ∈ V⟧ ⟹ f x' ≤ (if nofail (f x') then M x' else FAIL); pre x; REC⇩T body = f⟧ ⟹ body f x ≤ (if nofail (body f x) then M x else FAIL)"
  assume a3: "pre xa"
  assume a4: "nofail (REC⇩T body xa)"
  assume a5: "trimono body"
  have f6: "∀x. ¬ pre x ∨ (x, xa) ∉ V ∨ (if nofail (REC⇩T body x) then REC⇩T body x ≤ M x else REC⇩T body x ≤ FAIL)"
    using a1 by presburger
  have f7: "∀x f. ((∃xa. (pre xa ∧ (xa, x) ∈ V) ∧ ¬ f xa ≤ (if nofail (f xa) then M xa else FAIL)) ∨ ¬ pre x ∨ REC⇩T body ≠ f) ∨ body f x ≤ (if nofail (body f x) then M x else FAIL)"
    using a2 by blast
  obtain xx :: "('x ⇒ 'a nres) ⇒ 'x ⇒ 'x" where
    f8: "∀x0 x1. (∃v2. (pre v2 ∧ (v2, x1) ∈ V) ∧ ¬ x0 v2 ≤ (if nofail (x0 v2) then M v2 else FAIL)) = ((pre (xx x0 x1) ∧ (xx x0 x1, x1) ∈ V) ∧ ¬ x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL))"
    by moura
  have f9: "∀x0 x1. (x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL)) = (if nofail (x0 (xx x0 x1)) then x0 (xx x0 x1) ≤ M (xx x0 x1) else x0 (xx x0 x1) ≤ FAIL)"
    by presburger
  have "nofail (body (REC⇩T body) xa)"
    using a5 a4 by (metis (no_types) RECT_unfold)
  then show "body (REC⇩T body) xa ≤ M xa"
    using f9 f8 f7 f6 a3 by fastforce
qed  

(* TODO: REC_rule_leof! (However, this may require some fix 
     to the domain theory model of Refine_Monadic!) *)
      
      

end