## Stream: General

### Topic: locale

#### Anthony Bordg (Jul 07 2019 at 13:50):

Again, at some point someone should provide some explanations for newcomers about locales in Isabelle. :flashlight:

#### Roland Coghetto (Jul 15 2019 at 09:16):

I don't quite understand the difference between "local" and "class". Do the "local" resemble the notion of Bourbaki-Structure? For example, to encode the classic notion of Group, there is a difference to choose the definition of the notion of Group from "local" or "class"?

#### Anthony Bordg (Jul 15 2019 at 16:47):

@Roland Coghetto It's an excellent question. I don't have a definitive answer. However, my feeling is that for the formalization of mathematics locales should be preferred. I would bet that locales are closer to Bourbaki's structures. It might even be that `class` are deprecated.

#### Lawrence Paulson (Jul 16 2019 at 11:32):

There's a new paper online, From LCF to Isabelle/HOL, where you will find material on axiomatic type classes (Section 4.2) and locales (Section 8.4). Briefly, locales are more general but also more heavyweight in use.

#### Anthony Bordg (Jul 16 2019 at 12:44):

@Roland Coghetto The second half of page 17 in Larry's reference is particularly relevant. They mention explicitly the difference between type class for groups and locale for groups.

#### Roland Coghetto (Jul 16 2019 at 18:18):

Ok thanks but Let us take the following example:
The question: using locales and context, I have difficulty demonstrating these 2 proposals (independently of each other)
lemma two_distinct_points:
"∃ x ::'p. ∃ y :: 'p. x ≠ y"
or
lemma two_distinct_points_bis:
"∃ x y. x ≠ y"

I have, in the proof, the line " then have "x ≠ y" by blast" and after why I can't proof the thesis ?

The code (I cleaned the code to show only the 2 theorems that cause problems.)

section "Tarski's geometry"

theory TARSKI
imports Main
begin

locale TarskiBC =
fixes B :: "'p ⇒ 'p ⇒ 'p ⇒ bool" ("\<between> _ _ _" [99,99,99] 50)
and C :: "'p ⇒ 'p ⇒ 'p ⇒ 'p ⇒ bool" ("_ _ \<congruent> _ _" [99,99,99,99] 50)

locale Tarski1 = TarskiBC +
assumes A1: "∀a b. a b \<congruent> b a"
locale Tarski2 = TarskiBC +
assumes A2: "∀a b p q r s. a b \<congruent> p q ∧ a b \<congruent> r s ⟶ p q \<congruent> r s"
locale Tarski3 = TarskiBC +
assumes A3: "∀a b c. a b \<congruent> c c ⟶ a = b"
locale Tarski4 = TarskiBC +
assumes A4: "∀q a b c. ∃x. \<between> q a x ∧ a x \<congruent> b c"
locale Tarski8 = TarskiBC +
assumes A8: "∃ a b c. ¬ \<between> a b c ∧ ¬\<between> b c a ∧ ¬\<between> c a b"

locale Tarski12 = Tarski1 + Tarski2
locale Tarski123 = Tarski12 + Tarski3
locale Tarski34 = Tarski3 + Tarski4
locale Tarski1234 = Tarski123 + Tarski4

locale Tarski348 = Tarski34 + Tarski8
locale Tarski12348 = Tarski1234 + Tarski8

lemma (in Tarski3) A3':
assumes "a b \<congruent> c c"
shows "a = b"
using A3 assms(1) by blast

theorem (in Tarski12) Satz2p1: (GeoCoq cong_reflexivity)
"a b \<congruent> a b"
using A1 A2 by blast

theorem (in Tarski12) Satz2p2: (GeoCoq cong_symmetry)
assumes "a b \<congruent> c d"
shows "c d \<congruent> a b"
using A2 Satz2p1 assms(1) by blast

theorem (in Tarski34) Satz3p1: (GeoCoq between_trivial)
"\<between> a b b"
using A3' A4 by blast

theorem (in Tarski348) Satz3p13:
shows "∃ a b c. ¬ \<between> a b c ∧ ¬ \<between> b c a ∧ ¬ \<between> c a b ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a"
using A8 Satz3p1 by blast

context Tarski12348
begin

theorem Satz3p14: (* GeoCoq point_construction_different *)
shows "∀ a b. ∃ c. \<between> a b c ∧ b ≠ c"
by (metis (full_types) A3 A4 Tarski34.intro Tarski348.Satz3p13 Tarski348_def Tarski3_axioms Tarski4_axioms Tarski8_axioms Satz2p2)

lemma two_distinct_points:
"∃ x ::'p. ∃ y :: 'p. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then have "x ≠ y" by blast
then show ?thesis sorry
qed

lemma two_distinct_points_bis:
"∃ x y. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then have "x ≠ y" by blast
then show ?thesis sorry
qed

end

#### Anthony Bordg (Jul 16 2019 at 18:42):

@Roland Coghetto simply write

```lemma two_distinct_points:
"∃ x ::'a. ∃ y ::'a. x ≠ y"
proof-
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then show ?thesis by auto
qed
```

or more concisely

```lemma two_distinct_points:
"∃ x ::'a. ∃ y ::'a. x ≠ y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
```

and for the second version

```lemma two_distinct_points_bis:
"∃ x y::'a. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then show ?thesis by auto
qed
```

or more concisely

```lemma two_distinct_points_bis:
"∃ x y::'a. x ≠ y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
```

ok thanks

#### Roland Coghetto (Aug 02 2019 at 14:36):

In the previous example, I reconstructed the locale differently. But I get the following message: "Ambiguous input⌂ produces 15 parse trees (10 displayed):" What does that mean?

#### Mathias Fleury (Aug 02 2019 at 14:49):

Isabelle parses all possible outputs. If only one possible output is correctly typed, you get the warning you have. If more than one is type correct or none is, you get an error

#### Hanna Lachnitt (Aug 02 2019 at 14:51):

Add some parentheses to help Isabelle to find the intended parse tree out of all possible ones
Edit: Mathias was faster :)

Last updated: Dec 07 2023 at 12:30 UTC