open HolKernel Parse boolLib boolTheory;

infix THEN THENL;

val _ = new_theory "num";

val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false;

(*---------------------------------------------------------------------------
 * Define successor `SUC_REP:ind->ind` on ind.
 *---------------------------------------------------------------------------*)

val SUC_REP_DEF = new_specification
   ("SUC_REP_DEF",["SUC_REP"], boolTheory.INFINITY_AX);


val ZERO_REP_EXISTS = prove(
  Term`?z. !y. ~(z = SUC_REP y)`,
  Q.X_CHOOSE_THEN `zrep` ASSUME_TAC ((CONV_RULE NOT_FORALL_CONV o
                                      REWRITE_RULE [ONTO_THM] o
                                      CONJUNCT2) SUC_REP_DEF) THEN
  POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
  Q.EXISTS_TAC `zrep` THEN POP_ASSUM ACCEPT_TAC);

(*---------------------------------------------------------------------------
 * `ZERO_REP:ind` represents `0:num`
 *---------------------------------------------------------------------------*)

val ZERO_REP_DEF = new_specification
  ("ZERO_REP_DEF",["ZERO_REP"], ZERO_REP_EXISTS);


(*---------------------------------------------------------------------------*)
(* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent         *)
(* numbers.  It is the smallest subset containing `ZERO_REP` and closed      *)
(* under `SUC_REP`.                                                          *)
(*---------------------------------------------------------------------------*)

val IS_NUM_REP = new_definition("IS_NUM_REP",
     “IS_NUM_REP m =
      !P:ind->bool. (P ZERO_REP /\ (!n. P n ==> P(SUC_REP n))) ==> P m”);

(*---------------------------------------------------------------------------
 * Prove that there is a representation in :ind of at least one number.
 *---------------------------------------------------------------------------*)

val EXISTS_NUM_REP = TAC_PROOF(([],“?n. IS_NUM_REP n”),
     PURE_REWRITE_TAC [IS_NUM_REP] THEN
     EXISTS_TAC (“ZERO_REP”) THEN
     REPEAT STRIP_TAC);

(*---------------------------------------------------------------------------
 * Make the type definition.
 *---------------------------------------------------------------------------*)

val num_TY_DEF = new_type_definition ("num", EXISTS_NUM_REP);

val num_ISO_DEF = define_new_type_bijections
                   {name = "num_ISO_DEF",
                    ABS = "ABS_num",
                    REP = "REP_num",
                    tyax =  num_TY_DEF};

val R_11   = prove_rep_fn_one_one num_ISO_DEF
and R_ONTO = prove_rep_fn_onto    num_ISO_DEF
and A_11   = prove_abs_fn_one_one num_ISO_DEF
and A_ONTO = prove_abs_fn_onto    num_ISO_DEF;

(*---------------------------------------------------------------------------
 * Define ZERO.
 *---------------------------------------------------------------------------*)

val zero = mk_var("0", mk_thy_type{Tyop="num",Thy="num",Args=[]});

val ZERO_DEF = new_definition("ZERO_DEF", “^zero = ABS_num ZERO_REP”);


(*---------------------------------------------------------------------------
 * Define the successor function on num.
 *---------------------------------------------------------------------------*)

val SUC_DEF = new_definition("SUC_DEF",
 “SUC m = ABS_num(SUC_REP(REP_num m))”);

local open OpenTheoryMap in
val ns = ["Number","Natural"]
val _ = OpenTheory_tyop_name{tyop={Thy="num",Tyop="num"},name=(ns,"natural")}
val _ = OpenTheory_const_name{const={Thy="num",Name="0"},name=(ns,"zero")}
val _ = OpenTheory_const_name{const={Thy="num",Name="SUC"},name=(ns,"suc")}
end

(*---------------------------------------------------------------------------
 * Prove that IS_NUM_REP ZERO_REP.
 *---------------------------------------------------------------------------*)

val IS_NUM_REP_ZERO =
    TAC_PROOF
    (([], “IS_NUM_REP ZERO_REP”),
     REWRITE_TAC [IS_NUM_REP] THEN REPEAT STRIP_TAC);

(*---------------------------------------------------------------------------
 * Prove that IS_NUM_REP (SUC_REP x).
 *---------------------------------------------------------------------------*)

val IS_NUM_SUC_REP =
    TAC_PROOF
    (([], “!i. IS_NUM_REP i ==> IS_NUM_REP (SUC_REP i)”),
     REWRITE_TAC [IS_NUM_REP] THEN
     REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC);

val IS_NUM_REP_SUC_REP =
    TAC_PROOF
    (([], “!n. IS_NUM_REP(SUC_REP(REP_num n))”),
      GEN_TAC THEN MATCH_MP_TAC IS_NUM_SUC_REP THEN
      REWRITE_TAC [R_ONTO] THEN
      EXISTS_TAC (“n:num”) THEN REFL_TAC);

