*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Mon, 08 Feb 2010 23:55:01 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B6FE929.8060809@informatik.tu-muenchen.de>*References*: <4B6F1CA6.3080906@cse.unsw.edu.au> <4B6FE929.8060809@informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Dear Florian, Florian Haftmann wrote:

Hi Rafal,After porting my development from slightly pre-2009 to 2009-1, I've noticed that I need to help isabelle out by using '-' more than I used to, for example: case (Cons x xs) hence a: "blah" and a': "blah2" and IH: "someIH" this used to go away by simp or blast, but now I need to say: by - simp or by - blast I expect this for "by - assumption" as assumption doesn't chain in the assumptions, but I find it a little strange that simp no longer does. As this looks intentional, can anyone tell me why this has changed? Also, in my proofs when using force and auto, I've found I need to put in a lot more '!', especially on dest: and intro: arguments, and nearly always when saying "intro: ext". Once again, does anyone remember why this might be?This sounds indeed strange. Somehow erratic proof failures could always occur due to changes in default rules (esp. for classical reasoning), but your description sounds like a "systematic change". Can you provide me more explicit proof text=

I'm attaching my explorations in the area. Regarding more "!": - my memory was faulty with auto, it works pretty much how it used to - force is weaker, needs help with intro and dest more, especially intro!: ext - fast is weaker, needs ! with intro: ext

"Legacy feature! Implicit use of prems in assumption proof"

Sincerely, Rafal Kolanski.

theory BlahSep imports Word begin text {* Trivial setup for a typed heap and separating conjunction *} definition map_disj :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<bottom>" 51) where "h\<^isub>0 \<bottom> h\<^isub>1 \<equiv> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}" types heap_assert = "(32 word \<rightharpoonup> 8 word) \<Rightarrow> bool" constdefs sep_true :: "heap_assert" "sep_true \<equiv> \<lambda>s. True" constdefs sep_false :: "heap_assert" "sep_false \<equiv> \<lambda>s. False" constdefs sep_empty :: "heap_assert" ("\<box>") "\<box> \<equiv> \<lambda>h. h = empty" constdefs sep_conj :: "heap_assert \<Rightarrow> heap_assert \<Rightarrow> heap_assert" (infixr "\<and>\<^sup>*" 35) "P \<and>\<^sup>* Q \<equiv> \<lambda>h. \<exists>h\<^isub>0 h\<^isub>1. h\<^isub>0 \<bottom> h\<^isub>1 \<and> h = h\<^isub>0 ++ h\<^isub>1 \<and> P h\<^isub>0 \<and> Q h\<^isub>1" lemma sep_conjI: "\<lbrakk> P h\<^isub>0 ; Q h\<^isub>1 ; h\<^isub>0 \<bottom> h\<^isub>1 ; h = h\<^isub>0 ++ h\<^isub>1 \<rbrakk> \<Longrightarrow> (P \<and>\<^sup>* Q) h" by (simp add: sep_conj_def, blast) lemma sep_conjD: "(P \<and>\<^sup>* Q) h \<Longrightarrow> \<exists>h\<^isub>0 h\<^isub>1. h\<^isub>0 \<bottom> h\<^isub>1 \<and> h = h\<^isub>0 ++ h\<^isub>1 \<and> P h\<^isub>0 \<and> Q h\<^isub>1" by (simp add: sep_conj_def) lemma sep_true[simp]: "sep_true s" by (simp add: sep_true_def) lemma sep_false[simp]: "\<not>sep_false x" by (simp add: sep_false_def) text {* First example: used to be able to use intro: ext without the exclamation *} lemma sep_conj_false_right: "(P \<and>\<^sup>* sep_false) = sep_false" by (force dest: sep_conjD intro!: ext) (* NOTE: (auto dest: sep_conjD intro!: ext) also works, but needed the exclamation in the past, so that hasn't changed, only force has *) text {* Second example: didn't need any exclamation marks *} lemma sep_conj_exists2: "(P \<and>\<^sup>* (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P \<and>\<^sup>* Q x) s))" by (force intro!: sep_conjI ext dest!: sep_conjD) (* NOTE: same as above, auto can be used, but needs exclamations and also did in the past, probably why we used force here *) text {* Third example: fact chaining and extra "-" *} consts delete :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" lemma sep_conj_foldl_extract: assumes fold: "foldl op \<and>\<^sup>* \<box> Ps s" assumes inP: "P \<in> set Ps" shows "(P \<and>\<^sup>* sep_true) s" proof - let ?rest = "foldl op \<and>\<^sup>* \<box> (delete P Ps)" have notnil: "Ps \<noteq> []" using inP by auto have rewrite: "(foldl op \<and>\<^sup>* \<box> Ps) = (P \<and>\<^sup>* ?rest)" using notnil inP proof (induct Ps arbitrary: P) case Nil thus ?case by simp next case (Cons x xs) hence IH: "\<lbrakk> xs \<noteq> [] ; P \<in> set xs \<rbrakk> \<Longrightarrow> (foldl op \<and>\<^sup>* \<box> xs) = (P \<and>\<^sup>* foldl op \<and>\<^sup>* \<box> (delete P xs))" and in': "P \<in> set (x # xs)" (* These work, and work in slightly-pre-2009: by - assumption by - simp by - blast by auto *) (* And these do not work, but used to: by simp by blast *) (* However, in the old version I'm getting "Legacy feature! Implicit use of prems in assumption proof", so I guess there's my answer. Not sure what's the proper way to write these now. *) by - assumption oops

**Follow-Ups**:**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Lawrence Paulson

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Makarius

**References**:**[isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Rafal Kolanski

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Date: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Previous by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Cl-isabelle-users February 2010 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