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