Theory Test_Lazy_Case

subsection ‹Interaction with ‹Lazy_Case››

theory Test_Lazy_Case
imports
  Dict_Construction
  Lazy_Case.Lazy_Case
  Show.Show_Instances
begin

datatype 'a tree = Node | Fork 'a "'a tree list"

lemma map_tree[code]:
  "map_tree f t = (case t of Node ⇒ Node | Fork x ts ⇒ Fork (f x) (map (map_tree f) ts))"
by (induction t) auto

experiment begin

(* FIXME proper qualified path *)
text ‹
  Dictionary construction of @{const map_tree} requires the [@{attribute fundef_cong}] rule of
  @{const Test_Lazy_Case.tree.case_lazy}.
›

declassify valid: map_tree
thm valid

lemma "Test__Lazy__Case_tree_map__tree = map_tree" by (fact valid)

end


definition i :: "(unit × (bool list × string × nat option) list) option ⇒ string" where
"i = show"

experiment begin

text ‹This currently requires @{theory Lazy_Case.Lazy_Case} because of @{const Euclidean_Rings.divmod_nat}.›

(* FIXME get rid of Lazy_Case dependency *)
declassify valid: i
thm valid

lemma "Test__Lazy__Case_i = i" by (fact valid)

end

end