inttoScript.sml

1(* file inttoScript.sml, split off from totoScript 12/13/13 to be the  *)
2(* only theory that loads intLib. *)
3
4Theory intto
5Ancestors
6  pred_set relation pair arithmetic numeral toto integer
7Libs
8  pred_setLib PairRules Defn intLib
9
10
11val _ = set_trace "Unicode" 0;
12val _ = ParseExtras.temp_loose_equality()
13
14(* My habitual abbreviations: *)
15
16val AR = ASM_REWRITE_TAC [];
17fun ulist x = [x];
18
19(* **************************************************************** *)
20(* Theorems to support intto_CONV, for comparing at type int.       *)
21(* **************************************************************** *)
22
23(* integer parsing remains deprecated; note use of suffix i below. *)
24
25(* An integer ground term is, as well as I can see, either a application of
26   ``$&`` to a num ground term (which is either ``0`` or an application
27   of NUMERAL to a pile of ZERO, BIT0, and BIT1) or an application of
28   numeric_negate:int -> int to such a &-application. ``-0`` is possible. *)
29
30Definition intOrd:  intOrd = TO_of_LinearOrder ($< :int reln)
31End
32
33Theorem StrongLinearOrder_int_lt[local]:
34  StrongLinearOrder ($< :int reln)
35Proof
36SRW_TAC [][StrongLinearOrder,
37 StrongOrder_ALT, trichotomous, Order, irreflexive_def, transitive_def] THENL
38[IMP_RES_TAC integerTheory.INT_LT_TRANS
39,STRIP_ASSUME_TAC (SPECL [``a:int``, ``b:int``] integerTheory.INT_LT_TOTAL)
40 THEN AR]
41QED
42
43Theorem TO_intOrd[local]:
44  TotOrd intOrd
45Proof
46  REWRITE_TAC [intOrd] THEN MATCH_MP_TAC TotOrd_TO_of_Strong THEN
47  ACCEPT_TAC StrongLinearOrder_int_lt
48QED
49
50Definition intto:  intto = TO intOrd
51End
52
53Theorem apintto_thm:   apto intto = intOrd
54Proof
55REWRITE_TAC [intto, GSYM TO_apto_TO_ID, TO_intOrd]
56QED
57
58Theorem pos_pos_thm:
59  !m:num n:num. intOrd (&m) (&n) = numOrd m n
60Proof
61 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]
62QED
63
64Theorem neg_neg_thm:
65  !m:num n:num. intOrd (numeric_negate (&m)) (numeric_negate (&n)) =
66                numOrd n m
67Proof
68 SRW_TAC [] [TO_of_LinearOrder, intOrd, numOrd]
69QED
70
71Theorem BIT1_nz:
72  !n. BIT1 n <> 0
73Proof
74SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt,
75                    GSYM arithmeticTheory.ALT_ZERO]
76QED
77
78Theorem BIT2_nz:
79  !n. BIT2 n <> 0
80Proof
81SRW_TAC [] [arithmeticTheory.NOT_ZERO_LT_ZERO, numeralTheory.numeral_lt,
82                    GSYM arithmeticTheory.ALT_ZERO]
83QED
84
85Theorem neg_lt_BIT1_thm:
86  !m:num n:num. intOrd (numeric_negate (&m)) (& (BIT1 n)) = LESS
87Proof
88SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]
89QED
90
91Theorem neg_lt_BIT2_thm:
92  !m:num n:num. intOrd (numeric_negate (&m)) (& (BIT2 n)) = LESS
93Proof
94SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]
95QED
96
97Theorem neg_BIT1_lt_thm:
98  !m:num n:num. intOrd (numeric_negate (& (BIT1 m))) (& n) = LESS
99Proof
100SRW_TAC [] [TO_of_LinearOrder, intOrd,  BIT1_nz]
101QED
102
103Theorem neg_BIT2_lt_thm:
104  !m:num n:num. intOrd (numeric_negate (& (BIT2 m))) (& n) = LESS
105Proof
106SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]
107QED
108
109Theorem neg_ZERO_eq_ZERO_thm:
110  intOrd (numeric_negate (& ZERO)) (& ZERO) = EQUAL
111Proof
112SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]
113QED
114
115Theorem BIT1_gt_neg_thm:
116  !m:num n:num. intOrd (& (BIT1 m)) (numeric_negate (&n)) = GREATER
117Proof
118SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]
119QED
120
121Theorem BIT2_gt_neg_thm:
122  !m:num n:num. intOrd (& (BIT2 m)) (numeric_negate (&n)) = GREATER
123Proof
124SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]
125QED
126
127Theorem gt_neg_BIT1_thm:
128  !m:num n:num. intOrd (& m) (numeric_negate (& (BIT1 n))) = GREATER
129Proof
130SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT1_nz]
131QED
132
133Theorem gt_neg_BIT2_thm:
134  !m:num n:num. intOrd (& m) (numeric_negate (& (BIT2 n))) = GREATER
135Proof
136SRW_TAC [] [TO_of_LinearOrder, intOrd, BIT2_nz]
137QED
138
139Theorem ZERO_eq_neg_ZERO_thm:
140  intOrd (& ZERO) (numeric_negate (& ZERO)) = EQUAL
141Proof
142SRW_TAC [] [TO_of_LinearOrder, intOrd, GSYM arithmeticTheory.ALT_ZERO]
143QED