Skip to content

Instantly share code, notes, and snippets.

@tangentstorm

tangentstorm/failure.thy

Created August 1, 2018 04:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save tangentstorm/72dbd92f72f728ddbc8f162cb448a97b to your computer and use it in GitHub Desktop.
Save tangentstorm/72dbd92f72f728ddbc8f162cb448a97b to your computer and use it in GitHub Desktop.
Download ZIP
how do i do this in isabelle?
Raw
failure.thy
(* how do i do this?? *)
function simplex_count :: "int⇒int⇒int" where
"simplex_count 0 0 = 1" |
"simplex_count 0 1 = 0" |
"simplex_count 1 0 = 2" |
"simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))"
sorry
lemma simplex_count_lemma:
assumes "n simplex S" fixes k assumes "0 ≤ k" and "k ≤ n"
shows "k d_face_count S = simplex_count n k"
sorry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment