Re: [isabelle] dest_Trueprop question



On Monday 19 June 2006 08:47, Dimitrios Vytiniotis wrote:
> Thanks Jeremy, Makarius for the advice. Useful to know.
>
> For the dest_Trueprop issue, it is the 'auto' step that causes
> the TERM exception. To be concrete I have put a small theory file at:
>
>   http://www.cis.upenn.edu/~dimitriv/poplmark/Simple.thy
>
> which demonstrates what is happening
> thanks!
> -d

Looking at the source for auto_tac (in Provers/clasimp.ML), I found that auto 
makes calls to the simp, safe, and blast tactics. It appears that the problem 
in your example lies in the blast tactic. If you make Typing.elims and 
Val.elims into safe elimination rules (with "auto elim!:" instead of "auto 
elim:") then auto no longer fails, because the elimination rules are used by 
safe instead of blast. But if you replace auto with repeated calls to blast, 
the third subgoal produces the same dest_Trueprop error. I'm not an expert on 
how blast works, but it seems to me that there could be a bug in the blast 
tactic.

- Brian





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