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



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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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