1new_theory`mux`;; 2 3new_definition 4 (`NAND_SPEC`, "!i1 i2 o. NAND_SPEC(i1,i2,o) = o = ~(i1 /\ i2)");; 5 6new_definition 7 (`INV_SPEC`, "!i o. INV_SPEC(i,o) = o = ~i");; 8 9new_definition 10 (`MUX_SPEC`, "!c i1 i2 o. MUX_SPEC(c,i1,i2,o) = o = (c => i1 | i2)");; 11 12 new_definition 13 (`MUX_IMP`, 14 "!c i1 i2 o. 15 MUX_IMP(c,i1,i2,o) = 16 ?l1 l2 l3. 17 INV_SPEC(c,l1) /\ 18 NAND_SPEC(l1,i2,l2) /\ 19 NAND_SPEC(c,i1,l3) /\ 20 NAND_SPEC(l2,l3,o)");; 21 22close_theory();; 23 24load_theory`mux`;; 25 26let prims = maptok (axiom `mux`) `INV_SPEC NAND_SPEC`;; 27 28let MUX_IMP = axiom `mux` `MUX_IMP`;; 29 30let MUX_THM1 = save_thm(`MUX_THM1`, EXPAND prims MUX_IMP);; 31