Theory Test_Embed_Tree

theory Test_Embed_Tree
imports
  Lazy_Case.Lazy_Case
  "../Preproc/Embed"
  "../Preproc/Eval_Instances"
  "HOL-Library.Tree"
begin

derive evaluate tree

text ‹Integers are not supported out of the box, so we have to rewrite some code equations.›

definition nat_diff :: ‹nat ⇒ nat ⇒ nat›
  where nat_diff_abs_int: ‹nat_diff m n = nat ¦int m - int n¦›

lemma nat_diff_simps [simp, code]:
  ‹nat_diff 0 n = n›
  ‹nat_diff m 0 = m›
  ‹nat_diff (Suc m) (Suc n) = nat_diff m n›
  by (simp_all add: nat_diff_abs_int)

lemma [code]:
  ‹wbalanced Leaf ⟷ True›
  ‹wbalanced (Node l x r) ⟷ nat_diff (size l) (size r) ≤ 1 ∧ wbalanced l ∧ wbalanced r›
  by (auto simp add: nat_diff_abs_int)

text ‹Sets are also unsupported, so we have to rewrite @{const set_tree} to use @{const inorder}.›

lemma [code_unfold]:
  ‹(∀x ∈ set_tree l. P x) ⟷ list_all P (inorder l)›
  by (simp add: list_all_iff)

lemma [code]:
  ‹heap Leaf ⟷ True›
  ‹heap (Node l m r) ⟷ heap l ∧ heap r ∧ (∀x ∈ set_tree l. m ≤ x) ∧ (∀x ∈ set_tree r. m ≤ x)›
  by auto

text ‹@{term "(-)"} on @{typ nat} is not pattern compatible›

declassify valid: wbalanced ipl preorder inorder postorder bst_wrt heap
thm valid

experiment begin

code_thms Tree_wbalanced (* FIXME bogus error message when using the non-dict-eliminated constant *)
embed (eval) test1 is Tree_wbalanced .

end

experiment begin

code_thms Tree_ipl Tree_preorder Tree_inorder Tree_postorder
embed (eval) test2 is Tree_ipl Tree_preorder Tree_inorder Tree_postorder .

end

(* FIXME auto-derive these things? *)
derive evaluate
  Orderings_ord__dict
  Orderings_preorder__dict
  Orderings_order__dict
  Orderings_linorder__dict

experiment begin

code_thms Tree_bst__wrt Tree_linorder__class_heap
embed (eval) test3 is Tree_bst__wrt Tree_linorder__class_heap .

end

end