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

• To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
• Subject: Re: [isabelle] Decision procedures through computation & code_reflect
• From: Wenda Li <wl302 at cam.ac.uk>
• Date: Sun, 01 Feb 2015 16:50:56 +0000
• Cc: cl-isabelle-users at lists.cam.ac.uk
• References: <aed8a9a7a2389cd9d1c9b044b5c903bb@cam.ac.uk> <54B76A82.3030608@informatik.tu-muenchen.de> <f87b681650051ccd842112c7b897235a@cam.ac.uk> <54CC96ED.7000200@informatik.tu-muenchen.de>
• User-agent: Roundcube Webmail/1.0.2

```Dear Florian,

```
Many thanks for your previous reply. Your solution works perfectly. I can now observe the big difference between dynamic holds and static holds as well as the effect of code_reflect on dynamic holds. However, I fail to see the effect of code_reflect on static holds. Here is a minimal example:
```
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

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 Rat.of_int},
@{const_name sgn_at},
@{const_name pCons},@{const_name Rat.one_rat_inst.one_rat}
,@{const_name Polynomial.zero_poly_inst.zero_poly}
]} ;
*}

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

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

lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(*1-1.6s with code_reflect; 2-2.5s without code_reflect*)
apply eval_sgn_at_dynamic
oops

lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(*approx. 0.5s with or without code_reflect*)
apply eval_sgn_at_static
oops

end

Apologies for the lengthy example and thanks again for any help,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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