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; mnm'   m  m'"
    by (auto simp: pw_le_iff pw_leof_iff)
      
  lemma inres_leof_mono: "mnm'  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: " anb; nofail b; bnc   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 Φ)   mf n SPEC Φ" 
    by (auto simp add: pw_leof_iff refine_pw_simps)
  
  lemma RETURN_leof_RES_iff[simp]: "RETURN x n RES Y  xY"
    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. xX  Φ 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  anm  bnm)"  
    by (auto simp: pw_leof_iff refine_pw_simps)

  lemma sup_leof_rule[refine_vcg]:
    assumes "nofail a; nofail b  anm"
    assumes "nofail a; nofail b  bnm"
    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  mnm'   mnm'"
    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  RECT body x'  (if nofail (RECT 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; RECT body = f  body f x  (if nofail (body f x) then M x else FAIL)"
  assume a3: "pre xa"
  assume a4: "nofail (RECT body xa)"
  assume a5: "trimono body"
  have f6: "x. ¬ pre x  (x, xa)  V  (if nofail (RECT body x) then RECT body x  M x else RECT 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  RECT 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 (RECT body) xa)"
    using a5 a4 by (metis (no_types) RECT_unfold)
  then show "body (RECT 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