Einschränkungsvariablen in den Gebietsschemas

Question

Die Isabelle-Bibliothek enthält die Klassen real_inner und real_normed_vector, wobei letztere eine Unterklasse der früheren in ~~src/HOL/Library/Inner_Product.thy ist. Jetzt

Angenommen, wir haben eine locale

locale foo = 
    fixes goo :: "'a::{real_normed_vector} => bool" 

und wollen diese locale mit einigen neuen Konstanten zu erweitern, und auch die Art von 'a Zwang real_inner zugleich zu sein, etwa so:

locale extended = foo + 
    fixes ext :: "'a::{real_inner} => nat" 

Gibt es eine Möglichkeit, dies zu tun? Versucht man dies anhand der obigen Beispiele zu tun, bekommt Isabelle den Typ 'b::{real_normed_vector} => bool in extended, wenn ich stattdessen den Typ 'a::{real_inner} => bool benötige.

Answer 1

Sie können es wie folgt tun:

locale extended = foo goo 
    for goo :: "'a :: real_inner ⇒ bool" + 
    fixes ext :: "'a => nat"