Time 
Nick 
Message 
01:47 

ilbot3 joined #isabelle 
01: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:44 

cmr joined #isabelle 
10:25 
ammbauer 
Can I specify what file Isabelle/jedit opens up by default on startup (instead of ~/Scratch.thy)? 
10:38 

silver joined #isabelle 
11:22 

ThreeOfEight joined #isabelle 
11:24 
ThreeOfEight 
cocreature: apply assumption 
11:28 
cocreature 
ThreeOfEight: I tried that but I only got "Failed to apply proof method". maybe I simplified the example a bit too much to illustrate the problem, here’s the actual state http://lpaste.net/163003. fwiw I was able to solve it using subgoal premises prems and then apply (rule prems) but that seems a bit weird 
11:28 
larsrh 
cocreature: "subgoal" is kinda cheating :) 
11:29 
ThreeOfEight 
cocreature: I'm afraid this isn't terribly useful; people cannot really reproduce your problem if you just post the proof state 
11:29 
ThreeOfEight 
Can you post enough definitions etc. to actually reproduce this in Isabelle? 
11:30 
ThreeOfEight 
Anyway, I think the best answer these days is "Either let the automation do it for you or write it in Isar" 
11:30 
inte 
(presumably sorted (x # xs) implies sorted xs, and that'll prove the first subgoal) 
11:31 
ThreeOfEight 
but it is, of course, sometimes useful to know how to use low level tactic scripts 
11:31 
cocreature 
ThreeOfEight: sorry, I think this should be enough http://lpaste.net/163004 
11:31 
cocreature 
sorry for the german comments 
11:31 
ThreeOfEight 
no problem 
11:31 
inte 
the subgoal command is *very* useful in proof exploration 
11:31 
ThreeOfEight 
it's fine, I would imagine a significant portion of this channel is German ;) 
11:31 
ThreeOfEight 
(like me) 
11:31 
cocreature 
larsrh: cheating in what way? 
11:31 
ThreeOfEight 
and, yes, there is sorted_Cons, for instnace 
11:32 
cocreature 
inte: yep it does 
11:32 
ThreeOfEight 
I was a bit puzzled about what "subgoal" even is 
11:33 
larsrh 
cocreature: subgoal introduces a structured Isar proof, and you said you wanted to use a tactic :) 
11:33 
ThreeOfEight 
I should read the change logs more carefully 
11:33 
cocreature 
larsrh: ah good point :) 
11:33 
ThreeOfEight 
cocreature: KIT? 
11:34 
cocreature 
ThreeOfEight: yep :) 
11:34 
larsrh 
cocreature: Small world, both ThreeOfEight and me are TUMmies 
11:34 
ThreeOfEight 
How utterly surprising for two Isabelle users to be connected to TUM :P 
11:35 
cocreature 
also don’t worry about solving my exercises for me. we don’t need to use manual tactics and I have it solved in other ways already 
11:35 
cocreature 
heh :) 
11:37 
larsrh 
cocreature: who's teaching that course? 
11:37 
ThreeOfEight 
Who do you think 
11:37 
ThreeOfEight 
Joachim Breitner of course 
11:37 
cocreature 
yep 
11:37 
cocreature 
and dennis lohner 
11:37 
ThreeOfEight 
I still know that name from the Haskell competition 
11:37 
cocreature 
eh *denis 
11:38 
ThreeOfEight 
he's the one who always solved /every/ problem by throwing GLPK at it 
11:38 
larsrh 
Denis "linear programming" Lohner :D 
11:38 
ThreeOfEight 
cocreature: btw, referring to "trotz meiner manuellen Tactichacks…" 
11:38 
ThreeOfEight 
longwinded apply scripts actually tend to be slower than Isar proofs in many cases 
11:38 
larsrh 
cocreature: who told you about case_tac and rule_tac? 
11:38 
ThreeOfEight 
because when you write "by", the proof gets forked to the background and processing can resume immediately 
11:38 
larsrh 
I'd like to have a word with that person 
11:39 
ThreeOfEight 
whereas with an apply script, all of it is done in a single thread 
11:39 
cocreature 
ThreeOfEight: ah ok, I thought it would at least be faster than just using auto 
11:39 
ThreeOfEight 
depends 
11:39 
ThreeOfEight 
if auto has a lot of proof space to search, then yes, it may be faster 
11:39 
larsrh 
If auto solves it in <1 second, just use auto, that's the way I do it usually 
11:39 
cocreature 
larsrh: the manual :P 
11:40 
ThreeOfEight 
I do wonder why this is so horribly slow though 
11:40 
larsrh 
cocreature: most, if not all methods ending with _tac should not be used unless you know exactly what you're doing 
11:41 
cocreature 
yeah the manual told me that as well :) 
11:41 
larsrh 
... 
11:42 
larsrh 
We need to implement that jEdit plays some sound when you use such a method 
11:42 
larsrh 
or flashes a biohazard sign or something 
11:42 
inte 
uh this is so lowlevel. how does one turn (A ==> B) ==> C ==> B into C ==> A (i.e., use an assumption as an intro rule?) 
11:42 
ThreeOfEight 
inte: well, "assumption" should do the trick 
11:43 
ThreeOfEight 
but it will probably solve it as well 
11:43 
ThreeOfEight 
oh it can't solve it 
11:43 
ThreeOfEight 
yeah well then… 
11:45 
cocreature 
wait so what am I doing wrong that it doesn’t solve it for me? 
11:45 
inte 
subgoal apply (subst (asm) sorted.simps(2)) apply (erule conjE) apply assumption done solves the first subgoal 
11:45 
inte 
the assumptions don't fit. 
11:45 
ThreeOfEight 
cocreature: it only does that when the precondition of the implication is litteraly there in the premises 
11:46 
inte 
"litteraly" is cute. 
11:46 
ThreeOfEight 
I couldn't find any tactic that applies an assumption like an intro rule 
11:47 
inte 
ThreeOfEight: I doubt that is ever a problem in practice... it certainly hasn't come up for me. But thanks for looking! 
11:47 
ThreeOfEight 
Well, if it /is/ a problem in practice, then you probably shouldn't solve it this way 
11:47 
ThreeOfEight 
but write Isar instead 
11:48 
cocreature 
ThreeOfEight: ok, thanks for your help 
11:59 
ThreeOfEight 
inte: You /can/ do this: http://downthetypehole.de/paste/gS54gXg9 
11:59 
ThreeOfEight 
allows you to write e.g. "apply (intro_asm 2)" to apply the second assumption as an intro rule 
12:00 
inte 
cocreature: more usefully, perhaps: letrans is a very expensive simp rule, so I wouldn't declare it as simp. lemerge and sortmerge are actually good, safe, intro rules, so one may mark them as [intro!] 
12:00 
larsrh 
everyone: disregard what ThreeOfEight wrote, use Isar :p 
12:00 
ThreeOfEight 
pff 
12:00 
ThreeOfEight 
let me have my fun 
12:00 
inte 
cocreature: with lemerge marked as intro! and letrans not marked at all, the last proof goes throuh fairly quickly using by (induction xs ys rule: merge.induct) (auto, auto simp: letrans) 
12:01 
inte 
though. 
12:01 
inte 
(the two stage auto actually helps :/) 
12:06 
inte 
ThreeOfEight: thanks, I almost certainly won't use the tactic but I'll probably try to understand the ML code at some point. 
12:07 
cocreature 
inte: ah great. what’s the criteria for something to be a safe intro rule? 
12:07 
inte 
cocreature: an intro rule is safe if the premises follow from the conclusion. 
12:08 
cocreature 
inte: alright, thanks again! 
12:08 
inte 
(so it's an if and only if, P and Q iff R, expressed in the shape of an introduction rule, "P ==> Q ==> R") 
12:09 
chuchucorny 
what is the most simple way to get some sort of wellformndness constraint into a datatype. I have "datatype 'a foo = Foo 'a set 'a set" and want to enforce that for "Foo a b" b is a subset of a. And this should be in the type definition (I don't want additional assumptions in my lemmas) 
12:12 
inte 
cocreature: The premises should also be "simpler" than the conclusion, so that applying the intro rules terminates. But that's also true in your case. 
12:41 
chuchucorny 
(okay, dlists seem to be a nice exaple for what I'm looking for) 
13:07 
ThreeOfEight 
chuchucorny: probably define a datatype foo_rep, then a wellformedness predicate on the datatype, and then a typedef that enforces the definition 
13:08 
ThreeOfEight 
and use lifting/transfer to define functions on that type and transfer lemmas 
13:08 
ThreeOfEight 
cocreature: I for one would be careful about declaring things as intro! 
13:08 
ThreeOfEight 
because when these things do get you into trouble, it's difficult to find out why 
13:09 
ThreeOfEight 
(there is tracing for classical methods, but it's not very nice to use) 
13:10 
ThreeOfEight 
and another good rule (in my opinion): don't write simp rules where there are variables in the premises that do not occur in the goal (like in le trans) 
13:10 
ThreeOfEight 
you can maybe declare this as dest or something like that, but I wouldn't recommend it 
13:10 
larsrh 
tools are in general not very good with transitivity rules 
13:11 
ThreeOfEight 
but a simp/intro rule with variables in the premises that do not occur in the goal are basically guaranteed to blow up in your face 
13:11 
ThreeOfEight 
*is 
13:13 
cocreature 
thank I’ll keep that in mind 
13:15 
ThreeOfEight 
also, two consecutive autos are a bad idea 
13:16 
ThreeOfEight 
if you want a fast oneline proof, you can do something like this: 
13:16 
ThreeOfEight 
by (induction xs ys rule: merge.induct) (auto intro!: lemerge dest: letrans less_imp_le simp: not_le) 
13:17 
cocreature 
why are two consecutive autos a bad idea? 
13:17 
ThreeOfEight 
(after removing all the simp annotations from those rules) 
13:17 
ThreeOfEight 
because "auto" does a lot of things 
13:17 
ThreeOfEight 
and the exact things that it does may change with every new Isabelle release 
13:17 
ThreeOfEight 
and unlike blast, force, etc., auto doesn't fail when it can't solve the goal 
13:17 
ThreeOfEight 
it just leaves the remaining proof obligations behind 
13:18 
ThreeOfEight 
but if the behaviour of auto changes, what it leaves behind also changes 
13:18 
ThreeOfEight 
and then the subsequent proof methods will suddenly be used on a different proof state and might not work anymore 
13:18 
ThreeOfEight 
and the person who will have to fix it will have a hard time figuring out what went wrong and what to do 
13:19 
ThreeOfEight 
so it is considered good style to use auto only as the very last proof method 
13:19 
ThreeOfEight 
two consecutive autos may still work more or less 
13:19 
ThreeOfEight 
it's not great, but it can work fine in practice 
13:19 
ThreeOfEight 
however, I've seen people do "proof auto", or "apply auto proof" 
13:20 
ThreeOfEight 
and /that/ is pure evil 
13:20 

fracting joined #isabelle 
13:24 
cocreature 
makes sense 
13:39 

fracting joined #isabelle 
14:21 

fracting joined #isabelle 
19:11 
ammbauer 
"Linear arithmetic should have refuted the assumptions. 
19:11 
ammbauer 
Please inform Tobias Nipkow." 
19:11 
ammbauer 
... halp 
19:54 
ThreeOfEight 
haha 
19:54 
ThreeOfEight 
yeah that happens occasionally 
19:54 
ThreeOfEight 
unless you were actively hoping to use linear arithmetic there, I would just ignore that 
19:55 
ThreeOfEight 
but you can inform him if you want 
20:31 

tautologico joined #isabelle 
21:39 

ammbauer joined #isabelle 