Definition ohne Rekursion, durch Fälle, in Isabelle

Question

Ich versuche, eine unäre Operation auf einem Set stalk x zu definieren, deren typische Elemente der Form germ x U s sind. In diesem Fall gibt es keine Möglichkeit, eine Operation auf allgemeine Dinge des gleichen Typs wie germ x U s in einer Weise zu definieren, die auf das reduziert, was ich will, so dass es so aussieht, als müsste ich wirklich auf eine Definition von Fällen zurückgreifen. Ich habe versucht, die folgenden

definition stalk_mop2 :: "'a ⇒(('a set × 'a) set ⇒ ('a set × 'a) set) " where 
"stalk_mop2 x y = ((λ z . if (∃ U s. y= germ x U s) then 
(germ x U (-⇩a ⇘objectsmap U⇙ s)) else undefined) z) " , 

und bekam die Fehlermeldung, dass U s sind zusätzliche Variablen auf der RHS. Es scheint, als würde Isabelle mit dieser Syntax nicht die Verbindung zwischen der if Hypothese und dem folgenden Begriff herstellen, so dass ich, obwohl ich U und s in der Bedingungsanweisung gebunden habe, die nächsten Vorkommen von U und s (nach then) interpretiert. als freie Variablen.

Was ich wirklich will, ist nur eine Funktion, die x und etwas von der Form germ x U s nimmt und germ x U (-⇩a ⇘objectsmap U⇙ s) zurückgibt. Nichts hier ist rekursiv.

Gibt es einen Weg, um dieses Problem zu umgehen, oder vielleicht eine bessere Möglichkeit, Definitionen von Fällen zu machen, die es mir erlauben zu definieren, was ich will?

Answer 1

Seien Sie sich bewusst, dass dies an der Isabelle-Syntax nichts Fremdes ist, aber es gibt einfach keine Verbindung zwischen der If-Bedingung und den Then-and-Else-Zweigen. Der Umfang des Existenzquantors endet natürlich mit then.

Wenn Sie einen Zeugen für etwas zu erhalten, wollen Sie wissen, existiert, können Sie Hilberts Wahl Operator verwenden, zB SOME (U, s). y = germ x U s) gibt Ihnen ein Paar (U, s) die y = germ x U s erfüllt, wenn ein solches Paar vorhanden ist (die Sie sicher gemacht durch Ihre if-Bedingung) und ist ansonsten nicht definiert.

So wie etwa:

definition stalk_mop2 :: "'a ⇒(('a set × 'a) set ⇒ ('a set × 'a) set)" 
where 
    "stalk_mop2 x y = ((λz . 
    if ∃U s. y = germ x U s then 
     let (U, s) = (SOME (U, s). y = germ x U s) in 
     germ x U (-⇩a ⇘objectsmap U⇙ s) 
    else undefined) z)" 

Update: Sie mehrere let s in einem der folgenden Wege

let x1 = e1 in let x2 = e2 in ... 

oder

let x1 = e1; x2 = e2; ... in ...