[isabelle] Export auto-generated theorems
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 e ⟹ even (Suc (Suc e))”
Then I use print_theorems, I could get some 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
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and