Theory TicTacToe

chapter ‹An Application: Tic-Tac-Toe›

theory TicTacToe
imports
  "Alpha_Beta_Pruning.Alpha_Beta_Linear"
begin

text ‹We formalize a general nxn version of tic-tac-toe (noughts and crosses).
The winning condition is very simple: a full horizontal, vertical or diagonal line
occupied by one player.›

text ‹A square is either empty (‹None›) or occupied by one of the two players (‹Some b›).›

type_synonym sq = "bool option"
type_synonym row = "sq list"
type_synonym position = "row list"

text ‹Successor positions:›

fun next_rows :: "sq ⇒ row ⇒ row list" where
"next_rows s' (s#ss) = (if s=None then [s'#ss] else []) @ map ((#) s) (next_rows s' ss)" |
"next_rows _ [] = []"

fun next_poss :: "sq ⇒ position ⇒ position list"  where
"next_poss s' (ss#sss) = map (λss'. ss' # sss) (next_rows s' ss) @ map ((#) ss) (next_poss s' sss)" |
"next_poss _ [] = []"

text ‹A game is won if a full line is occupied by a given square:›

fun diag :: "'a list list ⇒ 'a list" where
"diag ((x#_) # xss) = x # diag (map tl xss)" |
"diag [] = []"

fun lines :: "position ⇒ sq list list" where
"lines sss = diag sss # diag (map rev sss) # sss @ transpose sss"

fun won :: "sq ⇒ position ⇒ bool" where
"won sq pos = (∃ss ∈ set (lines pos). ∀s ∈ set ss. s = sq)"

text ‹How many lines are almost won (i.e. all ‹sq› except one ‹None›)?
Not actually used for heuristic evaluation, too slow.›

fun awon :: "sq ⇒ position ⇒ nat" where
"awon sq sss = length (filter (λss. filter (λs. s≠sq) ss = [None]) (lines sss))"

text ‹The game tree up to a given depth ‹n›.
Trees at depth ‹≥ n› are replaced by ‹Lf 0› for simplicity; no heuristic evaluation.›

fun tree :: "nat ⇒ bool ⇒ position ⇒ ereal tree" where
"tree (Suc n) b pos = (
  if won (Some (¬b)) pos then Lf(if b then -∞ else ∞) ―‹Opponent won›
  else
  case next_poss (Some b) pos of
    [] ⇒ Lf 0  ―‹Draw› |
    poss ⇒ Nd (map (tree n (¬b)) poss))" |
"tree 0 b pos = Lf 0"

definition start :: "nat ⇒ position" where
"start n = replicate n (replicate n None)"


text ‹Now we evaluate the game for small ‹n›.›

text ‹The trivial cases:›

lemma "maxmin (tree 2 True (start 1)) = ∞"
by eval

lemma "maxmin (tree 5 True (start 2)) = ∞"
by eval

text ‹3x3, full game tree (depth=10), no noticeable speedup of alpha-beta.›

lemma "maxmin (tree 10 True (start 3)) = 0"
by eval
lemma "ab_max (-∞) ∞ (tree 10 True (start 3)) = 0"
by eval

text ‹4x4, game tree up to depth 7, alpha-beta noticeably faster.›

lemma "maxmin (tree 7 True (start 4)) = 0"
by eval
lemma "ab_max (-∞) ∞ (tree 7 True (start 4)) = 0"
by eval

end