/
onelineScript.sml
145 lines (117 loc) · 3.99 KB
/
onelineScript.sml
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
open HolKernel Parse boolLib bossLib;
val _ = new_theory "oneline";
Definition ZIP2:
(ZIP2 ([],[]) z = []) /\
(ZIP2 (x::xs,y::ys) z = (x,y) :: ZIP2 (xs, ys) (5:num))
Termination
WF_REL_TAC ‘measure (\p. LENGTH (FST (FST p)) + LENGTH (SND (FST p)))’ >>
simp[]
End
fun is_oneline th =
let val cs = th |> concl |> strip_conj
in
length cs = 1 andalso is_eq (hd cs)
end
val oneline_zip2 = DefnBase.one_line_ify NONE ZIP2
val _ = assert
(fn l => length l = 1 andalso is_disj (hd l))
(hyp oneline_zip2)
val _ = assert is_oneline oneline_zip2
Definition AEVERY_AUX_def:
(AEVERY_AUX aux P [] <=> T) /\
(AEVERY_AUX aux P ((x:'a,y:'b)::xs) <=>
if MEM x aux then AEVERY_AUX aux P xs
else
P (x,y) /\ AEVERY_AUX (x::aux) P xs)
End
Theorem oneline_aevery_aux[local] = DefnBase.one_line_ify NONE AEVERY_AUX_def
val _ = assert (null o hyp) oneline_aevery_aux
val _ = assert is_oneline oneline_aevery_aux
Definition incomplete_literal:
incomplete_literal 1 = 10 /\
incomplete_literal 2 = 11 /\
incomplete_literal 3 = 30
End
val oneline_incomplete = DefnBase.one_line_ify NONE incomplete_literal
val (theta, _) = match_term
“incomplete_literal svar =
case svar of 1 => 10 | 2 => 11 | 3 => 30 | _ => ARB”
(concl oneline_incomplete)
val _ = length (hyp oneline_incomplete) = 1 andalso
aconv (hd (hyp oneline_incomplete))
(subst theta “svar = 1 \/ svar = 2 \/ svar = 3”) orelse
raise Fail "incomplete_literal test fails"
Definition complete_literal0:
complete_literal0 1 = 10 /\
complete_literal0 2 = 12 /\
complete_literal0 _ = 15
End
Theorem oneline_complete0[local] = DefnBase.one_line_ify NONE complete_literal0
val _ = assert is_oneline oneline_complete0
val _ = assert (null o hyp) oneline_complete0
Definition complete_literal1a:
complete_literal1a [] 1 = 10 /\
complete_literal1a (3::t) 2 = 16 /\
complete_literal1a (h::t) 2 = 12 + h /\
complete_literal1a _ _ = 15
End
Theorem oneline_complete1a[local] =
DefnBase.one_line_ify NONE complete_literal1a
val _ = assert null (hyp oneline_complete1a)
val _ = assert is_oneline oneline_complete1a
Definition complete_literal1b:
complete_literal1b ([], 1) = 10 /\
complete_literal1b (3::t, 2) = 16 /\
complete_literal1b (h::t, 2) = 12 + h /\
complete_literal1b _ = 15
End
Theorem oneline_complete1b[local] =
DefnBase.one_line_ify NONE complete_literal1b
val _ = assert (null o hyp) oneline_complete1b
val _ = assert is_oneline oneline_complete1b
Definition complete_literal2:
complete_literal2 (3, [], 2) = 10 /\
complete_literal2 (5, h::t, x) = 12 + h + x /\
complete_literal2 _ = 15
End
Theorem oneline_complete2[local] = DefnBase.one_line_ify NONE complete_literal2
val _ = assert (null o hyp) oneline_complete2
val _ = assert is_oneline oneline_complete2
Definition ADEL_def:
(ADEL [] z = []) /\
(ADEL ((x:'a,y:'b)::xs) z = if x = z then ADEL xs z else (x,y)::ADEL xs z)
End
Theorem oneline_ADEL[local] = DefnBase.one_line_ify NONE ADEL_def
val _ = assert (null o hyp) oneline_ADEL
val _ = assert is_oneline oneline_ADEL
Definition bar_def:
bar = [] : 'a list
End
Theorem oneline_bar[local] = DefnBase.one_line_ify NONE bar_def
val _ = assert (null o hyp) oneline_bar
val _ = assert is_oneline oneline_bar
Definition foo1_def:
foo1 = if bar = []:'a list then []:'a list else []
End
Theorem oneline_foo1[local] = DefnBase.one_line_ify NONE foo1_def
val _ = assert (null o hyp) oneline_foo1
val _ = assert is_oneline oneline_foo1
Datatype:
tt = A1
| B1 tt
| C1 (tt option)
| D1 (tt list)
| E1 (tt # tt)
End
Definition test_def:
test A1 = [()] /\
test (B1 x) = test x ++ [()] /\
test (C1 NONE) = [] /\
test (C1 (SOME x)) = test x ++ REVERSE (test x) /\
test (D1 tts) = (case tts of [] => [(); ()]
| (tt :: tts) => test (D1 tts) ++ test tt) /\
test (E1 (x, y)) = REVERSE (test x) ++ test y
End
Theorem oneline_test[local] = DefnBase.one_line_ify NONE test_def
val _ = assert is_oneline oneline_test
val _ = export_theory();