Theory DFS_Framework_Refine_Aux

(* TODO: Integrate into Refinement Framework *)
theory DFS_Framework_Refine_Aux
imports "../../Libs/CAVA_Automata/CAVA_Base/CAVA_Base" DFS_Framework_Misc
begin

(*****************************)
(* Autoref *)

text {* General casting-tag, that allows type-casting on concrete level, while 
  being identity on abstract level. *}
definition [simp]: "CAST ≡ id"
lemma [autoref_itype]: "CAST ::⇩i I ->⇩i I" by simp

(* TODO: This idea does currently not work, b/c a homogeneity rule
  will be created from the (λx. x, CAST)∈R -> R rule, which will always
  be applied first! As a workaround, we make the cast mandatory!
*)
(*lemma [autoref_rules]: 
  assumes "PRIO_TAG_GEN_ALGO"
  shows "(λx. x,CAST) ∈ R -> R"
  by auto
*)


(*****************************)
(* Refine-Util *)

(* TODO: Move to Refine_Util *)
attribute_setup zero_var_indexes = {*
  Scan.succeed (Thm.rule_attribute (K Drule.zero_var_indexes))
*} "Set variable indexes to zero, renaming to avoid clashes"

(* TODO: Move, Refine_Util *)
(*
  mk_record_simp: Converts a lemma of the form 
    "f s = x" to the form "r ≡ s ==> f r = x"
  
  This is used to fold the x.simp - lemmas of a record x with a definition
  of the form "r ≡ (| ... |)),".

  Usage example:
    record foo = ...
    definition c :: foo where "c ≡ (| ... |)),"
    lemmas c_simps[simp] = foo.simps[mk_record_simp, OF c_def]
*)
lemma mk_record_simp_thm:
  fixes f :: "'a => 'b"
  assumes "f s = x"
  assumes "r ≡ s"
  shows "f r = x"
  using assms by simp

ML {*
  fun mk_record_simp thm = let
    val thy = theory_of_thm thm
    val cert = cterm_of thy
  in
    case concl_of thm of
      @{mpat "Trueprop (?f _=_)"} => 
        let
          val cf = cert f
          val r = cterm_instantiate 
            [(@{cpat "?f :: ?'a => ?'b"},cf)] 
            @{thm mk_record_simp_thm}
          val r = r OF [thm]
        in r end
    | _ => raise THM("",~1,[thm])

  end
*}

attribute_setup mk_record_simp = 
  {* Scan.succeed (Thm.rule_attribute (K mk_record_simp)) *}
  "Make simplification rule for record definition"


(*****************************)
(* RefineG_Domain *)
(* TODO: Move to RefineG_Domain *)
lemma flat_ge_sup_mono[refine_mono]: "!!a a'::'a::complete_lattice. 
  flat_ge a a' ==> flat_ge b b' ==> flat_ge (sup a b) (sup a' b')"
  by (auto simp: flat_ord_def)

declare sup_mono[refine_mono]


(*****************************)
(* Refine-Basic *)
(* TODO: Move to Refine_Basic *)
lemma nofail_RES_conv: "nofail m <-> (∃M. m=RES M)" by (cases m) auto

(* TODO: Move, near SPEC_nofail  *)
lemma nofail_SPEC: "nofail m ==> m ≤ SPEC (λ_. True)"
  by (simp add: pw_le_iff)

lemma nofail_SPEC_iff: "nofail m <-> m ≤ SPEC (λ_. True)"
  by (simp add: pw_le_iff)

lemma nofail_SPEC_triv_refine: "[| nofail m; !!x. Φ x |] ==> m ≤ SPEC Φ"
  by (simp add: pw_le_iff)

(* TODO: Move *)
lemma bind_cong:
  assumes "m=m'"
  assumes "!!x. RETURN x ≤ m' ==> f x = f' x"
  shows "bind m f = bind m' f'"  
  using assms
  by (auto simp: refine_pw_simps pw_eq_iff pw_le_iff)


primrec the_RES where "the_RES (RES X) = X"
lemma the_RES_inv[simp]: "nofail m ==> RES (the_RES m) = m"
  by (cases m) auto

lemma le_SPEC_UNIV_rule [refine_vcg]: 
  "m ≤ SPEC (λ_. True) ==> m ≤ RES UNIV" by auto

definition [refine_pw_simps]: "nf_inres m x ≡ nofail m ∧ inres m x"

lemma nf_inres_RES[simp]: "nf_inres (RES X) x <-> x∈X" 
  by (simp add: refine_pw_simps)
  
lemma nf_inres_SPEC[simp]: "nf_inres (SPEC Φ) x <-> Φ x" 
  by (simp add: refine_pw_simps)

lemma bind_refine_abs': (* Only keep nf_inres-information for abstract *)
  fixes R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ \<Down> R' M'"
  assumes R2: "!!x x'. [| (x,x')∈R'; nf_inres M' x'
  |] ==> f x ≤ \<Down> R (f' x')"
  shows "bind M (λx. f x) ≤ \<Down> R (bind M' (λx'. f' x'))"
  using assms
  apply (simp add: pw_le_iff refine_pw_simps)
  apply blast
  done

(* TODO: Move *)
lemma Let_refine':
  assumes "(m,m')∈R"
  assumes "(m,m')∈R ==> f m ≤\<Down>S (f' m')"
  shows "Let m f ≤ \<Down>S (Let m' f')"
  using assms by simp

(* TODO: Move, test as default simp-rule *)
lemma RETURN_refine_iff[simp]: "RETURN x ≤\<Down>R (RETURN y) <-> (x,y)∈R"
  by (auto simp: pw_le_iff refine_pw_simps)

lemma RETURN_RES_refine_iff: 
  "RETURN x ≤\<Down>R (RES Y) <-> (∃y∈Y. (x,y)∈R)"
  by (auto simp: pw_le_iff refine_pw_simps)

lemma in_nres_rel_iff: "(a,b)∈⟨R⟩nres_rel <-> a ≤\<Down>R b"
  by (auto simp: nres_rel_def)



lemma inf_RETURN_RES: 
  "inf (RETURN x) (RES X) = (if x∈X then RETURN x else SUCCEED)"
  "inf (RES X) (RETURN x) = (if x∈X then RETURN x else SUCCEED)"
  by (auto simp: pw_eq_iff refine_pw_simps)

(* TODO: MOve, test as default simp-rule *)
lemma inf_RETURN_SPEC[simp]:
  "inf (RETURN x) (SPEC (λy. Φ y)) = SPEC (λy. y=x ∧ Φ x)"
  "inf (SPEC (λy. Φ y)) (RETURN x) = SPEC (λy. y=x ∧ Φ x)"
  by (auto simp: pw_eq_iff refine_pw_simps)

lemma RES_sng_eq_RETURN: "RES {x} = RETURN x"
  by simp

lemma nofail_inf_serialize:
  "[|nofail a; nofail b|] ==> inf a b = do {x\<leftarrow>a; ASSUME (inres b x); RETURN x}"
  by (auto simp: pw_eq_iff refine_pw_simps)

lemma conc_fun_SPEC: 
  "\<Down>R (SPEC (λx. Φ x)) = SPEC (λy. ∃x. (y,x)∈R ∧ Φ x)"  
  by (auto simp: pw_eq_iff refine_pw_simps)

lemma conc_fun_RETURN: 
  "\<Down>R (RETURN x) = SPEC (λy. (y,x)∈R)"  
  by (auto simp: pw_eq_iff refine_pw_simps)



definition lift_assn :: "('a × 'b) set => ('b => bool) => ('a => bool)"
  -- ‹Lift assertion over refinement relation›
  where "lift_assn R Φ s ≡ ∃s'. (s,s')∈R ∧ Φ s'"
lemma lift_assnI: "[|(s,s')∈R; Φ s'|] ==> lift_assn R Φ s"
  unfolding lift_assn_def by auto

(* TODO: Replace original lemma *)
lemma case_option_refine[refine]:
  assumes "(x,x')∈Id"
  assumes "x=None ==> fn ≤ \<Down>R fn'"
  assumes "!!v v'. [|x=Some v; (v,v')∈Id|] ==> fs v ≤ \<Down>R (fs' v')"
  shows "case_option fn (λv. fs v) x ≤ \<Down>R (case_option fn' (λv'. fs' v') x')"
  using assms by (auto split: option.split)


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



text ‹The following set of rules executes a step on the LHS or RHS of 
  a refinement proof obligation, without changing the other side.
  These kind of rules is useful for performing refinements with 
  invisible steps.›  
lemma lhs_step_If:
  "[| b ==> t ≤ m; ¬b ==> e ≤ m |] ==> If b t e ≤ m" by simp

lemma lhs_step_RES:
  "[| !!x. x∈X ==> RETURN x ≤ m  |] ==> RES X ≤ m" 
  by (simp add: pw_le_iff)

lemma lhs_step_SPEC:
  "[| !!x. Φ x ==> RETURN x ≤ m |] ==> SPEC (λx. Φ x) ≤ m" 
  by (simp add: pw_le_iff)

lemma lhs_step_bind:
  fixes m :: "'a nres" and f :: "'a => 'b nres"
  assumes "nofail m' ==> nofail m"
  assumes "!!x. nf_inres m x ==> f x ≤ m'"
  shows "do {x\<leftarrow>m; f x} ≤ m'"
  using assms
  by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind:
  assumes "m ≤ \<Down>R m'" "inres m x" "!!x'. (x,x')∈R ==> lhs ≤\<Down>S (f' x')"
  shows "lhs ≤ \<Down>S (m' »= f')"
  using assms
  by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind_RES:
  assumes "x'∈X'"
  assumes "m ≤ \<Down>R (f' x')"
  shows "m ≤ \<Down>R (RES X' »= f')"
  using assms by (simp add: pw_le_iff refine_pw_simps) blast

lemma rhs_step_bind_SPEC:
  assumes "Φ x'"
  assumes "m ≤ \<Down>R (f' x')"
  shows "m ≤ \<Down>R (SPEC Φ »= f')"
  using assms by (simp add: pw_le_iff refine_pw_simps) blast

lemma RES_bind_choose:
  assumes "x∈X"
  assumes "m ≤ f x"
  shows "m ≤ RES X »= f"
  using assms by (auto simp: pw_le_iff refine_pw_simps)

lemma pw_RES_bind_choose: 
  "nofail (RES X »= f) <-> (∀x∈X. nofail (f x))"
  "inres (RES X »= f) y <-> (∃x∈X. inres (f x) y)"
  by (auto simp: refine_pw_simps)


(* TODO: Move to Refine_Basic: Convenience*)
lemma use_spec_rule:
  assumes "m ≤ SPEC Ψ"
  assumes "m ≤ SPEC (λs. Ψ s --> Φ s)"
  shows "m ≤ SPEC Φ"
  using assms
  by (auto simp: pw_le_iff refine_pw_simps)

lemma strengthen_SPEC: "m ≤ SPEC Φ ==> m ≤ SPEC(λs. inres m s ∧ Φ s)"
  -- "Strengthen SPEC by adding trivial upper bound for result"
  by (auto simp: pw_le_iff refine_pw_simps)

lemma weaken_SPEC:
  "m ≤ SPEC Φ ==> (!!x. Φ x ==> Ψ x) ==> m ≤ SPEC Ψ"
  by (force elim!: order_trans)


lemma ife_FAIL_to_ASSERT_cnv: 
  "(if Φ then m else FAIL) = op_nres_ASSERT_bnd Φ m"
  by (cases Φ, auto)



lemma param_op_nres_ASSERT_bnd[param]:
  assumes "Φ' ==> Φ"
  assumes "[|Φ'; Φ|] ==> (m,m')∈⟨R⟩nres_rel"
  shows "(op_nres_ASSERT_bnd Φ m, op_nres_ASSERT_bnd Φ' m') ∈ ⟨R⟩nres_rel"
  using assms
  by (auto simp: pw_le_iff refine_pw_simps nres_rel_def)

declare autoref_FAIL[param]


(* TODO: Move *)
method_setup refine_vcg = 
  {* Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
    Refine.rcg_tac (add_thms @ Refine.vcg.get ctxt) ctxt THEN_ALL_NEW (TRY o Refine.post_tac ctxt)
  )) *} 
  "Refinement framework: Generate refinement and verification conditions"



