theory Scratch
  imports Collections.Refine_Dflt
begin

definition
  "assume_test X \<equiv> do { ASSUME (finite X); RETURN X }"

lemma [simp]:
  "(X', X) \<in> \<langle>Id\<rangle>list_set_rel \<Longrightarrow> finite X"
  by (auto simp: list_set_rel_def br_def)

lemma assume_test_refine:
  assumes "(X', X) \<in> \<langle>Id\<rangle>list_set_rel"
  shows "(RETURN X', assume_test X) \<in> \<langle>\<langle>Id\<rangle>list_set_rel\<rangle>nres_rel"
  using assms
  unfolding nres_rel_def assume_test_def
  by (auto simp: assume_test_def)

lemma (* [autoref_rules]: *)
  assumes [autoref_rules]: "(X', X) \<in> \<langle>Id\<rangle>list_set_rel"
  shows "(RETURN (), ASSUME (finite X)) \<in> \<langle>Id\<rangle>nres_rel"
  using assms
  by (auto simp: nres_rel_def)

lemma (* [autoref_rules]: *)
  assumes [autoref_rules]: "(X', X) \<in> \<langle>Id\<rangle>list_set_rel"
  assumes [autoref_rules]: "(Z', Z) \<in> R"
  shows "(Z', op_nres_ASSUME_bnd (finite X) Z) \<in> R"
  using assms
  by auto

schematic_goal assume_test_refine:
  assumes [autoref_rules]: "(X', X) \<in> \<langle>Id\<rangle>list_set_rel"
  shows "(?f, assume_test X) \<in> \<langle>\<langle>Id\<rangle>list_set_rel\<rangle>nres_rel"
  unfolding assume_test_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal))
  oops

(* ASSERT works, of course *)
definition
 "assert_test X \<equiv> do { ASSERT (finite X); RETURN X }"

schematic_goal
  assumes [autoref_rules]: "(X', X) \<in> \<langle>Id\<rangle>set_rel"
  shows "(?f, assert_test X) \<in> \<langle>\<langle>Id\<rangle>set_rel\<rangle>nres_rel"
  unfolding assert_test_def
  by (autoref)

end