Email Gateway (Jun 13 2022 at 15:03): Email Gateway (Jun 13 2022 at 15:03):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I recently observed a problem with a lift_definition in combination with (code_dt):
Here is a minimal example:
theory Foo
imports Main
begin
typedef bounded_int = "{x :: int . 0 < x & x < 10}" by (intro exI[of _ 1], auto)
setup_lifting type_definition_bounded_int
lift_definition (code_dt) bounded_int_of_int :: "int ⇒ bounded_int option"
is "% x. if 0 < x & x < 10 then Some x else None"
by auto
(*
Tactic failed
The error(s) above occurred for the goal statement⌂:
rel_fun (eq_onp (pred_option (λx. 0 < x ∧ x < 10))) (eq_onp (λx. 0 < x ∧ x < 10)) (case_option (Rep_bounded_int undefined) (λx2. x2))
(case_option (Rep_bounded_int undefined) (λx2. x2))
*)
Strangely, if I just use a one-sided bound, e.g., by dropping the “x < 10” requirement, or if I encapsulate the conjunction in a separate
definition “bounded x = (0 < x & x < 10) … typedef bounded_int = {x :: int. bounded x}” then everything works out nicely.
Best,
René
Last updated: Jul 15 2022 at 23:21 UTC