Skip to content

Instantly share code, notes, and snippets.

@hatsugai
Created April 27, 2021 15:19
Show Gist options
  • Save hatsugai/470dd2691813d711115271a12962abb5 to your computer and use it in GitHub Desktop.
Save hatsugai/470dd2691813d711115271a12962abb5 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment