Time 
Nick 
Message 
00:17 
inte 
Oh well, I got a proof. 
00:20 
inte 
barrucadu: http://sprunge.us/ORJU 
00:21 
inte 
It's really stupid because it's a bona fide inductive definition on the data type definition; morally it *is* primitive recursive. 
00:23 
inte 
but the underlying wellfounded relation on POR is not readily available; that's what I'm defining as ?R in the proof 
00:34 
inte 
(or so I believe, I'd be happy to be shown wrong) 
06:46 
ThreeOfEight 
barrucadu: http://downthetypehole.de/paste/GajExEFx 
06:48 
ThreeOfEight 
inte is correct, this is a primitivelyrecursive 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 primitivelyrecursive 
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 infinitelybranching 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 inte) 
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 
inte: 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 