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