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

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
  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

Regarding "-" and fact chaining issues, it turns out that the pre-2009 Isabelle does warn me that this is a legacy feature:
	"Legacy feature! Implicit use of prems in assumption proof"
I just don't really get why this is, and how I should be writing my proof instead, what the "sanctioned" way is.

So it's not like there's bugs to report, really, just two proof methods suddenly getting weaker, and a legacy feature I found so intuitive I forgot it was a legacy feature. I'm just curious about the "why" of it.


Rafal Kolanski.
theory BlahSep imports Word begin

text {* Trivial setup for a typed heap and separating conjunction *}

  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 "-"
  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
    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

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