Re: [isabelle] On Recursion Induction



On 05/11/2012 02:27 PM, Brian Huffman wrote:
On Fri, May 11, 2012 at 6:59 AM, Christian Sternagel
<c-sterna at jaist.ac.jp>  wrote:
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).

You used a too-specific pattern with your theorem search. A term like
"?A ==>  ?B" is parsed as "Trueprop ?A ==>  Trueprop ?B", with ?A and ?B
of type "bool". Of course you want ?A and ?B to be parsed as type
"prop" here, so you need to add "PROP" tags to tell the parser what
you want:

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

found 1 theorem(s):

Pure.equal_intr_rule:
   [| PROP ?phi ==>  PROP ?psi; PROP ?psi ==>  PROP ?phi |] ==>  PROP ?phi
== PROP ?psi

If there is any "magic" it is in the parser, which magically inserts
"Trueprop" everywhere unless you tell it not to. ;)
Thanks, what a relief ;)

- Brian







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