Theory Refine_Det

header {* \isaheader{Deterministic Monad} *}
theory Refine_Det
imports 
  "~~/src/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 x dFAILi = x"
    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"

  instance
    apply intro_classes
    apply (simp add: less_dres_def)
    apply (case_tac x, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, 
      simp_all, case_tac [!] z, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, 
      simp_all, case_tac [!] z, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, simp_all) []

    apply (case_tac x, simp_all, case_tac [!] y, 
      simp_all, case_tac [!] z, simp_all) []

    apply (case_tac a, simp_all add: bot_dres_def) []
    apply (case_tac a, simp_all add: top_dres_def) []

    apply (case_tac x)
    apply (auto simp add: Inf_dres_def) [3]

    apply (case_tac z, simp_all add: Inf_dres_def) []
      apply (auto) [] 
        apply (case_tac x, fastforce+) []
        apply (case_tac x, fastforce+) []
        
      apply auto []
        apply (case_tac x) 
          apply force 
          apply force
          apply (subgoal_tac "dRETURN a ≤ dRETURN aa ∧ dRETURN a ≤ dRETURN b")
            apply auto []
            apply blast
        apply force

        apply (case_tac x) [] 
          apply force
          apply force
          apply auto []
          apply (subgoal_tac "(THE x. dRETURN x ∈ A) = aa")
          apply force
          apply force

    apply (case_tac x)
    apply (auto simp add: Sup_dres_def) [3]
    apply (case_tac xa, simp_all) [] 
    apply (subgoal_tac "(THE x. dRETURN x ∈ A) = aa")
    apply force
    apply force

    apply (case_tac z, auto simp add: Sup_dres_def) []
      apply force
      apply (case_tac x, force+) []

      apply (case_tac x, force, force) []
      apply (subgoal_tac "dRETURN aa ≤ dRETURN a ∧ dRETURN b ≤ dRETURN a")
        apply auto []
        apply blast

      apply force

      apply (case_tac x, force+)[]
    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.cases(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

setup {*
  Adhoc_Overloading.add_variant 
  @{const_name Monad_Syntax.bind} @{const_name 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'"
  apply (cases M, simp_all)
  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) 
  done

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


text {* 
  Syntactic criteria to prove @{text "s ≠ dSUCCEED"}
*}
lemma dres_ne_bot_basic[refine_transfer]:
  "dFAIL ≠ dSUCCEED"
  "dRETURN x ≠ dSUCCEED"
  "[| m≠dSUCCEED; !!x. f x ≠ dSUCCEED |] ==> dbind m f ≠ dSUCCEED"
  "dASSERT Φ ≠ dSUCCEED"
  "[| m1≠dSUCCEED; m2≠dSUCCEED |] ==> If b m1 m2 ≠ dSUCCEED"
  "[| !!x. f x≠dSUCCEED |] ==> Let x f ≠ dSUCCEED"
  "[| !!x1 x2. g x1 x2 ≠ dSUCCEED |] ==> prod_case g p ≠ dSUCCEED"
  apply (auto split: prod.split)
  apply (cases m, auto) []
  apply (cases Φ, auto) []
  done
  
lemma dres_ne_bot_RECT[rule_format, refine_transfer]:
  assumes A: "!!f x. [| !!x. f x ≠ dSUCCEED |] ==> B f x ≠ dSUCCEED"
  shows "∀x. RECT B x ≠ dSUCCEED"
  unfolding RECT_def
  apply (split split_if)
  apply (subst all_conj_distrib)
  apply (intro impI conjI)
  apply simp
  apply (intro impI)
  apply (erule gfp_cadm_induct[rotated])
  apply (intro allI)
  apply (rule A)
  apply simp

  apply rule
  apply simp
  apply (intro allI)
  apply (drule_tac x=x in point_chainI)
  apply (erule dres_Inf_chain_cases)
  apply (auto simp: Inf_fun_def INF_def dest!: subset_singletonD) []
  apply (auto simp: Inf_fun_def INF_def) []
  apply (auto simp: Inf_fun_def INF_def) []
  apply metis
  apply simp
  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