Re: [isabelle] Decision procedures through computation & code_reflect



Hi Wenda,

the attached theory shows by example how the static context of an
evaluation can be augmented with type class instances.  Watch out for
the text blocks.

Hope this helps,
	Florian

Am 05.02.2015 um 20:33 schrieb Wenda Li:
> 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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: Scratch3.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature



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