src/HOL/Library/normarith.ML
changeset 32402 5731300da417
parent 31446 2d91b2416de8
child 32645 1cc5b24f5a01
     1.1 --- a/src/HOL/Library/normarith.ML	Wed Aug 26 10:48:45 2009 +0200
     1.2 +++ b/src/HOL/Library/normarith.ML	Wed Aug 26 11:40:28 2009 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  structure NormArith : NORM_ARITH = 
     1.5  struct
     1.6  
     1.7 - open Conv Thm Conv2;
     1.8 + open Conv Thm;
     1.9   val bool_eq = op = : bool *bool -> bool
    1.10    fun dest_ratconst t = case term_of t of
    1.11     Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.12 @@ -322,6 +322,7 @@
    1.13       val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 
    1.14                                       else SOME(norm_cmul_rule v t))
    1.15                              (v ~~ nubs) 
    1.16 +     fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
    1.17      in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
    1.18      end
    1.19     val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
    1.20 @@ -332,9 +333,9 @@
    1.21    in RealArith.real_linear_prover translator
    1.22          (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
    1.23              zerodests,
    1.24 -        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
    1.25 +        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
    1.26                         arg_conv (arg_conv real_poly_conv))) ges',
    1.27 -        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
    1.28 +        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
    1.29                         arg_conv (arg_conv real_poly_conv))) gts)
    1.30    end
    1.31  in val real_vector_combo_prover = real_vector_combo_prover
    1.32 @@ -353,6 +354,7 @@
    1.33    val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
    1.34    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
    1.35    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
    1.36 +  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    1.37    fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
    1.38    fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
    1.39    val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns