Stream: Beginner Questions

Topic: Adding to a fact set

John Hughes (Jan 28 2025 at 19:08):

As an experiment, I'm accumulating a bunch of related facts in a fact set, using

lemma gtP1 [known]:

for instance (the fact set is called known). When I define a new term

definition gt::"r ⇒ r ⇒ bool"
  where "gt a b = ((a ⊖ b)  ∈ P)"

I automatically get a new fact gt_def. I'd like to add that to my fact set. But I don't see a way to add a fact except during the statement of a lemma/theorem/whatever. I tried putting [known] in various positions in that definition, but all of them produced errors.

Is this possible -- adding a fact to a fact-set after the fact has been created?

Jan van Brügge (Jan 28 2025 at 19:16):

Yes, declare gt_def[known]

John Hughes (Jan 28 2025 at 19:16):

Many thanks!

Balazs Toth (Jan 29 2025 at 11:05):

This should also work:

definition gt::"r ⇒ r ⇒ bool"
  where [known]: "gt a b = ((a ⊖ b)  ∈ P)"

Last updated: Feb 01 2025 at 20:19 UTC