*To*: Mark Wassell <mpwassell at gmail.com>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problem with monotonicity proof*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 28 Nov 2016 08:39:28 +0100*In-reply-to*: <CAK0o7cbjeTtTKvnVSn+UZ618x97xYeVCxJE38TtYiq6iEDObCw@mail.gmail.com>*References*: <CAK0o7cbjeTtTKvnVSn+UZ618x97xYeVCxJE38TtYiq6iEDObCw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hi Mark,

(!!x. P x --> Q x) ==> list_all P xs --> list_all Q xs Monotonicity must be expressed using HOL implication and Pure quantification.

Best, Andreas On 26/11/16 15:06, Mark Wassell wrote:

Hello, I have a simple inductive predicate: inductive Q' :: "nat â bool" where Q'0: "Q' 0" | Q'n: "List.list_all (Îk. Q' k) [0..<n] â Q' n" The monotonicity proof for this fails. I take the goal from the error window and prove it: lemma xx [mono]: "mono (Îp x. x = 0 â (ân. x = n â list_all p [0..<n]))" unfolding pred_list_def mono_def proof((rule allI)+,rule impI) fix x and y::"natâbool" assume "xây" show "(Îxa. xa = 0 â (ân. xa = n â Ball (set [0..<n]) x)) â (Îx. x = 0 â (ân. x = n â Ball (set [0..<n]) y))" using âx â yâ by blast qed However the monotonicity proof for the predicate still doesn't work. It has been added to the 'mono' list and if I include the line 'monos xx' after the inductive predicate definition, there is still no proof. The inductive predicate inductive Q :: "nat â bool" where Q0: "Q 0" | Qn: "(âkâset[0..<n]. Q k) â Q n" is ok. I believe that Q' and Q and equivalent. Cheers Mark

**References**:**[isabelle] Problem with monotonicity proof***From:*Mark Wassell

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC3: problem with records
- Next by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have
- Previous by Thread: [isabelle] Problem with monotonicity proof
- Next by Thread: [isabelle] Isabelle2016-1-RC4 available for testing
- Cl-isabelle-users November 2016 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