*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] \<^bsub> and \<^esub>*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 25 Feb 2015 08:05:36 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a06200764d112b21330ce@[192.168.1.20]>*References*: <a06200751d10980831257@[192.168.1.20]> <54E431C4.4090708@inf.ethz.ch> <a06200755d10a772bc6da@[192.168.1.20]> <54E4CFE2.8020207@inf.ethz.ch> <a06200756d10aa5699d51@[192.168.1.20]> <54E58E70.2040501@inf.ethz.ch> <a06200757d10bc1679a18@[192.168.1.20]> <54E6182D.6080505@inf.ethz.ch> <a0620075ad10d0f36ad42@[192.168.1.20]> <54EAD274.6000702@inf.ethz.ch> <a06200764d112b21330ce@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

a) Your show statement does not match a conclusion of a goal (often there is a typo).

lemma fixes x :: int assumes s: "2 dvd x*x" shows "2 dvd x"

Andreas On 25/02/15 00:41, W. Douglas Maurer wrote:

The annotations in square brackets are called attributes and they have a variety of purposes. In the case of [algebra] and [presburger], they indeed indicate that these rules should be used by these proof methods. From what I know, these two methods reason abstractly, not for concrete numbers like 38. Moreover, I am not familiar with the internals of try or try0. If you want to see whether algebra can solve this, just write "by algebra" and see whether this works, too.In Isabelle2013, try and try0 did not try "algebra", but in Isabelle2014 they do. In the example I gave (lemma "even((38::int)) <--> ((2::int) dvd (38::int))"), try0 indicated that this could be solved by presburger, force, simp, auto, or fastforce. I did try "by algebra" and the error message is: "Failed to apply initial proof method: goal (1 subgoal): 1. even 38 = (2 dvd 38)". Perhaps "algebra" reasons only abstractly, even though presburger does work on a concrete number like 38. Now, to my next issue: I was finally able to get a forward proof by contradiction to work; and then I tried rewriting it using fixes, assumes, and shows, and it no longer works. The proof I wrote was: lemma "2 dvd (x::int)*x ==> 2 dvd (x::int)" proof (rule ccontr) assume 1: "2 dvd (x::int)*x" assume "\not ?thesis" hence "odd(x)" by presburger hence "odd(x*x)" by simp hence "\not (2 dvd (x*x))" by presburger with 1 show False by simp qed This proof went through (here ==> represents \Longrightarrow). (Part of the point of this proof was to illustrate the power of presburger.) But then I tried rewriting the first line of this using fixes, assumes, and shows, like this: lemma fixes x::"int" assumes s: "2 dvd x*x" shows "2 dvd x" and now I get an error message under "show" on the last line (with 1 show False by simp): "Failed to refine any pending goal / Local statement fails to refine any pending goal / Failed attempt to solve goal by exported rule: (2 dvd x * x) ==> (\not 2 dvd x) ==> False". It looks as if "with 1" is not picking up the preceding statement any more, or else that would have been cited as part of the exported rule. Or am I misunderstanding this? And in any event, what do I have to do to get this to work? Thanks! -WDMaurer -- Prof. W. Douglas Maurer Washington, DC 20052, USA Department of Computer Science Tel. (1-202)994-5921 The George Washington University Fax (1-202)994-4875

**References**:**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*W. Douglas Maurer

**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*Andreas Lochbihler

**Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)***From:*Andreas Lochbihler

**Re: [isabelle] \<^bsub> and \<^esub>***From:*Andreas Lochbihler

**Re: [isabelle] \<^bsub> and \<^esub>***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Typo in Tutorial?
- Next by Date: Re: [isabelle] Measure definition on streams
- Previous by Thread: Re: [isabelle] \<^bsub> and \<^esub>
- Next by Thread: [isabelle] Formal semantics for Isar structured proof language
- Cl-isabelle-users February 2015 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