Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-03-20

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/rese​arch/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
10:45 silver joined #isabelle
11:08 ammbauer if I want something like namespaces should I just put my lemmas in a locale?
11:09 pruvisto What do you mean by "namespaces"?
11:15 larsrh if you want namespaces, you weep
11:16 int-e start at denial? :)
11:17 JCaesar Try bargaing with underscores.
11:17 int-e nice contraction
11:22 ammbauer what's wrong with something like this: http://downthetypehole.de/paste/7St45PXw ?
11:22 larsrh ammbauer: works fine until you define functions/constants/... that need to end up in generated code
11:29 pruvisto Really? Even if the locale has no assumptions?
11:29 chindy pruvisto: ahh... so do i need to declare the fact that i want to use this exact defintion of \ge or is that resolved automatically ?
11:31 JCaesar pruvisto: Don't you have to interpret it?
11:34 pruvisto chindy: I'm not sure what you mean
11:34 pruvisto you cannot re-define the meaning of "≤" once it has been defined once
11:36 pruvisto JCaesar: urgh, yes, apparently you have to do a global_interpretation for some reason
11:36 pruvisto I wasn't aware of that.
11:45 chindy pruvisto: nah that more or less answers my question... i was wondering that if wanted to use that defintion from Cartes.Eucl.Space if i needed to state that I want to use that one or if that is done automatically
11:48 pruvisto chindy: type class instantiations are universally valid and permanent
11:48 pruvisto if you import the theory, you have the instance and there's no way to disable or change it
11:48 pruvisto if you have two conflicting instances, you get an error message on theory import
11:49 pruvisto (that can be a bit of a problem sometimes)
11:49 pruvisto (but more so for the people maintaining the library than for users, I would say)
18:07 chindy okay thanks!
18:09 chindy unrelated question, are these two lemmas or similar already in the std, i could not find them in List.thy http://downthetypehole.de/paste/7IBLX8lS
18:11 ertesx joined #isabelle
18:15 larsrh chindy: try sledgehammering them?
18:16 chindy didn't work
18:30 JCaesar Btw, there's no real reason to use fold (op And), is there?
18:31 JCaesar There is list_all, and even ∀x ∈ set S. P x will be refined to executable code…
18:33 chindy JCaesar:  i did not know there is list_all
18:34 chindy so basically list_ex takes a predicate and looks if it holds for one element int he list and list_all does if P holds forall ?
18:35 JCaesar I won't sign that because I'm not a 100% sure, but you can just either look up the definition with a ctrl-click or do a "find_theorems list_ex Bex", that should give you the relevant theorem.
18:35 JCaesar The thing is: I don't get why they exist.
18:38 chindy what does the function/definition Bex entail ?
18:41 chindy i am confused what the difference is, between "list_ex P xs ⟷ Bex (set xs) P", "list_ex1 P xs ⟷ (∃! x. x ∈ set xs ∧ P x)" also not quite sure what Bex does
18:44 int-e Bex is a "bounded" existential quantifier: lemma "(∃x ∈ set xs. P x) ⟷ Bex (set xs) P" ..
18:44 int-e (these two expressions differ only in an eta-contraction)
18:47 chindy int-e: thanks!
20:00 JCaesar Actually, Bex is just the name of the syntax (∃x ∈ ?xs. ?P x)
20:02 JCaesar Oh, and Bex1 is literally "there exists exactly one"
20:22 ski_ joined #isabelle
20:32 int-e JCaesar: I would rather say that "∃x ∈ ?xs. ?P x" is syntax for "Bex ?xs (λx. ?P x)"
20:33 JCaesar Ah, yes, you're right.
20:33 JCaesar Bex is the name of the definition.
20:33 JCaesar chindy: We're splitting hairs, just so you know. ;)
20:34 chindy ;)
20:34 chindy just to be clear xs of tpye list? or of type some foldable
20:37 int-e no that's a set
20:37 int-e (note that  set :: 'a list => 'a set)
20:52 JCaesar hm, isn't there some function that will convert a foldable to a set? I don't know what's preferred in that case, though…
21:00 larsrh a ... foldable?
21:03 pruvisto There's Finite_Set.fold
21:03 pruvisto wait
21:03 pruvisto never mind
21:03 pruvisto okay I also have no idea what you mean
21:03 pruvisto datatypes defined with the "datatype" command usually have a "set" function though
21:04 int-e Must be too much exposure to Haskell.
21:05 JCaesar possibly…
21:05 JCaesar pruvisto: guess I was thinking of Finite_Set.fold, too… no idea.
22:25 tautologico joined #isabelle
23:00 tautologico joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary