Time 
Nick 
Message 
01:13 
chindy 
basically this: http://downthetypehole.de/paste/PrK1CVs5 
02:47 

ilbot3 joined #isabelle 
02:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
03:09 

stoopkid joined #isabelle 
10:20 
JCaesar 
doubt it… But if you just want ord, that should be easy, no? 
11:45 

silver joined #isabelle 
12:45 

stoopkid joined #isabelle 
14:50 
chindy 
JCaesar: well i just used the two definitions http://downthetypehole.de/paste/PrK1CVs5 or is there a fancier way of doing this? 
14:50 
chindy 
JCaesar: I know that there are these order (typeclasses?) but i am not sure how to use them 
15:01 
JCaesar 
Your vec type doesn't have a parameter, so it's pretty easy. (i always get it wrong with parameters…) 
15:02 
JCaesar 
you do a 'instantiation vec :: ord' 
15:02 
JCaesar 
then I think the output window should tell you which definitions you have to make. 
15:04 
JCaesar 
(oh, substitute ord by whatever typeclass you want to use. I'm not good at figuring out which is good for you. I don't think you can use linorder, simply because there isn't one on vectors (?). but there might be something else that's meaningful.) 
15:05 
JCaesar 
after you made all the necessary definitions, say 'instance apply standard'. That will give you some proof obligations you need to show about the definitions you made. Finish those proofs. Then say end. 
15:05 
JCaesar 
And that's it. 
15:06 
JCaesar 
oh, sorry, it is 'instantiation vec :: ord begin' 
15:07 
chindy 
... i do have vec arguments thoug :P 
15:09 
JCaesar 
Huh? then how is your type signature vec => vec => bool and not 'a vec => 'a vec => bool? 
15:10 
chindy 
its a type_synonym vec ="(real,2) vec" 
15:10 
JCaesar 
O_O. 
15:11 
JCaesar 
I don't even know if you can do instantiations on type synonyms… 
15:11 
JCaesar 
Also, I have no idea how to treat the length parameter in instantiations, so… meh, this is beyond my experience, sorry. 
15:14 
chindy 
okay then without type synonym 
15:14 
chindy 
so order on (real, 2) vec 
15:17 
chindy 
NVM... seems like i found an implementation example in Cartesian_Euclidean_Space.thy 
17:40 

IRCFrEAK joined #isabelle 
18:11 

ertesx joined #isabelle 
18:17 
chindy 
http://downthetypehole.de/paste/lE4D6fcm i want to instantiate that order defintion but i dont understand how the syntax works as i constantly get errors. 
18:46 

silver joined #isabelle 
19:22 
JCaesar 
this seems to be correct… 
19:23 
JCaesar 
not sure about the finite, but… 
19:28 
pruvisto 
JCaesar: the "finite" probably isn't needed 
19:29 
pruvisto 
not sure whether you can use "vec" with infinite indices properly though 
19:30 
pruvisto 
chindy: you realise that you can write "(real, 2) vec" as "real ^ 2", right? 
19:30 
pruvisto 
And the error that you get for "instantiation" has a very simple reason: There /is/ already an "ord" instance for "vec2 
19:30 
JCaesar 
Uh. Neat. 
19:30 
pruvisto 
*for "vec" 
19:31 
pruvisto 
search for "instantiation vec" in Cartesian_Euclidean_Space.thy 
19:31 
pruvisto 
It's a different one than yours though 
19:32 
pruvisto 
typically, "<" should be equivalent to "not ≥", which yours is not 