Theory ICF_Test

theory ICF_Test
imports 
  Collections.Refine_Dflt_ICF 
begin

declare [[autoref_trace_failed_id]]

subsection "Array Hash Map Tests"


schematic_goal
  "(?f::?'c, [{1::nat} |-> {2::nat}]) ∈ ?R"
  by (autoref (keep_goal))

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


schematic_goal
  "(?f::?'c, λm. (m:::⇩r⟨Id,Id⟩dflt_ahm_rel)(1::nat↦2::nat)) ∈ ?R"
  apply (autoref (keep_goal))
  done

schematic_goal
  "(?f::?'c, Map.empty:::⇩r⟨Id,Id⟩dflt_ahm_rel) ∈ ?R"
apply (autoref)
done

schematic_goal
  fixes mi m
  (* TODO: Obviously, we cannot override the tyREL-rule for 
    "nat⇀nat" with this: *)
  assumes [autoref_rules]: "(mi,m)∈⟨nat_rel,nat_rel⟩dflt_ahm_rel"
  shows "(?f::?'c, 
    RETURN (card (dom (m:::⇩r⟨nat_rel,nat_rel⟩dflt_ahm_rel)))) ∈ ?R"
  apply (autoref_monadic)
  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 :::⇩r ⟨⟨Id,Id⟩list_map_rel⟩nres_rel) ∈ ?R"
  unfolding foo_def 
  apply autoref_monadic
  done

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

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

(* Why does this work:*)
schematic_goal
  "(?f::?'c, RETURN (card (dom ([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⇩r⟨nat_rel,nat_rel⟩list_map_rel)))) ∈ ?R"
apply (autoref_monadic)
done

(* But this doesn't? This is not specific to list_map;
   it doesn't work with dflt_rbt_rel either.*)
(*schematic_lemma
  "(?f::?'c, RETURN (dom ([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⇩r⟨nat_rel,nat_rel⟩list_map_rel))) ∈ ?R"
apply (autoref_monadic)
done*)


subsection "Array-Map Tests"

term "{1,2::nat} ∪ {3,4}"

schematic_goal array_set_test_code:
  "(?f::?'c, RETURN (({1,2::nat} ∪ {3,4} 
       :::⇩r ⟨nat_rel⟩iam_set_rel )))∈?R" 
by (autoref_monadic (trace))

concrete_definition array_set_test uses array_set_test_code
print_theorems
value [nbe] array_set_test

schematic_goal
  "(?f::?'c, RETURN (({1} :::⇩r ⟨nat_rel⟩dflt_rs_rel) = {}))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (card {1,2,3::nat}))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (∀x∈{1,2,3::nat}. x<4))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (∃x∈{1,2,3::nat}. x<4))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (({1} :::⇩r ⟨nat_rel⟩iam_set_rel) = {}))∈?R" 
  apply (autoref_monadic (trace))
  done

schematic_goal
  assumes [autoref_rules]: "(f,f')∈nat_rel→Rb"
  shows "(?f::?'c,f' 3)∈?R"
  by (autoref)


schematic_goal "(?f::?'c,
  RETURN (({1,2::nat} × {3,4::nat}) :::⇩r ⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN ({1,2::nat} ∩ ({3,4::nat}) :::⇩r ⟨Id⟩list_set_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN ({1,2::nat} ∩ ({3,4::nat}) :::⇩r ⟨Id⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN (card (dom ([ 1::nat ↦ True, 2↦False ] :::⇩r ⟨Id,Id⟩dflt_rm_rel )))
)∈?R"
  by autoref_monadic


schematic_goal "(?f::?'c,
  {1,2::'a::numeral} × {3,4::'a}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::'a::{numeral,hashable}} × ({3,4::'a} :::⇩r ⟨Id⟩dflt_ahs_rel)
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::nat} × {3,4::nat}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::nat} ∩ {3,4::nat}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  RETURN (({1,2::nat} × {3,4::nat}) :::⇩r ⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

(* TODO: ty_REL hint is ignored. Reason: Seems to not properly work with GAs! *)
schematic_goal 
  notes [autoref_tyrel] = ty_REL[where 'a = "(nat×nat) set" 
    and R="⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel"] 
  shows "(?f::?'c,
    RETURN (({1,2::nat} × {3,4::nat}))
  )∈?R"
  by autoref_monadic

