*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Isabelle Foundation & Certification*From*: Holger Blasum <hbl at sysgo.com>*Date*: Thu, 17 Sep 2015 08:14:27 +0200*Cc*: Peter Lammich <lammich at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <6F85EB11-F2CC-47EE-924E-ED0A603E4A11@cam.ac.uk>*References*: <A3211BFC-696D-4616-AAD4-1E916B859A78@lri.fr> <1442414316.21093.50.camel@lapnipkow10> <9FDB3389-19DA-4B4D-9BAE-D3D9F51E2C8F@cam.ac.uk> <1442417943.21093.75.camel@lapnipkow10> <6F85EB11-F2CC-47EE-924E-ED0A603E4A11@cam.ac.uk>

Hello Larry, list, On 09-16, Larry Paulson wrote: > It would be interesting to find out how these problems were identified: whether they were looked for out of curiosity, or whether on the other hand they manifested themselves in the course of an actual proof. I can give more detail for the case of EURO-MILS: We were made aware of "Isabelle Isar-Reference Manual (Version 2013-2, pp. 103): "It is at the discretion of the user to avoid malformed theory specifications!"[1] Hence first attempt was to rule out use of "consts"[2]. This resulted in people even becoming more curious and playing with Kuncar/Popescu. Moreover, it has been pointed out that even if we rule out "consts" and "defs" in our theories then it is still used e.g. in HOL.thy[3] (probably without overloading, but it is hard to judge for me). The task at hand is not only convincing ourselves (arguably when proving some property oneself one usually/sometimes gets a feeling for what is correct and what not) but also others (who have limited resources). To give an example: in attached System_Is_Secure.thy the first derivation of "System_Is_Secure" (theorem System_Is_Secure_1) forces to make the assumptions of "A" and "~A" obvious. This makes it harder to cheat ourselves or others. The second derivation of "System_Is_Secure" (theorem System_Is_Secure_2) hides the assumptions and could be more easy be overlooked. My working understanding is (correct if that is wrong!) that fixing Isabelle would rule out hidden derivations such as System_Is_Secure_2. [1] http://isabelle.in.tum.de/doc/isar-ref.pdf p 121 The (unchecked) option disables global dependency checks for this def- inition, which is occasionally useful for exotic overloading. It is at the discretion of the user to avoid malformed theory specifications! [2] http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf Section 3.1 "Constants. The Isabelle consts command is not used." [3] http://afp.sourceforge.net/browser_info/current/HOL/HOL/HOL.html search for "defs" ---------(inlined: System_Is_Secure.thy, also attached) theory System_Is_Secure imports Main begin consts A :: bool consts System_Is_Secure :: bool (* formulation with explicit assumptions, easy for reviewer to spot that user made too strong assumptions *) theorem System_Is_Secure_1: assumes "A" and "~ A" shows System_Is_Secure proof- from assms show ?thesis by simp qed (* Kuncar/Popescu: A Consistent Foundation for Isabelle/HOL, ITP 2015 *) consts c :: bool typedef T = "{True, c}" by blast defs c_bool_def: "c::bool == ~ (ALL(x::T) y. x = y)" lemma L: "(ALL(x::T) y. x = y) <-> c" using Rep_T Rep_T_inject Abs_T_inject by blast lemma MyFalse: False using L unfolding c_bool_def by auto theorem MySystem_Is_Secure [simp]: System_Is_Secure using MyFalse by simp (* formulation with implicit assumptions, not that easy for reviewer to spot that user made too strong assumptions *) theorem System_Is_Secure_2: System_Is_Secure by simp end best, -- Holger

**Follow-Ups**:**Re: [isabelle] Isabelle Foundation & Certification***From:*Holger Blasum

**Re: [isabelle] Isabelle Foundation & Certification***From:*Larry Paulson

**References**:**[isabelle] Isabelle Foundation & Certification***From:*Burkhart Wolff

**Re: [isabelle] Isabelle Foundation & Certification***From:*Peter Lammich

**Re: [isabelle] Isabelle Foundation & Certification***From:*Larry Paulson

**Re: [isabelle] Isabelle Foundation & Certification***From:*Peter Lammich

**Re: [isabelle] Isabelle Foundation & Certification***From:*Larry Paulson

- Previous by Date: Re: [isabelle] Isabelle Foundation & Certification
- Next by Date: Re: [isabelle] Isabelle Foundation & Certification
- Previous by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Next by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Cl-isabelle-users September 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