Re: [isabelle] Export auto-generated theorems



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


On Mi, 2019-04-03 at 15:01 +0800, Yu Zhang wrote:
> 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.