1structure jrhCore :> jrhCore = 2struct 3 4open HolKernel boolLib integerTheory 5 arithmeticTheory intSyntax int_arithTheory intSimps; 6 7open CooperSyntax CooperThms CooperMath 8open Profile 9open DeepSyntaxTheory; 10 11val lhand = rand o rator 12val collect_additive_consts = profile "additive_consts" collect_additive_consts 13 14val ERR = mk_HOL_ERR "Cooper"; 15 16(* Fix the grammar used by this file *) 17structure Parse = struct 18 open Parse 19 val (Type,Term) = parse_from_grammars DeepSyntaxTheory.DeepSyntax_grammars 20end 21open Parse 22 23val REWRITE_CONV = GEN_REWRITE_CONV Conv.TOP_DEPTH_CONV bool_rewrites 24 25 26val tac = REWRITE_TAC [eval_form_def, Aset_def, Bset_def] 27val conjn_rwt = prove(``!f1 f2 x. eval_form f1 x /\ eval_form f2 x = 28 eval_form (Conjn f1 f2) x``, tac) 29val disjn_rwt = prove(``!f1 f2 x. eval_form f1 x \/ eval_form f2 x = 30 eval_form (Disjn f1 f2) x``, tac) 31val negn_rwt = prove(``!f x. ~eval_form f x = eval_form (Negn f) x``, tac); 32val unrelated_rwt = prove(``!b x. b = eval_form (UnrelatedBool b) x``, tac); 33val binop_rwt_CONV = REWR_CONV conjn_rwt ORELSEC REWR_CONV disjn_rwt 34 35val var_right_rwt = prove( 36 ``!i x. (i < x = eval_form (LTx i) x) /\ 37 (i int_divides x = eval_form (xDivided i 0) x)``, 38 REWRITE_TAC [eval_form_def, INT_ADD_RID]); 39val var_nright_rwt = prove( 40 ``!i1 i2 x. ((x = i1) = eval_form (xEQ i1) x) /\ 41 (x < i1 = eval_form (xLT i1) x) /\ 42 (i1 int_divides x + i2 = eval_form (xDivided i1 i2) x)``, 43 tac); 44 45fun convert_to_embedded_syntax tm = let 46 (* tm is of form ?x. ..., were x is always bare in the ... *) 47 val (var, body) = dest_exists tm 48 fun recurse tm = 49 if not (memt (free_vars tm) var) then 50 SPECL [tm, var] unrelated_rwt 51 else let 52 val (c1, c2) = dest_conj tm handle HOL_ERR _ => dest_disj tm 53 val eval1 = recurse c1 54 (* i.e., (|- c1 = eval_form f1 x, |- Aset pos f1 = ..., 55 |- Bset pos f1 = ..., lcm1) *) 56 val eval2 = recurse c2 57 val eval = MK_COMB (AP_TERM (rator (rator tm)) eval1, eval2) 58 (* i.e., c1 /\ c2 = eval_form f1 x /\ eval_form f2 x *) 59 in 60 TRANS eval (binop_rwt_CONV (rand (concl eval))) 61 end 62 handle HOL_ERR _ => let 63 val t0 = dest_neg tm 64 val eval0 = recurse t0 65 val eval = AP_TERM (rator tm) eval0 66 in 67 TRANS eval (REWR_CONV negn_rwt (rand (concl eval))) 68 end handle HOL_ERR _ => 69 if rand tm ~~ var then 70 REWRITE_CONV [var_right_rwt] tm 71 else 72 REWRITE_CONV [var_nright_rwt] tm 73in 74 EXISTS_EQ var (recurse body) 75end 76 77 78fun form_to_lcm var tm = let 79 fun recurse acc tm = 80 if not (memt (free_vars tm) var) then acc 81 else let 82 val (l,r) = dest_disj tm handle HOL_ERR _ => dest_conj tm 83 in 84 recurse (recurse acc l) r 85 end handle HOL_ERR _ => 86 if is_neg tm then recurse acc (rand tm) 87 else if is_divides tm then 88 lcm (int_of_term (rand (rator tm)), acc) 89 else acc 90in 91 recurse Arbint.one tm 92end 93 94val alldivide_t = ``alldivide`` 95fun prove_alldivide f d = 96 EQT_ELIM ((REWRITE_CONV [alldivide_def] THENC REDUCE_CONV) 97 (list_mk_comb(alldivide_t, [f,d]))) 98 99 100fun phase4_CONV tm = let 101 val (var, body) = dest_exists tm 102 val eval_thm = convert_to_embedded_syntax tm 103 val f_t = rand (rator (#2 (dest_exists (rand (concl eval_thm))))) 104 val lcm_i = form_to_lcm var body 105 val lcm_t = term_of_int lcm_i 106 val zero_lt_lcm = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, lcm_t))) 107 val alldiv_th = prove_alldivide f_t lcm_t 108 (* count a and b terms, also pair each count with the total number of free 109 variables in these terms *) 110 fun docount pos (acc as (ai as (a, afv), bi as (b, bfv))) tm = 111 if not (memt (free_vars tm) var) then acc 112 else let 113 val (l,r) = dest_disj tm handle HOL_ERR _ => dest_conj tm 114 in 115 docount pos (docount pos acc l) r 116 end handle HOL_ERR _ => let 117 val t0 = dest_neg tm 118 in 119 docount (not pos) acc t0 120 end handle HOL_ERR _ => let 121 val (l,r) = dest_less tm 122 in 123 if (pos = (l ~~ var)) then 124 ((a + 1, afv + length (free_vars r)), bi) 125 else 126 (ai, (b + 1, bfv + length (free_vars l))) 127 end handle HOL_ERR _ => (* must be equality or divides, neither 128 has any effect on contest *) acc 129 val ((ai,afv), (bi,bfv)) = docount true ((0,0), (0,0)) body 130 val qe_thm = 131 case Int.compare(ai,bi) of 132 LESS => posinf_exoriginal_eq_rhs 133 | EQUAL => if afv < bfv then posinf_exoriginal_eq_rhs 134 else neginf_exoriginal_eq_rhs 135 | GREATER => neginf_exoriginal_eq_rhs 136 val eliminated_th = MATCH_MP qe_thm (CONJ alldiv_th zero_lt_lcm) 137in 138 TRANS eval_thm eliminated_th 139end 140 141val phase4_CONV = profile "phase4" phase4_CONV 142 143val bset_thms = CONJUNCTS in_bset 144val aset_thms = CONJUNCTS in_aset 145fun in_set_CONV tm = let 146 val (v, body) = dest_exists tm 147 val (in_t, _) = dest_conj body 148 val (set_conjn::set_disjn::set_negnt::set_negnf::rest) = 149 if #1 (dest_const (#1 (strip_comb (rand in_t)))) = "Aset" then aset_thms 150 else bset_thms 151 152 fun recurse tm = let 153 val (v, body) = dest_exists tm 154 val (in_t, _) = dest_conj body 155 val f = rand (rand in_t) 156 in 157 case (#1 (dest_const (#1 (strip_comb f)))) of 158 "Conjn" => REWR_CONV set_conjn THENC BINOP_CONV recurse 159 | "Disjn" => REWR_CONV set_disjn THENC BINOP_CONV recurse 160 | "Negn" => FIRST_CONV (map REWR_CONV [set_negnf, set_negnt]) THENC 161 recurse 162 | _ => FIRST_CONV (map REWR_CONV rest) 163 end tm 164in 165 recurse tm 166end 167 168 169 170val eval_f_CONV = REWRITE_CONV [eval_form_def] 171 172fun elim_bterms tm = let 173 (* tm is of form 174 ?b. (b IN Xset pos f /\ K ... j) /\ .... 175 or 176 ?b. b IN Xset pos f /\ ... 177 *) 178 val (var, body) = dest_exists tm 179 val initially = if is_conj (lhand body) then REWR_CONV (GSYM CONJ_ASSOC) 180 else ALL_CONV 181in 182 BINDER_CONV (initially THENC 183 profile "eb.eval" eval_f_CONV THENC 184 profile "eb.abs" (RAND_CONV (UNBETA_CONV var))) THENC 185 profile "eb.in_set" in_set_CONV THENC 186 profile "eb.beta" (EVERY_DISJ_CONV (TRY_CONV BETA_CONV)) 187end tm 188 189val eval_form_neginf = prove( 190 ``(eval_form (neginf (Conjn f1 f2)) x = eval_form (neginf f1) x /\ 191 eval_form (neginf f2) x) /\ 192 (eval_form (neginf (Disjn f1 f2)) x = eval_form (neginf f1) x \/ 193 eval_form (neginf f2) x) /\ 194 (eval_form (neginf (Negn f)) x = ~eval_form (neginf f) x) /\ 195 (eval_form (neginf (UnrelatedBool b)) x = b) /\ 196 (eval_form (neginf (xLT i)) x = T) /\ 197 (eval_form (neginf (LTx i)) x = F) /\ 198 (eval_form (neginf (xEQ i)) x = F) /\ 199 (eval_form (neginf (xDivided i1 i2)) x = i1 int_divides x + i2)``, 200 REWRITE_TAC [eval_form_def, neginf_def]); 201val eval_form_posinf = prove( 202 ``(eval_form (posinf (Conjn f1 f2)) x = eval_form (posinf f1) x /\ 203 eval_form (posinf f2) x) /\ 204 (eval_form (posinf (Disjn f1 f2)) x = eval_form (posinf f1) x \/ 205 eval_form (posinf f2) x) /\ 206 (eval_form (posinf (Negn f)) x = ~eval_form (posinf f) x) /\ 207 (eval_form (posinf (UnrelatedBool b)) x = b) /\ 208 (eval_form (posinf (xLT i)) x = F) /\ 209 (eval_form (posinf (LTx i)) x = T) /\ 210 (eval_form (posinf (xEQ i)) x = F) /\ 211 (eval_form (posinf (xDivided i1 i2)) x = i1 int_divides x + i2)``, 212 REWRITE_TAC [eval_form_def, posinf_def]); 213 214val phase5_CONV = let 215 (* have something of the form 216 (?x. K (0 < x /\ x <= k) x /\ eval_form (neginf f) x) \/ 217 (?b k. (b IN Xset pos f /\ K (0 < k /\ k <= d) k) /\ 218 eval_form f (b + k)) 219 *) 220 val prelim_left = BINDER_CONV (RAND_CONV (REWRITE_CONV [eval_form_posinf, 221 eval_form_neginf])) 222 223 val efBETA_CONV = REWRITE_CONV [eval_form_def] 224 val efBETA_CONV = profile "phase5.efBETA" efBETA_CONV 225 (* if the term t is a conjunct, apply c to the left conjunct, otherwise 226 apply directly to the term *) 227 fun lconj_CONV c t = if is_conj t then LAND_CONV c t else c t 228 229 val elim_bterms = profile "phase5.er.elim_bterms" elim_bterms 230 val elim_bterms_on_right = 231 (* the second disjunct produced by phase4 is of form 232 ?b k. (b IN ... /\ K (lo < k /\ k <= hi) k) /\ F(b + k) *) 233 (* first try eliminating trivial constraints on k *) 234 profile "phase5.er.triv" ( 235 TRY_CONV (STRIP_QUANT_CONV (LAND_CONV (RAND_CONV quick_cst_elim)) THENC 236 (BINDER_CONV Unwind.UNWIND_EXISTS_CONV ORELSEC 237 REWRITE_CONV [])) ) THENC 238 (* at this stage, k may or may not have been eliminated by the previous 239 step, either by becoming false, which will have already turned the 240 whole term false, or by becoming unwound. 241 In the former, the TRY_CONV will do nothing because the LAND_CONV 242 will fail. 243 Otherwise, the basic action here is to expand out all of the 244 "b" possibilities in the list *) 245 TRY_CONV (((SWAP_VARS_CONV THENC BINDER_CONV elim_bterms) ORELSEC 246 elim_bterms) THENC 247 profile "phase5.er.r_i_g" reduce_if_ground THENC 248 profile "phase5.er.p1ex" push_one_exists_over_many_disjs) 249in 250 profile "phase5.el" (LAND_CONV prelim_left) THENC 251 profile "phase5.er" (RAND_CONV elim_bterms_on_right) THENC 252 profile "phase5.finish" 253 (EVERY_DISJ_CONV (TRY_CONV (profile "phase5.finish.fix" fixup_newvar) THENC 254 profile "phase5.finish.div" 255 (ONCE_DEPTH_CONV check_divides) THENC 256 profile "phase5.finish.simpdisj" 257 (TRY_CONV simplify_constrained_disjunct) THENC 258 TRY_CONV (REWR_CONV EXISTS_SIMP))) (* might pick up ?x. t *) 259end 260 261val phase5_CONV = profile "phase5" phase5_CONV 262 263end; 264