Theory Refine_Monadic.Refine_Det

section ‹Deterministic Monad›
theory Refine_Det
imports 
  "HOL-Library.Monad_Syntax"
  "Generic/RefineG_Assert"
  "Generic/RefineG_While"
begin

subsection ‹Deterministic Result Lattice›
text ‹
  We define the flat complete lattice of deterministic program results:
›
(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
  an isomorphic contruction. *)
datatype 'a dres = 
  dSUCCEEDi   ― ‹No result›
| dFAILi      ― ‹Failure›
| dRETURN 'a  ― ‹Regular result›

instantiation dres :: (type) complete_lattice
begin
  definition "top_dres ≡ dFAILi"
  definition "bot_dres ≡ dSUCCEEDi"
  fun sup_dres where
    "sup dFAILi _ = dFAILi" |
    "sup _ dFAILi = dFAILi" |
    "sup (dRETURN a) (dRETURN b) = (if a=b then dRETURN b else dFAILi)" |
    "sup dSUCCEEDi x = x" | 
    "sup x dSUCCEEDi = x"

  lemma sup_dres_addsimps[simp]:
    "sup x dFAILi = dFAILi"
    "sup x dSUCCEEDi = x"
    apply (case_tac [!] x)
    apply simp_all
    done

  fun inf_dres where
    "inf dFAILi x = x" |
    "inf x dFAILi = x" |
    "inf (dRETURN a) (dRETURN b) = (if a=b then dRETURN b else dSUCCEEDi)" |
    "inf dSUCCEEDi _ = dSUCCEEDi" | 
    "inf _ dSUCCEEDi = dSUCCEEDi"

  lemma inf_dres_addsimps[simp]:
    "inf x dSUCCEEDi = dSUCCEEDi"
    "inf dSUCCEEDi x = dSUCCEEDi"
    "inf x dFAILi = x"
    "inf (dRETURN v) x ≠ dFAILi"
    apply (case_tac [!] x)
    apply simp_all
    done
      
  definition "Sup_dres S ≡ 
    if S⊆{dSUCCEEDi} then dSUCCEEDi 
    else if dFAILi∈S then dFAILi
    else if ∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S then dFAILi
    else dRETURN (THE x. dRETURN x ∈ S)"

  definition "Inf_dres S ≡ 
    if S⊆{dFAILi} then dFAILi 
    else if dSUCCEEDi∈S then dSUCCEEDi
    else if ∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S then dSUCCEEDi
    else dRETURN (THE x. dRETURN x ∈ S)"
  
  fun less_eq_dres where
    "less_eq_dres dSUCCEEDi _ ⟷ True" |
    "less_eq_dres _ dFAILi ⟷ True" |
    "less_eq_dres (dRETURN (a::'a)) (dRETURN b) ⟷ a=b" |
    "less_eq_dres _ _ ⟷ False"

  definition less_dres where "less_dres (a::'a dres) b ⟷ a≤b ∧ ¬ b≤a"

  lemma less_eq_dres_split_conv: 
    "a≤b ⟷ (case (a,b) of 
        (dSUCCEEDi,_) ⇒ True 
      | (_,dFAILi) ⇒ True
      | (dRETURN (a::'a), dRETURN b) ⇒ a=b
      | _ ⇒ False
    )"  
    by (auto split: dres.split)
    
  lemma inf_dres_split_conv: 
    "inf a b = (case (a,b) of 
      (dFAILi,x) ⇒ x
    | (x,dFAILi) ⇒ x
    | (dRETURN a, dRETURN b) ⇒ (if a=b then dRETURN b else dSUCCEEDi)
    | _ ⇒ dSUCCEEDi)"
    by (auto split: dres.split)
      
  lemma sup_dres_split_conv: 
    "sup a b = (case (a,b) of 
      (dSUCCEEDi,x) ⇒ x
    | (x,dSUCCEEDi) ⇒ x
    | (dRETURN a, dRETURN b) ⇒ (if a=b then dRETURN b else dFAILi)
    | _ ⇒ dFAILi)"
    by (auto split: dres.split)
      
  instance
    apply intro_classes
    supply less_eq_dres_split_conv[simp] less_dres_def[simp] dres.splits[split]
    supply inf_dres_split_conv[simp] sup_dres_split_conv[simp] if_splits[split]
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by auto  
    subgoal by (auto simp: Inf_dres_def)
    subgoal for A z
      apply (clarsimp simp: Inf_dres_def; safe)
      subgoal by force  
      subgoal by force  
      subgoal premises prems  
        using prems(2-) apply (drule_tac prems(1)) apply (drule_tac prems(1))
        apply (auto)
        done  
      subgoal premises prems  
        using prems(2-) apply (frule_tac prems(1))
        by (auto; metis the_equality) 
      done    
    subgoal by (auto simp: Sup_dres_def; metis the_equality)
    subgoal 
      apply (clarsimp simp: Sup_dres_def; safe)
      apply force
      apply force
      subgoal premises prems  
        using prems(2-) 
        apply (drule_tac prems(1))
        apply (drule_tac prems(1))
        apply (drule_tac prems(1)) 
        apply (auto)
        done  
      apply force  
      subgoal premises prems  
        using prems(2-) apply (frule_tac prems(1))
        by (auto; metis the_equality) 
      done
    subgoal by (auto simp: Inf_dres_def top_dres_def)    
    subgoal by (auto simp: Sup_dres_def bot_dres_def)    
    done

