Theory DFS_Framework.DFS_Framework_Refine_Aux

theory DFS_Framework_Refine_Aux
imports DFS_Framework_Misc Refine_Monadic.Refine_Monadic

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)  

(* 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)

  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! *)
  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  WHILETIb f y  WHILE⇗Ib f y"

  show "f x  WHILETIb f  f x  WHILE⇗Ib 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)
    assume B: "¬(f x  SPEC I)"
    hence "f x  WHILE⇗Ib f = FAIL"
      apply (subst WHILEI_unfold[abs_def])
      apply (auto simp: pw_eq_iff pw_le_iff refine_pw_simps)
    thus ?thesis by simp  

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

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)