needs "lib/ssrbool-compiled.hl";; prioritize_num();; (* Lemma succnK *) let succnK = section_proof ["n"] `SUC n - 1 = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma succn_inj *) let succn_inj = section_proof ["n";"m"] `SUC n = SUC m ==> n = m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eqSS *) let eqSS = section_proof ["m";"n"] `(SUC m = SUC n) = (m = n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma add0n *) let add0n = section_proof ["n"] `0 + n = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addSn *) let addSn = section_proof ["m";"n"] `SUC m + n = SUC (m + n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma add1n *) let add1n = section_proof ["n"] `1 + n = SUC n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addn0 *) let addn0 = section_proof ["n"] `n + 0 = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addnS *) let addnS = section_proof ["m";"n"] `m + SUC n = SUC (m + n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addSnnS *) let addSnnS = section_proof ["m";"n"] `SUC m + n = m + SUC n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addnCA *) let addnCA = section_proof ["m";"n";"p"] `m + (n + p) = n + (m + p)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addnC *) let addnC = section_proof ["m";"n"] `m + n = n + m` [ (((((fun arg_tac -> (use_arg_then "addn0") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addn1 *) let addn1 = section_proof ["n"] `n + 1 = SUC n` [ (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addnA *) let addnA = section_proof ["n";"m";"p"] `n + (m + p) = (n + m) + p` [ (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m + p`)])))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addnAC *) let addnAC = section_proof ["m";"n";"p"] `(n + m) + p = (n + p) + m` [ (((repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`p + m`)]))))) THEN (done_tac)); ];; (* Lemma addn_eq0 *) let addn_eq0 = section_proof ["m";"n"] `(m + n = 0) <=> (m = 0) /\ (n = 0)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eqn_addl *) let eqn_addl = section_proof ["p";"m";"n"] `(p + m = p + n) <=> (m = n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eqn_addr *) let eqn_addr = section_proof ["p";"m";"n"] `(m + p = n + p) = (m = n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addnI *) let addnI = section_proof ["m";"n1";"n2"] `m + n1 = m + n2 ==> n1 = n2` [ ((BETA_TAC THEN (move ["Heq"])) THEN (((fun arg_tac -> (use_arg_then "eqn_addl") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addIn *) let addIn = section_proof ["m";"n1";"n2"] `n1 + m = n2 + m ==> n1 = n2` [ ((repeat_tactic 1 9 (((use_arg_then "addnC")(gsym_then (thm_tac (new_rewrite [] [(`_1 + m`)])))))) THEN (move ["Heq"])); ((((fun arg_tac -> (use_arg_then "addnI") (fun fst_arg -> (use_arg_then "Heq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac)); ];; (* Lemma sub0n *) let sub0n = section_proof ["n"] `0 - n = 0` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subn0 *) let subn0 = section_proof ["n"] `n - 0 = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subnn *) let subnn = section_proof [] `!n. n - n = 0` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subSS *) let subSS = section_proof [] `!n m. SUC m - SUC n = m - n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subn_add2l *) let subn_add2l = section_proof [] `!p m n. (p + m) - (p + n) = m - n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subn_add2r *) let subn_add2r = section_proof [] `!p m n. (m + p) - (n + p) = m - n` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])); (((repeat_tactic 1 9 (((use_arg_then "addnC")(gsym_then (thm_tac (new_rewrite [] [(`_1 + p`)])))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addKn *) let addKn = section_proof ["n"] `!x. (n + x) - n = x` [ ((BETA_TAC THEN (move ["m"])) THEN ((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addnK *) let addnK = section_proof [] `!n x. (x + n) - n = x` [ ((BETA_TAC THEN (move ["n"]) THEN (move ["m"])) THEN ((((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addKn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subSnn *) let subSnn = section_proof ["n"] `SUC n - n = 1` [ (((((use_arg_then "add1n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subn_sub *) let subn_sub = section_proof ["m";"n";"p"] `(n - m) - p = n - (m + p)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subnAC *) let subnAC = section_proof [] `!m n p. (m - n) - p = (m - p) - n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "subn_sub")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma predn_sub *) let predn_sub = section_proof [] `!m n. (m - n) - 1 = m - SUC n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN ((((use_arg_then "subn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn1")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma predn_subS *) let predn_subS = section_proof [] `!m n. (SUC m - n) - 1 = m - n` [ (((((use_arg_then "predn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltnS *) let ltnS = section_proof [] `!m n. (m < SUC n) = (m <= n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leq0n *) let leq0n = section_proof [] `!n. 0 <= n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltn0Sn *) let ltn0Sn = section_proof [] `!n. 0 < SUC n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltn0 *) let ltn0 = section_proof [] `!n. n < 0 <=> F` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leqnn *) let leqnn = section_proof [] `!n. n <= n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltnSn *) let ltnSn = section_proof [] `!n. n < SUC n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eq_leq *) let eq_leq = section_proof [] `!m n. m = n ==> m <= n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leqnSn *) let leqnSn = section_proof [] `!n. n <= SUC n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leq_pred *) let leq_pred = section_proof [] `!n. n - 1 <= n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leqSpred *) let leqSpred = section_proof [] `!n. n <= SUC (n - 1)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltn_predK *) let ltn_predK = section_proof [] `!m n. m < n ==> SUC (n - 1) = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma prednK *) let prednK = section_proof [] `!n. 0 < n ==> SUC (n - 1) = n` [ ((BETA_TAC THEN (move ["n"]) THEN (move ["H"])) THEN (((fun arg_tac -> (use_arg_then "ltn_predK") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac))); ];; (* Lemma leqNgt *) let leqNgt = section_proof [] `!m n. (m <= n) <=> ~(n < m)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltnNge *) let ltnNge = section_proof [] `!m n. (m < n) = ~(n <= m)` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma ltnn *) let ltnn = section_proof [] `!n. n < n <=> F` [ ((BETA_TAC THEN (move ["n"])) THEN ((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leqn0 *) let leqn0 = section_proof [] `!n. (n <= 0) = (n = 0)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma lt0n *) let lt0n = section_proof [] `!n. (0 < n) = ~(n = 0)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma lt0n_neq0 *) let lt0n_neq0 = section_proof [] `!n. 0 < n ==> ~(n = 0)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eqn0Ngt *) let eqn0Ngt = section_proof [] `!n. (n = 0) = ~(0 < n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma neq0_lt0n *) let neq0_lt0n = section_proof [] `!n. (n = 0) = F ==> 0 < n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eqn_leq *) let eqn_leq = section_proof [] `!m n. (m = n) = (m <= n /\ n <= m)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma anti_leq *) let anti_leq = section_proof [] `!m n. m <= n /\ n <= m ==> m = n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma neq_ltn *) let neq_ltn = section_proof [] `!m n. ~(m = n) <=> (m < n) \/ (n < m)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac)); ];; (* Lemma leq_eqVlt *) let leq_eqVlt = section_proof ["m";"n"] `(m <= n) <=> (m = n) \/ (m < n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma eq_sym *) let eq_sym = section_proof [] `!x y:A. x = y <=> y = x` [ ((((use_arg_then "EQ_SYM_EQ") (disch_tac [])) THEN (clear_assumption "EQ_SYM_EQ") THEN BETA_TAC) THEN (done_tac)); ];; (* Lemma ltn_neqAle *) let ltn_neqAle = section_proof [] `!m n. (m < n) <=> ~(m = n) /\ (m <= n)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_eqVlt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`n = m`)]))))) THEN (done_tac)); ];; (* Lemma leq_trans *) let leq_trans = section_proof [] `!n m p. m <= n ==> n <= p ==> m <= p` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltE *) let ltE = section_proof [] `!n m. n < m <=> SUC n <= m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leqSS *) let leqSS = section_proof [] `!n m. SUC n <= SUC m <=> n <= m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leq_ltn_trans *) let leq_ltn_trans = section_proof [] `!n m p. m <= n ==> n < p ==> m < p` [ (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["Hmn"])); (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))) THEN (done_tac)) THEN (done_tac)); ];; (* Lemma ltn_leq_trans *) let ltn_leq_trans = section_proof ["n";"m";"p"] `m < n ==> n <= p ==> m < p` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltnW *) let ltnW = section_proof [] `!m n. m < n ==> m <= n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqnSn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leqW *) let leqW = section_proof [] `!m n. m <= n ==> m <= SUC n` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"])) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_trans *) let ltn_trans = section_proof [] `!n m p. m < n ==> n < p ==> m < p` [ (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["lt_mn"])); (((DISCH_THEN (fun snd_th -> (use_arg_then "ltnW") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma geqE *) let geqE = section_proof [] `!m n. m >= n <=> n <= m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma gtE *) let gtE = section_proof ["m";"n"] `m > n <=> n < m` [ (arith_tac); ];; (* Lemma leq_total *) let leq_total = section_proof ["m";"n"] `(m <= n) \/ (n <= m)` [ ((((((use_arg_then "implyNb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["lt_nm"])) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac)); ];; (* Lemma leqP *) let leqP = section_proof ["m";"n"] `m <= n \/ n < m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltnP *) let ltnP = section_proof ["m";"n"] `m < n \/ n <= m` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma posnP *) let posnP = section_proof ["n"] `n = 0 \/ 0 < n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltngtP *) let ltngtP = section_proof ["m";"n"] `m < n \/ n < m \/ m = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leq_add2l *) let leq_add2l = section_proof [] `!p m n. (p + m <= p + n) = (m <= n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma ltn_add2l *) let ltn_add2l = section_proof [] `!p m n. (p + m < p + n) = (m < n)` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])); (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnS")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_add2r *) let leq_add2r = section_proof ["p";"m";"n"] `(m + p <= n + p) = (m <= n)` [ (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "p") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_add2r *) let ltn_add2r = section_proof [] `!p m n. (m + p < n + p) = (m < n)` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])); (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addSn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_add *) let leq_add = section_proof [] `!m1 m2 n1 n2. m1 <= n1 ==> m2 <= n2 ==> m1 + m2 <= n1 + n2` [ (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"]) THEN (move ["le_mn1"]) THEN (move ["le_mn2"])); (((((fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 + n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_addr *) let leq_addr = section_proof [] `!m n. n <= n + m` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_addl *) let leq_addl = section_proof [] `!m n. n <= m + n` [ (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_addr *) let ltn_addr = section_proof ["m";"n";"p"] `m < n ==> m < n + p` [ ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "leq_trans") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_addr")(thm_tac (new_rewrite [] []))))); ];; (* Lemma ltn_addl *) let ltn_addl = section_proof [] `!m n p. m < n ==> m < p + n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma addn_gt0 *) let addn_gt0 = section_proof [] `!m n. (0 < m + n) <=> (0 < m) \/ (0 < n)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((repeat_tactic 1 9 (((use_arg_then "lt0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "negb_and")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addn_eq0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subn_gt0 *) let subn_gt0 = section_proof ["m";"n"] `(0 < n - m) = (m < n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subn_eq0 *) let subn_eq0 = section_proof [] `!m n. (m - n = 0) = (m <= n)` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leqE *) let leqE = section_proof [] `!m n. m <= n <=> m - n = 0` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma leq_sub_add *) let leq_sub_add = section_proof [] `!m n p. (m - n <= p) = (m <= n + p)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])); (((((use_arg_then "subn_eq0")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma leq_subr *) let leq_subr = section_proof [] `!m n. n - m <= n` [ (((((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subnKC *) let subnKC = section_proof [] `!m n. m <= n ==> m + (n - m) = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma subnK *) let subnK = section_proof [] `!m n. m <= n ==> (n - m) + m = n` [ ((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subnKC") (disch_tac [])) THEN (clear_assumption "subnKC") THEN (exact_tac)) THEN (done_tac)); ];; (* Lemma addn_subA *) let addn_subA = section_proof [] `!m n p. p <= n ==> m + (n - p) = (m + n) - p` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"])); (((((fun arg_tac -> (use_arg_then "subnK") (fun fst_arg -> (use_arg_then "le_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subn_subA *) let subn_subA = section_proof [] `!m n p. p <= n ==> m - (n - p) = (m + p) - n` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"])); (((((fun arg_tac -> (use_arg_then "subnK") (fun fst_arg -> (use_arg_then "le_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subKn *) let subKn = section_proof [] `!m n. m <= n ==> n - (n - m) = m` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "subn_subA") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addKn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leq_subS *) let leq_subS = section_proof [] `!m n. m <= n ==> SUC n - m = SUC (n - m)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); ((((use_arg_then "add1n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "addn_subA") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))); ((((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma ltn_subS *) let ltn_subS = section_proof [] `!m n. m < n ==> n - m = SUC (n - SUC m)` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["lt_mn"])) THEN ((((use_arg_then "leq_subS")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma leq_sub2r *) let leq_sub2r = section_proof [] `!p m n. m <= n ==> m - p <= n - p` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"])); (((((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (use_arg_then "le_mn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_sub_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_sub2l *) let leq_sub2l = section_proof [] `!p m n. m <= n ==> p - n <= p - m` [ ((BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])) THEN ((((fun arg_tac -> (use_arg_then "leq_add2r") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`p - m`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] [])))))); ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then "leq_sub_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_sub2 *) let leq_sub2 = section_proof [] `!m1 m2 n1 n2. m1 <= m2 ==> n2 <= n1 ==> m1 - n1 <= m2 - n2` [ (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"])); (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2r") (fun fst_arg -> (use_arg_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["le_m12"])) THEN ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2l") (fun fst_arg -> (use_arg_then "m2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (exact_tac))); ];; (* Lemma ltn_sub2r *) let ltn_sub2r = section_proof [] `!p m n. p < n ==> m < n ==> m - p < n - p` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])); (((DISCH_THEN (fun snd_th -> (use_arg_then "ltn_subS") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))))); (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2r") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SUC p`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "subSS")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma ltn_sub2l *) let ltn_sub2l = section_proof [] `!p m n. m < p ==> m < n ==> p - n < p - m` [ (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])); (((DISCH_THEN (fun snd_th -> (use_arg_then "ltn_subS") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))))); (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2l") (fun fst_arg -> (use_arg_then "p") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (done_tac)); ];; (* Lemma ltn_add_sub *) let ltn_add_sub = section_proof [] `!m n p. (m + n < p) = (n < p - m)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])); (((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; let maxn = new_definition `maxn m n = if m < n then n else m`;; let minn = new_definition `minn m n = if m < n then m else n`;; (* Lemma max0n *) let max0n = section_proof [] `!n. maxn 0 n = n` [ ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxn0 *) let maxn0 = section_proof [] `!n. maxn n 0 = n` [ ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxnC *) let maxnC = section_proof [] `!m n. maxn m n = maxn n m` [ ((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxnl *) let maxnl = section_proof [] `!m n. n <= m ==> maxn m n = m` [ ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxnr *) let maxnr = section_proof [] `!m n. m <= n ==> maxn m n = n` [ ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma add_sub_maxn *) let add_sub_maxn = section_proof [] `!m n. m + (n - m) = maxn m n` [ ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxnAC *) let maxnAC = section_proof [] `!m n p. maxn (maxn m n) p = maxn (maxn m p) n` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])); (((repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_sub")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxnA *) let maxnA = section_proof [] `!m n p. maxn m (maxn n p) = maxn (maxn m n) p` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])); (((repeat_tactic 1 9 (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then "maxnAC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxnCA *) let maxnCA = section_proof [] `!m n p. maxn m (maxn n p) = maxn n (maxn m p)` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "maxnA")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (done_tac)); ];; (* Lemma eqn_maxr *) let eqn_maxr = section_proof [] `!m n. (maxn m n = n) = (m <= n)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_maxl *) let eqn_maxl = section_proof [] `!m n. (maxn m n = m) = (n <= m)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxnn *) let maxnn = section_proof [] `!n. maxn n n = n` [ (BETA_TAC THEN (move ["n"])); (((((use_arg_then "maxnl")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_maxr *) let leq_maxr = section_proof ["m";"n1";"n2"] `(m <= maxn n1 n2) <=> (m <= n1) \/ (m <= n2)` [ ((fun arg_tac -> arg_tac (Arg_term (`n2 <= n1`))) (term_tac (wlog_tac (move ["le_n21"])[`n1`; `n2`]))); (((THENL_LAST) (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "n2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["le_n12"])) ((((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "le_n21")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); (BETA_TAC THEN (move ["le_n21"])); (((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_n21")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((fun arg_tac -> (use_arg_then "EXCLUDED_MIDDLE") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m <= n1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (simp_tac))); ((((use_arg_then "contra") (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "leq_trans") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac)); ];; (* Lemma leq_maxl *) let leq_maxl = section_proof ["m";"n1";"n2"] `(maxn n1 n2 <= m) <=> (n1 <= m) /\ (n2 <= m)` [ (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_maxr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac)); ];; (* Lemma addn_maxl *) let addn_maxl = section_proof [] `!m1 m2 n. (maxn m1 m2) + n = maxn (m1 + n) (m2 + n)` [ ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addn_maxr *) let addn_maxr = section_proof [] `!m n1 n2. m + maxn n1 n2 = maxn (m + n1) (m + n2)` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"])) THEN ((repeat_tactic 1 9 (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then "addn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma min0n *) let min0n = section_proof ["n"] `minn 0 n = 0` [ ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma minn0 *) let minn0 = section_proof ["n"] `minn n 0 = 0` [ ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma minnC *) let minnC = section_proof ["m";"n"] `minn m n = minn n m` [ ((repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma minnr *) let minnr = section_proof ["m";"n"] `n <= m ==> minn m n = n` [ ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma minnl *) let minnl = section_proof ["m";"n"] `m <= n ==> minn m n = m` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "minnr") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma addn_min_max *) let addn_min_max = section_proof ["m";"n"] `minn m n + maxn m n = m + n` [ (((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma minn_to_maxn *) let minn_to_maxn = section_proof ["m";"n"] `minn m n = (m + n) - maxn m n` [ (((((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma sub_sub_minn *) let sub_sub_minn = section_proof ["m";"n"] `m - (m - n) = minn m n` [ (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minnCA *) let minnCA = section_proof [] `!m1 m2 m3. minn m1 (minn m2 m3) = minn m2 (minn m1 m3)` [ ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"])) THEN (repeat_tactic 1 9 (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] [(`minn _1 (minn _2 _3)`)])))))); ((((fun arg_tac -> (use_arg_then "subn_add2r") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`maxn m2 m3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then "subn_add2r") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`maxn m1 m3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`(m2 + _1) - _2`)]))))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))))); (((repeat_tactic 1 9 (((use_arg_then "addn_maxl")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addn_min_max")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addn_maxr")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnAC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m2 + m1`)]))))) THEN (done_tac)); ];; (* Lemma minnA *) let minnA = section_proof [] `!m1 m2 m3. minn m1 (minn m2 m3) = minn (minn m1 m2) m3` [ (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"])); (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [(`minn m2 _1`)])))) THEN (((use_arg_then "minnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minnAC *) let minnAC = section_proof ["m1";"m2";"m3"] `minn (minn m1 m2) m3 = minn (minn m1 m3) m2` [ (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_minr *) let eqn_minr = section_proof ["m";"n"] `(minn m n = n) = (n <= m)` [ (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))); (((((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] [(`n + m`)]))))) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`m = _1`)])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_minl *) let eqn_minl = section_proof ["m";"n"] `(minn m n = m) = (m <= n)` [ (((((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`_1 = m + n`)])))) THEN (((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_maxr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minnn *) let minnn = section_proof ["n"] `minn n n = n` [ (((((use_arg_then "minnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_minr *) let leq_minr = section_proof ["m";"n1";"n2"] `(m <= minn n1 n2) <=> (m <= n1) /\ (m <= n2)` [ ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma leq_minl *) let leq_minl = section_proof ["m";"n1";"n2"] `(minn n1 n2 <= m) <=> (n1 <= m) \/ (n2 <= m)` [ (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_minr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac)); ];; (* Lemma addn_minl *) let addn_minl = section_proof [] `!m1 m2 n. (minn m1 m2) + n = minn (m1 + n) (m2 + n)` [ ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addn_maxl")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] [])))))); (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 + n`)])))))) THEN (((use_arg_then "addn_subA")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma addn_minr *) let addn_minr = section_proof [] `!m n1 n2. m + minn n1 n2 = minn (m + n1) (m + n2)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"])); (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then "addn_minl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxnK *) let maxnK = section_proof ["m";"n"] `minn (maxn m n) m = m` [ (((((use_arg_then "minnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leq_maxr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxKn *) let maxKn = section_proof ["m";"n"] `minn n (maxn m n) = n` [ (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minnK *) let minnK = section_proof ["m";"n"] `maxn (minn m n) m = m` [ (((((use_arg_then "maxnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leq_minl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minKn *) let minKn = section_proof ["m";"n"] `maxn n (minn m n) = n` [ (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxn_minl *) let maxn_minl = section_proof ["m1";"m2";"n"] `maxn (minn m1 m2) n = minn (maxn m1 n) (maxn m2 n)` [ (((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] [])))))) THEN (arith_tac)); ];; (* Lemma maxn_minr *) let maxn_minr = section_proof ["m";"n1";"n2"] `maxn m (minn n1 n2) = minn (maxn m n1) (maxn m n2)` [ (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "maxnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then "maxn_minl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minn_maxl *) let minn_maxl = section_proof [] `!m1 m2 n. minn (maxn m1 m2) n = maxn (minn m1 n) (minn m2 n)` [ ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((((use_arg_then "maxn_minr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "maxn_minl")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "minnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn _1 n`)])))) THEN (repeat_tactic 1 9 (((use_arg_then "maxnK")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma minn_maxr *) let minn_maxr = section_proof [] `!m n1 n2. minn m (maxn n1 n2) = maxn (minn m n1) (minn m n2)` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"])); (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "minnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`minn m _1`)]))))) THEN (((use_arg_then "minn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Section Iteration *) begin_section "Iteration";; (add_section_var (mk_var ("m", (`:num`))); add_section_var (mk_var ("n", (`:num`))));; (add_section_var (mk_var ("x", (`:A`))); add_section_var (mk_var ("y", (`:A`))));; let iter = define `iter (SUC n) f (x:A) = f (iter n f x) /\ iter 0 f x = x`;; let iteri = define `iteri (SUC n) f (x:A) = f n (iteri n f x) /\ iteri 0 f x = x`;; (* Lemma iterSr *) let iterSr = section_proof ["n";"f";"x"] `iter (SUC n) f (x : A) = iter n f (f x)` [ ((((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN ((repeat_tactic 1 9 (((use_arg_then "iter")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma iterS *) let iterS = section_proof ["n";"f";"x"] `iter (SUC n) f (x:A) = f (iter n f x)` [ ((((use_arg_then "iter")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma iter_add *) let iter_add = section_proof ["n";"m";"f";"x"] `iter (n + m) f (x:A) = iter n f (iter m f x)` [ ((((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN (((repeat_tactic 1 9 (((use_arg_then "iter")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (((use_arg_then "add0n")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN ((TRY done_tac)) THEN (((use_arg_then "addSn")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "iterS")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma iteriS *) let iteriS = section_proof ["n";"f";"x"] `iteri (SUC n) f x = f n (iteri n f (x:A))` [ ((((use_arg_then "iteri")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Finalization of the section Iteration *) let iterSr = finalize_theorem iterSr;; let iterS = finalize_theorem iterS;; let iter_add = finalize_theorem iter_add;; let iteriS = finalize_theorem iteriS;; end_section "Iteration";; (* Lemma mul0n *) let mul0n = section_proof ["n"] `0 * n = 0` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma muln0 *) let muln0 = section_proof ["n"] `n * 0 = 0` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma mul1n *) let mul1n = section_proof ["n"] `1 * n = n` [ ((arith_tac) THEN (done_tac)); ];; (* Lemma mulSn *) let mulSn = section_proof ["m";"n"] `SUC m * n = n + m * n` [ (arith_tac); ];; (* Lemma mulSnr *) let mulSnr = section_proof ["m";"n"] `SUC m * n = m * n + n` [ (arith_tac); ];; (* Lemma mulnS *) let mulnS = section_proof ["m";"n"] `m * SUC n = m + m * n` [ ((((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) THEN (((repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["m"]))); ((((repeat_tactic 1 9 (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mulnSr *) let mulnSr = section_proof ["m";"n"] `m * SUC n = m * n + m` [ (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln1 *) let muln1 = section_proof ["n"] `n * 1 = n` [ (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `1 = SUC 0`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnSr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mulnC *) let mulnC = section_proof [] `!m n. m * n = n * m` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) THEN (((repeat_tactic 0 10 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mulnS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln_addl *) let muln_addl = section_proof ["m1";"m2";"n"] `(m1 + m2) * n = m1 * n + m2 * n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "m1") (disch_tac [])) THEN (clear_assumption "m1") THEN elim) [ALL_TAC; ((move ["m1"]) THEN (move ["IHm"]))]) (((((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))))) THEN (done_tac))); (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mulSn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln_addr *) let muln_addr = section_proof ["m";"n1";"n2"] `m * (n1 + n2) = m * n1 + m * n2` [ (((repeat_tactic 1 9 (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln_subl *) let muln_subl = section_proof [] `!m n p. (m - n) * p = m * p - n * p` [ ((THENL_FIRST) (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN ((THENL) case [ALL_TAC; (move ["n'"])])) (((repeat_tactic 1 9 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then "mul0n")(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then "sub0n")(fun tmp_arg1 -> (use_arg_then "subn0")(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))))); (((((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln_subr *) let muln_subr = section_proof [] `!m n p. m * (n - p) = m * n - m * p` [ ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then "muln_subl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mulnA *) let mulnA = section_proof [] `!m n p. m * (n * p) = (m * n) * p` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])); ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) ((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((repeat_tactic 1 9 (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mulnCA *) let mulnCA = section_proof ["m";"n1";"n2"] `m * (n1 * n2) = n1 * (m * n2)` [ (((repeat_tactic 1 9 (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (done_tac)); ];; (* Lemma mulnAC *) let mulnAC = section_proof ["m";"n";"p"] `(n * m) * p = (n * p) * m` [ (((repeat_tactic 1 9 (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`p * _1`)]))))) THEN (done_tac)); ];; (* Lemma muln_eq0 *) let muln_eq0 = section_proof ["m";"n"] `(m * n = 0) <=> (m = 0) \/ (n = 0)` [ ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then "muln0")(fun tmp_arg1 -> (use_arg_then "mul0n")(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (arith_tac)); ];; (* Lemma eqn_mul1 *) let eqn_mul1 = section_proof ["m";"n"] `(m * n = 1) <=> (m = 1) /\ (n = 1)` [ ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((THENL) case [ALL_TAC; ((THENL) case [ALL_TAC; (move ["n"])])])) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma muln_gt0 *) let muln_gt0 = section_proof ["m";"n"] `(0 < m * n) <=> (0 < m) /\ (0 < n)` [ ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma leq_pmull *) let leq_pmull = section_proof ["m";"n"] `0 < n ==> m <= n * m` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_pmulr *) let leq_pmulr = section_proof ["m";"n"] `0 < n ==> m <= m * n` [ (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_pmull") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leq_mul2l *) let leq_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 <= m * n2) <=> (m = 0) \/ (n1 <= n2)` [ (((((use_arg_then "leqE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_subr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_eq0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma leq_mul2r *) let leq_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m <= n2 * m) <=> (m = 0) \/ (n1 <= n2)` [ (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * m`)])))))) THEN (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_mul *) let leq_mul = section_proof ["m1";"m2";"n1";"n2"] `m1 <= n1 ==> m2 <= n2 ==> m1 * m2 <= n1 * n2` [ (BETA_TAC THEN (move ["le_mn1"]) THEN (move ["le_mn2"])); (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * m2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); ((THENL_FIRST) (ANTS_TAC) (((((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn2")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (DISCH_THEN apply_tac); (((((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn1")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_mul2l *) let eqn_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 = m * n2) <=> (m = 0) \/ (n1 = n2)` [ (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "orb_andr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma eqn_mul2r *) let eqn_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m = n2 * m) <=> (m = 0) \/ (n1 = n2)` [ (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "orb_andr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma leq_pmul2l *) let leq_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 <= m * n2) <=> (n1 <= n2))` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma leq_pmul2r *) let leq_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> ((n1 * m <= n2 * m) <=> (n1 <= n2))` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma eqn_pmul2l *) let eqn_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 = m * n2) <=> (n1 = n2))` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "eqn_mul2l")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma eqn_pmul2r *) let eqn_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> ((n1 * m = n2 * m) <=> (n1 = n2))` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "eqn_mul2r")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma ltn_mul2l *) let ltn_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 < m * n2) <=> (0 < m) /\ (n1 < n2)` [ (((((use_arg_then "lt0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_mul2r *) let ltn_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m < n2 * m) <=> (0 < m) /\ (n1 < n2)` [ (((((use_arg_then "lt0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_pmul2l *) let ltn_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 < m * n2) <=> (n1 < n2))` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then "ltn_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_pmul2r *) let ltn_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> (n1 * m < n2 * m <=> n1 < n2)` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "prednK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then "ltn_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_Pmull *) let ltn_Pmull = section_proof ["m";"n"] `1 < n ==> 0 < m ==> m < n * m` [ ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then "mul1n")(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then "ltn_pmul2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_Pmulr *) let ltn_Pmulr = section_proof ["m";"n"] `1 < n ==> 0 < m ==> m < m * n` [ ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_Pmull")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_mul *) let ltn_mul = section_proof ["m1";"m2";"n1";"n2"] `m1 < n1 ==> m2 < n2 ==> m1 * m2 < n1 * n2` [ (BETA_TAC THEN (move ["lt_mn1"]) THEN (move ["lt_mn2"])); (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_ltn_trans") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * m2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC); (ANTS_TAC); (((((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (DISCH_THEN apply_tac); ((((use_arg_then "ltn_pmul2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then "lt_mn2") (disch_tac [])) THEN (clear_assumption "lt_mn2") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma maxn_mulr *) let maxn_mulr = section_proof ["m";"n1";"n2"] `m * maxn n1 n2 = maxn (m * n1) (m * n2)` [ ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "fun_if")(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then "ltn_pmul2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma maxn_mull *) let maxn_mull = section_proof ["m1";"m2";"n"] `maxn m1 m2 * n = maxn (m1 * n) (m2 * n)` [ (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then "maxn_mulr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma minn_mulr *) let minn_mulr = section_proof ["m";"n1";"n2"] `m * minn n1 n2 = minn (m * n1) (m * n2)` [ ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "if_same")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "fun_if")(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then "ltn_pmul2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] []))))); ];; (* Lemma minn_mull *) let minn_mull = section_proof ["m1";"m2";"n"] `minn m1 m2 * n = minn (m1 * n) (m2 * n)` [ (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then "minn_mulr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; parse_as_infix("^", (24, "left"));; override_interface("^", `EXP`);; (* Lemma expn0 *) let expn0 = section_proof ["m"] `m ^ 0 = 1` [ ((((use_arg_then "EXP")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma expn1 *) let expn1 = section_proof ["m"] `m ^ 1 = m` [ ((((use_arg_then "EXP_1")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma expnS *) let expnS = section_proof ["m";"n"] `m ^ SUC n = m * m ^ n` [ ((((use_arg_then "EXP")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma expnSr *) let expnSr = section_proof ["m";"n"] `m ^ SUC n = m ^ n * m` [ (((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma exp0n *) let exp0n = section_proof ["n"] `0 < n ==> 0 ^ n = 0` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) ((((use_arg_then "LT_REFL")(thm_tac (new_rewrite [] [])))) THEN (done_tac))); (((((use_arg_then "EXP")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma exp1n *) let exp1n = section_proof ["n"] `1 ^ n = 1` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [(((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))); ((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul1n")(thm_tac (new_rewrite [] [])))))]) THEN (done_tac)); ];; (* Lemma expn_add *) let expn_add = section_proof ["m";"n1";"n2"] `m ^ (n1 + n2) = m ^ n1 * m ^ n2` [ (((THENL) (((use_arg_then "n1") (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))))); (((((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma expn_mull *) let expn_mull = section_proof ["m1";"m2";"n"] `(m1 * m2) ^ n = m1 ^ n * m2 ^ n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln1")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnCA")(thm_tac (new_rewrite [] [(`m2 * _1`)]))))) THEN (done_tac)); ];; (* Lemma expn_mulr *) let expn_mulr = section_proof ["m";"n1";"n2"] `m ^ (n1 * n2) = (m ^ n1) ^ n2` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n1") (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "exp1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_mull")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma expn_gt0 *) let expn_gt0 = section_proof ["m";"n"] `(0 < m ^ n) <=> (0 < m) \/ (n = 0)` [ ((THENL_FIRST) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))])) ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac))); (((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); (((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma expn_eq0 *) let expn_eq0 = section_proof ["m";"e"] `(m ^ e = 0) <=> (m = 0) /\ (0 < e)` [ (((repeat_tactic 1 9 (((use_arg_then "eqn0Ngt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt0n")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma ltn_expl *) let ltn_expl = section_proof ["m";"n"] `1 < m ==> n < m ^ n` [ ((THENL_FIRST) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])])) ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac))); ((((fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "m_gt1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2l") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC)); (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))); ((((fun arg_tac -> (use_arg_then "ltn_Pmull") (fun fst_arg -> (use_arg_then "m_gt1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma leq_exp2l *) let leq_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 <= m ^ n2 <=> n1 <= n2)` [ ((THENL_ROT (-1)) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then "n2") (disch_tac [])) THEN (clear_assumption "n2") THEN ((use_arg_then "n1") (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) THEN (BETA_TAC THEN ((THENL) case [ALL_TAC; (move ["q"])])) THEN ((repeat_tactic 0 10 (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))))); (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_pmul2l")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (move ["m_gt1"]))); ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (use_arg_then "m_gt1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_pmulr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma ltn_exp2l *) let ltn_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 < m ^ n2 <=> n1 < n2)` [ ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_exp2l *) let eqn_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 = m ^ n2 <=> n1 = n2)` [ ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma expnI *) let expnI = section_proof ["m"] `1 < m ==> !e1 e2. m ^ e1 = m ^ e2 ==> e1 = e2` [ ((BETA_TAC THEN (move ["m_gt1"]) THEN (move ["e1"]) THEN (move ["e2"])) THEN (((use_arg_then "eqn_exp2l")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leq_pexp2l *) let leq_pexp2l = section_proof ["m";"n1";"n2"] `0 < m ==> n1 <= n2 ==> m ^ n1 <= m ^ n2` [ (((THENL) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "exp1n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma ltn_pexp2l *) let ltn_pexp2l = section_proof ["m";"n1";"n2"] `0 < m ==> m ^ n1 < m ^ n2 ==> n1 < n2` [ (((THENL) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "exp1n")(thm_tac (new_rewrite [] [])))))); (((use_arg_then "ltn_exp2l")(thm_tac (new_rewrite [] []))))]) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma ltn_exp2r *) let ltn_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e < n ^ e <=> m < n)` [ ((BETA_TAC THEN (move ["e_gt0"])) THEN ((THENL) (split_tac) [ALL_TAC; (move ["ltmn"])])); ((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "contra") (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["lemn"]))); (((THENL) (((use_arg_then "e") (disch_tac [])) THEN (clear_assumption "e") THEN elim) [ALL_TAC; ((move ["e'"]) THEN (move ["IHe"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) (((use_arg_then "e_gt0") (disch_tac [])) THEN (clear_assumption "e_gt0") THEN ((use_arg_then "e") (disch_tac [])) THEN (clear_assumption "e") THEN elim) ((((use_arg_then "ltnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((THENL_FIRST) (BETA_TAC THEN ((THENL) case [ALL_TAC; ((move ["e"]) THEN (move ["IHe"]))])) (((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "expn1")(thm_tac (new_rewrite [] [])))))) THEN (done_tac))); (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "ltn_mul")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "IHe")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac)); ];; (* Lemma leq_exp2r *) let leq_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e <= n ^ e <=> m <= n)` [ ((BETA_TAC THEN (move ["e_gt0"])) THEN ((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma eqn_exp2r *) let eqn_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e = n ^ e <=> m = n)` [ ((BETA_TAC THEN (move ["e_gt0"])) THEN ((repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_exp2r")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma expIn *) let expIn = section_proof ["e"] `0 < e ==> !m n. m ^ e = n ^ e ==> m = n` [ ((BETA_TAC THEN (move ["e_gt0"]) THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "eqn_exp2r")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma fact0 *) let fact0 = section_proof [] `FACT 0 = 1` [ ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma factS *) let factS = section_proof ["n"] `FACT (SUC n) = (SUC n) * FACT n` [ ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma fact_gt0 *) let fact_gt0 = section_proof ["n"] `0 < FACT n` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) THEN ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (repeat_tactic 0 10 (((use_arg_then "muln_gt0")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))))) THEN (arith_tac) THEN (done_tac)); ];; let odd = new_basic_definition `odd = ODD`;; (* Lemma odd0 *) let odd0 = section_proof [] `odd 0 = F` [ ((((use_arg_then "odd")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 2 0 (((use_arg_then "ODD")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma oddS *) let oddS = section_proof ["n"] `odd (SUC n) = ~odd n` [ (((((use_arg_then "odd")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "ODD")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma odd1 *) let odd1 = section_proof [] `odd 1 = T` [ (((((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_add *) let odd_add = section_proof ["m";"n"] `odd (m + n) = odd m + odd n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHn"]))]) (((((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "oddS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addbA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_sub *) let odd_sub = section_proof ["m";"n"] `n <= m ==> odd (m - n) = odd m + odd n` [ ((BETA_TAC THEN (move ["le_nm"])) THEN (((fun arg_tac -> (use_arg_then "addIb") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`odd n`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then "odd_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "addbK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_opp *) let odd_opp = section_proof ["i";"m"] `odd m = F ==> i < m ==> odd (m - i) = odd i` [ (BETA_TAC THEN (move ["oddm"]) THEN (move ["lt_im"])); (((((fun arg_tac -> (use_arg_then "odd_sub") (fun fst_arg -> (fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "lt_im") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddm")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_mul *) let odd_mul = section_proof ["m";"n"] `odd (m * n) <=> odd m /\ odd n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) (((((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "andb_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_exp *) let odd_exp = section_proof ["m";"n"] `odd (m ^ n) <=> (n = 0) \/ odd m` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd1")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_mul")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `SUC n = 0 <=> F`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orFb")(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`odd m`))) (term_tac (set_tac "b"))); (((use_arg_then "IHn") (disch_tac [])) THEN (clear_assumption "IHn") THEN ((use_arg_then "b_def") (disch_tac [])) THEN (clear_assumption "b_def") THEN BETA_TAC THEN (move ["_"]) THEN (move ["_"])); ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac)); ];; let double = define `double 0 = 0 /\ (!n. double (SUC n) = SUC (SUC (double n)))`;; (* Lemma double0 *) let double0 = section_proof [] `double 0 = 0` [ ((((use_arg_then "double")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma doubleS *) let doubleS = section_proof ["n"] `double (SUC n) = SUC (SUC (double n))` [ ((((use_arg_then "double")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac)); ];; (* Lemma addnn *) let addnn = section_proof ["n"] `n + n = double n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "addn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then "addnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma mul2n *) let mul2n = section_proof ["m"] `2 * m = double m` [ (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC 1`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma muln2 *) let muln2 = section_proof ["m"] `m * 2 = double m` [ (((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma double_add *) let double_add = section_proof ["m";"n"] `double (m + n) = double m + double n` [ (((repeat_tactic 1 9 (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then "addnCA") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`n + _1`)]))))) THEN (done_tac)); ];; (* Lemma double_sub *) let double_sub = section_proof ["m";"n"] `double (m - n) = double m - double n` [ ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((use_arg_then "sub0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "sub0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); (((repeat_tactic 1 9 (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHm")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_double *) let leq_double = section_proof ["m";"n"] `(double m <= double n <=> m <= n)` [ (((repeat_tactic 1 9 (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "double_sub")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((THENL) (((fun arg_tac -> arg_tac (Arg_term (`m - n`))) (disch_tac [])) THEN case) [ALL_TAC; (move ["n"])]) THEN (((use_arg_then "double")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma ltn_double *) let ltn_double = section_proof ["m";"n"] `(double m < double n) = (m < n)` [ (((repeat_tactic 2 0 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_double")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma ltn_Sdouble *) let ltn_Sdouble = section_proof ["m";"n"] `(SUC (double m) < double n) = (m < n)` [ ((repeat_tactic 1 9 (((use_arg_then "muln2")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma leq_Sdouble *) let leq_Sdouble = section_proof ["m";"n"] `(double m <= SUC (double n)) = (m <= n)` [ (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_Sdouble")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma odd_double *) let odd_double = section_proof ["n"] `odd (double n) = F` [ (((((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "odd_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addbb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma double_gt0 *) let double_gt0 = section_proof ["n"] `(0 < double n) = (0 < n)` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (arith_tac)); ];; (* Lemma double_eq0 *) let double_eq0 = section_proof ["n"] `(double n = 0) = (n = 0)` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (arith_tac)); ];; (* Lemma double_mull *) let double_mull = section_proof ["m";"n"] `double (m * n) = double m * n` [ (((repeat_tactic 1 9 (((use_arg_then "mul2n")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma double_mulr *) let double_mulr = section_proof ["m";"n"] `double (m * n) = m * double n` [ (((repeat_tactic 1 9 (((use_arg_then "muln2")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; let half_def = define `HALF 0 = (0, 0) /\ !n. HALF (SUC n) = (SND (HALF n), SUC (FST (HALF n)))`;; let half = new_basic_definition `half = FST o HALF`;; let uphalf = new_basic_definition `uphalf = SND o HALF`;; (* Lemma half0 *) let half0 = section_proof [] `half 0 = 0` [ (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma uphalf0 *) let uphalf0 = section_proof [] `uphalf 0 = 0` [ (((((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma halfS *) let halfS = section_proof ["n"] `half (SUC n) = uphalf n` [ (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma uphalfS *) let uphalfS = section_proof ["n"] `uphalf (SUC n) = SUC (half n)` [ (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac)); ];; (* Lemma doubleK *) let doubleK = section_proof ["x"] `half (double x) = x` [ ((THENL_FIRST) ((THENL) (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; let half_double = doubleK;; (* Lemma double_inj *) let double_inj = section_proof [] `!m n. double m = double n ==> m = n` [ (BETA_TAC THEN (move ["m"]) THEN (move ["n"])); ((((((use_arg_then "doubleK")(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then "doubleK")(gsym_then (thm_tac (new_rewrite [2] [(`n`)])))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uphalf_double *) let uphalf_double = section_proof ["n"] `uphalf (double n) = n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalf0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma uphalf_half *) let uphalf_half = section_proof ["n"] `uphalf n = (if odd n then 1 else 0) + half n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "uphalf0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))); ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((fun arg_tac ->(use_arg_then "add0n")(fun tmp_arg1 -> (use_arg_then "addn0")(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma odd_double_half *) let odd_double_half = section_proof ["n"] `(if odd n then 1 else 0) + double (half n) = n` [ ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((((use_arg_then "IHn")(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalf_half")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] []))))); (((use_arg_then "IHn") (disch_tac [])) THEN (clear_assumption "IHn") THEN BETA_TAC THEN (move ["_"])); ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma half_bit_double *) let half_bit_double = section_proof ["n";"b"] `half ((if b then 1 else 0) + double n) = n` [ ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN ((simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac ->(use_arg_then "half_double")(fun tmp_arg1 -> (use_arg_then "uphalf_double")(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma half_add *) let half_add = section_proof ["m";"n"] `half (m + n) = (if odd m /\ odd n then 1 else 0) + (half m + half n)` [ ((((use_arg_then "odd_double_half")(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_double_half")(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "double_add")(gsym_then (thm_tac (new_rewrite [] [])))))); ((repeat_tactic 2 0 ((((fun arg_tac -> arg_tac (Arg_term (`odd _`))) (disch_tac [])) THEN case))) THEN ((simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "half_double")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalf_double")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))); ((((use_arg_then "half_double")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma half_leq *) let half_leq = section_proof ["m";"n"] `m <= n ==> half m <= half n` [ (((DISCH_THEN (fun snd_th -> (use_arg_then "subnK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then "half_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma half_gt0 *) let half_gt0 = section_proof ["n"] `(0 < half n) = (1 < n)` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (case THEN ALL_TAC)]) THEN ((repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalf0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma mulnn *) let mulnn = section_proof ["m"] `m * m = m ^ 2` [ (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC (SUC 0)`)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln1")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma sqrn_add *) let sqrn_add = section_proof ["m";"n"] `(m + n) ^ 2 = (m ^ 2 + n ^ 2) + 2 * (m * n)` [ ((repeat_tactic 1 9 (((use_arg_then "mulnn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_addr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))))); (((((use_arg_then "EQ_ADD_LCANCEL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma sqrn_sub *) let sqrn_sub = section_proof ["m";"n"] `n <= m ==> (m - n) ^ 2 = (m ^ 2 + n ^ 2) - 2 * (m * n)` [ ((DISCH_THEN (fun snd_th -> (use_arg_then "subnK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["def_m"])); ((((use_arg_then "def_m")(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] []))))); (((repeat_tactic 2 0 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_addr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mulnn")(gsym_then (thm_tac (new_rewrite [] [(`n EXP 2`)]))))) THEN (((use_arg_then "muln_addl")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "def_m")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma sqrn_add_sub *) let sqrn_add_sub = section_proof ["m";"n"] `n <= m ==> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2` [ ((BETA_TAC THEN (move ["le_nm"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 = 2 * 2`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_sub")(gsym_then (thm_tac (new_rewrite [] []))))))); (((((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "sqrn_sub")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma subn_sqr *) let subn_sqr = section_proof ["m";"n"] `m ^ 2 - n ^ 2 = (m - n) * (m + n)` [ (((((use_arg_then "muln_subl")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "muln_addr")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "mulnn")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma ltn_sqr *) let ltn_sqr = section_proof ["m";"n"] `(m ^ 2 < n ^ 2) = (m < n)` [ (((((use_arg_then "ltn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma leq_sqr *) let leq_sqr = section_proof ["m";"n"] `(m ^ 2 <= n ^ 2) = (m <= n)` [ (((((use_arg_then "leq_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma sqrn_gt0 *) let sqrn_gt0 = section_proof ["n"] `(0 < n ^ 2) = (0 < n)` [ ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then "ltn_sqr") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then "exp0n")(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac))); ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma eqn_sqr *) let eqn_sqr = section_proof ["m";"n"] `(m ^ 2 = n ^ 2) = (m = n)` [ (((((use_arg_then "eqn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac)); ];; (* Lemma sqrn_inj *) let sqrn_inj = section_proof ["m";"n"] `m ^ 2 = n ^ 2 ==> m = n` [ (BETA_TAC THEN (move ["eq"])); (((fun arg_tac -> (use_arg_then "expIn") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `0 < 2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["inj"])); ((((fun arg_tac -> (use_arg_then "inj") (fun fst_arg -> (use_arg_then "eq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; let leqif = new_definition `!m n c. leqif m n c <=> (m <= n /\ ((m = n) <=> c))`;; (* Lemma leqifP *) let leqifP = section_proof ["m";"n";"c"] `leqif m n c <=> if c then m = n else m < n` [ ((THENL_FIRST) (((((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqif")(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac))); ((((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leqif_imp_le *) let leqif_imp_le = section_proof ["m";"n";"c"] `leqif m n c ==> m <= n` [ (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma leqif_imp_eq *) let leqif_imp_eq = section_proof ["m";"n";"c"] `leqif m n c ==> (m = n <=> c)` [ (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma leqif_refl *) let leqif_refl = section_proof ["m";"c"] `(leqif m m c) <=> c` [ (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leqif_trans *) let leqif_trans = section_proof ["m1";"m2";"m3";"c1";"c2"] `leqif m1 m2 c1 ==> leqif m2 m3 c2 ==> leqif m1 m3 (c1 /\ c2)` [ (repeat_tactic 1 9 (((use_arg_then "leqifP")(thm_tac (new_rewrite [] []))))); ((THENL_FIRST) ((((use_arg_then "c1") (disch_tac [])) THEN (clear_assumption "c1") THEN case) THEN (((use_arg_then "c2") (disch_tac [])) THEN (clear_assumption "c2") THEN case THEN (simp_tac) THEN (move ["lt12"]))) ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac))); ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac)); ];; (* Lemma monotone_leqif *) let monotone_leqif = section_proof ["f"] `(!m n. f m <= f n <=> m <= n) ==> !m n c. (leqif (f m) (f n) c) <=> (leqif m n c)` [ (BETA_TAC THEN (move ["f_mono"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["c"])); (((repeat_tactic 1 9 (((use_arg_then "leqifP")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "f_mono")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma leqif_geq *) let leqif_geq = section_proof ["m";"n"] `m <= n ==> leqif m n (n <= m)` [ ((BETA_TAC THEN (move ["lemn"])) THEN (((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN ((TRY done_tac))) THEN (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "lemn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma leqif_eq *) let leqif_eq = section_proof ["m";"n"] `m <= n ==> leqif m n (m = n)` [ ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma geq_leqif *) let geq_leqif = section_proof ["a";"b";"C"] `leqif a b C ==> ((b <= a) <=> C)` [ ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (case THEN (move ["le_ab"])) THEN (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "le_ab")(thm_tac (new_rewrite [] [])))) THEN (done_tac)); ];; (* Lemma ltn_leqif *) let ltn_leqif = section_proof ["a";"b";"C"] `leqif a b C ==> (a < b <=> ~ C)` [ (BETA_TAC THEN (move ["le_ab"])); (((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "geq_leqif") (fun fst_arg -> (use_arg_then "le_ab") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leqif_add *) let leqif_add = section_proof ["m1";"n1";"c1";"m2";"n2";"c2"] `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==> leqif (m1 + m2) (n1 + n2) (c1 /\ c2)` [ ((((fun arg_tac -> (use_arg_then "monotone_leqif") (fun fst_arg -> (fun arg_tac -> (use_arg_then "leq_add2r") (fun fst_arg -> (use_arg_then "m2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["le1"])); (((fun arg_tac -> (use_arg_then "monotone_leqif") (fun fst_arg -> (fun arg_tac -> (use_arg_then "leq_add2l") (fun fst_arg -> (use_arg_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))); (((use_arg_then "leqif_trans") (disch_tac [])) THEN (clear_assumption "leqif_trans") THEN (exact_tac)); ];; (* Lemma leqif_mul *) let leqif_mul = section_proof ["m1";"n1";"c1";"m2";"n2";"c2"] `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==> leqif (m1 * m2) (n1 * n2) (n1 * n2 = 0 \/ (c1 /\ c2))` [ (BETA_TAC THEN (move ["le1"]) THEN (move ["le2"])); ((THENL) (((fun arg_tac -> (use_arg_then "posnP") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["n12_0"]); ALL_TAC]); ((((use_arg_then "n12_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le2") (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then "le1") (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then "n12_0") (disch_tac [])) THEN (clear_assumption "n12_0") THEN BETA_TAC) THEN (((use_arg_then "muln_eq0")(thm_tac (new_rewrite [] []))))); ((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((THENL) (((use_arg_then "m2") (disch_tac [])) THEN (clear_assumption "m2") THEN ((use_arg_then "m1") (disch_tac [])) THEN (clear_assumption "m1") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["m'"])]) THEN ((repeat_tactic 1 9 (((use_arg_then "leqif")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (arith_tac)); ((((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (BETA_TAC THEN (case THEN ((move ["n1_gt0"]) THEN (move ["n2_gt0"]))))); (((fun arg_tac -> (use_arg_then "posnP") (fun fst_arg -> (use_arg_then "m2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN ((THENL) case [(move ["m2_0"]); (move ["m2_gt0"])])); ((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le2") (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))))); (((((use_arg_then "andbC")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "m2_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n1_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n2_gt0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then "n1_gt0") (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2l") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "monotone_leqif") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mn1"]))); (((use_arg_then "le2") (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then "Mn1") (disch_tac [])) THEN (clear_assumption "Mn1") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))); ((((use_arg_then "m2_gt0") (disch_tac [])) THEN (clear_assumption "m2_gt0") THEN (DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2r") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "monotone_leqif") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mm2"]))); (((use_arg_then "le1") (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then "Mm2") (disch_tac [])) THEN (clear_assumption "Mm2") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))); (BETA_TAC THEN (move ["leq1"]) THEN (move ["leq2"])); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leqif_trans") (fun fst_arg -> (use_arg_then "leq1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "leq2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))))); (((fun arg_tac -> arg_tac (Arg_term (`c1 /\ c2`))) (disch_tac [])) THEN case THEN (simp_tac)); (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n1_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n2_gt0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma nat_Cauchy *) let nat_Cauchy = section_proof ["m";"n"] `leqif (2 * (m * n)) (m ^ 2 + n ^ 2) (m = n)` [ ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`]))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leqP") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN ((TRY done_tac))) THEN (((((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (move ["mn"]))); ((((use_arg_then "le_nm") (disch_tac [])) THEN (clear_assumption "le_nm") THEN (DISCH_THEN apply_tac)) THEN (((fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "mn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac)); (BETA_TAC THEN (move ["le_nm"])); (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))); ((THENL_FIRST) ((THENL) (((fun arg_tac -> (use_arg_then "EXCLUDED_MIDDLE") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m = n`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); (move ["ne_mn"])]) (((((use_arg_then "mulnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] []))))) THEN (done_tac))); (((((use_arg_then "ne_mn")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac)) THEN ((((use_arg_then "subn_gt0")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "sqrn_sub")(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "sqrn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma nat_AGM2 *) let nat_AGM2 = section_proof ["m";"n"] `leqif (4 * (m * n)) ((m + n) ^ 2) (m = n)` [ ((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 = 2 * 2`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqifP")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "ltn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_addr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] []))))); (((((fun arg_tac -> (use_arg_then "leqif_imp_eq") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "if_same")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; let distn = new_definition `!m n. distn m n = (m - n) + (n - m)`;; (* Lemma distnC *) let distnC = section_proof ["m";"n"] `distn m n = distn n m` [ (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distn_add2l *) let distn_add2l = section_proof ["d";"m";"n"] `distn (d + m) (d + n) = distn m n` [ (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma distn_add2r *) let distn_add2r = section_proof ["d";"m";"n"] `distn (m + d) (n + d) = distn m n` [ (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma distnEr *) let distnEr = section_proof ["m";"n"] `m <= n ==> distn m n = n - m` [ (BETA_TAC THEN (move ["le_m_n"])); (((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then "EQ_IMP") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leqE") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "le_m_n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distnEl *) let distnEl = section_proof ["m";"n"] `n <= m ==> distn m n = m - n` [ ((BETA_TAC THEN (move ["le_n_m"])) THEN ((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma dist0n *) let dist0n = section_proof ["n"] `distn 0 n = n` [ (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["m"])]) THEN ((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "sub0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distn0 *) let distn0 = section_proof ["n"] `distn n 0 = n` [ (((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "dist0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distnn *) let distnn = section_proof ["m"] `distn m m = 0` [ (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distn_eq0 *) let distn_eq0 = section_proof ["m";"n"] `(distn m n = 0) <=> (m = n)` [ (((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn_eq0")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_eq0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)); ];; (* Lemma distnS *) let distnS = section_proof ["m"] `distn m (SUC m) = 1` [ ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "distn_add2r") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "dist0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distSn *) let distSn = section_proof ["m"] `distn (SUC m) m = 1` [ (((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma distn_eq1 *) let distn_eq1 = section_proof ["m";"n"] `(distn m n = 1) <=> (if m < n then SUC m = n else m = SUC n)` [ ((THENL) (((fun arg_tac -> (fun arg_tac -> (use_arg_then "ltnP") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["lt_mn"]); (move ["le_mn"])]); (((((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`_ = 1`)])))) THEN (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subnK")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "distnEl")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subnK")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac)); ];; (* Lemma leqif_add_distn *) let leqif_add_distn = section_proof ["m";"n";"p"] `leqif (distn m p) (distn m n + distn n p) ((m <= n /\ n <= p) \/ (p <= n /\ n <= m))` [ (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`!m p. m <= p ==> leqif (distn m p) (distn m n + distn n p) (m <= n /\ n <= p \/ p <= n /\ n <= m)`))) (term_tac (have_gen_tac [](move ["IH"]))))); ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "p") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN ((TRY done_tac))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "IH") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC)); (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "distnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`distn n _`)])))) THEN (repeat_tactic 1 9 (((use_arg_then "distnC")(thm_tac (new_rewrite [] [(`distn p _`)])))))) THEN (done_tac)); (BETA_TAC THEN (move ["m"]) THEN (move ["p"]) THEN (move ["le_mp"])); ((((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((THENL) (((fun arg_tac -> (use_arg_then "EXCLUDED_MIDDLE") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m <= n /\ n <= p`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [((case THEN ((move ["le_mn"]) THEN (move ["le_np"]))) THEN ((simp_tac THEN TRY done_tac))); ALL_TAC]); (((repeat_tactic 1 9 (((use_arg_then "distnEr")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)); (((((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN ALL_TAC THEN ((THENL) case [(move ["lt_nm"]); (move ["lt_pn"])])); (((fun arg_tac -> (fun arg_tac -> (use_arg_then "ltn_leq_trans") (fun fst_arg -> (use_arg_then "lt_nm") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "le_mp") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_np"])); (((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "lt_nm")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt_np")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ltn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltn_sub2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_ltn_trans") (fun fst_arg -> (use_arg_then "le_mp") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "lt_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_mn"])); (((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "lt_mn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt_pn")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ltn_addr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "ltn_sub2r")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];; (* Lemma leq_add_distn *) let leq_add_distn = section_proof ["m";"n";"p"] `distn m p <= distn m n + distn n p` [ ((((fun arg_tac -> (use_arg_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leqif_add_distn") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "p") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac)); ];; (* Lemma sqrn_distn *) let sqrn_distn = section_proof ["m";"n"] `(distn m n) ^ 2 + 2 * (m * n) = m ^ 2 + n ^ 2` [ ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`]))); (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (DISCH_THEN (fun snd_th -> (use_arg_then "le_nm") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN ((TRY done_tac))); (((((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n EXP 2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (move ["le_nm"])) THEN ((((use_arg_then "distnEl")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "sqrn_sub")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ];;