[7860bc]: thys / Collections / FTPrioImpl.thy Maximize Restore History

Download this file

FTPrioImpl.thy    115 lines (102 with data), 4.0 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
header {*\isaheader{Implementation of Priority Queues by Finger Trees}*}
theory FTPrioImpl
imports FTAnnotatedListImpl AnnotatedListGAPrioImpl
begin
text {* Instantiation of adapter *}
subsection "Definitions"
definition alprioi_\<alpha> where
"alprioi_\<alpha> = alprio_\<alpha> ft_\<alpha>"
definition alprioi_invar where
"alprioi_invar = alprio_invar ft_\<alpha> ft_invar"
definition alprioi_empty :: "(unit,('a,'b::linorder) Prio) FingerTree" where
"alprioi_empty = alprio_empty ft_empty"
definition alprioi_isEmpty where
"alprioi_isEmpty \<equiv> alprio_isEmpty ft_isEmpty"
definition alprioi_insert :: "_ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> (unit,('a,'b::linorder) Prio) FingerTree" where
"alprioi_insert = alprio_insert ft_consl"
definition alprioi_find where
"alprioi_find = alprio_find ft_annot"
definition alprioi_delete where
"alprioi_delete = alprio_delete ft_splits ft_annot ft_app"
definition alprioi_meld where
"alprioi_meld = alprio_meld ft_app"
definition "alprioi_ops == \<lparr>
prio_op_\<alpha> = alprioi_\<alpha>,
prio_op_invar = alprioi_invar,
prio_op_empty = alprioi_empty,
prio_op_isEmpty = alprioi_isEmpty,
prio_op_insert = alprioi_insert,
prio_op_find = alprioi_find,
prio_op_delete = alprioi_delete,
prio_op_meld = alprioi_meld
\<rparr>"
subsection "Correctness"
lemmas alprioi_defs =
alprioi_invar_def
alprioi_\<alpha>_def
alprioi_empty_def
alprioi_isEmpty_def
alprioi_insert_def
alprioi_find_def
alprioi_delete_def
alprioi_meld_def
lemmas alprioi_empty_impl = alprio_empty_correct[OF ft_empty_impl, folded alprioi_defs]
lemmas alprioi_isEmpty_impl = alprio_isEmpty_correct[OF ft_isEmpty_impl, folded alprioi_defs]
lemmas alprioi_insert_impl = alprio_insert_correct[OF ft_consl_impl, folded alprioi_defs]
lemmas alprioi_find_impl = alprio_find_correct[OF ft_annot_impl, folded alprioi_defs]
lemmas alprioi_delete_impl = alprio_delete_correct[OF ft_annot_impl ft_splits_impl ft_app_impl, folded alprioi_defs]
lemmas alprioi_meld_impl = alprio_meld_correct[OF ft_app_impl, folded alprioi_defs]
lemmas alprioi_impl =
alprioi_empty_impl
alprioi_isEmpty_impl
alprioi_insert_impl
alprioi_find_impl
alprioi_delete_impl
alprioi_meld_impl
interpretation alprioi: prio_empty alprioi_\<alpha> alprioi_invar alprioi_empty
by (rule alprioi_impl)
interpretation alprioi: prio_isEmpty alprioi_\<alpha> alprioi_invar alprioi_isEmpty
by (rule alprioi_impl)
interpretation alprioi: prio_insert alprioi_\<alpha> alprioi_invar alprioi_insert
by (rule alprioi_impl)
interpretation alprioi: prio_find alprioi_\<alpha> alprioi_invar alprioi_find
by (rule alprioi_impl)
interpretation alprioi: prio_delete alprioi_\<alpha> alprioi_invar alprioi_find alprioi_delete
by (rule alprioi_impl)
interpretation alprioi: prio_meld alprioi_\<alpha> alprioi_invar alprioi_meld
by (rule alprioi_impl)
lemmas alprioi_correct =
alprioi.empty_correct
alprioi.isEmpty_correct
alprioi.insert_correct
alprioi.meld_correct
alprioi.find_correct
alprioi.delete_correct
subsubsection "Record Based Interface"
interpretation alprioir: StdPrio alprioi_ops
apply (unfold alprioi_ops_def)
apply intro_locales
apply (simp_all add: alprioi_impl alprioi_delete_impl[unfolded prio_delete_def])
done
subsection "Code Generation"
-- "Unfold record definition for code generation"
lemma alprioi_ops_unfold [code_unfold]:
"prio_op_\<alpha> alprioi_ops = alprioi_\<alpha>"
"prio_op_invar alprioi_ops = alprioi_invar"
"prio_op_empty alprioi_ops = alprioi_empty"
"prio_op_isEmpty alprioi_ops = alprioi_isEmpty"
"prio_op_insert alprioi_ops = alprioi_insert"
"prio_op_find alprioi_ops = alprioi_find"
"prio_op_delete alprioi_ops = alprioi_delete"
"prio_op_meld alprioi_ops = alprioi_meld"
by (auto simp add: alprioi_ops_def)
export_code
alprioi_empty
alprioi_isEmpty
alprioi_insert
alprioi_find
alprioi_delete
alprioi_meld
in SML
module_name ALPRIOI
end