Theory Derive_Examples

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
section Examples

theory Derive_Examples
imports 
  Derive
  "Comparator_Generator/Compare_Order_Instances"
  "Equality_Generator/Equality_Instances"
  HOL.Rat
begin

subsection "Rational Numbers"

text ‹The rational numbers are not a datatype, so it will not be possible to derive 
  corresponding instances of comparators, hashcodes, etc. via the generators. But we can and should
  still register the existing instances, so that later datatypes are supported 
  which use rational numbers.› 

text ‹Use the linear order on rationals to define the @{class compare_order}-instance.›
derive (linorder) compare_order rat

text ‹Use @{term "(=) :: rat => rat => bool"} as equality function.›
derive (eq) equality rat

text ‹First manually define a hashcode function.›

instantiation rat :: hashable
begin
definition "def_hashmap_size = (λ_ :: rat itself. 10)"
definition "hashcode (r :: rat) = hashcode (quotient_of r)"
instance
  by (intro_classes)(simp_all add: def_hashmap_size_rat_def)
end

text ‹And then register it at the generator.›

derive (hashcode) hash_code rat

subsection "A Datatype Without Nested Recursion"

datatype 'a bintree = BEmpty | BNode "'a bintree" 'a "'a bintree"

derive compare_order bintree
derive countable bintree
derive equality bintree
derive hashable bintree

subsection "Using Other datatypes"

datatype nat_list_list = NNil | CCons "nat list × rat option" nat_list_list

derive compare_order nat_list_list
derive countable nat_list_list
derive (eq) equality nat_list_list
derive hashable nat_list_list

subsection "Mutual Recursion"

datatype
  'a mtree = MEmpty | MNode 'a "'a mtree_list" and
  'a mtree_list = MNil | MCons "'a mtree" "'a mtree_list"

derive compare_order mtree mtree_list
derive countable mtree mtree_list
derive hashable mtree mtree_list

text ‹For ‹derive (equality|comparator|hash_code) mutual_recursive_type› 
  there is the speciality that only one of the mutual recursive types has to be mentioned in
  order to register all of them. So one of @{type mtree} and @{type mtree_list} suffices.›

derive equality mtree 
 
subsection "Nested recursion"

datatype 'a tree = Empty | Node 'a "'a tree list"
datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"

derive compare_order tree ttree
derive countable tree ttree
derive equality tree ttree
derive hashable tree ttree

subsection ‹Examples from \isafor›

datatype ('f,'v) "term" = Var 'v | Fun 'f "('f,'v) term list"
datatype ('f, 'l) lab =
  Lab "('f, 'l) lab" 'l
| FunLab "('f, 'l) lab" "('f, 'l) lab list"
| UnLab 'f
| Sharp "('f, 'l) lab"

derive compare_order "term" lab
derive countable "term" lab
derive equality "term" lab
derive hashable "term" lab

subsection "A Complex Datatype"
text ‹
The following datatype has nested and mutual recursion, and
uses other datatypes.
›

datatype ('a, 'b) complex = 
  C1 nat "'a ttree × rat + ('a,'b) complex list" |
  C2 "('a, 'b) complex list tree tree" 'b "('a, 'b) complex" "('a, 'b) complex2 ttree list"
and ('a, 'b) complex2 = D1 "('a, 'b) complex ttree"

text ‹On this last example type we illustrate the difference of the various comparator- and order-generators.

  For @{type complex} we create an instance of @{class compare_order} which also defines
  a linear order. Note however that the instance will 
  be @{type complex} :: (@{class compare}, @{class compare}) @{class compare_order}, i.e., the 
  argument types have to be in class @{class compare}. 

  For @{type complex2} we only derive @{class compare} which is not a subclass of @{class linorder}.
  The instance will be @{type complex2} :: (@{class compare}, @{class compare}) @{class compare}, i.e., 
  again the argument types have to be in class @{class compare}.

  To avoid the dependence on @{class compare}, we can also instruct ‹derive› to be based on 
  @{class linorder}. Here, the command ‹derive linorder complex2› will create the instance
  @{type complex2} :: (@{class linorder}, @{class linorder}) @{class linorder}, i.e., 
  here the argument types have to be in class @{class linorder}.
  ›
derive compare_order complex 
derive compare complex2
derive linorder complex2
derive countable complex complex2
derive equality complex
derive hashable complex complex2

end