end

abbreviation "dSUCCEED ≡ (bot::'a dres)"
abbreviation "dFAIL ≡ (top::'a dres)"

lemma dres_cases[cases type, case_names dSUCCEED dRETURN dFAIL]:
  obtains "x=dSUCCEED" | r where "x=dRETURN r" | "x=dFAIL" 
  unfolding bot_dres_def top_dres_def by (cases x) auto

lemmas [simp] = dres.case(1,2)[folded top_dres_def bot_dres_def]

lemma dres_order_simps[simp]:
  "x≤dSUCCEED ⟷ x=dSUCCEED" 
  "dFAIL≤x ⟷ x=dFAIL"
  "dRETURN r ≠ dFAIL"
  "dRETURN r ≠ dSUCCEED"
  "dFAIL ≠ dRETURN r"
  "dSUCCEED ≠ dRETURN r"
  "dFAIL≠dSUCCEED"
  "dSUCCEED≠dFAIL"
  "x=y ⟹ inf (dRETURN x) (dRETURN y) = dRETURN y"
  "x≠y ⟹ inf (dRETURN x) (dRETURN y) = dSUCCEED"
  "x=y ⟹ sup (dRETURN x) (dRETURN y) = dRETURN y"
  "x≠y ⟹ sup (dRETURN x) (dRETURN y) = dFAIL"
  apply (simp_all add: bot_unique top_unique) 
  apply (simp_all add: bot_dres_def top_dres_def)
  done

lemma dres_Sup_cases:
  obtains "S⊆{dSUCCEED}" and "Sup S = dSUCCEED"
  | "dFAIL∈S" and "Sup S = dFAIL"
  | a b where "a≠b" "dRETURN a∈S" "dRETURN b∈S" "dFAIL∉S" "Sup S = dFAIL"
  | a where "S ⊆ {dSUCCEED, dRETURN a}" "dRETURN a∈S" "Sup S = dRETURN a"
proof -
  show ?thesis
    apply (cases "S⊆{dSUCCEED}")
    apply (rule that(1), assumption)
    apply (simp add: Sup_dres_def bot_dres_def)

    apply (cases "dFAIL∈S")
    apply (rule that(2), assumption)
    apply (simp add: Sup_dres_def bot_dres_def top_dres_def)

    apply (cases "∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S")
    apply (elim exE conjE)
    apply (rule that(3), assumption+)
    apply (auto simp add: Sup_dres_def bot_dres_def top_dres_def) []

    apply simp
    apply (cases "∃a. dRETURN a ∈ S")
    apply (elim exE)
    apply (rule_tac a=a in that(4)) []
    apply auto [] apply (case_tac xa, auto) []
    apply auto []
    apply (auto simp add: Sup_dres_def bot_dres_def top_dres_def) []

    apply auto apply (case_tac x, auto) []
    done
qed

lemma dres_Inf_cases:
  obtains "S⊆{dFAIL}" and "Inf S = dFAIL"
  | "dSUCCEED∈S" and "Inf S = dSUCCEED"
  | a b where "a≠b" "dRETURN a∈S" "dRETURN b∈S" "dSUCCEED∉S" "Inf S = dSUCCEED"
  | a where "S ⊆ {dFAIL, dRETURN a}" "dRETURN a∈S" "Inf S = dRETURN a"
