Email Gateway (Mar 17 2022 at 10:53): Email Gateway (Mar 17 2022 at 10:53):From: Klenze Tobias <tobias.klenze@inf.ethz.ch>
Hello everyone,
how can I show a datatype containing a record to be countable?
record 'a testrecord = field :: 'a
datatype 'a testdatatype = F "'a testrecord"
instance testdatatype :: (countable) countable
(* by countable_datatype *)
(* exception TYPE raised (line 87 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
Type is not of sort countable
'aa__ testrecord *)
Thank you in advance!
Best,
Tobias
Email Gateway (Mar 17 2022 at 11:04):From: Jasmin Blanchette <cl-isabelle-users@lists.cam.ac.uk>
Dear Tobias,
I can help you a little bit. For the tactic invocation to "countable_datatype" to succeed, you'll need first to show that your record is countable. Here's the proof, modulo a "sorry":
instance testrecord_ext :: (countable, countable) countable
sorry
I'm not aware of any automation for proving records countable. I'm presuming it's not very difficult since there's no recursion involved.
Cheers,
Jasmin
Email Gateway (Mar 17 2022 at 13:33):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi Tobias,
to connect to Jasmin’s reply, here is a solution that leverages the countable_datatype proof method. I am not sure, whether it is the prettiest solution, but it seems to generalize well to other countable record types and works with little proof effort.
Cheers,
Christoph
― ‹countable record types›
record point = x :: nat y :: nat
― ‹define an isomorphic datatype and inject the record type into it›
datatype 'a pointt = Point nat nat 'a
instance pointt :: (countable) countable
by countable_datatype
definition point_to_pointt :: "'a point_ext ⇒ 'a pointt" where
"point_to_pointt pt = Point (x pt) (y pt) (more pt)"
― ‹show that the record type is countable›
instance point_ext :: (countable) countable
proof
obtain pointt_to_nat :: "('a::countable) pointt ⇒ nat" where "inj pointt_to_nat" by auto
then have "inj (pointt_to_nat o point_to_pointt)"
by (auto simp add: point_to_pointt_def intro!: inj_compose intro: injI)
then show "∃to_nat::'a point_scheme ⇒ nat. inj to_nat" by auto
qed
Email Gateway (Mar 17 2022 at 14:03):From: Thomas Sewell <tals4@cam.ac.uk>
Just for fun, here's a slightly more automatic version using the shape of a fact (f.splits) defined by the record package.
record rec =
rec_x :: nat rec_y :: nat
lemma exists_to_prod:
"(∃a b. P a b) = (∃t. P (fst t) (snd t))"
by simp
lemma exists_equiv_inj[rule_format]:
"(∀P. (∃x. P x) = (∃y. P (f y))) ⟹ surj f"
by auto
instance rec_ext :: (countable)countable
proof -
note surj = rec.splits(3)[simplified exists_to_prod, THEN exists_equiv_inj]
note inj = surj_imp_inj_inv[OF surj]
note inj_rec_to_nat = inj_compose[OF inj_to_nat inj]
then show "PROP ?thesis"
by intro_classes auto
qed
Best regards,
Thomas.
Last updated: Jan 04 2025 at 20:18 UTC