Re: [isabelle] transfer / lifting / quotient - questions



Hi Salomon,

value "Abs (leaf 0) = Abs (leaf 1)"

(*
   Question 3:

   The command fails with:

     Wellsortedness error:
     Type same_size_tree not of sort equal
     No type arity same_size_tree :: equal

   Is there something I can do about this?
   Will this cause issues, if I want to generate code?
*)
Equality is executable only on types with an instance of the equal type class (similar to Haskell's Eq type class). The command datatype automatically makes new types instances of equal. Since same_size_tree has been defined by other means (the quotient package), you have to do the instantiation manually. Something along the following lines should work (not tested!).

instantiation same_size_tree :: equal begin
lift_definition equal_same_size_tree :: "tree => tree => bool"
  is "%t1 t2. size t1 = size t2"
  <proof>

instance by intro_classes(transfer, simp add: tree_equivp_def)
end

Andreas

PS: I leave the Nitpick question to nitpick experts.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.