There's a typo in my last message. It should read
let [v1;v2] = (snd o strip_comb o snd o dest_conj o snd o
dest_exists o snd o dest_abs o snd o dest_comb o snd o dest_eq) (concl
real_neg);;
Mark.
on 9/11/11 1:59 PM, Mark <[email protected]> wrote:
> Apologies for joining this discussion rather late.
>
> Jonathan, To answer one of your questions in the last posting, I think
there
> are neater ways than to disable the pretty printer for terms. In HOL
Light
> there is a function called 'variables', which lists all the variables that
> occur in a term (either bound variables or free variables). Using this on
> the conclusion of 'real_neg' gives 2 variables called 'x1' (with different
> HOL types). So the thing to do is apply 'dest_var' on each of the
variables
> returned by 'variables':
>
> map dest_var (variables (concl real_neg));;
>
> which returns:
>
> [("x1", `:hreal#hreal`); ("u", `:hreal#hreal`); ("x1", `:real`)]
>
> So you can use HOL Light's 'vsubst' to rename the free 'x1' if you wish
(or
> INST if dealing with a theorem).
>
> An alternative but rather cumbersome approach is to use HOL Light's term
> destructors to pull apart the expression piece-by-piece:
>
> let (tm1,tm2) = dest_eq (concl real_neg);;
> let (tm3,tm4) = dest_comb tm2;;
> etc, etc .....
>
> or if you just want to get to a specific subterm buried deep within, use a
> chain of destructors composed together:
>
> let (_,[v1;v2]) = (snd o strip_comb o snd o dest_conj o snd o
> dest_exists o snd o dest_abs o snd o dest_comb o snd o dest_eq) (concl
> real_neg);;
>
> I should point out that there is another HOL system called HOL Zero that
> deals with this problem of parsing/printing overloaded variables in term
> quotations. It uses an adapted form of Hindley-Milner type inference when
> parsing, so any sufficiently-type-annotated term will get successfully
> parsed. Also, the pretty printer type-annotates its output so that there
is
> no ambiguity about the types of any variables or constants, so any output
of
> the pretty printer can be cut-and-pasted back for parser input. Your
> example term would parse without requiring any type annotation, because it
> is clear from the type of 'dest_real' that the `x1` first argument to
> 'dest_real' is of type `:real` and the `x1` second argument is of type
> `:hreal#hreal`. If you did wish to see the types excplicitly, HOL Zero
has
> a display option to display the types of all printed variables.
>
> Mark.
>
> on 13/10/11 9:57 AM, Jonathan von Schroeder
<[email protected]>
> wrote:
>
>> Hi Czeray,
>> thanks for the clarification. Looking at src/HOL/Import/* I couldn't
> really
>> figure out how to invoke the automatic generation myself. Can you give me
>> any hints?
>>
>> I'd also greatly appreciate if you could tell me how to pragmatically
>> distinguish these two variables to be able to rename them (maybe you can
>> point me to how it's done in the automatic translation). The only
approach
> I
>> can currently think of is to do it by looking at the types and renaming
> all
>> variables that have the same name but incompatible types since on the rhs
>> both variables are "below" the existential quantification:
>>
>> # #remove_printer print_qterm;;
>>> # concl (real_neg);;
>>> val it : term >> Comb
>>> (Comb (Const ("=", `:real->real->bool`),
>>> Comb (Const ("real_neg", `:real->real`), Var ("x1", `:real`))),
>>> Comb (Const ("mk_real", `:(hreal#hreal->bool)->real`),
>>> Abs (Var ("u", `:hreal#hreal`),
>>> Comb (Const ("?", `:(hreal#hreal->bool)->bool`),
>>> Abs (Var ("x1", `:hreal#hreal`),
>>> Comb
>>> (Comb (Const ("/\\", `:bool->bool->bool`),
>>> Comb
>>> (Comb (Const ("treal_eq", `:hreal#hreal->hreal#hreal->bool`),
>>> Comb (Const ("treal_neg", `:hreal#hreal->hreal#hreal`),
>>> Var ("x1", `:hreal#hreal`))),
>>> Var ("u", `:hreal#hreal`))),
>>> Comb
>>> (Comb (Const ("dest_real", `:real->hreal#hreal->bool`),
>>> Var ("x1", `:real`)),
>>> Var ("x1", `:hreal#hreal`))))))))
>>
>> Jonathan
>>
>> On 12 October 2011 03:38, Cezary Kaliszyk <[email protected]>
> wrote:
>>
>>> 2011/10/11 Jonathan von Schroeder <[email protected]>:
>>> > Hi all,
>>> > im currently having a problem figuring out the meaning of the
following
>>> > theorem (from realax.ml):
>>> >>
>>> >> # real_neg;;
>>> >> val it : thm >> >> |- --x1 = mk_real (\u. ?x1. treal_neg x1
treal_eq
> u /\ dest_real x1
>>> x1)
>>>
>>> You can also look at the version automatically translated to Isabelle
>>> by HOL/Import. In the isabelle source the file:
>>> src/HOL/Import/HOLLight/HOLLight.thy
>>> You can find the following:
>>>
>>> definition real_neg :: "hollight.real => hollight.real" where
>>> "real_neg == %x1. mk_real (%u. EX x1a. treal_eq (treal_neg x1a) u &
>>> dest_real x1 x1a)"
>>>
>>> In the above, the name of the other variable has been automatically
>> changed
>>> from 'x1' to 'x1a' to avoid the name clash.
>>>
>>> Cezary
>>>
>>
>>
>>
>> ----------------------------------------
>>
>>
>
----------------------------------------------------------------------------
>> --
>> All the data continuously generated in your IT infrastructure contains a
>> definitive record of customers, application performance, security
>> threats, fraudulent activity and more. Splunk takes this data and makes
>> sense of it. Business sense. IT sense. Common sense.
>> http://p.sf.net/sfu/splunk-d2d-oct
>>
>>
>> ----------------------------------------
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>
>
------------------------------------------------------------------------------
RSA(R) Conference 2012
Save $700 by Nov 18
Register now
http://p.sf.net/sfu/rsa-sfdev2dev1
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
