1(*************************************************************************** 2 * 3 * intExtensionLib.sml 4 * 5 * Jens Brandt 6 * 7 ***************************************************************************) 8 9structure intExtensionLib :> intExtensionLib = 10struct 11 12open HolKernel boolLib Parse bossLib; 13 14(* interactive mode 15app load ["pairTheory", "pairLib", "integerTheory","intLib", 16 "ringLib", "integerRingTheory","integerRingLib", 17 "fracTheory","fracUtils", "intExtensionTheory"]; 18*) 19 20open 21 arithmeticTheory 22 pairTheory pairLib integerTheory intLib 23 ringLib integerRingTheory integerRingLib 24 intExtensionTheory; 25 26val ERR = mk_HOL_ERR "intExtensionLib" 27 28(*-------------------------------------------------------------------------- 29 * INT_SGN_CASES_TAC: term -> tactic 30 * 31 * A ?- P 32 * ======================== INT_SGN_CASES_TAC t1 33 * A, (SGN t1 = ~1) ?- P 34 * A, (SGN t1 = 0) ?- P 35 * A, (SGN t1 = 1) ?- P 36 *--------------------------------------------------------------------------*) 37 38val INT_SGN_CASES_TAC = fn term1 => 39 MATCH_MP_TAC (SPEC term1 INT_SGN_CASES) THEN REPEAT CONJ_TAC THEN STRIP_TAC 40handle HOL_ERR _ => raise ERR "INT_SGN_CASES_TAC" ""; 41 42(*-------------------------------------------------------------------------- 43 * INT_CALCEQ_TAC : tactic 44 *--------------------------------------------------------------------------*) 45 46val INT_CALCEQ_TAC = 47 RW_TAC int_ss [] THEN 48 INT_RING_TAC; 49 50(*========================================================================== 51 * end of structure 52 *==========================================================================*) 53end; 54