*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] On Recursion Induction*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Fri, 11 May 2012 01:11:25 -0300*Cc*: Brian Huffman <huffman.brian.c at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA9E98D.6020302@jaist.ac.jp>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp> <CAAPnxw1OQXEw7TaWg8Ft2G9q5=SEp-8FeYCGeS_Oiz2RZFn_2Q@mail.gmail.com> <4FA9E98D.6020302@jaist.ac.jp>*Sender*: alfio.martini at gmail.com

Dear Christian, I was a little puzzled by you "atomic" proof below lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)" by (rule) (rule allI, assumption, rule spec) and wanted to see the details myself. But using step-by-step apply commands this was the only way I could solve the goal: lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)" apply (rule) apply (rule allI) apply (assumption) apply (rename_tac x0) apply (erule allE) apply (assumption) done That is to say, I had to use "allE" instead of "spec". The renaming above was included because I was a little confused by a scope of a specific arbitrary variable. best! On Wed, May 9, 2012 at 12:50 AM, Christian Sternagel <c-sterna at jaist.ac.jp>wrote: > Dear Alfio, > > > On 05/09/2012 04:40 AM, Alfio Martini wrote: > >> >Your original version results in "ALL b e. valbool b e = valbool (NNF >> >b) e" (which is equivalent, but not so nice to use, since you cannot >> >directly instantiate it). >> >> I think I spoke about this above, but I would like to capture in a >> precise way (in a theorem) this equivalence. Informally we >> all know that they are. I often think about it. Do you know how >> to write (in Isabelle) this "equivalence"? >> > Maybe the closest you get to this equivalence is > > lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)" > by (rule) (rule allI, assumption, rule spec) > > which shows that meta-all-quantification is the same as > HOL-all-quantification. It is not possible to prove that schematic > variables are equivalent to meta-all-quantified variables inside the logic. > Also the need for the explicit Trueprop (which turns something of type > "bool" [the type of HOL formulas] into type "prop" [the type of > propositions in the general Isabelle framework]) in the above proof hints > that we are doing something non-standard (for lack of a better expression). > > To convince yourself that the equivalence is not only informal, the > theorems allI and spec should be enough. > > just my 2 cents > > chris > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**References**:**[isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

- Previous by Date: [isabelle] 6th International School on Rewriting (ISR), Valencia, July 16-20, 2012
- Next by Date: Re: [isabelle] On Recursion Induction
- Previous by Thread: Re: [isabelle] On Recursion Induction
- Next by Thread: Re: [isabelle] On Recursion Induction
- Cl-isabelle-users May 2012 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