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