proof -
  show ?thesis
    apply (cases "S⊆{dFAIL}")
    apply (rule that(1), assumption)
    apply (simp add: Inf_dres_def top_dres_def)

    apply (cases "dSUCCEED∈S")
    apply (rule that(2), assumption)
    apply (simp add: Inf_dres_def bot_dres_def top_dres_def)

    apply (cases "∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S")
    apply (elim exE conjE)
    apply (rule that(3), assumption+)
    apply (auto simp add: Inf_dres_def bot_dres_def top_dres_def) []

    apply simp
    apply (cases "∃a. dRETURN a ∈ S")
    apply (elim exE)
    apply (rule_tac a=a in that(4)) []
    apply auto [] apply (case_tac xa, auto) []
    apply auto []
    apply (auto simp add: Inf_dres_def bot_dres_def top_dres_def) []

    apply auto apply (case_tac x, auto) []
    done
qed

lemma dres_chain_eq_res:
  "is_chain M ⟹ 
    dRETURN r ∈ M ⟹ dRETURN s ∈ M ⟹ r=s"
  by (metis chainD less_eq_dres.simps(4))

lemma dres_Sup_chain_cases:
  assumes CHAIN: "is_chain M"
  obtains "M ⊆ {dSUCCEED}" "Sup M = dSUCCEED"
  | r where "M ⊆ {dSUCCEED,dRETURN r}" "dRETURN r∈M" "Sup M = dRETURN r"
  | "dFAIL∈M" "Sup M = dFAIL"
  apply (rule dres_Sup_cases[of M])
  using dres_chain_eq_res[OF CHAIN]
  by auto

lemma dres_Inf_chain_cases:
  assumes CHAIN: "is_chain M"
  obtains "M ⊆ {dFAIL}" "Inf M = dFAIL"
  | r where "M ⊆ {dFAIL,dRETURN r}" "dRETURN r∈M" "Inf M = dRETURN r"
  | "dSUCCEED∈M" "Inf M = dSUCCEED"
  apply (rule dres_Inf_cases[of M])
  using dres_chain_eq_res[OF CHAIN]
  by auto

lemma dres_internal_simps[simp]:
  "dSUCCEEDi = dSUCCEED"
  "dFAILi = dFAIL"
  unfolding top_dres_def bot_dres_def by auto
 
subsubsection ‹Monad Operations›
function dbind where 
  "dbind dFAIL _ = dFAIL"
| "dbind dSUCCEED _ = dSUCCEED"
| "dbind (dRETURN x) f = f x"
  unfolding bot_dres_def top_dres_def
  by pat_completeness auto
termination by lexicographic_order

adhoc_overloading
  Monad_Syntax.bind dbind

lemma [code]:
  "dbind (dRETURN x) f = f x"
  "dbind (dSUCCEEDi) f = dSUCCEEDi"
  "dbind (dFAILi) f = dFAILi"
  by simp_all

lemma dres_monad1[simp]: "dbind (dRETURN x) f = f x"
  by (simp)
lemma dres_monad2[simp]: "dbind M dRETURN = M"
  apply (cases M)
  apply (auto)
  done

lemma dres_monad3[simp]: "dbind (dbind M f) g = dbind M (λx. dbind (f x) g)"
  apply (cases M)
  apply auto
  done

lemmas dres_monad_laws = dres_monad1 dres_monad2 dres_monad3

