*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] [ForMaRE] Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]*From*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Date*: Thu, 22 Nov 2012 17:54:47 +0000*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <50AE4BDF.2070302@cs.bham.ac.uk>*Organization*: University of Birmingham*References*: <50916DB3.4030707@cs.bham.ac.uk> <B342CF2B-EEC3-4932-A98D-193702F57A14@cam.ac.uk> <5091CE53.6020006@cs.bham.ac.uk> <C76381F2-5127-48DF-B198-DE2B3AABEAB1@cam.ac.uk> <509271BB.5070705@cs.bham.ac.uk> <3C709666-94F3-4882-A3F3-2749C3E0DB3D@cam.ac.uk> <CCD547CD67BE55438725862FF2FA601302A294C338B2@CSSEMAIL2.adf.bham.ac.uk> <50944479.1080201@in.tum.de> <50AE4BDF.2070302@cs.bham.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121029 Thunderbird/16.0.1

2012-11-22 15:59 Christoph LANGE:

2012-11-02 22:08 Tobias Nipkow:It may still be a bit simpler to write "1<=i & i <=n" instead of "in_range n i" - no need to expand in_range. In general it is a good idea not to invent new constants for existing concepts: "in_range n i" is actually the same as "i : {1..n}".I have now followed your advice; thanks! Another advantage that is important to us is that it makes the code more readable. Overall it helped simplifying my formalisation; however there were some surprises.

Cheers, Christoph -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Enabling Domain Experts to use Formalised Reasoning @ AISB 2013 2–5 April 2013, Exeter, UK. Deadlines 10 Dec (stage 1), 14 Jan (st. 2) http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

theory in_range imports Main Real begin type_synonym real_vector = "nat \<Rightarrow> real" definition in_range :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "in_range n i \<equiv> 1 \<le> i \<and> i \<le> n" definition non_negative_real_vector :: "nat \<Rightarrow> real_vector \<Rightarrow> bool" where "non_negative_real_vector n v \<equiv> \<forall> i::nat . i \<in> {1..n} \<longrightarrow> v i \<ge> 0" fun maximum :: "nat \<Rightarrow> real_vector \<Rightarrow> real" where "maximum 0 _ = 0" | (* In our setting with non-negative real numbers it makes sense to define the maximum of the empty set as 0 *) "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" (* we don't enforce that y is non-negative, but this computation only makes sense for a non-negative y *) lemma maximum_sufficient : fixes n::nat and y::real_vector and m::real assumes non_negative: "non_negative_real_vector n y" and non_empty: "n > 0" and greater_or_equal: "\<forall> i::nat . i \<in> {1..n} \<longrightarrow> m \<ge> y i" and is_component: "\<exists> i::nat . i \<in> {1..n} \<and> m = y i" shows "m = maximum n y" using assms proof (induct n) case 0 show ?case sorry next case (Suc n) (* removed some steps *) have "maximum (Suc n) y = m" proof (cases "n = 0") case True show ?thesis sorry next case False show ?thesis proof (cases "y (Suc n) = m") case True show ?thesis sorry next case False (* The following doesn't work: with Suc.prems(4) have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k" by auto Therefore we have to use the auxiliary predicate in_range: *) from Suc.prems(4) have "\<exists>i::nat . in_range (Suc n) i \<and> m = y i" unfolding in_range_def by simp with False have "\<exists>k::nat . in_range n k \<and> m = y k" unfolding in_range_def by (metis le_antisym not_less_eq_eq) (* Sledgehammer fails to prove the former when in_range is defined using i \<in> {1..n}; we need the form 1 \<le> i \<and> i \<le> n *) then have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k" unfolding in_range_def by simp (* OK, we got what we wanted. *) show ?thesis sorry qed qed show ?case sorry qed end

**References**:**[isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Previous by Thread: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Thread: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Cl-isabelle-users November 2012 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