(* TODO: Iterator optimization does not capture 
    foldli ((map fst ∘ rbt_to_list) x)
pattern!
*)

text ‹We have an optimized version for add on red-black trees›
schematic_goal "(?f::?'c,
  [ 1::nat ↦ True, 2::nat ↦ False ] ++ [ 3::nat ↦ True, 4::nat ↦ False ]
)∈?R"
  by (autoref (keep_goal))

text ‹The optimized version is also transfered through the map2set converter›
schematic_goal "(?f::?'c,
  {1,2::nat} ∪ {3,4}
)∈?R"
  by (autoref (keep_goal))

text ‹For list-sets, the generic version is used›
schematic_goal "(?f::?'c,
  {1,2::nat} ∪ {3,4} :::⇩r ⟨Id⟩list_set_rel
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  ({{1::nat}:::⇩r⟨Id⟩ map2set_rel dflt_rm_rel} ) 
  ∪ ({{2,3,4,5,5,6,7,8,98,9,0}}) 
)∈?R"
  by (autoref (keep_goal))

text ‹The next two lemmas demonstrate optimization: The insert-operation
  is translated by @{term "(#)"}›
schematic_goal "(?f::?'c, {1,2,3,4::nat}:::⇩r⟨Id⟩list_set_rel
  )∈?R"
  by (autoref (keep_goal))

schematic_goal 
  "(?f::?'c, {{1},{2},{3},{4::nat}}:::⇩r⟨?R'::(?'d×_) set⟩list_set_rel
  )∈?R"
  by (autoref (keep_goal))


schematic_goal "(?f::?'c,
  SPEC (λx. x∈({1,2,3::nat}:::⇩r⟨Id⟩dflt_rs_rel)) 
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  λs::nat set. {s} ∪ {{1,2,3}} = {{1}}
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  ∀(k,v)∈map_to_set [1::nat↦2::nat]. k>v
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c, do {
  let s = ({1,2,3::nat}:::⇩r⟨Id⟩dflt_rs_rel);
  FOREACH s (λn s. RETURN (n+s)) 0
}
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c, do {
  let s = ({{1,2,3::nat}, {}, {1,2}});
  FOREACH s (λn s. RETURN (n ∪ s)) {}
}
)∈?R"
  by (autoref_monadic)

schematic_goal "(?f::?'c,
  SPEC (λx. x∈({1,2,3::nat})) 
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  λs::nat set. {s} ∪ {{1,2,3}} = {{1}}
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  ∀(k,v)∈map_to_set [1::nat↦2::nat]. k>v
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  [ 1::nat ↦ [ 2::nat ↦ 3::nat, 1::nat ↦ 3::nat ] ]
)∈?R"
  apply (autoref (keep_goal))
  done



text ‹Indirect Annotation›
consts 
  rel_set1 :: rel_name
  rel_set2 :: rel_name

definition 
  "algo ≡ ( {1,2,3::nat}::#⇩rrel_set1, {1,2,3::nat}::#⇩rrel_set2 )"

schematic_goal 
  notes [autoref_rel_indirect] = 
    REL_INDIRECT[of rel_set1 "⟨Rk⟩list_set_rel" for Rk]
    REL_INDIRECT[of rel_set2 "⟨Rk⟩dflt_rs_rel" for Rk]
  shows "(?f::?'c,algo) ∈ ?R"
  unfolding algo_def
  by (autoref)

schematic_goal 
  notes [autoref_rel_indirect] = 
    REL_INDIRECT[of rel_set1 "⟨Rk⟩dflt_rs_rel" for Rk]
    REL_INDIRECT[of rel_set2 "⟨Rk⟩dflt_rs_rel" for Rk]
  shows "(?f::?'c,algo) ∈ ?R"
  unfolding algo_def
  by (autoref)

end