Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Automatic pair splitting by auto

view this post on Zulip Email Gateway (Aug 18 2022 at 11:31):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

How can I tell the auto-method NOT to do pair splitting automatically?
E.g. having

consts P::"'a*'a => bool"

lemma test: "!!a. P a \<and> (True --> True)"
apply auto

gives
"!!a b. P (a,b)"

but I need:
!!a. P a

regards and thanks in advance,
Peter

p.s. I could have used simp for this particular example, but for my
actual task, I need auto.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:31):

From: Daniel Wasserrab <wasserrab@uni-passau.de>
Hi Peter,

someone once told me this ML command:

declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
change_claset (fn cs => cs delSWrapper "split_all_tac");
*}

to turn pair splitting off and

declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}

to turn it on again. Worked fine for me.

Daniel

Last updated: May 03 2024 at 08:18 UTC