Theory Test_Embed_Data2

theory Test_Embed_Data2
imports
  Lazy_Case.Lazy_Case
  "../Preproc/Embed"
  "../Preproc/Eval_Instances"
  "Pairing_Heap.Pairing_Heap_Tree"
begin

declare List.Ball_set[code_unfold]

lemma [code_unfold]: "(∀x ∈ set_tree l. P x) ⟷ list_all P (inorder l)"
  by (induction l) auto

declassify valid:
  Pairing_Heap_Tree.link
  Pairing_Heap_Tree.pass1
  Pairing_Heap_Tree.pass2
  Pairing_Heap_Tree.is_root
  Pairing_Heap_Tree.pheap

thm valid

derive evaluate
  Tree.tree
  Orderings_ord__dict
  Orderings_preorder__dict
  Orderings_order__dict
  Orderings_linorder__dict
  HOL_equal__dict

experiment begin

embed (eval) test1 is
  Pairing__Heap__Tree_link
  Pairing__Heap__Tree_pass1
  Pairing__Heap__Tree_pass2
  Pairing__Heap__Tree_pheap
  .

end

end