Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-18

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

All times shown according to UTC.

Time Nick Message
00:17 int-e Oh well, I got a proof.
00:20 int-e barrucadu: http://sprunge.us/ORJU
00:21 int-e It's really stupid because it's a bona fide inductive definition on the data type definition; morally it *is* primitive recursive.
00:23 int-e but the underlying well-founded relation on POR is not readily available; that's what I'm defining as ?R in the proof
00:34 int-e (or so I believe, I'd be happy to be shown wrong)
06:46 ThreeOfEight barrucadu: http://downthetypehole.de/paste/GajExEFx
06:48 ThreeOfEight int-e is correct, this is a primitively-recursive function, so the easiest way to define it is to define it as noe
06:48 ThreeOfEight *one
06:48 ThreeOfEight the problem is that "primrec" is apparently not smart enough to figure out that your definition is primitively-recursive
06:49 ThreeOfEight so I just did it by hand and proved the "simp" rule separately afterwards
06:51 ThreeOfEight Two more remarks: 1. you datatype is essentially an infinitely-branching tree, which means you can have potentially unbounded traversal paths in it, so there simply is no sensible "size" function for them, which makes proving termination more painful (although in this case, it can be done with relatively little effort, as shown by int-e)
06:53 ThreeOfEight 2. your function implicitly enforces the domain of "done" to be finite, so you could actually define a "size" function for this case, and it would be something "size (POR _ _ done) = 1 + Max (size ` ran done)". But you'd also have to add conj_cong as a fundef_cong rule or rewrite your definition with if _ then _ else in order to be able to use the fact that "done" has finite domain
14:16 barrucadu int-e: ThreeOfEight: Thanks, I was able to make some progress with that.
14:51 barrucadu I'm trying to work out how to use pattern matching inside an Isar proof to deconstruct a variable. If I am doing an induction proof and have a "case (Cons x xs)", where "x" is a pair, how do I split that apart?
14:52 barrucadu I want to do something like "let (a, b) = x; proof (cases "P a") ..."
15:19 mal`` joined #isabelle
23:57 rofer joined #isabelle

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