Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2018 RC3: metis gripes about an "unused" theor...

view this post on Zulip Email Gateway (Aug 22 2022 at 18:10):

From: Michal Wallace <michal.wallace@gmail.com>
Minor quirk:

theory Scratch
imports Main "HOL-Analysis.Polytope"
begin

lemma
assumes 0: "¬affine_dependent C0"
and 1: "¬affine_dependent C1"
and 2: "convex hull C0 = convex hull C1"
and 3: "aff_dim C0 = aff_dim C1"
shows "C0 = C1"
by (metis 0 1 2 3 subsetI subset_antisym
extreme_point_of_convex_hull_affine_independent)

end

Metis: Unused theorems: "local.3"

However, if I remove assumption 3, the proof fails...

Last updated: Apr 25 2024 at 08:20 UTC