(*****************************)
(* Refine_Transfer *)
lemma (in transfer) transfer_sum[refine_transfer]:
  assumes "!!l. α (fl l) ≤ Fl l"
  assumes "!!r. α (fr r) ≤ Fr r"
  shows "α (case_sum fl fr x) ≤ (case_sum Fl Fr x)"
  using assms by (auto split: sum.split)


(* TODO: Move *)
lemma nres_of_transfer[refine_transfer]: "nres_of x ≤ nres_of x" by simp



(*****************************)
(* Refine_Foreach  *)
(* TODO: Change in Refine_Foreach(?)! *)
declare FOREACH_patterns[autoref_op_pat_def]

(*****************************)
(* Refine_Recursion  *)
theorem param_RECT[param]:
  assumes "(B, B') ∈ (Ra -> ⟨Rr⟩nres_rel) -> Ra -> ⟨Rr⟩nres_rel"
    and "trimono B"
  shows "(REC⇩T B, REC⇩T B')∈ Ra -> ⟨Rr⟩nres_rel"
  using autoref_RECT assms by simp

definition "REC_annot pre post body x ≡ 
  REC (λD x. do {ASSERT (pre x); r\<leftarrow>body D x; ASSERT (post x r); RETURN r}) x"

theorem REC_annot_rule[refine_vcg]:
  assumes M: "trimono body"
  and P: "pre x"
  and S: "!!f x. [|!!x. pre x ==> f x ≤ SPEC (post x); pre x|] 
          ==> body f x ≤ SPEC (post x)"
  and C: "!!r. post x r ==> Φ r"
  shows "REC_annot pre post body x ≤ SPEC Φ"
proof -
  from `trimono body` have [refine_mono]:
    "!!f g x xa. (!!x. flat_ge (f x) (g x)) ==> flat_ge (body f x) (body g x)"
    "!!f g x xa. (!!x. f x ≤ g x) ==> body f x ≤ body g x"
    apply -
    unfolding trimono_def monotone_def fun_ord_def mono_def le_fun_def
    apply (auto)
    done

  show ?thesis
    unfolding REC_annot_def
    apply (rule order_trans[where y="SPEC (post x)"])
    apply (refine_rcg 
      refine_vcg 
      REC_rule[where pre=pre and M="λx. SPEC (post x)"]
      order_trans[OF S]
    )
    apply fact
    apply simp
    using C apply (auto) []
    done
qed



(*****************************)
(* Refine_While  *)
context begin interpretation autoref_syn .
(* TODO: Change in Refine_While *)
lemma [autoref_op_pat_def]:
  "WHILEIT I ≡ OP (WHILEIT I)"
  "WHILEI I ≡ OP (WHILEI I)"
  by auto
end

context begin interpretation autoref_syn .

(* TODO: Move, change original WHILE-rule  *)
lemma autoref_WHILE'[autoref_rules]:
  assumes "!!x x'. [| (x,x')∈R|] ==> (c x,c'$x') ∈ Id"
  assumes "!!x x'. [| REMOVE_INTERNAL c' x'; (x,x')∈R|] 
    ==> (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILE c f,
      (OP WHILE ::: (R->Id) -> (R->⟨R⟩nres_rel) -> R -> ⟨R⟩nres_rel)$c'$f'
    )∈R -> ⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILE_refine)

(* TODO: Move, change original WHILE-rule  *)
lemma autoref_WHILEI[autoref_rules]:
  assumes "!!x x'. [|I x'; (x,x')∈R|] ==> (c x,c'$x') ∈ Id"
  assumes "!!x x'. [|REMOVE_INTERNAL c' x'; I x'; (x,x')∈R|] ==>(f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "I s' ==> (s,s')∈R"
  shows "(WHILE c f s,
      (OP (WHILEI I) ::: (R->Id) -> (R->⟨R⟩nres_rel) -> R -> ⟨R⟩nres_rel)$c'$f'$s'
    )∈⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILE_refine')


