Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-09-05

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

All times shown according to UTC.

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 [substitution-name] 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

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