Re: [isabelle] discarding an assumption



Dave Cunningham wrote:
Is it possible to delete an assumption from the current subgoal?  While
unnecessary, I sometimes find this useful while proving in proof general
if the list of assumptions gets too big.  Maybe this makes the proof
space smaller while using the automatic methods too?  I've been doing

apply(erule_tac ?x="blah" in discard_assumption)

where I've previously proved "discard_assumption" as

[| ?x ; ?y |] ==> ?y

but I'm assuming this is a bad idea.  Isabelle certainly warns about it.
Is there a better way?


thanks

Dave,

I can't see why it is a bad idea, except for the fact that your

"discard_assumption"

is in fact thin_rl, already in Isabelle.

In fact the tactic thin_tac does exactly what you have done

tactic.ML:fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;

You say "Isabelle certainly warns about it" but I don't get such a warning, what does it say?

regards,

Jeremy






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