MU_Puzzle.thy

theory MU_Puzzle imports Main begin

datatype miu = M | I | U

inductive_set S :: "miu list set" where
  "[M, I] : S" |
  "x @ [I] : S ==> x @ [I, U] : S" |
  "[M] @ x : S ==> [M] @ x @ x : S" |
  "x @ [I, I, I] @ y : S ==> x @ [U] @ y : S" |
  "x @ [U, U] @ y : S ==> x @ y : S"

fun ci :: "miu list => nat" where
  "ci [] = 0" |
  "ci (x#xs) = (if x = I then 1 + (ci xs) else ci xs)"

lemma [rule_format,simp]: "ALL y. ci (x @ y) = ci x + ci y"
apply(induct_tac x)
apply(auto)
done

lemma miu_inv: "x : S ==> (ci x) mod 3 ~= 0"
apply(erule S.induct)
apply(auto)
apply(arith)
done

theorem "[M, U] ~: S"
apply(rule classical)
apply(simp)
apply(drule miu_inv)
apply(simp)
done

end