(* TODO: Move, change original WHILE-rule  *)
lemma autoref_WHILEI'[autoref_rules]:
  assumes "!!x x'. [| (x,x')∈R; I x'|] ==> (c x,c'$x') ∈ Id"
  assumes "!!x x'. [| REMOVE_INTERNAL c' x'; (x,x')∈R; I x'|] 
    ==> (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILE c f,
      (OP (WHILEI I) ::: (R->Id) -> (R->⟨R⟩nres_rel) -> R -> ⟨R⟩nres_rel)$c'$f'
    )∈R -> ⟨R⟩nres_rel"
    unfolding autoref_tag_defs
    by (parametricity 
      add: autoref_WHILEI[unfolded autoref_tag_defs]
      assms[unfolded autoref_tag_defs])


(* TODO: Move, change original WHILE-rule  *)
lemma autoref_WHILEIT[autoref_rules]:
  assumes "!!x x'. [|I x'; (x,x')∈R|] ==> (c x,c'$x') ∈ Id"
  assumes "!!x x'. [|REMOVE_INTERNAL c' x'; I x'; (x,x')∈R|] ==>(f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "I s' ==> (s,s')∈R"
  shows "(WHILET c f s,
      (OP (WHILEIT I) ::: (R->Id) -> (R->⟨R⟩nres_rel) -> R -> ⟨R⟩nres_rel)$c'$f'$s'
    )∈⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILET_refine')


(* TODO: Move, change original WHILE-rule  *)
lemma autoref_WHILEIT'[autoref_rules]:
  assumes "!!x x'. [| (x,x')∈R; I x'|] ==> (c x,c'$x') ∈ Id"
  assumes "!!x x'. [| REMOVE_INTERNAL c' x'; (x,x')∈R; I x'|] 
    ==> (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILET c f,
      (OP (WHILEIT I) ::: (R->Id) -> (R->⟨R⟩nres_rel) -> R -> ⟨R⟩nres_rel)$c'$f'
    )∈R -> ⟨R⟩nres_rel"
    unfolding autoref_tag_defs
    by (parametricity 
      add: autoref_WHILEIT[unfolded autoref_tag_defs]
      assms[unfolded autoref_tag_defs])


end



(*****************************)
(* Relators *)
lemma set_relD: "(s,s')∈⟨R⟩set_rel ==> x∈s ==> ∃x'∈s'. (x,x')∈R"
  unfolding set_rel_def by blast

lemma set_relE[consumes 2]: 
  assumes "(s,s')∈⟨R⟩set_rel" "x∈s"
  obtains x' where "x'∈s'" "(x,x')∈R"
  using set_relD[OF assms] ..

lemma param_prod': "[| 
  !!a b a' b'. [|p=(a,b); p'=(a',b')|] ==> (f a b,f' a' b')∈R  
  |] ==> (case_prod f p, case_prod f' p')∈R"
  by (auto split: prod.split)

(* TODO: Move to Relators *)
lemma list_rel_append1: "(as @ bs, l) ∈ ⟨R⟩list_rel 
  <-> (∃cs ds. l = cs@ds ∧ (as,cs)∈⟨R⟩list_rel ∧ (bs,ds)∈⟨R⟩list_rel)"
  apply (simp add: list_rel_def list_all2_append1)
  apply auto
  apply (metis list_all2_lengthD)
  done

lemma list_rel_append2: "(l,as @ bs) ∈ ⟨R⟩list_rel 
  <-> (∃cs ds. l = cs@ds ∧ (cs,as)∈⟨R⟩list_rel ∧ (ds,bs)∈⟨R⟩list_rel)"
  apply (simp add: list_rel_def list_all2_append2)
  apply auto
  apply (metis list_all2_lengthD)
  done


(* TODO: Move *)

ML {*
  (* Prefix p_ or wrong type supresses generation of relAPP *)

  fun cnv_relAPP t = let
    fun consider (Var ((name,_),T)) =
      if String.isPrefix "p_" name then false   
      else (
        case T of
          Type(@{type_name set},[Type(@{type_name prod},_)]) => true
        | _ => false)
    | consider _ = true

    fun strip_rcomb u : term * term list =
      let 
        fun stripc (x as (f$t, ts)) = 
          if consider t then stripc (f, t::ts) else x
        | stripc  x =  x
      in  stripc(u,[])  end;

    val (f,a) = strip_rcomb t
  in 
    Relators.list_relAPP a f
  end

  fun to_relAPP_conv ctxt = Refine_Util.f_tac_conv ctxt 
    cnv_relAPP 
    (ALLGOALS (simp_tac 
      (put_simpset HOL_basic_ss ctxt addsimps @{thms relAPP_def})))


  val to_relAPP_attr = Thm.rule_attribute (fn context => let
    val ctxt = Context.proof_of context
  in
    Conv.fconv_rule (Conv.arg1_conv (to_relAPP_conv ctxt))
  end)
*}

