Re: [isabelle] simplification at the ML level
On Thursday 20 April 2006 08:44, Clement.Hurlin at esial.uhp-nancy.fr wrote:
> I woud like to simplify goals having the following pattern : "X ==>
> False" . Like for example simplifying
> ¬ ( (a /= b) \/ (f a = b)) ==> False
> (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
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)".
This archive was generated by a fusion of
Pipermail (Mailman edition) and