Re: [isabelle] Decision procedures through computation & code_reflect



Dear Florian,

Thanks again for your patience and wonderful suggestions.

add here sth. like

declare [[code drop: sgn_at]]

By dropping the code equation for sgn_at after "code_reflect" it, dynamic hold runs much faster than before as what has happened in RenÃ's case. However, static hold runs at the same speed as before, which is much slower than dynamic hold. I can roughly understand the explanation related to reprocessing, but this (i.e. static hold runs slower than dynamic hold) is quite unexpected.

The current code is as follows:

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

declare [[code drop: sgn_at]]

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"
  (*0.5s-1s*)
  apply eval_sgn_at_static
oops

end

Thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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