Email Gateway (Jan 26 2025 at 09:26): Email Gateway (Jan 26 2025 at 09:26):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi all,
I have a couple of related questions concerning the current state of the
datatype package.
Find my motivation in the attached theory: I want to »register« a type a
posteriori as a datatype.
a) Construct the type
b) Define the appropriate constructors
c) Prove them as free constructors
d) Prove the corresponding induction rule
But then? Primrec still fails, obviously due to the lack of a recursion
combinator.
How to proceed from there?
(When examining how it is done for the existing elementary types in HOL,
I found that the »old« datatype package with the traditional
»rep_datatype« is still in place – which leads to the somehow related
question if there are further migrations plans there.)
For the presented example an appropriate solution is to introduce the
type as a datatype and establish lifting a posteriori, but there might
be other instances where this is the less comfortable way.
Cheers,
Florian
Numeral.thy
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Feb 01 2025 at 08:24):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi Florian,
There is indeed no explicit rep_datatype command anymore, but there is an interface to register a recursor, which makes primrec work. I attach the code below. The ML bits are copied from the equivalent setup for natural numbers (which is the reason why this interface exists in the first place).
To also make fun work with num, it would be good to also include the corresponding size class instance.
Best wishes,
Dmitriy
fun rec_num_raw :: "'a ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ nat ⇒ 'a" where
"rec_num_raw one bit0 bit1 (Suc 0) = one"
| "rec_num_raw one bit0 bit1 (Suc n) = (if even n then bit1 (n div 2) (rec_num_raw one bit0 bit1 (n div 2))
else bit0 ((Suc n) div 2) (rec_num_raw one bit0 bit1 ((Suc n) div 2)))"
lift_definition rec_num :: "'a ⇒ (num ⇒ 'a ⇒ 'a) ⇒ (num ⇒ 'a ⇒ 'a) ⇒ num ⇒ 'a" is
rec_num_raw
subgoal for one bit0 bit0' bit1 bit1' n
by (induct one bit0 bit1 n rule: rec_num_raw.induct) auto
done
lemma rec_num:
"rec_num one bit0 bit1 One = one"
"rec_num one bit0 bit1 (Bit0 x) = bit0 x (rec_num one bit0 bit1 x)"
"rec_num one bit0 bit1 (Bit1 x) = bit1 x (rec_num one bit0 bit1 x)"
by (transfer; auto simp: gr0_conv_Suc)+
ML ‹
val num_basic_lfp_sugar =
let
val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global \<^theory> \<^type_name>‹num›);
val recx = Logic.varify_types_global \<^term>‹rec_num›;
val C = body_type (fastype_of recx);
in
{T = @{typ num}, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[@{typ num}, C]], [[@{typ num}, C]]],
ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms rec_num}}
end;
›
ML ‹nat_basic_lfp_sugar›
setup ‹
let
fun basic_lfp_sugars_of _ [\<^typ>‹num›] _ _ ctxt =
([], [0], [num_basic_lfp_sugar], [], [], [], TrueI (dummy), [], false, ctxt)
| basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
in
BNF_LFP_Rec_Sugar.register_lfp_rec_extension
{nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
end
›
On 26 Jan 2025, at 10.26, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
Hi all,
I have a couple of related questions concerning the current state of the datatype package.
Find my motivation in the attached theory: I want to »register« a type a posteriori as a datatype.
a) Construct the type
b) Define the appropriate constructors
c) Prove them as free constructors
d) Prove the corresponding induction rule
But then? Primrec still fails, obviously due to the lack of a recursion combinator.
How to proceed from there?
(When examining how it is done for the existing elementary types in HOL, I found that the »old« datatype package with the traditional »rep_datatype« is still in place – which leads to the somehow related question if there are further migrations plans there.)
For the presented example an appropriate solution is to introduce the type as a datatype and establish lifting a posteriori, but there might be other instances where this is the less comfortable way.
Cheers,
Florian
<Numeral.thy><OpenPGP_0xA707172232CFA4E9.asc>
Email Gateway (Feb 01 2025 at 08:25):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Thanks a lot.
Florian
Am 01.02.25 um 09:23 schrieb Dmitriy Traytel (via cl-isabelle-users
Mailing List):
Hi Florian,
There is indeed no explicit rep_datatype command anymore, but there is an interface to register a recursor, which makes primrec work. I attach the code below. The ML bits are copied from the equivalent setup for natural numbers (which is the reason why this interface exists in the first place).
To also make fun work with num, it would be good to also include the corresponding size class instance.
Best wishes,
Dmitriyfun rec_num_raw :: "'a ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ (nat ⇒ 'a ⇒ 'a) ⇒ nat ⇒ 'a" where
"rec_num_raw one bit0 bit1 (Suc 0) = one"
| "rec_num_raw one bit0 bit1 (Suc n) = (if even n then bit1 (n div 2) (rec_num_raw one bit0 bit1 (n div 2))
else bit0 ((Suc n) div 2) (rec_num_raw one bit0 bit1 ((Suc n) div 2)))"lift_definition rec_num :: "'a ⇒ (num ⇒ 'a ⇒ 'a) ⇒ (num ⇒ 'a ⇒ 'a) ⇒ num ⇒ 'a" is
rec_num_raw
subgoal for one bit0 bit0' bit1 bit1' n
by (induct one bit0 bit1 n rule: rec_num_raw.induct) auto
donelemma rec_num:
"rec_num one bit0 bit1 One = one"
"rec_num one bit0 bit1 (Bit0 x) = bit0 x (rec_num one bit0 bit1 x)"
"rec_num one bit0 bit1 (Bit1 x) = bit1 x (rec_num one bit0 bit1 x)"
by (transfer; auto simp: gr0_conv_Suc)+ML ‹
val num_basic_lfp_sugar =
let
val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global \<^theory> \<^type_name>‹num›);
val recx = Logic.varify_types_global \<^term>‹rec_num›;
val C = body_type (fastype_of recx);
in
{T = @{typ num}, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[@{typ num}, C]], [[@{typ num}, C]]],
ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms rec_num}}
end;
›ML ‹nat_basic_lfp_sugar›
setup ‹
let
fun basic_lfp_sugars_of _ [\<^typ>‹num›] _ _ ctxt =
([], [0], [num_basic_lfp_sugar], [], [], [], TrueI (dummy), [], false, ctxt)
| basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
in
BNF_LFP_Rec_Sugar.register_lfp_rec_extension
{nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
end
›On 26 Jan 2025, at 10.26, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
Hi all,
I have a couple of related questions concerning the current state of the datatype package.
Find my motivation in the attached theory: I want to »register« a type a posteriori as a datatype.
a) Construct the type
b) Define the appropriate constructors
c) Prove them as free constructors
d) Prove the corresponding induction rule
But then? Primrec still fails, obviously due to the lack of a recursion combinator.
How to proceed from there?
(When examining how it is done for the existing elementary types in HOL, I found that the »old« datatype package with the traditional »rep_datatype« is still in place – which leads to the somehow related question if there are further migrations plans there.)
For the presented example an appropriate solution is to introduce the type as a datatype and establish lifting a posteriori, but there might be other instances where this is the less comfortable way.
Cheers,
Florian
<Numeral.thy><OpenPGP_0xA707172232CFA4E9.asc>
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Dec 21 2025 at 20:24 UTC