1open HolKernel Parse boolLib IndDefLib
2
3open testutils
4
5fun checkhyps th = if null (hyp th) then ()
6                   else die "FAILED - Hyps in theorem!"
7
8(* set up a fake arithmetic theory *)
9val _ = new_type ("num", 0)
10val _ = new_constant("Z", ``:num``)
11val _ = new_constant("ONE", ``:num``)
12val _ = new_constant("TWO", ``:num``)
13val _ = new_constant("FOUR", ``:num``)
14val _ = new_constant("<=", ``:num -> num -> bool``)
15val _ = set_fixity "<=" (Infix(NONASSOC, 450))
16val _ = new_constant("<", ``:num -> num -> bool``)
17val _ = set_fixity "<" (Infix(NONASSOC, 450))
18val _ = new_constant ("+", ``:num -> num -> num``)
19val _ = set_fixity "+" (Infixl 500)
20val _ = new_constant ("*", ``:num -> num -> num``)
21val _ = set_fixity "*" (Infixl 600)
22val _ = new_constant ("SUC", ``:num -> num``)
23
24
25val _ = print "*** Testing inductive definitions - mutual recursion\n"
26
27
28val (oe_rules, oe_ind, oe_cases) = Hol_reln`
29  even Z /\
30  (!m. odd m /\ ONE <= m ==> even (m + ONE)) /\
31  (!m. even m ==> odd (m + ONE))
32`;
33val _ = checkhyps oe_rules
34
35val _ = print "*** Testing inductive definitions - scheme variables\n"
36
37val (rtc_rules, rtc_ind, rtc_cases) = Hol_reln`
38  (!x. rtc r x x) /\
39  (!x y z. rtc r x y /\ r y z ==> rtc r x z)
40`;
41val _ = checkhyps rtc_rules
42
43val _ = print "*** Testing schematic variables for multiple relations\n"
44val (mscheme_rules, mscheme_ind, mscheme_cases) = Hol_reln`
45  (!n m. n < m ==> foo P n m) /\
46  (!n m. P n ==> foo P n m) /\
47  (!n m. bar P n ==> foo P n m) /\
48  (!n. FOUR < n ==> bar P (TWO * n))
49`
50val _ = checkhyps mscheme_rules
51
52val _ = print "*** Testing inductive definitions - existential vars\n"
53
54val (rtc'_rules, rtc'_ind, rtc'_cases) = Hol_reln`
55  (!x. rtc' r x x) /\
56  (!x y. r x y /\ (?z. rtc' r z y) ==> rtc' r x y)
57`;
58val _ = checkhyps rtc'_rules
59
60(* emulate the example in examples/opsemScript.sml *)
61val _ = print "*** Testing opsem example\n"
62val _ = new_type ("comm", 0)
63val _ = new_constant("Skip", ``:comm``)
64val _ = new_constant("::=", ``:num -> ((num -> num) -> num) -> comm``)
65val _ = new_constant(";;", ``:comm -> comm -> comm``)
66val _ = new_constant("If", ``:((num -> num) -> bool) -> comm -> comm -> comm``)
67val _ = new_constant("While", ``:((num -> num) -> bool) -> comm -> comm``)
68val _ = set_fixity "::=" (Infixr 400);
69val _ = set_fixity ";;"  (Infixr 350);
70
71val (rules,induction,ecases) = Hol_reln
72     `(!s. EVAL Skip s s)
73 /\   (!s V E. EVAL (V ::= E) s (\v. if v=V then E s else s v))
74 /\   (!C1 C2 s1 s3.
75        (?s2. EVAL C1 s1 s2 /\ EVAL C2 s2 s3) ==> EVAL (C1;;C2) s1 s3)
76 /\   (!C1 C2 s1 s2 B. EVAL C1 s1 s2 /\  B s1 ==> EVAL (If B C1 C2) s1 s2)
77 /\   (!C1 C2 s1 s2 B. EVAL C2 s1 s2 /\ ~B s1 ==> EVAL (If B C1 C2) s1 s2)
78 /\   (!C s B.                           ~B s ==> EVAL (While B C) s s)
79 /\   (!C s1 s3 B.
80        (?s2. EVAL C s1 s2 /\
81              EVAL (While B C) s2 s3 /\ B s1) ==> EVAL (While B C) s1 s3)`;
82
83val _ = checkhyps rules
84
85(* check MONO_COND *)
86val _ = Hol_reln
87`(foo p x x) /\
88 ((if p y then foo p y x else foo p y y) ==> foo p x y)`
89
90
91val _ = tprint "With Unicode should fail"
92val _ = if (xHol_reln "tr" `
93                      (!x. ��� x Z) /\
94                      (!x y. ��� (SUC x) (SUC y) ==> ��� x y)
95           ` ; false) handle HOL_ERR _ => true then OK()
96        else die "FAILED"
97
98val _ = tprint "Vacuous clause failure"
99val _ = if (with_flag (Feedback.emit_ERR, false)
100              Hol_reln `(!x. rel x Z) /\ (!x y. rel x y)` ; false)
101               handle HOL_ERR {message,...} =>
102                      String.isSuffix
103                          "Vacuous clause trivialises whole definition"
104                          message
105        then OK()
106        else die "FAILED"
107
108
109val _ = OS.Process.exit OS.Process.success
110