Email Gateway (Aug 22 2022 at 19:37): Email Gateway (Aug 22 2022 at 19:37):From: Yu Zhang <yu7161zh-s@student.lu.se>
Hi list,
I was wondering if there is any methods to export the theorems that come together with an inductive definition.
For example, I could write down the following definition:
inductive even :: "nat ⇒ bool" where
"even 0"
| "even e ⟹ even (Suc (Suc e))”
Then I use print_theorems, I could get some theorems:
theorems:
even.cases: ⟦Scratch.even ?a; ?a = 0 ⟹ ?P; ⋀e. ⟦?a = Suc (Suc e); Scratch.even e⟧ ⟹ ?P⟧ ⟹ ?P
even.induct: ⟦Scratch.even ?x; ?P 0; ⋀e. ⟦Scratch.even e; ?P e⟧ ⟹ ?P (Suc (Suc e))⟧ ⟹ ?P ?x
even.inducts: ⟦Scratch.even ?x; ?P 0; ⋀e. ⟦Scratch.even e; ?P e⟧ ⟹ ?P (Suc (Suc e))⟧ ⟹ ?P ?x
even.intros:
Scratch.even 0
Scratch.even ?e ⟹ Scratch.even (Suc (Suc ?e))
even.simps: Scratch.even ?a = (?a = 0 ∨ (∃e. ?a = Suc (Suc e) ∧ Scratch.even e))
So far so good. But what if I want to export all these theorems to a single .thy file? What should I do except copy&paste?
Any suggestions will be appreciated!
Sincerely,
Yu Zhang
Email Gateway (Aug 22 2022 at 19:38):From: Peter Lammich <lammich@in.tum.de>
Hi,
this looks like a strange use case. The theorems are, of course, only
valid together with the definitions made by the inductive-command.
So just having the theorems in isolation, without the inductive command
makes no sense.
If you want to use the theorems, you can simply refer to them by their
names (as printed by print_theorems, e.g. thm even.cases).
Hope this helps,
Peter
Last updated: Apr 26 2024 at 12:28 UTC