Alloyでアフィン平面を作ってみた

affine_plane.als

// 2011/10/14 Fri 21:45
// 2011/10/15 Sat 03:04
module AffinePlane

// 点
sig Point {}
// 直線
sig Line {
	pts : some Point
}{
	// 直線は点を2個以上通る(これで表現出来ているのか?)
	#pts > 1
}

// 任意の2点を通る直線がちょうど1つ存在する
pred AffineAxiom1{
	all p1, p2: Point | 
		p1 != p2 => 
			one l :Line | p1 in l.pts and p2 in l.pts
}

// 平行条件
pred Parallel(l : Line , m: Line){
	l = m or
	no p:Point | (p in l.pts) and (p in m.pts)
}

// 任意の直線lとl上にはない任意の点pを与えたとき、pを通りlと交わらない
// 直線hがちょうど一つ存在する
pred AffineAxiom2{
	all l:Line, p:Point | 
		p not in l.pts => 
			one h:Line | p in h.pts and Parallel[l,h]
}

// 同一直線上にない3点が存在する
pred AffineAxiom3{
	some l : Line, p: Point | p not in l.pts
}

// アフィン平面の公理
pred affine_plane {
	AffineAxiom1 
	AffineAxiom2
	AffineAxiom3
}

pred show {
	affine_plane
}

// 例を探す
run show for 10 but 12 Line

// アフィン平面での関係式の確認(反例探し)
// アフィン平面AGの位数がnなら、AGは (n^2, n(n+1), n+1, n, 1)-BIBDである

// 直線上の点の数は位数に等しい
assert 直線上の点の数は全て等しい {
	affine_plane => all l, m : Line | #l.pts = #m.pts
}
check 直線上の点の数は全て等しい

assert 点を通る直線の数は全ての点で等しい {
	affine_plane =>
		all p, q:Point | #{l:Line | p in l.pts} = #{ l:Line | q in l.pts}
}
check 点を通る直線の数は全ての点で等しい

// 本当に確認出来ているのか不安
assert 点の総数はひとつの直線の通る点の数より多い {
	affine_plane => 
		 #Point = #Line
}
check 点の総数はひとつの直線の通る点の数より多い

assert 点の総数は位数の2乗 {
	// かけ算どうすればいいかわからないので
	// 直積集合の要素数で2乗の値を取得
	affine_plane => 
		some l:Line | #pts = #{l.pts -> l.pts}
}
check 点の総数は位数の2乗

assert 直線の総数は位数の2乗と位数の和{
	affine_plane => 
		some l:Line | #Line = #{l.pts -> l.pts} + #l.pts
}
check 直線の総数は位数の2乗と位数の和

// affine平面が作るBIBDの会合数は1
assert 任意の2点についてこれらを同時に持つ直線はひとつだけ {
	affine_plane =>
		all p, q : Point | one l : Line | p in l.pts and q in l.pts
}
check 任意の2点についてこれらを同時に持つ直線はひとつだけ
 
assert 点の出現回数は位数より1多い数 {
	affine_plane =>
		some p:Point, l:Line | #l.pts = #{l:Line | p in l.pts} + 1
}
check 点の出現回数は位数より1多い数