# IRC log for #isabelle, 2017-03-19

All times shown according to UTC.

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