Permalink
Browse files

Remove proof of two pointless lemmas from tutorial

  • Loading branch information...
myreen committed Jan 11, 2019
1 parent 345d8b1 commit 521e6395b158b55e21d5f58094042d573dcb5a78
Showing with 0 additions and 24 deletions.
  1. +0 −12 tutorial/solutions/wordfreqProgScript.sml
  2. +0 −12 tutorial/wordfreqProgScript.sml
@@ -34,18 +34,6 @@ val insert_line_def = Define`

(* and their verification *)

Theorem key_set_compare_unique[simp]
`key_set compare k = {k}`
(rw[key_set_def,EXTENSION] \\
metis_tac[TotOrd_compare,totoTheory.TotOrd]);

Theorem IMAGE_key_set_compare_inj[simp]
`IMAGE (key_set compare) s1 = IMAGE (key_set compare) s2 ⇔ s1 = s2`
(rw[EQ_IMP_THM]
\\ fs[Once EXTENSION]
\\ fs[EQ_IMP_THM] \\ rw[]
\\ res_tac \\ fs[]);

Theorem lookup0_insert
`map_ok t ⇒
lookup0 k (insert t k' v) =
@@ -34,18 +34,6 @@ val insert_line_def = Define`

(* and their verification *)

Theorem key_set_compare_unique[simp]
`key_set compare k = {k}`
(rw[key_set_def,EXTENSION] \\
metis_tac[TotOrd_compare,totoTheory.TotOrd]);

Theorem IMAGE_key_set_compare_inj[simp]
`IMAGE (key_set compare) s1 = IMAGE (key_set compare) s2 ⇔ s1 = s2`
(rw[EQ_IMP_THM]
\\ fs[Once EXTENSION]
\\ fs[EQ_IMP_THM] \\ rw[]
\\ res_tac \\ fs[]);

Theorem lookup0_insert
`map_ok t ⇒
lookup0 k (insert t k' v) =

0 comments on commit 521e639

Please sign in to comment.