Package char-thm: Properties of Unicode characters
Information
| name | char-thm |
| version | 1.6 |
| description | Properties of Unicode characters |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2011-11-30 |
| requires | bool pair char-def |
| show | Data.Bool Data.Byte Data.Char Data.Pair Data.Word16 |
Files
- Package tarball char-thm-1.6.tgz
- Theory file char-thm.thy (included in the package tarball)
Theorems
⊦ ∀pos. ∃w. pos = mkPosition w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b
⊦ ∀pos. ∃w. pos = mkPosition w ∧ destPosition pos = w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b ∧ destPlane pl = b
⊦ ∀c. ∃pl pos. isChar (pl, pos) ∧ c = mkChar (pl, pos)
⊦ ∀c.
∃pl pos.
isChar (pl, pos) ∧ c = mkChar (pl, pos) ∧ destChar c = (pl, pos)
Input Type Operators
- →
- bool
- Data
- Byte
- byte
- Char
- char
- plane
- position
- Pair
- ×
- Word16
- word16
- Byte
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- T
- Char
- destChar
- destPlane
- destPosition
- isChar
- isPlane
- mkChar
- mkPlane
- mkPosition
- Pair
- ,
- fst
- snd
- Bool
Assumptions
⊦ T
⊦ (∀) = λp. p = λx. T
⊦ ∀t. T ∧ t ⇔ t
⊦ ∀a. mkChar (destChar a) = a
⊦ ∀a. mkPlane (destPlane a) = a
⊦ ∀a. mkPosition (destPosition a) = a
⊦ ∀r. destPosition (mkPosition r) = r
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀x. (fst x, snd x) = x
⊦ ∀r. isPlane r ⇔ destPlane (mkPlane r) = r
⊦ ∀r. isChar r ⇔ destChar (mkChar r) = r
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q