*To*: Clement.Hurlin at esial.uhp-nancy.fr*Subject*: Re: [isabelle] simplification at the ML level*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Mon, 24 Apr 2006 11:09:02 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20060420174442.hiu3s8cvlwkgw4os@venus.esial.uhp-nancy.fr>*References*: <20060420174442.hiu3s8cvlwkgw4os@venus.esial.uhp-nancy.fr>*User-agent*: KMail/1.8

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

**References**:**[isabelle] simplification at the ML level***From:*Clement . Hurlin

- Previous by Date: [isabelle] 2nd CFP: 3rd International Verification Workshop, VERIFY'06
- Next by Date: Re: [isabelle] Transitioning between ZF and HOL
- Previous by Thread: Re: [isabelle] simplification at the ML level
- Next by Thread: [isabelle] Transitioning between ZF and HOL
- Cl-isabelle-users April 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list