Re: [isabelle] Announcing Isabelle2013-2



By the way, I've made an error as I forget the “for” part in the sample case which I noticed it in the real case when I failed with a proof. I fixed the sample in the while to see if it behave the same, and it differs. With this case, the issue does not occur. The original case is still an issue, as it should behave correctly in all circumstances, even with definitions not written as intended.

Test_2.thy (also as attached file):

    theory Test_2
    imports BNF
    begin

      declare [[rule_trace]]

      type_synonym 'a pp = "['a, 'a] ⇒ bool"

      inductive ppinduct :: "'a pp ⇒ 'a list pp" for f where
        r1: "ppinduct f [] []"
      | r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 # t2)"

      lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2

    end


Le Sat, 21 Dec 2013 08:24:02 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:

Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius
<makarius at sketis.net> a écrit:

Isabelle2013-2 is now available.

I found what is I believe an issue with Sledgehammer and its “Isar proofs”
option.

In the test theory below (also as attached file), if I move the caret next
to “using r1 r2” then in the Sledgehammer pan, check “Isar proofs”, then
click “Apply”, something strange happens: if first run up to displaying a
proof, then something appears in the output pan saying “ENTER MATCH”, then
the content in the Sledgehammer pan disappears then the content of the
output pan is back to what is was just before it displayed “ENTER MATCH”
and Sledgehammer continue running and cannot be stopped with “Cancel”.

The issue does not occur if “Isar proofs” is not checked.

Test.thy:

     theory Test
     imports BNF
     begin

       declare [[rule_trace]]

       type_synonym 'a pp = "['a, 'a] ⇒ bool"

       inductive ppinduct :: "'a pp ⇒ 'a list pp" where
         r1: "ppinduct _ [] []"
| r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 # t2)"

       lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2

     end




--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Attachment: Test_2.thy
Description: Binary data



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