Email Gateway (Aug 17 2022 at 14:16): Email Gateway (Aug 17 2022 at 14:16):From: Clement.Hurlin@esial.uhp-nancy.fr
Hello,
I woud like to simplify goals having the following pattern : "X ==> False" .
Like for example simplifying
¬ ( (a /= b) \/ (f a = b)) ==> False
to
(a = b /\ f b /= b) ==> False
(at the ML level) But the Simp_tac tactic fails, I guess because it
works from bottom to up.
What should I use ?
Another problem I'm running into is that I want to simplify goal
without implicitly applying assumption too. For example I would like
to get
"X ==> X" from " X ==> X"
At the proof general level, using "simp" is too strong and finishs the
proof in 1 step. Using "simp (no_asm)" only simplifies the right hand
side which is not what I want too. I'm maybe confused by the term
"assumption" sometimes refering to the hypothesis, sometimes refering
to the "assumption" tactic.
And what about that at the ML level ?
Thanks for your help,
Clément
Email Gateway (Aug 17 2022 at 14:16):From: Tjark Weber <tjark.weber@gmx.de>
Clément,
if you just need CNF conversion, I suggest you take a look at the existing
code in HOL/Tools/cnf_funcs.ML, and also in HOL/Tools/meson.ML.
Best,
Tjark
Email Gateway (Aug 17 2022 at 14:16):From: Brian Huffman <brianh@csee.ogi.edu>
Hi Clement,
On Thursday 20 April 2006 08:44, Clement.Hurlin@esial.uhp-nancy.fr wrote:
Hello,
I woud like to simplify goals having the following pattern : "X ==>
False" . Like for example simplifying
¬ ( (a /= b) \/ (f a = b)) ==> False
to
(a = b /\ f b /= b) ==> False(at the ML level) But the Simp_tac tactic fails, I guess because it
works from bottom to up.
What should I use ?
In addition to Simp_tac, the following variations are also available:
Asm_simp_tac, Full_simp_tac, Asm_lr_simp_tac, and Asm_full_simp_tac. They are
defined in Pure/simplifier.ML in the Isabelle sources. They each call the
generic simplifier tactic with different sets of flags. (These lower-case
versions are basically the same as the upper-case ones but take a simpset as
an argument.)
val simp_tac = generic_simp_tac false (false, false, false);
val asm_simp_tac = generic_simp_tac false (false, true, false);
val full_simp_tac = generic_simp_tac false (true, false, false);
val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
Each variation has a "mode" with three boolean flags, which control:
1) whether to simplify premises;
2) whether to use premises as additional simp rules;
3) whether to allow later premises to simplify earlier ones.
In your case, it seems that you want to simplify the premises, but without
using the premises to simplify the conclusion: You should use Full_simp_tac.
Another problem I'm running into is that I want to simplify goal
without implicitly applying assumption too. For example I would like
to get
"X ==> X" from "X ==>X"
At the proof general level, using "simp" is too strong and finishs the
proof in 1 step. Using "simp (no_asm)" only simplifies the right hand
side which is not what I want too. I'm maybe confused by the term
"assumption" sometimes refering to the hypothesis, sometimes refering
to the "assumption" tactic.
In theory files, using "simp" is like Asm_full_simp_tac, "simp (no_asm)" is
like Simp_tac, "simp (no_asm_simp)" is like Asm_simp_tac, and "simp
(no_asm_use)" is like Full_simp_tac. These simp options are described in the
Isabelle Tutorial, section 3.1.5.
In your case, it seems that you would want "simp (no_asm_use)".
Last updated: May 03 2024 at 04:19 UTC