Theory Test_Utils

theory Test_Utils
imports
  Code_Utils
  Huffman.Huffman
  "HOL-Data_Structures.Leftist_Heap"
  "Pairing_Heap.Pairing_Heap_Tree"
  "Root_Balanced_Tree.Root_Balanced_Tree"
  "Dict_Construction.Dict_Construction"
begin

section ‹Dynamic unfolding›

definition one :: nat where
"one = 1"

fun plus_one :: "nat ⇒ nat" where
"plus_one (Suc x) = one + plus_one x" |
"plus_one _ = one"

ML‹
fun has_one ctxt =
  let
    val const = @{const_name plus_one}
    val {eqngr, ...} = Code_Preproc.obtain true {ctxt = ctxt, consts = [const], terms = []}
    val all_consts = Graph.all_succs eqngr [const]
  in
    member op = all_consts @{const_name one}
  end
›

ML‹@{assert} (has_one @{context})›

context
  notes [[dynamic_unfold]]
begin

ML‹@{assert} (not (has_one @{context}))›

end

section ‹Pattern compatibility›

subsection ‹Cannot deal with diagonal function›

fun diagonal :: "_ ⇒ _ ⇒ _ ⇒ nat" where
"diagonal x True False = 1" |
"diagonal False y True = 2" |
"diagonal True False z = 3"

code_thms diagonal

code_thms Leftist_Heap.ltree

context
  notes [[pattern_compatibility]]
begin

ML‹
  {ctxt = @{context}, consts = [@{const_name diagonal}], terms = []}
  |> can (Code_Preproc.obtain true)
  |> not
  |> @{assert}
›

export_code huffman checking SML Scala

export_code
  Leftist_Heap.ltree
  Leftist_Heap.node
  Leftist_Heap.merge
  Leftist_Heap.insert
  Leftist_Heap.del_min
  checking SML Scala

export_code
  Pairing_Heap_Tree.link
  Pairing_Heap_Tree.pass1
  Pairing_Heap_Tree.pass2
  Pairing_Heap_Tree.is_root
  Pairing_Heap_Tree.pheap
  checking SML Scala

export_code
  Root_Balanced_Tree.size_tree_tm
  Root_Balanced_Tree.inorder2_tm
  Root_Balanced_Tree.split_min_tm
  checking SML Scala

end

(* FIXME RBT *)

(* FIXME move to Dict_Construction *)

ML‹open Dict_Construction_Util›

lemma
  assumes "P" "Q" "R"
  shows "P ∧ Q ∧ R"
apply (tactic ‹
  (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH
    [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}, resolve_tac @{context} @{thms assms(3)}]) 1
›)
done

lemma
  assumes "P" "Q" "R"
  shows "P ∧ Q ∧ R"
apply (tactic ‹
  (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH_FW
    [resolve_tac @{context} @{thms assms(1)}, K all_tac, resolve_tac @{context} @{thms assms(3)}]) 1
›)
apply (rule assms(2))
done

lemma
  assumes "P" "Q"
  shows "(P ∧ Q)" "(P ∧ Q)"
apply (tactic ‹Goal.recover_conjunction_tac THEN
  (Goal.conjunction_tac THEN_ALL_NEW
    (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH
    [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}])) 1
›)
done

lemma
  assumes "Q" "P"
  shows "P ∧ Q"
apply (tactic ‹
  (resolve_tac @{context} @{thms conjI conjI[rotated]} CONTINUE_WITH
    [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}]) 1
›)
done

end