Re: [isabelle] fast + force prefer 'intro!' over assumptions?



There is no right or wrong here. In the context of a broader proof search and a goal free of logical variables, backtracking should ultimately find a proof if one exists. But with logical variables in the goal, you could get anything. I would need to look at the code to see which one is preferred.
Larry Paulson


On 9 Jul 2014, at 10:44, René Neumann <rene.neumann at in.tum.de> wrote:

> Hi,
> 
> I just noticed, that for a goal like
> 
> [| ...; it ⊆ S; ... |] ==> (?it it a b c) ⊆ S
> 
> force unifies "?it it a b c" with {} -- and not with 'it' as one would
> expect.
> 
> I suspect, that it first tries to apply intro! rules before looking at
> the assumptions. Is this the intended behavior? Or is it due to
> something completely different?
> 
> A simply DIY-example:
> 
> schematic_lemma
>  "it ⊆ S ==> ?it ⊆ S"
>  by force
> 
> This results in "S ⊆ S"...
> 
> - René
> 
> P.S.: This mattered to me, because it was part of an 'apply force+'
> which then instantiated '?it' wrong...
> 
> -- 
> René Neumann
> 
> Institut für Informatik (I7)
> Technische Universität München
> Boltzmannstr. 3
> 85748 Garching b. München
> 
> Tel: +49-89-289-17232
> Office: MI 03.11.055
> 





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