Re: [isabelle] Automatic pair splitting by auto



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

> 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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.