Re: [isabelle] On Recursion Induction



Thanks Christian,

This was a very instructive explanation!  Besides, taking into account the
sequence
of apply steps I sent before, I have just read in the very good old
tutorial the following
statement:

"The methods drule spec and erule allE do precisely the same inference."

All the best!

On Fri, May 11, 2012 at 1:59 AM, Christian Sternagel
<c-sterna at jaist.ac.jp>wrote:

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


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