lemma dbind_mono[refine_mono]:
  "⟦ M ≤ M'; ⋀x. dRETURN x ≤ M ⟹ f x ≤ f' x ⟧ ⟹ dbind M f ≤ dbind M' f'"
  "⟦ flat_ge M M'; ⋀x. flat_ge (f x) (f' x) ⟧ ⟹ flat_ge (dbind M f) (dbind M' f')"
  apply (cases M, simp_all)
  apply (cases M', simp_all)
  apply (cases M, simp_all add: flat_ord_def)
  apply (cases M', simp_all)
  done

lemma dbind_mono1[simp, intro!]: "mono dbind"
  apply (rule monoI)
  apply (rule le_funI)
  apply (rule dbind_mono)
  by auto

lemma dbind_mono2[simp, intro!]: "mono (dbind M)"
  apply (rule monoI)
  apply (rule dbind_mono)
  by (auto dest: le_funD)

lemma dr_mono_bind:
  assumes MA: "mono A" and MB: "⋀s. mono (B s)"
  shows "mono (λF s. dbind (A F s) (λs'. B s F s'))"
  apply (rule monoI)
  apply (rule le_funI)
  apply (rule dbind_mono)
  apply (auto dest: monoD[OF MA, THEN le_funD]) []
  apply (auto dest: monoD[OF MB, THEN le_funD]) []
  done

lemma dr_mono_bind': "mono (λF s. dbind (f s) F)"
  apply rule
  apply (rule le_funI)
  apply (rule dbind_mono)
  apply (auto dest: le_funD)
  done

(* TODO: Replace by monotonicity prover! *)
lemmas dr_mono = mono_if dr_mono_bind dr_mono_bind' mono_const mono_id

lemma [refine_mono]:
  "dbind dSUCCEED f = dSUCCEED"
  "dbind dFAIL f = dFAIL"
  by (simp_all)

definition "dASSERT ≡ iASSERT dRETURN"
definition "dASSUME ≡ iASSUME dRETURN"
interpretation dres_assert: generic_Assert dbind dRETURN dASSERT dASSUME
  apply unfold_locales
  by (auto simp: dASSERT_def dASSUME_def)

definition "dWHILEIT ≡ iWHILEIT dbind dRETURN"
definition "dWHILEI ≡ iWHILEI dbind dRETURN"
definition "dWHILET ≡ iWHILET dbind dRETURN"
definition "dWHILE ≡ iWHILE dbind dRETURN"

interpretation dres_while: generic_WHILE dbind dRETURN
  dWHILEIT dWHILEI dWHILET dWHILE
  apply unfold_locales
  apply (auto simp: dWHILEIT_def dWHILEI_def dWHILET_def dWHILE_def) 
  apply refine_mono+
  done

lemmas [code] = 
  dres_while.WHILEIT_unfold
  dres_while.WHILEI_unfold
  dres_while.WHILET_unfold
  dres_while.WHILE_unfold


text ‹
  Syntactic criteria to prove ‹s ≠ dSUCCEED›
›
lemma dres_ne_bot_basic[refine_transfer]:
  "dFAIL ≠ dSUCCEED"
  "⋀x. dRETURN x ≠ dSUCCEED"
  "⋀m f. ⟦ m≠dSUCCEED; ⋀x. f x ≠ dSUCCEED ⟧ ⟹ dbind m f ≠ dSUCCEED"
  "⋀Φ. dASSERT Φ ≠ dSUCCEED"
  "⋀b m1 m2. ⟦ m1≠dSUCCEED; m2≠dSUCCEED ⟧ ⟹ If b m1 m2 ≠ dSUCCEED"
  "⋀x f. ⟦ ⋀x. f x≠dSUCCEED ⟧ ⟹ Let x f ≠ dSUCCEED"
  "⋀g p. ⟦ ⋀x1 x2. g x1 x2 ≠ dSUCCEED ⟧ ⟹ case_prod g p ≠ dSUCCEED"
  "⋀fn fs x. 
    ⟦ fn≠dSUCCEED; ⋀v. fs v ≠ dSUCCEED ⟧ ⟹ case_option fn fs x ≠ dSUCCEED"
  "⋀fn fc x. 
    ⟦ fn≠dSUCCEED; ⋀x xs. fc x xs ≠ dSUCCEED ⟧ ⟹ case_list fn fc x ≠ dSUCCEED"
  apply (auto split: prod.split option.split list.split)
  apply (case_tac m, auto) []
  apply (case_tac Φ, auto) []
  done
  
lemma dres_ne_bot_RECT[refine_transfer]:
  assumes A: "⋀f x. ⟦ ⋀x. f x ≠ dSUCCEED ⟧ ⟹ B f x ≠ dSUCCEED"
  shows "RECT B x ≠ dSUCCEED"
  unfolding RECT_def
  apply (split if_split)
  apply (intro impI conjI)
  apply simp_all
  
  apply (rule flatf_fp_induct_pointwise[where pre="λ_ _. True" and B=B and b=top and post="λ_ _ m. m≠dSUCCEED"])
  apply (simp_all add: trimonoD A)
  done

lemma dres_ne_bot_dWHILEIT[refine_transfer]:
  assumes "⋀x. f x ≠ dSUCCEED" 
  shows "dWHILEIT I b f s ≠ dSUCCEED" using assms
  unfolding dWHILEIT_def iWHILEIT_def WHILEI_body_def
  apply refine_transfer
  done

lemma dres_ne_bot_dWHILET[refine_transfer]:
  assumes "⋀x. f x ≠ dSUCCEED" 
  shows "dWHILET b f s ≠ dSUCCEED" using assms
  unfolding dWHILET_def iWHILET_def iWHILEIT_def WHILEI_body_def
  apply refine_transfer
  done

end