1structure CSimp :> CSimp =
2struct
3
4open HolKernel boolLib CooperThms intSyntax integerTheory int_arithTheory
5
6(* Fix the grammar used by this file *)
7structure Parse = struct
8  open Parse
9  val (Type,Term) = parse_from_grammars boolTheory.bool_grammars
10end
11open Parse
12
13val lhand = rand o rator
14
15fun has_atom dthis is_other t = let
16  val (t1, t2) = dthis t
17in
18  has_atom dthis is_other t1 orelse has_atom dthis is_other t2
19end handle HOL_ERR _ => not (is_other t)
20
21fun find_atom ASSOC COMM dthis is_other t = let
22  val find_atom = find_atom ASSOC COMM dthis is_other
23  val is_this = can dthis
24  fun move_atom_from_left t =
25      if is_this (lhand t) then REWR_CONV (GSYM ASSOC) t
26      else ALL_CONV t
27  val move_atom_from_right = REWR_CONV COMM THENC move_atom_from_left
28  val (t1, t2) = dthis t
29in
30  if has_atom dthis is_other t1 then
31    LAND_CONV find_atom THENC move_atom_from_left
32  else
33    RAND_CONV find_atom THENC move_atom_from_right
34end t handle (e as HOL_ERR _) => if is_other t then raise e else ALL_CONV t
35
36datatype matchmode = NOMATCH | NEGATED | POSITIVE
37fun compare_pair accmode eqnp tp =
38    if rand eqnp <> rand tp then NOMATCH
39    else let
40        val e_coeff = lhand eqnp
41        val t_coeff = lhand tp
42        val (e_negged, e_core) =
43            if is_negated e_coeff then (true, rand e_coeff)
44            else (false, e_coeff)
45        val (t_negged, t_core) =
46            if is_negated t_coeff then (true, rand t_coeff)
47            else (false, t_coeff)
48        val possible_mode =
49            if e_negged <> t_negged then NEGATED else POSITIVE
50      in
51        if accmode = NOMATCH orelse possible_mode = accmode then
52          if e_core = t_core then possible_mode
53          else NOMATCH
54        else NOMATCH
55      end
56fun determine_match accmode eqnpart tpart =
57    case (is_plus eqnpart, is_plus tpart) of
58      (true, true) => let
59      in
60        case compare_pair accmode (rand eqnpart) (rand tpart) of
61          NOMATCH => NOMATCH
62        | newacc => determine_match newacc (lhand eqnpart) (lhand tpart)
63      end
64    | (false, false) => compare_pair accmode eqnpart tpart
65    | _ => NOMATCH
66
67val cvar = mk_var("c", intSyntax.int_ty)
68val xvar = mk_var("x", intSyntax.int_ty)
69val yvar = mk_var("y", intSyntax.int_ty)
70val gv = genvar int_ty
71val handle_negs = PURE_REWRITE_RULE [INT_NEG_ADD, INT_NEG_LMUL, INT_NEGNEG,
72                                     INT_NEG_0]
73fun EQRWT eqn = let
74  val (varpart, numpart) = dest_plus (rand (concl eqn))
75  val eq1 = MP (INST [cvar |-> varpart, xvar |-> numpart, yvar |-> gv]
76                     eq_context_rwt1) eqn
77  val eq2 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart,
78                                   yvar |-> gv]
79                                  eq_context_rwt2) eqn)
80in
81  (fn t =>
82      if is_eq t then
83        case determine_match NOMATCH varpart (lhand (rand t)) of
84          NOMATCH => ALL_CONV t
85        | POSITIVE => (LAND_CONV (K eqn) THENC REWR_CONV INT_EQ_LADD THENC
86                       CooperMath.REDUCE_CONV) t
87        | NEGATED => raise Fail "EQRWT : should never happen"
88      else if is_leq t then
89        case determine_match NOMATCH varpart (lhand (rand t)) of
90          NOMATCH => ALL_CONV t
91        | POSITIVE => (K (INST [gv |-> rand (rand t)] eq1) THENC
92                       CooperMath.REDUCE_CONV) t
93        | NEGATED => (K (INST [gv |-> rand (rand t)] eq2) THENC
94                      CooperMath.REDUCE_CONV) t
95      else ALL_CONV t)
96end
97
98
99fun LTRWT ltthm = let
100  val (varpart, numpart) = dest_plus (rand (concl ltthm))
101  val n = int_of_term numpart
102  val rwt1 = MP (INST [cvar |-> varpart, xvar |-> numpart,
103                       yvar |-> gv] le_context_rwt1) ltthm
104  val rwt2 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart,
105                                    yvar |-> gv] le_context_rwt2) ltthm)
106  val rwt3 = MP (INST [cvar |-> varpart, xvar |-> numpart,
107                       yvar |-> gv] le_context_rwt3) ltthm
108  val rwt4 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart,
109                                    yvar |-> gv] le_context_rwt4) ltthm)
110  val rwt5 = CONV_RULE (RAND_CONV (TRY_CONV OmegaMath.leaf_normalise))
111                       (handle_negs (MP (INST [cvar |-> varpart,
112                                               xvar |-> numpart]
113                                              le_context_rwt5)
114                                        ltthm))
115in
116  (fn t =>
117      if is_eq t then
118        case determine_match NOMATCH varpart (lhand (rand t)) of
119          NOMATCH => ALL_CONV t
120        | POSITIVE => let val tnumpart = rand (rand t)
121                      in
122                        if Arbint.<(n, int_of_term tnumpart) then
123                          MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV)
124                                        (INST [gv |-> tnumpart] rwt3)) TRUTH
125                        else ALL_CONV t
126                      end
127        | NEGATED => let val tnumpart = rand (rand t)
128                     in
129                       if Arbint.<(n, Arbint.~(int_of_term tnumpart)) then
130                         MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV)
131                                       (INST [gv |-> tnumpart] rwt4)) TRUTH
132                       else ALL_CONV t
133                     end
134      else if is_leq t then
135        case determine_match NOMATCH varpart (lhand (rand t)) of
136          NOMATCH => ALL_CONV t
137        | POSITIVE => let val tnumpart = rand (rand t)
138                      in
139                        if Arbint.<=(n, int_of_term tnumpart) then
140                          MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV)
141                                        (INST [gv |-> tnumpart] rwt1)) TRUTH
142                        else
143                          ALL_CONV t
144                      end
145        | NEGATIVE => let val tnumpart = rand (rand t)
146                          open Arbint
147                      in
148                        case compare(int_of_term tnumpart, ~ n) of
149                          LESS => MP (CONV_RULE
150                                        (LAND_CONV CooperMath.REDUCE_CONV)
151                                        (INST [gv |-> tnumpart] rwt2))
152                                     TRUTH
153                        | EQUAL => rwt5
154                        | GREATER => ALL_CONV t
155                      end
156      else ALL_CONV t)
157end
158
159
160fun disj_cong0 t = let
161  val (d1, d2) = dest_disj t
162  val notd1_t = mk_neg d1
163  val notd1_th = ASSUME notd1_t
164  val d2_rewritten =
165      if is_neg d1 then
166        DISCH notd1_t
167              (REWRITE_CONV [CONV_RULE (REWR_CONV NOT_NOT_P) notd1_th] d2)
168      else if is_divides d1 orelse is_eq d1 then
169        DISCH notd1_t (REWRITE_CONV [notd1_th] d2)
170      else let
171          val notd1_thm = CONV_RULE OmegaMath.leaf_normalise notd1_th
172        in
173          DISCH notd1_t (CooperMath.BLEAF_CONV (op THENC) (LTRWT notd1_thm) d2)
174        end
175in
176  K (MATCH_MP simple_disj_congruence d2_rewritten) THENC
177  TRY_CONV (REWR_CONV T_or_r ORELSEC REWR_CONV F_or_r)
178end t
179
180val disj_cong =
181    REWR_CONV T_or_l ORELSEC REWR_CONV F_or_l ORELSEC disj_cong0
182
183fun conj_cong0 t = let
184  val (c1, c2) = dest_conj t
185  val c1_thm = ASSUME c1
186  val c2_rewritten =
187      if is_eq c1 then
188        DISCH c1 (CooperMath.BLEAF_CONV (op THENC) (EQRWT c1_thm) c2)
189      else if is_leq c1 then
190        DISCH c1 (CooperMath.BLEAF_CONV (op THENC) (LTRWT c1_thm) c2)
191      else
192        DISCH c1 (REWRITE_CONV [EQT_INTRO c1_thm
193                                handle HOL_ERR _ => EQF_INTRO c1_thm] c2)
194in
195  K (MATCH_MP simple_conj_congruence c2_rewritten) THENC
196  TRY_CONV (REWR_CONV T_and_r ORELSEC REWR_CONV F_and_r)
197end t
198
199val conj_cong =
200    REWR_CONV T_and_l ORELSEC REWR_CONV F_and_l ORELSEC conj_cong0
201
202fun IFP is c tm = if is tm then c tm else ALL_CONV tm
203
204fun csimp tm = let
205in
206  if is_disj tm then
207    if has_atom dest_disj is_conj tm then
208      find_atom DISJ_ASSOC DISJ_COMM dest_disj is_conj THENC
209      disj_cong THENC IFP is_disj (RAND_CONV csimp)
210    else BINOP_CONV csimp
211  else if is_conj tm then
212    if has_atom dest_conj is_disj tm then
213      find_atom CONJ_ASSOC CONJ_COMM dest_conj is_disj THENC
214      conj_cong THENC IFP is_conj (RAND_CONV csimp)
215    else BINOP_CONV csimp
216  else ALL_CONV
217end tm
218
219end (* struct *)
220