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