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