Time 
Nick 
Message 
01:51 

ilbot3 joined #isabelle 
01:51 

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:04 

relrod joined #isabelle 
03:04 

relrod joined #isabelle 
08:19 

ammbauer joined #isabelle 
13:05 

qertyyyy joined #isabelle 
13:15 
qertyyyy 
hi , is there a proof method that basically does subst [substitutionname] and rule refl in one "command"? I know you can do simp only but even then simp only does more than just the rules specified... 
13:22 
JCaesar 
I mean, you can just put the two commands into one subcommand? 
13:22 
JCaesar 
apply(subst foo; rule refl) 
13:26 
JCaesar 
(whether to use , or ; is tricky business. essentially, ; will apply the command after the ; to all subgoals that resulted from the command before. , is a bit more magic to me and someone else shall explain it… I think it is just like sequential application with multiple appl statements) 
13:29 
qertyyyy 
yes , that's what I usually do (with the comma) . I often like to do proofs very explicitly ... so I often write subt [rule] and then "rule refl" which seems a bit redundant (the rule refl part). So I thought that there might be some command which does the rule refl part for me 
14:00 
JCaesar 
hm, just putting .. (no apply or anything) should do that… 
14:08 
pruvisto 
qertyyyy: well, you can just use Isar's "also" command to specifically rewrite only the subterm you're interested in 
15:26 

juanbono joined #isabelle 
15:36 

logicmoo joined #isabelle 
19:59 
qertyyyy 
ok I guess I was too vague , sorry. So I want to proof an equality TermA = TermB and I often do it like this : have TermA = TermC by (subst bla , rule refl) also have "... = TermD " by (subst bla2, rule refl) .... also have "... = TermB" by (subst bla3, rule refl) finally show ?thesis by assumption 
20:01 
qertyyyy 
and that's where all those rule refl are comming from . I know this "problem" would just not exist , if I would just use simp auto etc. I just want to know if there exists exactly what I want .... 
22:29 

dmiles joined #isabelle 
23:26 

Warrigal_ joined #isabelle 