attribute_setup to_relAPP = {* Scan.succeed (to_relAPP_attr) *} 
  "Convert relator definition to prefix-form"




(*****************************)  
(* Parametricity-HOL *)

lemma dropWhile_param[param]: 
  "(dropWhile, dropWhile) ∈ (a -> bool_rel) -> ⟨a⟩list_rel -> ⟨a⟩list_rel"
  unfolding dropWhile_def by parametricity

term takeWhile
lemma takeWhile_param[param]: 
  "(takeWhile, takeWhile) ∈ (a -> bool_rel) -> ⟨a⟩list_rel -> ⟨a⟩list_rel"
  unfolding takeWhile_def by parametricity


lemma [relator_props]:  
  "bijective R ==> single_valued R"
  "bijective R ==> single_valued (R¯)"
  by (simp_all add: bijective_alt)

(* TODO: Move *)
declare bijective_Id[relator_props]
declare bijective_Empty[relator_props]

lemma param_subseteq[param]: 
  "[|single_valued (R¯)|] ==> (op ⊆, op ⊆) ∈ ⟨R⟩set_rel -> ⟨R⟩set_rel -> bool_rel"
  by (clarsimp simp: set_rel_def single_valued_def) blast

lemma param_subset[param]: 
  "[|single_valued (R¯)|] ==> (op ⊂, op ⊂) ∈ ⟨R⟩set_rel -> ⟨R⟩set_rel -> bool_rel"
  (* Fine-tuned proof for speed *)
  apply (simp add: set_rel_def single_valued_def)
  apply safe
  apply blast+
  done

lemma bij_set_rel_for_inj: 
  fixes R
  defines "α ≡ fun_of_rel R" 
  assumes "bijective R" "(s,s')∈⟨R⟩set_rel"  
  shows "inj_on α s" "s' = α`s"
  using assms
  unfolding bijective_def set_rel_def α_def fun_of_rel_def[abs_def]
  apply (auto intro!: inj_onI ImageI simp: image_def)
  apply (metis (mono_tags) Domain.simps contra_subsetD tfl_some)
  apply (metis (mono_tags) someI)
  apply (metis DomainE contra_subsetD tfl_some)
  done


(*****************************)
(* Autoref-HOL  *)
lemmas [autoref_rules] = dropWhile_param takeWhile_param


(*****************************)
(* Autoref-Tool *)

method_setup autoref_solve_id_op = {*
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (
    Autoref_Id_Ops.id_tac (Config.put Autoref_Id_Ops.cfg_ss_id_op false ctxt)
  ))
*}


(*****************************)
(* Autoref_Monadic  *)

(* TODO: Replace! *)
text {* Default setup of the autoref-tool for the monadic framework. *}

lemma autoref_monadicI1:
  assumes "(b,a)∈⟨R⟩nres_rel"
  assumes "RETURN c ≤ b"
  shows "(RETURN c, a)∈⟨R⟩nres_rel" "RETURN c ≤\<Down>R a"
  using assms
  unfolding nres_rel_def
  by simp_all

lemma autoref_monadicI2:
  assumes "(b,a)∈⟨R⟩nres_rel"
  assumes "nres_of c ≤ b"
  shows "(nres_of c, a)∈⟨R⟩nres_rel" "nres_of c ≤ \<Down>R a"
  using assms
  unfolding nres_rel_def
  by simp_all

lemmas autoref_monadicI = autoref_monadicI1 autoref_monadicI2

ML {*
  structure Autoref_Monadic = struct

    val cfg_plain = Attrib.setup_config_bool @{binding autoref_plain} (K false)

    fun autoref_monadic_tac ctxt = let
      open Autoref_Tacticals
      val ctxt = Autoref_Phases.init_data ctxt
      val plain = Config.get ctxt cfg_plain
      val trans_thms = if plain then [] else @{thms the_resI}
  
    in
      resolve_tac @{thms autoref_monadicI}
      THEN' 
      IF_SOLVED (Autoref_Phases.all_phases_tac ctxt)
        (RefineG_Transfer.post_transfer_tac trans_thms ctxt)
        (K all_tac) (* Autoref failed *)

    end
  end
*}