(*---------------------------------------------------------------------------
 * |- !x1 x2. (SUC_REP x1 = SUC_REP x2) ==> (x1 = x2)
 *---------------------------------------------------------------------------*)

val SUC_REP_11 = CONJUNCT1 (REWRITE_RULE [ONE_ONE_THM] SUC_REP_DEF);

(*---------------------------------------------------------------------------
 *  |- !x. ~(SUC_REP x = ZERO_REP)
 *---------------------------------------------------------------------------*)

val NOT_SUC_ZERO = GSYM ZERO_REP_DEF;

(*----------------------------------------------------------------------*)
(* Proof of NOT_SUC : |- !n. ~(SUC n = ZERO)                            *)
(* ---------------------------------------------------------------------*)

val NOT_SUC = store_thm("NOT_SUC",
    “!n. ~(SUC n = 0)”,
     PURE_REWRITE_TAC [SUC_DEF,ZERO_DEF] THEN GEN_TAC THEN
     MP_TAC (SPECL [“SUC_REP(REP_num n)”,“ZERO_REP”] A_11) THEN
     REWRITE_TAC [IS_NUM_REP_ZERO,IS_NUM_REP_SUC_REP] THEN
     DISCH_THEN SUBST1_TAC THEN
     MATCH_ACCEPT_TAC NOT_SUC_ZERO);

(* ---------------------------------------------------------------------*)
(* Prove that |-  !m n. (SUC m = SUC n) ==> (m = n)                     *)
(* ---------------------------------------------------------------------*)

val INV_SUC = store_thm("INV_SUC",
    “!m n. (SUC m = SUC n) ==> (m = n)”,
     REPEAT GEN_TAC THEN REWRITE_TAC [SUC_DEF] THEN
     MP_TAC (SPECL [“SUC_REP(REP_num m)”,
                    “SUC_REP(REP_num n)”] A_11) THEN
     REWRITE_TAC [IS_NUM_REP_SUC_REP] THEN DISCH_THEN SUBST1_TAC THEN
     DISCH_THEN (MP_TAC o MATCH_MP SUC_REP_11) THEN
     REWRITE_TAC [R_11]);

(* ---------------------------------------------------------------------*)
(* Prove induction theorem.                                             *)
(* ---------------------------------------------------------------------*)

val ind_lemma1 =
    TAC_PROOF
    (([], “!P. P ZERO_REP /\ (!i. P i ==> P(SUC_REP i))
                 ==>
              !i. IS_NUM_REP i ==> P i”),
     PURE_ONCE_REWRITE_TAC [IS_NUM_REP] THEN
     REPEAT STRIP_TAC THEN RES_TAC);

val lemma =
    TAC_PROOF(([], “(A ==> (A /\ B)) = (A ==> B)”),
               ASM_CASES_TAC (“A:bool”) THEN ASM_REWRITE_TAC []);

val ind_lemma2 = TAC_PROOF(([],
  “!P. P ZERO_REP /\ (!i. IS_NUM_REP i /\ P i ==> P(SUC_REP i))
           ==>
         !i. IS_NUM_REP i ==> P i”),
     GEN_TAC THEN STRIP_TAC THEN
     MP_TAC (SPEC “\i. IS_NUM_REP i /\ P i” ind_lemma1) THEN
     CONV_TAC(DEPTH_CONV BETA_CONV) THEN
     REWRITE_TAC [lemma] THEN DISCH_THEN MATCH_MP_TAC THEN
     ASM_REWRITE_TAC [IS_NUM_REP_ZERO] THEN
     REPEAT STRIP_TAC THEN IMP_RES_TAC IS_NUM_SUC_REP THEN
     RES_TAC);

val lemma1 =
    TAC_PROOF
    (([], “(!i. IS_NUM_REP i ==> P(ABS_num i)) = (!n. P n)”),
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [STRIP_ASSUME_TAC (SPEC (“n:num”) A_ONTO) THEN
      RES_TAC THEN ASM_REWRITE_TAC [],
      POP_ASSUM MP_TAC THEN REWRITE_TAC [R_ONTO] THEN
      STRIP_GOAL_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
      ASM_REWRITE_TAC []]);

val INDUCTION = store_thm("INDUCTION",
    “!P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n”,
     GEN_TAC THEN STRIP_TAC THEN
     MP_TAC (SPEC “\i. ((P(ABS_num i)):bool)” ind_lemma2) THEN
     CONV_TAC(DEPTH_CONV BETA_CONV) THEN
     REWRITE_TAC [SYM ZERO_DEF,lemma1] THEN
     DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL
     [FIRST_ASSUM ACCEPT_TAC,
      REWRITE_TAC [R_ONTO] THEN
      GEN_TAC THEN  CONV_TAC ANTE_CONJ_CONV THEN
      DISCH_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
      ASM_REWRITE_TAC [num_ISO_DEF,SYM (SPEC_ALL SUC_DEF)]]);

val _ = export_theory();