Re: [isabelle] simplification at the ML level



Hi Clement,

On Thursday 20 April 2006 08:44, Clement.Hurlin at 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)".

- Brian





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