Isabelleで再帰を使わない定義

Question

私は、stalk xの単項演算を定義しようとしています。その典型的な要素の形式はgerm x U sです。この場合、同じタイプの一般的なものに対して操作を定義する方法はありません。つまり、私が望むものに減らす方法でgerm x U sを定義する方法はありません。したがって、実際にはケースで定義する必要があるようです。私は、次の

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) " , 

を試みたとU sはRHS上の余分な変数であることを示すエラーメッセージが表示されました。私は条件文でUとsを結合しなかったが、それは明らかに（then後）Uとsの次の出現を解釈するように、この構文を使用することにより、イザベルは、if仮説と、次の用語との間の接続を行わないように思えます自由変数として。

私が本当に欲しいのは、という形式のものと、germ x U sの何らかの形をとり、germ x U (-⇩a ⇘objectsmap U⇙ s)を返す関数です。ここでは再帰的なものはありません。

この問題を回避する方法がありますか、または私が欲しいものを定義できるケースで定義するのが良い方法でしょうか？

Answer 1

これはIsabelleの構文については何も変わりありませんが、if-conditionとthen-およびelse-ブランチの間には接続がないことに注意してください。実在限定子のスコープは当然thenで終わります。

あなたは例えば、ヒルベルトの選択演算子を使用することができ、あなたが存在することがわかっている何かのために証人を取得したい場合は、このようなペアは、あなたの場合、条件によって確認しました（存在する場合、SOME (U, s). y = germ x U s)はあなたに満足しy = germ x U sペア(U, s)を与えます）、それ以外の場合は未定義です。

だから、どのくらいの：

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)" 

更新：あなたは

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

または

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