Re: [isabelle] discarding an assumption



>> where I've previously proved "discard_assumption" as
>>
>> [| ?x ; ?y |] ==> ?y
>>
>
> 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;

awesome, it seems i can just go

apply(thin_tac "blah") to make "blah" disappear from the assumptions!


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

ah i just looked again and noticed i was doing (for some unknown reason):

lemma discard_assumption: "[| ?x ; ?y |] ==> ?y"

which produced the message:

[Isabelle] ### Goal statement contains unbound schematic variable(s): ?y, ?x

Which is what I was seeing as i was skipping through all my definitions
up to the main proof i'm working on.

Replacing them with x and y made it go away.  However now I don't need
it anymore, anyway :)


thanks








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