61 | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) |
61 | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) |
62 | add_term_typed_consts (_, cs) = cs; |
62 | add_term_typed_consts (_, cs) = cs; |
63 |
63 |
64 fun term_typed_consts t = add_term_typed_consts(t,[]); |
64 fun term_typed_consts t = add_term_typed_consts(t,[]); |
65 |
65 |
66 (* put a term into eta long beta normal form *) |
|
67 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) |
|
68 | eta_long Ts t = (case strip_comb t of |
|
69 (Abs _, _) => eta_long Ts (Envir.beta_norm t) |
|
70 | (u, ts) => |
|
71 let |
|
72 val Us = binder_types (fastype_of1 (Ts, t)); |
|
73 val i = length Us |
|
74 in list_abs (map (pair "x") Us, |
|
75 list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts)) |
|
76 (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0)))) |
|
77 end); |
|
78 |
|
79 (* Some Types*) |
66 (* Some Types*) |
80 val bT = HOLogic.boolT; |
67 val bT = HOLogic.boolT; |
81 val iT = HOLogic.intT; |
68 val iT = HOLogic.intT; |
82 val binT = HOLogic.binT; |
69 val binT = HOLogic.binT; |
83 val nT = HOLogic.natT; |
70 val nT = HOLogic.natT; |
105 ("op +", iT --> iT --> iT), |
92 ("op +", iT --> iT --> iT), |
106 ("op -", iT --> iT --> iT), |
93 ("op -", iT --> iT --> iT), |
107 ("op *", iT --> iT --> iT), |
94 ("op *", iT --> iT --> iT), |
108 ("HOL.abs", iT --> iT), |
95 ("HOL.abs", iT --> iT), |
109 ("uminus", iT --> iT), |
96 ("uminus", iT --> iT), |
|
97 ("HOL.max", iT --> iT --> iT), |
|
98 ("HOL.min", iT --> iT --> iT), |
110 |
99 |
111 ("op <=", nT --> nT --> bT), |
100 ("op <=", nT --> nT --> bT), |
112 ("op =", nT --> nT --> bT), |
101 ("op =", nT --> nT --> bT), |
113 ("op <", nT --> nT --> bT), |
102 ("op <", nT --> nT --> bT), |
114 ("Divides.op dvd", nT --> nT --> bT), |
103 ("Divides.op dvd", nT --> nT --> bT), |
116 ("Divides.op mod", nT --> nT --> nT), |
105 ("Divides.op mod", nT --> nT --> nT), |
117 ("op +", nT --> nT --> nT), |
106 ("op +", nT --> nT --> nT), |
118 ("op -", nT --> nT --> nT), |
107 ("op -", nT --> nT --> nT), |
119 ("op *", nT --> nT --> nT), |
108 ("op *", nT --> nT --> nT), |
120 ("Suc", nT --> nT), |
109 ("Suc", nT --> nT), |
|
110 ("HOL.max", nT --> nT --> nT), |
|
111 ("HOL.min", nT --> nT --> nT), |
121 |
112 |
122 ("Numeral.bin.Bit", binT --> bT --> binT), |
113 ("Numeral.bin.Bit", binT --> bT --> binT), |
123 ("Numeral.bin.Pls", binT), |
114 ("Numeral.bin.Pls", binT), |
124 ("Numeral.bin.Min", binT), |
115 ("Numeral.bin.Min", binT), |
125 ("Numeral.number_of", binT --> iT), |
116 ("Numeral.number_of", binT --> iT), |
175 val (t,np,nh) = prepare_for_presburger q g |
166 val (t,np,nh) = prepare_for_presburger q g |
176 (* Some simpsets for dealing with mod div abs and nat*) |
167 (* Some simpsets for dealing with mod div abs and nat*) |
177 |
168 |
178 val simpset0 = HOL_basic_ss |
169 val simpset0 = HOL_basic_ss |
179 addsimps [mod_div_equality', Suc_plus1] |
170 addsimps [mod_div_equality', Suc_plus1] |
180 addsplits [split_zdiv, split_zmod, split_div'] |
171 addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] |
181 (* Simp rules for changing (n::int) to int n *) |
172 (* Simp rules for changing (n::int) to int n *) |
182 val simpset1 = HOL_basic_ss |
173 val simpset1 = HOL_basic_ss |
183 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
174 addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
184 [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
175 [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
185 addsplits [zdiff_int_split] |
176 addsplits [zdiff_int_split] |
206 (* The result of the quantifier elimination *) |
197 (* The result of the quantifier elimination *) |
207 val (th, tac) = case (prop_of pre_thm) of |
198 val (th, tac) = case (prop_of pre_thm) of |
208 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
199 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
209 (trace_msg ("calling procedure with term:\n" ^ |
200 (trace_msg ("calling procedure with term:\n" ^ |
210 Sign.string_of_term sg t1); |
201 Sign.string_of_term sg t1); |
211 ((mproof_of_int_qelim sg (eta_long [] t1) RS iffD2) RS pre_thm, |
202 ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm, |
212 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
203 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
213 | _ => (pre_thm, assm_tac i) |
204 | _ => (pre_thm, assm_tac i) |
214 in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st |
205 in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st |
215 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st; |
206 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st; |
216 |
207 |