*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Printing instantiations*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 21 Jun 2010 08:55:26 +0200*In-reply-to*: <AANLkTim9oeVLRq2OnFPMq1-X7Cou5xvmXpU6gpxwlxuO@mail.gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <0015174a032837804904894338c3@google.com> <4C1B1CA3.8030204@informatik.tu-muenchen.de> <AANLkTim9oeVLRq2OnFPMq1-X7Cou5xvmXpU6gpxwlxuO@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

Hi Steve, > How come the 'default proof' can't try to instantiate 'F' to 'f' and 'x' to > 'd'? I presume there are no rules declared in the current context of this > proof and of your proof, so what exactly does '..' or 'by rule' actually > apply here and in your proof? The ".." proof indeed defaults to (rule exI) in the example. But rule does only perform one resolution step, hence you have to apply it twice. Here the proof is given by an apply scripts: axiomatization f :: "real => real" and d :: real where ax1: "f d = 0" lemma test1: "EX (F::real=>real) x. F x = 0" apply (rule exI) apply (rule exI) apply (rule ax1) done In Isar the matter is a little bit difficult: we cannot write from `EX x. ...` have `EX y x. ...` since the "EX x. ..." fact would trigger existential elimination. So we must write it as backward proof: lemma test2: "EX (F::real=>real) x. F x = 0" proof - from ax1 have *: "EX x. f x = 0" by (rule exI) show ?thesis by (rule exI) (rule *) qed This looks not so beautiful but in practice such chained existential introduction would be accomplished e.g. by blast. The details can be found in the tutorial, chapter "The rules of the game". > But doesn't Isabelle support polymorphism? If so, types shouldn't need to be > explicitly declared, right? These are two different things: polymorphism vs. type inference. Type inference assigns most general types, which may be more general than actually wanted. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Follow-Ups**:**Re: [isabelle] Printing instantiations***From:*Steve W

**References**:**Re: [isabelle] Printing instantiations***From:*Florian Haftmann

**Re: [isabelle] Printing instantiations***From:*Steve W

- Previous by Date: Re: [isabelle] Printing instantiations
- Next by Date: [isabelle] Problems with cong-rules for parser
- Previous by Thread: Re: [isabelle] Printing instantiations
- Next by Thread: Re: [isabelle] Printing instantiations
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list