[isabelle] Export auto-generated theorems



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.