method_setup autoref_monadic = {* let
    open Refine_Util Autoref_Monadic
    val autoref_flags = 
          parse_bool_config "trace" Autoref_Phases.cfg_trace
      ||  parse_bool_config "debug" Autoref_Phases.cfg_debug
      ||  parse_bool_config "plain" Autoref_Monadic.cfg_plain

  in
    parse_paren_lists autoref_flags 
    >>
    ( fn _ => fn ctxt => SIMPLE_METHOD' (
      let 
        val ctxt = Config.put Autoref_Phases.cfg_keep_goal true ctxt
      in autoref_monadic_tac ctxt end
    ))

  end

 *} 
 "Automatic Refinement and Determinization for the Monadic Refinement Framework"

(* Move to Refine Transfer *)
lemma dres_unit_simps[refine_transfer_post_simp]:
  "dbind (dRETURN (u::unit)) f = f ()"
  by auto

lemma Let_dRETURN_simp[refine_transfer_post_simp]:
  "Let m dRETURN = dRETURN m" by auto

(* TODO: Move *)
lemmas [refine_transfer_post_simp] = dres_monad_laws



(* TODO: Move *)
lemma le_ASSERT_defI1:
  assumes "c ≡ do {ASSERT Φ; m}"
  assumes "Φ ==> m' ≤ c"
  shows "m' ≤ c"
  using assms
  by (simp add: le_ASSERTI)

lemma refine_ASSERT_defI1:
  assumes "c ≡ do {ASSERT Φ; m}"
  assumes "Φ ==> m' ≤ \<Down>R c"
  shows "m' ≤ \<Down>R c"
  using assms
  by (simp, refine_vcg)

lemma le_ASSERT_defI2:
  assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
  assumes "[|Φ; Ψ|] ==> m' ≤ c"
  shows "m' ≤ c"
  using assms
  by (simp add: le_ASSERTI)

lemma refine_ASSERT_defI2:
  assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
  assumes "[|Φ; Ψ|] ==> m' ≤ \<Down>R c"
  shows "m' ≤ \<Down>R c"
  using assms
  by (simp, refine_vcg)

lemma ASSERT_le_defI:
  assumes "c ≡ do { ASSERT Φ; m'}"
  assumes "Φ"
  assumes "Φ ==> m' ≤ m"
  shows "c ≤ m"
  using assms by (auto)








(*****************************)
(* ICF *)

(* Note, currently select is defined in CAVA_Base! *)
lemma select_correct: 
  "select X ≤ SPEC (λr. case r of None => X={} | Some x => x∈X)"
  unfolding select_def
  apply (refine_rcg refine_vcg)
  by auto


definition "prod_bhc bhc1 bhc2 ≡ λn (a,b). (bhc1 n a * 33 + bhc2 n b) mod n"

lemma prod_bhc_ga[autoref_ga_rules]:
  "[| GEN_ALGO_tag (is_bounded_hashcode R eq1 bhc1); 
     GEN_ALGO_tag (is_bounded_hashcode S eq2 bhc2)|] 
  ==> is_bounded_hashcode (R×⇩rS) (prod_eq eq1 eq2) (prod_bhc bhc1 bhc2)"
  unfolding is_bounded_hashcode_def prod_bhc_def prod_eq_def[abs_def]
  apply safe
  apply (auto dest: fun_relD)
  done

lemma prod_dhs_ga[autoref_ga_rules]:
  "[| GEN_ALGO_tag (is_valid_def_hm_size TYPE('a) n1);
     GEN_ALGO_tag (is_valid_def_hm_size TYPE('b) n2) |]
   ==> is_valid_def_hm_size TYPE('a*'b) (n1+n2)"
   unfolding is_valid_def_hm_size_def by auto

(* TODO: Move *)
abbreviation ahs_rel where "ahs_rel bhc ≡ (map2set_rel (ahm_rel bhc))"



(*****************************)
(*  *)

end