Theory ICF_Only_Test

theory ICF_Only_Test
imports 
  Collections.Refine_Dflt_Only_ICF 
begin

declare [[autoref_trace_failed_id]]

subsection "Array Hash Map Tests"

context begin interpretation autoref_syn .

schematic_goal
  "(?f::?'c, λm. (m)(1::nat↦2::nat)) ∈ ?R"
  apply (autoref (keep_goal))
  done

(* Optimizations *)

subsection "List Map Tests"

definition foo::"(nat⇀nat) nres" where "foo ≡
  do {
    let X = Map.empty;
    ASSERT (1 ∉ dom X);
    RETURN (X(1 ↦ 2))
  }"

schematic_goal list_map_update_dj_test:
  "(?f::?'c, foo ::: ⟨⟨Id,Id⟩lm.rel⟩nres_rel) ∈ ?R"
  unfolding foo_def 
  apply autoref_monadic
  done

schematic_goal 
  "(?f::?'c, [1::nat ↦ 2::nat, 3↦4] ::: ⟨nat_rel,nat_rel⟩lm.rel) ∈ ?R"
  apply autoref
  done

schematic_goal list_map_test:
  "(?f::?'c, RETURN (([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⟨nat_rel,nat_rel⟩lm.rel) |`(-{1}))) ∈ ?R"
apply (autoref_monadic)
done
concrete_definition list_map_test uses list_map_test
value list_map_test

schematic_goal
  "(?f::?'c, RETURN (card (dom ([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⟨nat_rel,nat_rel⟩lm.rel)))) ∈ ?R"
apply (autoref_monadic)
done

end
end