Re: [isabelle] On Recursion Induction



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

But I agree that there are some "strange" steps. Lets try to go through the proof step by step (please correct me if I claim anything wrong in the following ;)).

In Line 1 we apply "rule", which on its own (without arguments) uses a default rule that is determined by the syntactic structure of the goal. Since I was not able to find any rule that directly reduces a meta-equality into two implications with

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

but such a rule is obviously applied. This step is somewhat "magic" (I guess it is part of the Isabelle/Isar/Pure framework).

Lines 2 and 3 are nothing special.

Line 4, applies spec directly followed by assumption (internally many methods do not just return a single result, but in fact an (possibly) infinite list of results (due to higher-order unification)). Thus, by composing methods into a single apply step, we can "pick" the desired result of such a sequence, more specifically, the above states "use the first result of spec which is directly solvable by assumption". If such a result does not exist, the composition returns an empty result sequence (i.e., fails). If we do not compose these two steps, the first element of the result sequence is taken. To this end, let as have a look at "spec", which is

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

with "rule spec" we try to unify the conclusion of the current goal with the conclusion of spec, i.e,

  P x with ?P ?x

one possible unifier is ?x = P x and ?P = (%x. x) (the identity function), instantiating spec to

  ALL x. (%x. x) x ==> (%x. x) (P x)

which is immediately beta-reduced to

  ALL x. x ==> P x

and thus explains the result of applying just "rule spec" without "assumption".

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







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