Re: [isabelle] tactic being executed twice



On 05/06/18 17:52, Makarius wrote:
> On 05/06/18 17:17, Jeremy Dawson wrote:
>>
>> What I'm doing right now is trying to code up an absurdly trivial
>> example of a tactic which should succeed using an absurdly trivial
>> oracle, which isn't included in the code I showed, but fails in the same
>> way (at least, the same, in that the tactic gets applied to a goal which
>> does not have the requisite number of subgoals).
> 
> Just some guesses from a long distance:
> 
>   * there is something wrong with the goal context (type Proof.context)
> 
>   * type-inference has produced unexpectedly general results (usually
> due to a wrong context)

Yet another guess:

    * You access the raw "thm" representation of the goal state outside
the parts that are meant for user tools (e.g. the main conclusion), and
thus bump into delicate details managed by the system.

Semantic side-conditions on type tactic are specified in
"implementation" section 4.2. More side-condition on Isar proof methods
in section 7.2.

In practice, it is often better to look at canonical examples, and
modify them to fit a particular application. The "isar-ref" manual has a
brief section 5.14 on Oracles, with a link to the worked example
~~/src/HOL/ex/IFF_Oracle.thy -- as usual it is best to study the
material in the Prover IDE (Isabelle/jEdit).


	Makarius




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