Structure string_encodingTheory
signature string_encodingTheory =
sig
type thm = Thm.thm
(* Definitions *)
val char_decode_def : thm
val char_encode_def : thm
val del_to_char_def : thm
val delimiter_BIJ : thm
val delimiter_CASE : thm
val delimiter_TY_DEF : thm
val delimiter_size_def : thm
val delopt_to_str_def : thm
val strencode_def : thm
(* Theorems *)
val char_decode_encode : thm
val char_decode_reduces : thm
val char_encode_isPrintable : thm
val datatype_delimiter : thm
val delimiter2num_11 : thm
val delimiter2num_ONTO : thm
val delimiter2num_num2delimiter : thm
val delimiter2num_thm : thm
val delimiter_Axiom : thm
val delimiter_EQ_delimiter : thm
val delimiter_case_cong : thm
val delimiter_case_def : thm
val delimiter_case_eq : thm
val delimiter_distinct : thm
val delimiter_induction : thm
val delimiter_nchotomy : thm
val num2delimiter_11 : thm
val num2delimiter_ONTO : thm
val num2delimiter_delimiter2num : thm
val num2delimiter_thm : thm
val strdecode_def : thm
val strdecode_ind : thm
val strdecode_strencode : thm
val strdecode_strencode_tail_delimited : thm
val strencode_isPrintable : thm
val string_encoding_grammars : type_grammar.grammar * term_grammar.grammar
(*
[ASCIInumbers] Parent theory of "string_encoding"
[char_decode_def] Definition
⊢ (∀delopt. char_decode delopt "" = NONE) ∧
∀delopt c s.
char_decode delopt (STRING c s) =
if c = #"\\" then
case s of
"" => NONE
| STRING #"n" stl => SOME (#"\n",stl)
| STRING #"t" stl => SOME (#"\t",stl)
| STRING #"\\" stl => SOME (#"\\",stl)
| STRING c2 stl =>
if isDigit c2 then
(let
d23 = TAKE 2 stl
in
if STRLEN d23 = 2 ∧ EVERY isDigit d23 then
(let
n = toNum (STRING c2 d23)
in
if n < 256 then SOME (CHR n,DROP 2 stl) else NONE)
else NONE)
else
case delopt of
NONE => NONE
| SOME d =>
if del_to_char d = c2 then SOME (c2,stl) else NONE
else if isPrint c then
case delopt of
NONE => SOME (c,s)
| SOME d => if del_to_char d = c then NONE else SOME (c,s)
else NONE
[char_encode_def] Definition
⊢ ∀delopt c.
char_encode delopt c =
if ¬isPrint c then
if c = #"\n" then "\\n"
else if c = #"\t" then "\\t"
else if ORD c < 10 then STRCAT "\\00" (toString (ORD c))
else if ORD c < 100 then STRCAT "\\0" (toString (ORD c))
else STRCAT "\\" (toString (ORD c))
else if c = #"\\" then "\\\\"
else
case delopt of
NONE => STRING c ""
| SOME d =>
if c = del_to_char d then STRCAT "\\" (STRING c "")
else STRING c ""
[del_to_char_def] Definition
⊢ del_to_char DQ = #"\"" ∧ del_to_char SQ = #"'" ∧
del_to_char PIPE = #"|"
[delimiter_BIJ] Definition
⊢ (∀a. num2delimiter (delimiter2num a) = a) ∧
∀r. (λn. n < 3) r ⇔ delimiter2num (num2delimiter r) = r
[delimiter_CASE] Definition
⊢ ∀x v0 v1 v2.
(case x of DQ => v0 | SQ => v1 | PIPE => v2) =
(λm. if m < 1 then v0 else if m = 1 then v1 else v2)
(delimiter2num x)
[delimiter_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION (λn. n < 3) rep
[delimiter_size_def] Definition
⊢ ∀x. delimiter_size x = 0
[delopt_to_str_def] Definition
⊢ delopt_to_str NONE = "" ∧
∀d. delopt_to_str (SOME d) = STRING (del_to_char d) ""
[strencode_def] Definition
⊢ ∀delopt s. strencode delopt s = CONCAT (MAP (char_encode delopt) s)
[char_decode_encode] Theorem
⊢ char_decode delopt (STRCAT (char_encode delopt c) s) = SOME (c,s)
[char_decode_reduces] Theorem
⊢ char_decode delopt s = SOME (c,s') ⇒ STRLEN s' < STRLEN s
[char_encode_isPrintable] Theorem
⊢ EVERY isPrint (char_encode delopt c)
[datatype_delimiter] Theorem
⊢ DATATYPE (delimiter DQ SQ PIPE)
[delimiter2num_11] Theorem
⊢ ∀a a'. delimiter2num a = delimiter2num a' ⇔ a = a'
[delimiter2num_ONTO] Theorem
⊢ ∀r. r < 3 ⇔ ∃a. r = delimiter2num a
[delimiter2num_num2delimiter] Theorem
⊢ ∀r. r < 3 ⇔ delimiter2num (num2delimiter r) = r
[delimiter2num_thm] Theorem
⊢ delimiter2num DQ = 0 ∧ delimiter2num SQ = 1 ∧
delimiter2num PIPE = 2
[delimiter_Axiom] Theorem
⊢ ∀x0 x1 x2. ∃f. f DQ = x0 ∧ f SQ = x1 ∧ f PIPE = x2
[delimiter_EQ_delimiter] Theorem
⊢ ∀a a'. a = a' ⇔ delimiter2num a = delimiter2num a'
[delimiter_case_cong] Theorem
⊢ ∀M M' v0 v1 v2.
M = M' ∧ (M' = DQ ⇒ v0 = v0') ∧ (M' = SQ ⇒ v1 = v1') ∧
(M' = PIPE ⇒ v2 = v2') ⇒
(case M of DQ => v0 | SQ => v1 | PIPE => v2) =
case M' of DQ => v0' | SQ => v1' | PIPE => v2'
[delimiter_case_def] Theorem
⊢ (∀v0 v1 v2. (case DQ of DQ => v0 | SQ => v1 | PIPE => v2) = v0) ∧
(∀v0 v1 v2. (case SQ of DQ => v0 | SQ => v1 | PIPE => v2) = v1) ∧
∀v0 v1 v2. (case PIPE of DQ => v0 | SQ => v1 | PIPE => v2) = v2
[delimiter_case_eq] Theorem
⊢ (case x of DQ => v0 | SQ => v1 | PIPE => v2) = v ⇔
x = DQ ∧ v0 = v ∨ x = SQ ∧ v1 = v ∨ x = PIPE ∧ v2 = v
[delimiter_distinct] Theorem
⊢ DQ ≠ SQ ∧ DQ ≠ PIPE ∧ SQ ≠ PIPE
[delimiter_induction] Theorem
⊢ ∀P. P DQ ∧ P PIPE ∧ P SQ ⇒ ∀a. P a
[delimiter_nchotomy] Theorem
⊢ ∀a. a = DQ ∨ a = SQ ∨ a = PIPE
[num2delimiter_11] Theorem
⊢ ∀r r'.
r < 3 ⇒ r' < 3 ⇒ (num2delimiter r = num2delimiter r' ⇔ r = r')
[num2delimiter_ONTO] Theorem
⊢ ∀a. ∃r. a = num2delimiter r ∧ r < 3
[num2delimiter_delimiter2num] Theorem
⊢ ∀a. num2delimiter (delimiter2num a) = a
[num2delimiter_thm] Theorem
⊢ num2delimiter 0 = DQ ∧ num2delimiter 1 = SQ ∧
num2delimiter 2 = PIPE
[strdecode_def] Theorem
⊢ ∀s delopt.
strdecode delopt s =
case char_decode delopt s of
NONE =>
(case (s,delopt) of
("",v1) => SOME ("","")
| (STRING c tl,NONE) => NONE
| (STRING c tl,SOME d) =>
if c = del_to_char d then SOME ("",STRING c tl) else NONE)
| SOME (c,rest) =>
OPTION_MAP (STRING c ## I) (strdecode delopt rest)
[strdecode_ind] Theorem
⊢ ∀P. (∀delopt s.
(∀v2 c rest.
char_decode delopt s = SOME v2 ∧ v2 = (c,rest) ⇒
P delopt rest) ⇒
P delopt s) ⇒
∀v v1. P v v1
[strdecode_strencode] Theorem
⊢ strdecode delopt (strencode delopt s) = SOME (s,"")
[strdecode_strencode_tail_delimited] Theorem
⊢ strdecode delopt
(STRCAT (strencode delopt s) (delopt_to_str delopt)) =
SOME (s,delopt_to_str delopt)
[strencode_isPrintable] Theorem
⊢ EVERY isPrint (strencode delopt s)
*)
end
HOL 4, Trindemossen-1