我開始學習伊莎貝爾，想試着在伊莎貝爾定義一個幺半羣，但不知道如何。伊莎貝爾的類型參數的歸納謂詞

在勒柯克，我會做這樣的事情：

Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop := 
| axioms: (forall (e: τ), op e i = e) -> 
      (forall (e: τ), op i e = e) -> 
      monoid τ op i.

我不知道該怎麼做同樣的事情在伊莎貝爾。從概念上講，我想到了這樣的事情：

inductive 'a monoid "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where 
    axioms: "⟦f e i = e; f i e = e⟧ ⇒ monoid f i"

但是，這在伊莎貝爾是無效的。

如何在Isabelle中定義帶有輸入參數的歸納謂詞？

來源

2015-02-12 Alex

我對Coq知之甚少，但Isabelle的類型系統卻非常不同。 Isabelle值不會採用「類型參數」，Isabelle類型不會採用「值參數」。

在伊莎貝爾，你的例子是一個簡單的多態的定義，可以這樣做：

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where 
    axioms: "⟦f e i = e; f i e = e⟧ ⟹ monoid f i"

我必須指出，這意味着，如果存在甚至一個e針對此成立，你有一個monoid。你大概意思寫的是

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where 
    axioms: "⟦⋀e. f e i = e; ⋀e. f i e = e⟧ ⟹ monoid f i"

這裏，e普遍在假設量化，這意味着法律必須以構成幺持有所有e。

這樣做是一種歸納定義是可能的，並且具有自動生成適當的引入/排除規則（以及能夠使用inductive_cases生成更多）的優點。但是，還有其他方法。

使用定義

但是，你也可以這樣寫一個簡單的定義：

definition monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" where 
    "monoid f i = ((∀e. f e i = e) ∧ (∀e. f i e = e))"

這給你的monoid定義爲引理monoid_def。如果你想要引入/消除規則，你必須自己派生它們。

使用區域設置

第三，也可能是最合適的解決方案是，區域設置。語言環境是一種在上下文和原因的背景下保留某些固定變量和假設的方法。以下示例演示如何將monoid定義爲語言環境，派生該語言環境中的引理，然後解釋具體示例monoid（即列表）的語言環境，並使用我們在語言環境中爲他們證明的引理。

locale monoid = 
    fixes i :: 'a and f :: "'a ⇒ 'a ⇒ 'a" 
    assumes left_neutral: "f i e = e" 
     and right_neutral: "f e i = e" 
begin 
    lemma neutral_unique_left: 
    assumes "⋀e. f i' e = e" 
    shows "i' = i" 
    proof- 
    from right_neutral have "i' = f i' i" by simp 
    also from assms have "f i' i = i" by simp 
    finally show "i' = i" . 
    qed 
end 

thm monoid.neutral_unique_left 
(* Output: monoid i f ⟹ (⋀e. f i' e = e) ⟹ i' = i *) 

(* Let's interpret our monoid for the type "'a list", with [] 
    as neutral element and concatenation (_ @ _) as the operation. *) 
interpretation list_monoid: monoid "[]" "λxs ys. xs @ ys" 
    by default simp_all 

thm list_monoid.neutral_unique_left 
(* Output: (⋀e. i' @ e = e) ⟹ i' = [] *)

使用類型類

第四種可能性，其類似於語言環境，它這種類型的類。伊莎貝爾支持類型類（像那些在Haskell，儘管更嚴格的），你可以創建一個monoid類型的類，然後實例它的具體類型，如nat，int，'a list等

伊莎貝爾的類型參數的歸納謂詞

回答

使用定義

使用區域設置

使用類型類

更多信息

伊莎貝爾的類型參數的歸納謂詞

回答

使用定義

使用區域設置

使用類型類

更多信息

相關問題