1%----------------------------------------------------------------------------% 2% The parity checker example from the paper "HOL: A Proof Generating % 3% System for Higher-Order Logic" (which can be found on hol/doc/HOLSYS.tex). % 4% % 5% For a more complicated parity checker see RESET_PARITY.ml. % 6%----------------------------------------------------------------------------% 7 8new_theory `PARITY`;; 9 10let PARITY_DEF = 11 new_prim_rec_definition 12 (`PARITY_DEF`, 13 "(PARITY 0 f = T) /\ 14 (PARITY(SUC n)f = (f(SUC n) => ~(PARITY n f) | PARITY n f))");; 15 16let UNIQUENESS_LEMMA = 17 prove_thm 18 (`UNIQUENESS_LEMMA`, 19 "!in out. 20 (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~(out t) | out t)) 21 ==> 22 (!t. out t = PARITY t in)", 23 REPEAT GEN_TAC 24 THEN STRIP_TAC 25 THEN INDUCT_TAC 26 THEN ASM_REWRITE_TAC[PARITY_DEF]);; 27 28let ONE_DEF = 29 new_definition 30 (`ONE_DEF`, "ONE(out:num->bool) = !t. out t = T");; 31 32let NOT_DEF = 33 new_definition 34 (`NOT_DEF`, "NOT(in,out:num->bool) = !t. out t = ~(in t)");; 35 36let MUX_DEF = 37 new_definition 38 (`MUX_DEF`, 39 "MUX(sw,in1,in2,out:num->bool) = !t. out t = (sw t => in1 t | in2 t)");; 40 41let REG_DEF = 42 new_definition 43 (`REG_DEF`, "REG(in,out:num->bool) = !t. out t = ((t=0) => F | in(t-1))");; 44 45let PARITY_IMP_DEF = 46 new_definition 47 (`PARITY_IMP_DEF`, 48 "PARITY_IMP(in,out) = 49 ?l1 l2 l3 l4 l5. NOT(l2,l1) /\ 50 MUX(in,l1,l2,l3) /\ 51 REG(out,l2) /\ 52 ONE l4 /\ 53 REG(l4,l5) /\ 54 MUX(l5,l3,l4,out)");; 55 56let lines tok t = 57 (let x = (fst o dest_var o rator o lhs o snd o dest_forall) t 58 in 59 mem x (words tok)) ? false;; 60 61let PARITY_LEMMA = 62 prove_thm 63 (`PARITY_LEMMA`, 64 "!in out. 65 PARITY_IMP(in,out) ==> 66 (out 0 = T) /\ !t. out(SUC t) = (in(SUC t) => ~(out t) | out t)", 67 PURE_REWRITE_TAC[PARITY_IMP_DEF;ONE_DEF;NOT_DEF;MUX_DEF;REG_DEF] 68 THEN REPEAT STRIP_TAC 69 THENL 70 [FILTER_ASM_REWRITE_TAC(lines`out l4 l5`)[];ALL_TAC] 71 THEN FIRST_ASSUM 72 (\th. if lines`out`(concl th) 73 then SUBST_TAC[SPEC "SUC t" th] 74 else NO_TAC) 75 THEN FILTER_ASM_REWRITE_TAC(lines`l1 l3 l4 l5`)[] 76 THEN FILTER_ASM_REWRITE_TAC(lines`l2`)[] 77 THEN REWRITE_TAC[NOT_SUC;SUC_SUB1]);; 78 79let PARITY_CORRECT = 80 prove_thm 81 (`PARITY_CORRECT`, 82 "!in out. PARITY_IMP(in,out) ==> (!t. out t = PARITY t in)", 83 REPEAT GEN_TAC 84 THEN DISCH_TAC 85 THEN IMP_RES_TAC PARITY_LEMMA 86 THEN IMP_RES_TAC UNIQUENESS_LEMMA);; 87 88