1open HolKernel Parse boolLib normalForms; 2 3open testutils; 4 5val _ = let 6 val p = mk_var("p", bool) 7 val q = mk_var("q", bool) 8 val v1 = genvar bool 9 val v2 = genvar bool 10 val t1 = mk_conj(p,q) 11 val C = normalForms.PRETTIFY_VARS_CONV 12 val gt1 = mk_abs(v1, mk_conj(v1, p)) 13 val gt2 = list_mk_abs([q, v1,v2], list_mk_conj([p,q,v1,q,v2])) 14 fun test (t1,t2) = convtest ("PRETTIFY_CONV "^term_to_string t1, C, t1, t2) 15in 16 app test [(t1, t1), (mk_abs(p,t1), mk_abs(p,t1)), 17 (v1, v1), (gt1, ``\v. v /\ p``), 18 (gt2, ``\q v v0. p /\ q /\ v /\ q /\ v0``)] 19end 20 21val _ = Parse.reveal "C"; 22 23fun normalForms_test (fname, function :conv, problem, result) = let 24 val padr = StringCvt.padRight #" "; 25 val padl = StringCvt.padLeft #" "; 26 val f_s = padr 16 fname; 27 val p_s = padr 25 (term_to_string problem); 28 val r_s = padl 10 (term_to_string result); 29 val _ = tprint (f_s ^ p_s ^ " = " ^ r_s); 30in 31 require_msg (check_result (fn tm => (result ~~ (rhs (concl tm))))) 32 (term_to_string o rhs o concl) 33 function (* 'b -> 'a *) 34 problem (* 'b *) 35end; 36 37val test_cases = 38 [("PRETTIFY_VARS_CONV", PRETTIFY_VARS_CONV, 39 (rhs (concl (DEF_CNF_CONV ``~(p <=> q) ==> q /\ r``))), 40 ``?v x. (x \/ p \/ q) /\ (x \/ ~p \/ ~q) /\ (p \/ ~q \/ ~x) /\ 41 (q \/ ~p \/ ~x) /\ (v \/ ~q \/ ~r) /\ (r \/ ~v) /\ (q \/ ~v) /\ 42 (v \/ x)``), 43(* "No numerals currently allowed" 44 ("SKI_CONV", SKI_CONV, ``?f. !y. f y = y + 1``, 45 ``$? (S (K $!) (S (S (K S) (S (K (S (K $=))) I)) (K (S $+ (K 1)))))``), 46 *) 47 ("SKI_CONV", SKI_CONV, ``\x:'a. ((f :'a->'a->'a) x o (g :'a->'a))``, 48 ``S (S (K $o) (f :'a->'a->'a)) (K (g :'a->'a))``), 49 ("SKI_CONV", SKI_CONV, ``\x y. (f :'a->'a->'a) x y``, 50 ``S (S (K S) (S (K K) (f :'a->'a->'a))) (K I)``), 51 ("SKI_CONV", SKI_CONV, ``$? = \P. P ($@ P)``, ``$? = S I $@``), 52 ("SKI_CONV", SKI_CONV, ``$==> = \a b. ~a \/ b``, 53 ``$==> = S (S (K S) (S (K K) (S (K $\/) $~))) (K I)``), 54 ("SKI_CONV", SKI_CONV, ``$! = \P. K T = P``, ``$! = S (K ($= (K T))) I``), 55 ("SKI_CONV", SKI_CONV, ``!x:'a y:'a. P x y``, 56 ``$! (S (K $!) (S (S (K S) (S (K K) (P :'a->'a->bool))) (K I)))``), 57 ("SKI_CONV", SKI_CONV, ``!x:'a y:'a. P y x``, 58 ``$! (S (K $!) (S (K (S (P :'a->'a->bool))) K))``), 59 ("SKI_CONV", SKI_CONV, ``(P = Q) <=> (!x. P x <=> Q x)``, 60 ``(P = Q <=> $! (S (S (K $<=>) P) Q))``), 61(* "No numerals currently allowed" 62 ("SKICo_CONV", SKICo_CONV, ``?f. !y. f y = y + 1``, 63 ``$? ($! o C (S o $o $=) (C $+ 1))``), 64 *) 65 ("SKICo_CONV", SKICo_CONV, ``\x:'a. ((f :'a->'a->'a) x o (g :'a->'a))``, 66 ``C ($o o (f :'a->'a->'a)) (g :'a->'a)``), 67 ("SKICo_CONV", SKICo_CONV, ``\x y. (f :'a->'a->'a) x y``, 68 ``C ($o o (f :'a->'a->'a)) I``), 69 ("SKICo_CONV", SKICo_CONV, ``$? = \P. P ($@ P)``, ``$? = S I $@``), 70 ("SKICo_CONV", SKICo_CONV, ``$==> = \a b. ~a \/ b``, 71 ``$==> = C ($o o $\/ o $~) I``), 72 ("SKICo_CONV", SKICo_CONV, ``$! = \P. K T = P``, ``$! = $= (K T)``), 73 ("SKICo_CONV", SKICo_CONV, ``!x y. (P :'a->'a->bool) x y``, 74 ``$! ($! o C ($o o (P :'a->'a->bool)) I)``), 75 ("SKICo_CONV", SKICo_CONV, ``!x y. (P :'a->'a->bool) y x``, 76 ``$! ($! o C (P :'a->'a->bool))``), 77 ("SKICo_CONV", SKICo_CONV, ``(P = Q) = (!x. P x = Q x)``, 78 ``(P = Q <=> $! (S ($= o P) Q))``), 79 ("SIMPLIFY_CONV", SIMPLIFY_CONV, ``(!x y. P x \/ (P y /\ F)) ==> ?z. P z``, 80 ``(!x. P x) ==> ?z. P z``), 81 ("NNF_CONV", NNF_CONV, ``(!x. P(x)) ==> ((?y. Q(y)) = (?z. P(z) /\ Q(z)))``, 82 ``((?y. Q y) \/ !z. ~P z \/ ~Q z) /\ ((!y. ~Q y) \/ ?z. P z /\ Q z) \/ 83 ?x. ~P x``), 84 ("NNF_CONV", NNF_CONV, ``~(~(x = y) = z) = ~(x = ~(y = z))``, 85 ``(((x \/ y) /\ (~x \/ ~y) \/ z) /\ ((x \/ ~y) /\ (~x \/ y) \/ ~z) \/ 86 (x \/ (y \/ ~z) /\ (~y \/ z)) /\ (~x \/ (y \/ z) /\ (~y \/ ~z))) /\ 87 (((x \/ y) /\ (~x \/ ~y) \/ ~z) /\ ((x \/ ~y) /\ (~x \/ y) \/ z) \/ 88 (x \/ (y \/ z) /\ (~y \/ ~z)) /\ (~x \/ (y \/ ~z) /\ (~y \/ z)))``), 89 ("SKOLEMIZE_CONV", SKOLEMIZE_CONV, 90 ``!x. (?y. Q y \/ !z. ~P z \/ ~Q z) \/ ~P x``, 91 ``?y. !x. (Q (y x) \/ !z. ~P z \/ ~Q z) \/ ~P x``), 92 ("TAUTOLOGY_CONV", TAUTOLOGY_CONV, ``p \/ r \/ ~p \/ ~q``, T), 93 ("CONTRACT_CONV", CONTRACT_CONV, ``(p \/ r) \/ p \/ ~q``, ``r \/ p \/ ~q``) 94 ]; 95 96val _ = List.app (ignore o normalForms_test) test_cases; 97 98val _ = Process.exit Process.success; 99