Isabelle에 "Power.thy"의 추가 버전이 있습니까?

Question

Isabelle에서 함수를 정의했습니다. f:'a -> nat 여기서 'a은 monoid (즉, 그룹, 반올림, 반지, 정수 도메인, 필드 등)를 확장하는 일부 대수 구조입니다.

다른 구성에서는 내 유형 'a에 대해이 기능의 출력을 "계수"로 사용하고 싶습니다. 즉, x:'a과 n:nat이라면, 내가 n·x = x + x + ... + x이라는 Isabelle에게 알릴 수있는 몇 가지 작업 인 ·:'a -> nat -> 'a을 사용하고 싶습니다.

조금만 검색하면 "Power.thy"이론을 발견했으며, 어떤면에서는 내가 원하는 것을 수행합니다. 그러나, 그것은 내 문제의 "곱셈 버전"을 위해 그것을한다. 예를 들어 'a을 변경하려는 경우 문제가됩니다. 정수. 이를 사용하면 n·x을 계산하는 대신 Isabelle이 x^n을 수행합니다. "Power.thy"에 대한 유사한 버전이 있습니까? 아니면이 문제를 우회하는 다른 방법이 있습니까?

Answer 1

나는 그런 작업을 구현하는 미리 정의 된 상수의 모르겠지만, 쉽게 사용, 예를 들어, 추가 반복에 의해 구현 될 수있다 comppownat에 : plus가의 추가 작업을 의미

definition scale :: "nat => 'a => 'a" where 
    "scale a n = ((plus a) ^^ n) 0" 

귀하의 구조와 0 중립적 인 요소입니다. Isabelle/HOL의 산술 유형 클래스를 사용하는 경우 정렬 제한 'a :: monoid을 scale의 유형에 추가해야합니다.

이 또한 계수 스케일링 동작을 구현 Complex_Main의 유형 클래스 작업 scaleR이지만, 당신의 구조가 필요한 모든 공리 (유형 클래스 real_vector)을 만족하지 수 있도록이 real 숫자뿐만 아니라 nat들 수 있습니다.

Answer 2

A 본을 표현하는 매우 관용적 인 방법은 곱셈과«of_nat»입니다 :

context semiring_1 
begin 

definition scale :: "nat ⇒ 'a ⇒ 'a" 
    where "scale n = times (of_nat n)" 

lemma [simp]: 
    "scale 0 a = 0" 
    "scale (Suc n) a = a + scale n a" 
    by (simp_all add: scale_def algebra_simps) 

lemma 
    "((plus a) ^^ n) 0 = scale n a" 
    by (induct n) (simp_all) 

end