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
|
\DOC mk_rewrites
\TYPE {mk_rewrites : bool -> thm -> thm list -> thm list}
\SYNOPSIS
Turn theorem into list of (conditional) rewrites.
\DESCRIBE
Given a Boolean flag {b}, a theorem {th} and a list of theorems {thl}, the call
{mk_rewrites b th thl} breaks {th} down into a collection of rewrites (for
example, splitting conjunctions up into several sub-theorems) and appends them
to the front of {thl} (which are normally theorems already processed in this
way). Non-equational theorems {|- p} are converted to {|- p <=> T}. If the flag
{b} is true, then implicational theorems {|- p ==> s = t} are used as
conditional rewrites; otherwise they are converted to {|- (p ==> s = t) <=> T}.
This function is applied inside {extend_basic_rewrites} and
{set_basic_rewrites}.
\FAILURE
Never fails.
\EXAMPLE
{
# ADD_CLAUSES;;
val it : thm =
|- (!n. 0 + n = n) /\
(!m. m + 0 = m) /\
(!m n. SUC m + n = SUC (m + n)) /\
(!m n. m + SUC n = SUC (m + n))
# mk_rewrites false ADD_CLAUSES [];;
val it : thm list =
[|- 0 + n = n; |- m + 0 = m; |- SUC m + n = SUC (m + n);
|- m + SUC n = SUC (m + n)]
}
\SEEALSO
extend_basic_rewrites, GEN_REWRITE_CONV, REWRITE_CONV, set_basic_rewrites,
SIMP_CONV.
\ENDDOC
|
