File: theorems.tex

package info (click to toggle)
hol88 2.02.19940316-35
  • links: PTS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 65,988 kB
  • ctags: 21,623
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (94 lines) | stat: -rw-r--r-- 2,570 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
\chapter{Pre-proved Theorems}\input{theorems-intro}\section{Definitions}\THEOREM ASCII\_DEF ascii
|- !b0 b1 b2 b3 b4 b5 b6 b7.
    ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
    ABS_ascii(Node(b0,b1,b2,b3,b4,b5,b6,b7)[])
\ENDTHEOREM
\THEOREM ascii\_ISO\_DEF ascii
|- (!a. ABS_ascii(REP_ascii a) = a) /\
   (!r.
     TRP
     (\v tl.
       (?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
       (LENGTH tl = 0))
     r =
     (REP_ascii(ABS_ascii r) = r))
\ENDTHEOREM
\THEOREM ascii\_TY\_DEF ascii
|- ?rep.
    TYPE_DEFINITION
    (TRP
     (\v tl.
       (?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
       (LENGTH tl = 0)))
    rep
\ENDTHEOREM
\THEOREM ``\_DEF string
|- `` = ABS_string(Node(INL one)[]))
\ENDTHEOREM
\THEOREM STRING\_DEF string
|- !a s. STRING a s = ABS_string(Node(INR a)[REP_string s])
\ENDTHEOREM
\THEOREM string\_ISO\_DEF string
|- (!a. ABS_string(REP_string a) = a) /\
   (!r.
     TRP
     (\v tl.
       (v = INL one) /\ (LENGTH tl = 0) \/
       (?a. v = INR a) /\ (LENGTH tl = SUC 0))
     r =
     (REP_string(ABS_string r) = r))
\ENDTHEOREM
\THEOREM string\_TY\_DEF string
|- ?rep.
    TYPE_DEFINITION
    (TRP
     (\v tl.
       (v = INL one) /\ (LENGTH tl = 0) \/
       (?a. v = INR a) /\ (LENGTH tl = SUC 0)))
    rep
\ENDTHEOREM
\section{Theorems}\THEOREM ASCII\_11 ascii
|- !b0 b1 b2 b3 b4 b5 b6 b7 b0' b1' b2' b3' b4' b5' b6' b7'.
    (ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
     ASCII b0' b1' b2' b3' b4' b5' b6' b7') =
    (b0 = b0') /\
    (b1 = b1') /\
    (b2 = b2') /\
    (b3 = b3') /\
    (b4 = b4') /\
    (b5 = b5') /\
    (b6 = b6') /\
    (b7 = b7')
\ENDTHEOREM
\THEOREM ascii\_Axiom ascii
|- !f.
    ?! fn.
     !b0 b1 b2 b3 b4 b5 b6 b7.
      fn(ASCII b0 b1 b2 b3 b4 b5 b6 b7) = f b0 b1 b2 b3 b4 b5 b6 b7
\ENDTHEOREM
\THEOREM ascii\_CASES ascii
|- !a. ?b0 b1 b2 b3 b4 b5 b6 b7. a = ASCII b0 b1 b2 b3 b4 b5 b6 b7
\ENDTHEOREM
\THEOREM ascii\_Induct ascii
|- !P.
    (!b0 b1 b2 b3 b4 b5 b6 b7. P(ASCII b0 b1 b2 b3 b4 b5 b6 b7)) ==>
    (!a. P a)
\ENDTHEOREM
\THEOREM NOT\_EMPTY\_STRING string
|- !a s. ~(STRING a s = ``)
\ENDTHEOREM
\THEOREM NOT\_STRING\_EMPTY string
|- !a s. ~(`` = STRING a s)
\ENDTHEOREM
\THEOREM STRING\_11 string
|- !a s a' s'. (STRING a s = STRING a' s') = (a = a') /\ (s = s')
\ENDTHEOREM
\THEOREM string\_Axiom string
|- !e f. ?! fn. (fn `` = e) /\ (!a s. fn(STRING a s) = f(fn s)a s)
\ENDTHEOREM
\THEOREM string\_CASES string
|- !s. (s = ``) \/ (?s' a. s = STRING a s')
\ENDTHEOREM
\THEOREM string\_Induct string
|- !P. P `` /\ (!s. P s ==> (!a. P(STRING a s))) ==> (!s. P s)
\ENDTHEOREM