Theory BinoPrioImpl

section ‹\isaheader{Implementation of Priority Queues by Binomial Heap}›

theory BinoPrioImpl
imports 
  "Binomial-Heaps.BinomialHeap" 
  "../spec/PrioSpec"
  "../tools/Record_Intf"
  "../tools/Locale_Code"
begin

(*@impl Prio
  @type ('a,'p::linorder) bino
  @abbrv bino
  Binomial heaps.
*)

type_synonym ('a,'b) bino = "('a,'b) BinomialHeap"

subsection "Definitions"
definition bino_α where "bino_α q ≡ BinomialHeap.to_mset q"
definition bino_insert where "bino_insert ≡ BinomialHeap.insert"
abbreviation (input) bino_invar :: "('a,'b) BinomialHeap ⇒ bool"
  where "bino_invar ≡ λ_. True"
definition bino_find where "bino_find ≡ BinomialHeap.findMin"
definition bino_delete where "bino_delete ≡ BinomialHeap.deleteMin"
definition bino_meld where "bino_meld ≡ BinomialHeap.meld"
definition bino_empty where "bino_empty ≡ λ_::unit. BinomialHeap.empty"
definition bino_isEmpty where "bino_isEmpty = BinomialHeap.isEmpty"

definition [icf_rec_def]: "bino_ops == ⦇
  prio_op_α = bino_α,
  prio_op_invar = bino_invar,
  prio_op_empty = bino_empty,
  prio_op_isEmpty = bino_isEmpty,
  prio_op_insert = bino_insert,
  prio_op_find = bino_find,
  prio_op_delete = bino_delete,
  prio_op_meld = bino_meld
⦈"

lemmas bino_defs =
  bino_α_def
  bino_insert_def
  bino_find_def
  bino_delete_def
  bino_meld_def
  bino_empty_def
  bino_isEmpty_def

subsection "Correctness"

theorem bino_empty_impl: "prio_empty bino_α bino_invar bino_empty"
  by (unfold_locales, auto simp add: bino_defs)

theorem bino_isEmpty_impl: "prio_isEmpty bino_α bino_invar bino_isEmpty"
  by unfold_locales 
     (simp add: bino_defs BinomialHeap.isEmpty_correct BinomialHeap.empty_correct)

theorem bino_find_impl: "prio_find bino_α bino_invar bino_find"
  apply unfold_locales
  apply (simp add: bino_defs BinomialHeap.empty_correct BinomialHeap.findMin_correct)
  done

lemma bino_insert_impl: "prio_insert bino_α bino_invar bino_insert"
  apply(unfold_locales)
  apply(unfold bino_defs) 
  apply (simp_all add: BinomialHeap.insert_correct)
  done

lemma bino_meld_impl: "prio_meld bino_α bino_invar bino_meld"
  apply(unfold_locales)
  apply(unfold bino_defs)
  apply(simp_all add: BinomialHeap.meld_correct)
  done
      
lemma bino_delete_impl: 
  "prio_delete bino_α bino_invar bino_find bino_delete"
  apply intro_locales
  apply (rule bino_find_impl)
  apply(unfold_locales)
  apply(simp_all add: bino_defs BinomialHeap.empty_correct BinomialHeap.deleteMin_correct)
done 

setup Locale_Code.open_block
interpretation bino: StdPrio bino_ops
  apply (rule StdPrio.intro)
  apply (simp_all add: icf_rec_unf)
  apply (rule 
    bino_empty_impl
    bino_isEmpty_impl
    bino_find_impl
    bino_insert_impl
    bino_meld_impl
    bino_delete_impl
  )+
  done
interpretation bino: StdPrio_no_invar bino_ops
  apply unfold_locales
  apply (simp add: icf_rec_unf)
  done
setup Locale_Code.close_block

setup ‹ICF_Tools.revert_abbrevs "bino"›

definition test_codegen where "test_codegen = (
  bino.empty,
  bino.isEmpty,
  bino.find,
  bino.insert,
  bino.meld,
  bino.delete
)"

export_code test_codegen checking SML

end