# Re: [isabelle] Decision procedures through computation & code_reflect

```Dear Florian,

```
The following code leads to the wellsortedness error, and I really don't know which const causes it.
```
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Poly_Deriv"
begin

consts smods:: "real poly â real poly â (real poly) list"
```
lemma [code]: "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod q))))" sorry
```
fun changes:: "real list â int" where
"changes [] = 0"|
"changes [_] = 0" |
"changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs)
else if x2=0 then changes (x1#xs)
else changes (x2#xs))"

definition changes_poly_at::"real poly list â real â int" where
"changes_poly_at ps a= changes (map (Îp. poly p a) ps)"

```
definition changes_itv_smods:: "real â real âreal poly â real poly â int" where "changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a - changes_poly_at ps b)"
```
lift_definition real_poly:: "rat poly â real poly" is
"Îp. real_of_rat o p " sorry

```
lemma [code abstract]: "coeffs (real_poly p)= (map of_rat (coeffs p))" sorry
```
definition isolate::"real poly â real â real â bool" where
"isolate p lb ub= (if poly p lb=0 â poly p ub =0 â lbâub
then False else changes_itv_smods lb ub p (pderiv p) =1)"

definition valid_alg::"rat poly â rat â rat â bool" where
```
"valid_alg p lb ub = (lb<ub â poly p lb * poly p ub <0 â isolate (real_poly p) (of_rat lb) (of_rat ub))"
```
consts Alg::"rat poly â rat â rat â real"

code_datatype Alg Ratreal

consts sgn_at :: "real poly â real â real"

lemma sgn_at_code_alg[code]: "sgn_at q (Alg p lb ub) = (
if valid_alg p lb ub then
```
of_int (changes_itv_smods (of_rat lb) (of_rat ub) (real_poly p) (pderiv (real_poly p) * q))
```    else sgn (poly q undefined))"
sorry

method_setup eval_sgn_at_dynamic = {*
Scan.succeed
```
(fn ctxt => SIMPLE_METHOD' (CONVERSION (Code_Runtime.dynamic_holds_conv ctxt)))
```*}

code_reflect Foo
datatypes real="_" and rat = "_"  and int="_" and poly="_"
functions sgn_at

declare [[code drop: sgn_at]]

definition pCons::"rat â rat poly â rat poly" where
"pCons=Polynomial.pCons"

ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
```
consts = [ at {const_name HOL.Trueprop},@{const_name Real.equal_real_inst.equal_real}
```         , @{const_name sgn_at}, @{const_name pCons}
]} ;
*}

method_setup eval_sgn_at_static = {*
```
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds ctxt)))
```*}

lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(*almost instant*)
apply eval_sgn_at_dynamic
oops

lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(*Wellsortedness error*)
apply eval_sgn_at_static
oops

end

Many thanks,
Wenda
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.