Theory DFS_Framework_Refine_Aux

theory DFS_Framework_Refine_Aux
imports DFS_Framework_Misc Refine_Monadic.Refine_Monadic
begin


definition GHOST :: "'a ⇒ 'a" 
  ― ‹Ghost tag to mark ghost variables in let-expressions›
  where [simp]: "GHOST ≡ λx. x"
lemma GHOST_elim_Let: ― ‹Unfold rule to inline GHOST-Lets›
  shows "(let x=GHOST m in f x) = f m" by simp


lemma "WHILEI I b f s ≤ 
  do {ASSERT (I s); WHILE b (λs. do {s ← f s; ASSERT (I s); RETURN s}) s}"
  unfolding WHILEI_def WHILE_def WHILEI_body_def
  apply (rule refine_IdD)
  apply refine_rcg
  apply (rule introR[where R="br id I"])
  apply (simp_all add: br_def)
  apply (rule intro_prgR[where R="br id I"])
  apply (simp_all add: br_def)
  apply (auto simp: pw_le_iff refine_pw_simps)  
  done

(* TODO: Move to RefineG_While *)
lemma WHILET_eq_WHILE:
  assumes "WHILET b f s0 ≠ top"
  shows "WHILET b f s0 = WHILE b f s0"
  using assms
  unfolding WHILET_def WHILE_def WHILEIT_def WHILEI_def
  by (rule RECT_eq_REC)

lemma WHILEIT_eq_WHILEI:
  assumes "WHILEIT I b f s0 ≠ top"
  shows "WHILEIT I b f s0 = WHILEI I b f s0"
  using assms
  unfolding WHILEIT_def WHILEI_def
  by (rule RECT_eq_REC)

(* TODO: Move to refinement framework! *)
lemma WHILEIT_le_WHILEI:
  assumes "wf V"
  assumes VAR: "⋀s. ⟦ I s; b s; f s ≤ SPEC I ⟧ ⟹ f s ≤ SPEC (λs'. (s',s)∈V)"
  shows "WHILEIT I b f s ≤ WHILEI I b f s"
  using ‹wf V›
  apply (induction s rule: wf_induct[consumes 1])
  apply (subst WHILEIT_unfold) 
  apply (subst WHILEI_unfold)
proof (clarsimp)
  fix x
  assume A: "I x" "b x"
  assume IH: "∀y. (y, x) ∈ V ⟶ WHILE⇩T⇗I⇖ b f y ≤ WHILE⇗I⇖ b f y"

  show "f x ⤜ WHILE⇩T⇗I⇖ b f ≤ f x ⤜ WHILE⇗I⇖ b f"
  proof cases
    assume B: "f x ≤ SPEC I"
    show "?thesis"
      apply (rule Refine_Basic.bind_mono(1)[OF order_refl])
      using IH VAR[OF A B]
      by (auto simp: pw_le_iff)
  next
    assume B: "¬(f x ≤ SPEC I)"
    hence "f x ⤜ WHILE⇗I⇖ b f = FAIL"
      apply (subst WHILEI_unfold[abs_def])
      apply (auto simp: pw_eq_iff pw_le_iff refine_pw_simps)
      done
    thus ?thesis by simp  
  qed
qed

lemmas WHILEIT_refine_WHILEI = order_trans[OF WHILEIT_le_WHILEI WHILEI_refine]


lemma WHILET_eq_WHILE_tproof:
  assumes "wf V"
  assumes "I s0"
  assumes "⋀s. ⟦ I s; b s ⟧ ⟹ f s ≤ SPEC (λs'. I s' ∧ (s',s)∈V)"
  shows "WHILET b f s0 = WHILE b f s0"
proof -
  have "WHILET b f s0 ≤ SPEC I"
    by (rule WHILET_rule[where I=I], fact+)
  hence "WHILET b f s0 ≠ top" by auto 

  thus ?thesis
    unfolding WHILE_def WHILEI_def WHILET_def WHILEIT_def
    by (subst RECT_eq_REC) auto
qed  


lemma WHILEIT_eq_WHILEI_tproof:
  assumes "wf V"
  assumes "⋀s. ⟦ I s; b s ⟧ ⟹ f s ≤ SPEC (λs'. (s',s)∈V)"
  shows "WHILEIT I b f s0 = WHILEI I b f s0"
  apply (rule antisym)
    subgoal by (rule WHILEIT_le_WHILEI[OF assms])
    subgoal by (rule WHILEI_le_WHILEIT)
  done  



end