(****************************************************************************%
% ML input for the parity checking example in TUTORIAL.                      %
% The number in comment boxes correspond to the numbers in the text.          %
%****************************************************************************)


(*---------------------------------------------------------------------------%
%                                    1                                       %
%---------------------------------------------------------------------------*)

new_theory "PARITY";

(*---------------------------------------------------------------------------%
%                                    2                                       %
%---------------------------------------------------------------------------*)

val num_Axiom = theorem "prim_rec" "num_Axiom";
val PARITY_DEF = new_recursive_definition
{ name = "PARITY_DEF",
  fixity = Prefix,
  rec_axiom = num_Axiom,
  def = --`(PARITY 0 f = T) /\
           (PARITY(SUC n)f = (f(SUC n) => ~(PARITY n f) | PARITY n f))`--};

(*---------------------------------------------------------------------------%
%                                    3                                       %
%---------------------------------------------------------------------------*)

set_goal
([],
 --`!in1 out. 
     (out 0 = T) /\ (!t. out(SUC t) = (in1(SUC t) => ~(out t) | out t))
     ==>
     (!t. out t = PARITY t in1)`--);

(*---------------------------------------------------------------------------%
%                                    4                                       %
%---------------------------------------------------------------------------*)

expand(REPEAT GEN_TAC THEN STRIP_TAC);

(*---------------------------------------------------------------------------%
%                                    5                                       %
%---------------------------------------------------------------------------*)

expand INDUCT_TAC;

(*---------------------------------------------------------------------------%
%                                    6                                       %
%---------------------------------------------------------------------------*)

expand(ASM_REWRITE_TAC[PARITY_DEF]);

(*---------------------------------------------------------------------------%
%                                    7                                       %
%---------------------------------------------------------------------------*)

expand(ASM_REWRITE_TAC[PARITY_DEF]);

(*---------------------------------------------------------------------------%
%                                    8                                       %
%---------------------------------------------------------------------------*)

val UNIQUENESS_LEMMA = save_top_thm "UNIQUENESS_LEMMA";

(*---------------------------------------------------------------------------%
%                                    9                                       %
%---------------------------------------------------------------------------*)

val ONE_DEF =
 new_definition
  ("ONE_DEF", --`ONE(out:num->bool) = !t. out t = T`--);

(*---------------------------------------------------------------------------%
%                                    10                                      %
%---------------------------------------------------------------------------*)

val NOT_DEF =
 new_definition
  ("NOT_DEF", --`NOT(in1,(out:num->bool)) = !t. out t = ~(in1 t)`--);

(*---------------------------------------------------------------------------%
%                                    11                                      %
%---------------------------------------------------------------------------*)

val MUX_DEF =
 new_definition
  ("MUX_DEF", 
   --`MUX(sw,in1,in2,(out:num->bool)) = 
        !t. out t = (sw t => in1 t | in2 t)`--);

(*---------------------------------------------------------------------------%
%                                    12                                      %
%---------------------------------------------------------------------------*)

val REG_DEF =
 new_definition
 ("REG_DEF", --`REG(in1,(out:num->bool)) = 
                  !t. out t = ((t=0) => F | in1(t-1))`--);

(*---------------------------------------------------------------------------%
%                                    13                                      %
%---------------------------------------------------------------------------*)

val PARITY_IMP_DEF =
 new_definition
  ("PARITY_IMP_DEF",
   --`PARITY_IMP(in1,out) =
      ?l1 l2 l3 l4 l5. 
       NOT(l2,l1) /\ MUX(in1,l1,l2,l3) /\ REG(out,l2) /\
       ONE l4     /\ REG(l4,l5)       /\ MUX(l5,l3,l4,out)`--);

(*---------------------------------------------------------------------------%
%                                    14                                      %
%---------------------------------------------------------------------------*)

set_goal
 ([], --`!in1 out. 
         PARITY_IMP(in1,out) ==> 
         (out 0 = T) /\ 
         !t. out(SUC t) = (in1(SUC t) => ~(out t) | out t)`--);

(*---------------------------------------------------------------------------%
%                                    15                                      %
%---------------------------------------------------------------------------*)

expand(PURE_REWRITE_TAC
        [PARITY_IMP_DEF, ONE_DEF, NOT_DEF, MUX_DEF, REG_DEF]
        THEN REPEAT STRIP_TAC);

(*---------------------------------------------------------------------------%
%                                    16                                      %
%---------------------------------------------------------------------------*)

fun lines tok t =
 (let val x = #Name(dest_var(rator(lhs(#Body(dest_forall t)))))
  in
  mem x (words2 " " tok)
  end);

(*---------------------------------------------------------------------------%
%                                    17                                      %
%---------------------------------------------------------------------------*)

expand(FILTER_ASM_REWRITE_TAC(lines "out l4 l5")[]);

(*---------------------------------------------------------------------------%
%                                    18                                      %
%---------------------------------------------------------------------------*)

expand
 (FIRST_ASSUM
   (fn th => if lines "out" (concl th)
             then SUBST_TAC[SPEC (--`SUC t`--) th]
             else NO_TAC));

(*---------------------------------------------------------------------------%
%                                    19                                      %
%---------------------------------------------------------------------------*)

expand(FILTER_ASM_REWRITE_TAC(lines "l1 l3 l4 l5")[]
        THEN FILTER_ASM_REWRITE_TAC(lines "l2")[]);

(*---------------------------------------------------------------------------%
%                                    20                                      %
%---------------------------------------------------------------------------*)

add_theory_to_sml "arithmetic";
val NOT_SUC = theorem "num" "NOT_SUC";
expand(REWRITE_TAC[NOT_SUC, SUC_SUB1]);

(*---------------------------------------------------------------------------%
%                                    21                                      %
%---------------------------------------------------------------------------*)

val PARITY_LEMMA = save_top_thm "PARITY_LEMMA";

(*---------------------------------------------------------------------------%
%                                    22                                      %
%---------------------------------------------------------------------------*)

set_goal
 ([], --`!in1 out. 
           PARITY_IMP(in1,out) ==> 
           (out 0 = T) /\ 
         !t. out(SUC t) = (in1(SUC t) => ~(out t) | out t)`--);

(*---------------------------------------------------------------------------%
%                                    23                                      %
%---------------------------------------------------------------------------*)

expand
 (PURE_REWRITE_TAC[PARITY_IMP_DEF, ONE_DEF, NOT_DEF, MUX_DEF, REG_DEF]
  THEN REPEAT STRIP_TAC
  THENL
   [FILTER_ASM_REWRITE_TAC(lines "out l4 l5")[], ALL_TAC]
  THEN FIRST_ASSUM
        (fn th => if lines "out" (concl th) 
                  then SUBST_TAC[SPEC (--`SUC t`--) th]
                  else NO_TAC)
  THEN FILTER_ASM_REWRITE_TAC(lines "l1 l3 l4 l5")[]
  THEN FILTER_ASM_REWRITE_TAC(lines "l2")[]
  THEN REWRITE_TAC[NOT_SUC, SUC_SUB1]);

(*---------------------------------------------------------------------------%
%                                    24