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
