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

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))"

method_setup eval_sgn_at_dynamic = {*
(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

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

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


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

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