theory Scratch1
  imports Collections.Refine_Dflt
begin

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

lemma list_set_rel_imp_finite[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

find_theorems op_nres_ASSUME_bnd
thm Refine_Basic.autoref_ASSUME   (* <-- this rule is already registered *)

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
  apply (autoref (keep_goal))
  oops (* <-- The translation phase already ran too far, and stripped of the argument m
    from the op_nres_ASSUME_bnd function, although there is no rule that would refine 
    the function without a parameter.
    
    This is a known inconvenience when debugging autoref, but I did not yet fix it (though it's fixed in sepref!)
    
    The only way to see what is happening behind the scenes is to single-step the translation phase:
   *)
  
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
  apply (autoref (trace,keep_goal) phases: id_op rel_inf fix_rel)
  apply autoref_trans_step (* <-- repeat as often as necessary, using 'back' to select the right rule out of many possibilities *)
  apply autoref_side (* <-- Try to solve this side condition *)
  apply clarsimp (* <-- We need to show finite X without any preconditions, which is not possible ...  *)
  oops

(* Unless we add this fact explicitly to the simpset *)    
schematic_goal assume_test_refine':
  assumes R[autoref_rules]: "(X', X) \<in> \<langle>Id\<rangle>list_set_rel"
  notes [simp] = list_set_rel_imp_finite[OF R]
  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]]
  by autoref
  

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