equal
deleted
inserted
replaced
166 let |
166 let |
167 (* FIXME : Should be computed statically!! *) |
167 (* FIXME : Should be computed statically!! *) |
168 val real_poly_conv = |
168 val real_poly_conv = |
169 Normalizer.semiring_normalize_wrapper ctxt |
169 Normalizer.semiring_normalize_wrapper ctxt |
170 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
170 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
171 in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) |
171 in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv))) |
172 end; |
172 end; |
173 |
173 |
174 fun absc cv ct = case term_of ct of |
174 fun absc cv ct = case term_of ct of |
175 Abs (v,_, _) => |
175 Abs (v,_, _) => |
176 let val (x,t) = Thm.dest_abs (SOME v) ct |
176 let val (x,t) = Thm.dest_abs (SOME v) ct |
188 val apply_pth3 = rewr_conv @{thm pth_3}; |
188 val apply_pth3 = rewr_conv @{thm pth_3}; |
189 val apply_pth4 = rewrs_conv @{thms pth_4}; |
189 val apply_pth4 = rewrs_conv @{thms pth_4}; |
190 val apply_pth5 = rewr_conv @{thm pth_5}; |
190 val apply_pth5 = rewr_conv @{thm pth_5}; |
191 val apply_pth6 = rewr_conv @{thm pth_6}; |
191 val apply_pth6 = rewr_conv @{thm pth_6}; |
192 val apply_pth7 = rewrs_conv @{thms pth_7}; |
192 val apply_pth7 = rewrs_conv @{thms pth_7}; |
193 val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); |
193 val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); |
194 val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); |
194 val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv); |
195 val apply_ptha = rewr_conv @{thm pth_a}; |
195 val apply_ptha = rewr_conv @{thm pth_a}; |
196 val apply_pthb = rewrs_conv @{thms pth_b}; |
196 val apply_pthb = rewrs_conv @{thms pth_b}; |
197 val apply_pthc = rewrs_conv @{thms pth_c}; |
197 val apply_pthc = rewrs_conv @{thms pth_c}; |
198 val apply_pthd = try_conv (rewr_conv @{thm pth_d}); |
198 val apply_pthd = try_conv (rewr_conv @{thm pth_d}); |
199 |
199 |
202 (Const(@{const_name scaleR}, _)$l$v)$r => v |
202 (Const(@{const_name scaleR}, _)$l$v)$r => v |
203 | Const(@{const_name scaleR}, _)$l$v => v |
203 | Const(@{const_name scaleR}, _)$l$v => v |
204 | _ => error "headvector: non-canonical term" |
204 | _ => error "headvector: non-canonical term" |
205 |
205 |
206 fun vector_cmul_conv ct = |
206 fun vector_cmul_conv ct = |
207 ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv |
207 ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv |
208 (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct |
208 (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct |
209 |
209 |
210 fun vector_add_conv ct = apply_pth7 ct |
210 fun vector_add_conv ct = apply_pth7 ct |
211 handle CTERM _ => |
211 handle CTERM _ => |
212 (apply_pth8 ct |
212 (apply_pth8 ct |
394 end; |
394 end; |
395 |
395 |
396 fun init_conv ctxt = |
396 fun init_conv ctxt = |
397 Simplifier.rewrite (Simplifier.context ctxt |
397 Simplifier.rewrite (Simplifier.context ctxt |
398 (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) |
398 (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) |
399 then_conv field_comp_conv |
399 then_conv Normalizer.field_comp_conv |
400 then_conv nnf_conv |
400 then_conv nnf_conv |
401 |
401 |
402 fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); |
402 fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); |
403 fun norm_arith ctxt ct = |
403 fun norm_arith ctxt ct = |
404 let |
404 let |