*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] On Recursion Induction*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Fri, 11 May 2012 13:59:31 +0900*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw10SB2Z8vhWKCBqOZYNkyVaHQUU8qTaJiZ4Q-0BcBaEXQ@mail.gmail.com>*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> <CAAPnxw10SB2Z8vhWKCBqOZYNkyVaHQUU8qTaJiZ4Q-0BcBaEXQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

Dear Alfio, it works like this lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)" apply (rule) apply (rule allI) apply (assumption) apply (rule spec, assumption) done

find_theorems "(?A ==> ?B) ==> (?B ==> ?A) ==> ?A == ?B"

Lines 2 and 3 are nothing special.

ALL x. ?P x ==> ?P ?x

P x with ?P ?x

ALL x. (%x. x) x ==> (%x. x) (P x) which is immediately beta-reduced to ALL x. x ==> P x

hope this helps chris On 05/11/2012 01:11 PM, Alfio Martini wrote:

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 <mailto: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:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Brian Huffman

**Re: [isabelle] On Recursion Induction***From:*Makarius

**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

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

- Previous by Date: Re: [isabelle] On Recursion Induction
- 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