1(* file inttoScript.sml, split off from totoScript 12/13/13 to be the  *)
2(* only theory that loads intLib. *)
3
4(* app load ["totoTheory", "intLib"]; *)
5
6open HolKernel boolLib Parse;
7
8val _ = set_trace "Unicode" 0;
9open pred_setLib pred_setTheory relationTheory pairTheory;
10open bossLib PairRules arithmeticTheory numeralTheory Defn;
11open totoTheory intLib;
12
13val _ = new_theory "intto";
14val _ = ParseExtras.temp_loose_equality()
15
16(* My habitual abbreviations: *)
17
18val AR = ASM_REWRITE_TAC [];
19fun ulist x = [x];
20
21val _ = intLib.deprecate_int ();
22
23val _ = Defn.def_suffix := ""; (* replacing default "_def" *)
24
25(* ***************************************************************** *)
26(* Following switch, BigSig, allows "maybe_thm" to act either as     *)
27(* store_thm or as prove, thus maximizing or minimizing the output   *)
28(* from print_theory and the stuff known to DB.match, DB.find        *)
29(* ***************************************************************** *)
30
31val BigSig = false;
32
33fun maybe_thm (s, tm, tac) = if BigSig then store_thm (s, tm, tac)
34                                       else prove (tm, tac);
35
36(* **************************************************************** *)
37(* Theorems to support intto_CONV, for comparing at type int.       *)
38(* **************************************************************** *)
39
40(* integer parsing remains deprecated; note use of suffix i below. *)
41
42(* An integer ground term is, as well as I can see, either a application of
43   ``$&`` to a num ground term (which is either ``0`` or an application
44   of NUMERAL to a pile of ZERO, BIT0, and BIT1) or an application of
45   numeric_negate:int -> int to such a &-application. ``-0`` is possible. *)
46
47val intOrd = Define`intOrd = TO_of_LinearOrder ($< :int reln)`;
48
49val StrongLinearOrder_int_lt = maybe_thm ("StrongLinearOrder_int_lt",
50``StrongLinearOrder ($< :int reln)``,
51SRW_TAC [][StrongLinearOrder,
52 StrongOrder_ALT, trichotomous, Order, irreflexive_def, transitive_def] THENL
53[IMP_RES_TAC integerTheory.INT_LT_TRANS
54,STRIP_ASSUME_TAC (SPECL [``a:int``, ``b:int``] integerTheory.INT_LT_TOTAL)
55 THEN AR]);
56
57val TO_intOrd = maybe_thm ("TO_intOrd", ``TotOrd intOrd``,
58REWRITE_TAC [intOrd] THEN MATCH_MP_TAC TotOrd_TO_of_Strong THEN
59ACCEPT_TAC StrongLinearOrder_int_lt);
60
61val intto = Define`intto = TO intOrd`;
62
63val apintto_thm = store_thm ("apintto_thm", ``apto intto = intOrd``,
64REWRITE_TAC [intto, GSYM TO_apto_TO_ID, TO_intOrd]);
65
66val pos_pos_thm = store_thm ("pos_pos_thm",
67``!m:num n:num. intOrd (&m) (&n) = numOrd m n``,
68 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]);
69
70val neg_neg_thm = store_thm ("neg_neg_thm",
71``!m:num n:num. intOrd (numeric_negate (&m)) (numeric_negate (&n)) =
72                numOrd n m``,
73 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]);
74
75val BIT1_nz = store_thm ("BIT1_nz",
76``!n. BIT1 n <> 0``,
77SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt,
78                    GSYM arithmeticTheory.ALT_ZERO]);
79
80val BIT2_nz = store_thm ("BIT2_nz",
81``!n. BIT2 n <> 0``,
82SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt,
83                    GSYM arithmeticTheory.ALT_ZERO]);
84
85val neg_lt_BIT1_thm = store_thm ("neg_lt_BIT1_thm",
86``!m:num n:num. intOrd (numeric_negate (&m)) (& (BIT1 n)) = LESS``,
87SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]);
88
89val neg_lt_BIT2_thm = store_thm ("neg_lt_BIT2_thm",
90``!m:num n:num. intOrd (numeric_negate (&m)) (& (BIT2 n)) = LESS``,
91SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]);
92
93val neg_BIT1_lt_thm = store_thm ("neg_BIT1_lt_thm",
94``!m:num n:num. intOrd (numeric_negate (& (BIT1 m))) (& n) = LESS``,
95SRW_TAC [] [TO_of_LinearOrder, intOrd,  BIT1_nz]);
96
97val neg_BIT2_lt_thm = store_thm ("neg_BIT2_lt_thm",
98``!m:num n:num. intOrd (numeric_negate (& (BIT2 m))) (& n) = LESS``,
99SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]);
100
101val neg_ZERO_eq_ZERO_thm = store_thm ("neg_ZERO_eq_ZERO_thm",
102``intOrd (numeric_negate (& ZERO)) (& ZERO) = EQUAL``,
103SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]);
104
105val BIT1_gt_neg_thm = store_thm ("BIT1_gt_neg_thm",
106``!m:num n:num. intOrd (& (BIT1 m)) (numeric_negate (&n)) = GREATER``,
107SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]);
108
109val BIT2_gt_neg_thm = store_thm ("BIT2_gt_neg_thm",
110``!m:num n:num. intOrd (& (BIT2 m)) (numeric_negate (&n)) = GREATER``,
111SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]);
112
113val gt_neg_BIT1_thm = store_thm ("gt_neg_BIT1_thm",
114``!m:num n:num. intOrd (& m) (numeric_negate (& (BIT1 n))) = GREATER``,
115SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]);
116
117val gt_neg_BIT2_thm = store_thm ("gt_neg_BIT2_thm",
118``!m:num n:num. intOrd (& m) (numeric_negate (& (BIT2 n))) = GREATER``,
119SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]);
120
121val ZERO_eq_neg_ZERO_thm = store_thm ("ZERO_eq_neg_ZERO_thm",
122``intOrd (& ZERO) (numeric_negate (& ZERO)) = EQUAL``,
123SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]);
124
125val _ = export_theory ();
126