clarified signature;
authorwenzelm
Thu Feb 01 17:15:07 2018 +0100 (21 months ago)
changeset 675622427d3e72b6e
parent 67561 f0b11413f1c9
child 67563 6e5316a43079
clarified signature;
eliminated aliases of Thm.term_ord;
src/HOL/Analysis/normarith.ML
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Tools/semiring_normalizer.ML
     1.1 --- a/src/HOL/Analysis/normarith.ML	Thu Feb 01 15:31:25 2018 +0100
     1.2 +++ b/src/HOL/Analysis/normarith.ML	Thu Feb 01 17:15:07 2018 +0100
     1.3 @@ -375,13 +375,12 @@
     1.4  local
     1.5   val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
     1.6   fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
     1.7 - fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
     1.8    (* FIXME: Lookup in the context every time!!! Fix this !!!*)
     1.9   fun splitequation ctxt th acc =
    1.10    let
    1.11     val real_poly_neg_conv = #neg
    1.12         (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.13 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    1.14 +        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) Thm.term_ord)
    1.15     val (th1,th2) = conj_pair(rawrule th)
    1.16    in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc
    1.17    end
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 15:31:25 2018 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:15:07 2018 +0100
     2.3 @@ -890,9 +890,11 @@
     2.4  
     2.5  declaration \<open>
     2.6  let
     2.7 -  fun earlier [] x y = false
     2.8 -    | earlier (h::t) x y =
     2.9 -        if h aconvc y then false else if h aconvc x then true else earlier t x y;
    2.10 +  fun earlier [] _ = false
    2.11 +    | earlier (h::t) (x, y) =
    2.12 +        if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
    2.13 +
    2.14 +  val earlier_ord = make_ord o earlier;
    2.15  
    2.16  fun dest_frac ct =
    2.17    case Thm.term_of ct of
    2.18 @@ -932,14 +934,14 @@
    2.19          val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
    2.20               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    2.21          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.22 -                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.23 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.24        in rth end
    2.25      | ("x+t",[t]) =>
    2.26         let
    2.27          val T = Thm.ctyp_of_cterm x
    2.28          val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    2.29          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.30 -              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.31 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.32         in  rth end
    2.33      | ("c*x",[c]) =>
    2.34         let
    2.35 @@ -977,14 +979,14 @@
    2.36          val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
    2.37               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    2.38          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.39 -                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.40 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.41        in rth end
    2.42      | ("x+t",[t]) =>
    2.43         let
    2.44          val T = Thm.ctyp_of_cterm x
    2.45          val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    2.46          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.47 -              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.48 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.49         in  rth end
    2.50      | ("c*x",[c]) =>
    2.51         let
    2.52 @@ -1020,14 +1022,14 @@
    2.53          val th = Thm.implies_elim
    2.54                   (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    2.55          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.56 -                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.57 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.58        in rth end
    2.59      | ("x+t",[t]) =>
    2.60         let
    2.61          val T = Thm.ctyp_of_cterm x
    2.62          val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    2.63          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.64 -              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.65 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
    2.66         in  rth end
    2.67      | ("c*x",[c]) =>
    2.68         let
    2.69 @@ -1057,7 +1059,7 @@
    2.70         val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    2.71         val nth = Conv.fconv_rule
    2.72           (Conv.arg_conv (Conv.arg1_conv
    2.73 -              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
    2.74 +              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
    2.75         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.76     in rth end
    2.77  | Const(@{const_name Orderings.less_eq},_)$a$b =>
    2.78 @@ -1066,7 +1068,7 @@
    2.79         val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    2.80         val nth = Conv.fconv_rule
    2.81           (Conv.arg_conv (Conv.arg1_conv
    2.82 -              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
    2.83 +              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
    2.84         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.85     in rth end
    2.86  
    2.87 @@ -1076,7 +1078,7 @@
    2.88         val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
    2.89         val nth = Conv.fconv_rule
    2.90           (Conv.arg_conv (Conv.arg1_conv
    2.91 -              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
    2.92 +              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
    2.93         val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.94     in rth end
    2.95  | @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
     3.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 15:31:25 2018 +0100
     3.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 17:15:07 2018 +0100
     3.3 @@ -750,7 +750,6 @@
     3.4  local
     3.5    open Conv
     3.6    val concl = Thm.dest_arg o Thm.cprop_of
     3.7 -  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     3.8  in
     3.9  (* FIXME: Replace tryfind by get_first !! *)
    3.10  fun real_nonlinear_prover proof_method ctxt =
    3.11 @@ -758,7 +757,7 @@
    3.12      val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} =
    3.13        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.14          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    3.15 -        simple_cterm_ord
    3.16 +        Thm.term_ord
    3.17      fun mainf cert_choice translator (eqs, les, lts) =
    3.18        let
    3.19          val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
    3.20 @@ -851,7 +850,6 @@
    3.21  
    3.22  local
    3.23    open Conv
    3.24 -  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
    3.25    val concl = Thm.dest_arg o Thm.cprop_of
    3.26    val shuffle1 =
    3.27      fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
    3.28 @@ -894,7 +892,7 @@
    3.29      val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} =
    3.30        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.31          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    3.32 -        simple_cterm_ord
    3.33 +        Thm.term_ord
    3.34  
    3.35      fun make_substitution th =
    3.36        let
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:31:25 2018 +0100
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 17:15:07 2018 +0100
     4.3 @@ -764,11 +764,10 @@
     4.4  
     4.5  fun gen_prover_real_arith ctxt prover =
     4.6    let
     4.7 -    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     4.8      val {add, mul, neg, pow = _, sub = _, main} =
     4.9          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.10          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    4.11 -        simple_cterm_ord
    4.12 +        Thm.term_ord
    4.13    in gen_real_arith ctxt
    4.14       (cterm_of_rat,
    4.15        Numeral_Simprocs.field_comp_conv ctxt,
     5.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 15:31:25 2018 +0100
     5.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 17:15:07 2018 +0100
     5.3 @@ -18,13 +18,13 @@
     5.4      local_theory -> local_theory
     5.5  
     5.6    val semiring_normalize_conv: Proof.context -> conv
     5.7 -  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
     5.8 +  val semiring_normalize_ord_conv: Proof.context -> (cterm * cterm -> order) -> conv
     5.9    val semiring_normalize_wrapper: Proof.context -> entry -> conv
    5.10    val semiring_normalize_ord_wrapper: Proof.context -> entry
    5.11 -    -> (cterm -> cterm -> bool) -> conv
    5.12 +    -> (cterm * cterm -> order) -> conv
    5.13    val semiring_normalizers_conv: cterm list -> cterm list * thm list
    5.14      -> cterm list * thm list -> cterm list * thm list ->
    5.15 -      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    5.16 +      (cterm -> bool) * conv * conv * conv -> (cterm * cterm -> order) ->
    5.17          {add: Proof.context -> conv,
    5.18           mul: Proof.context -> conv,
    5.19           neg: Proof.context -> conv,
    5.20 @@ -32,7 +32,7 @@
    5.21           pow: Proof.context -> conv,
    5.22           sub: Proof.context -> conv}
    5.23    val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    5.24 -    (cterm -> cterm -> bool) ->
    5.25 +    (cterm * cterm -> order) ->
    5.26        {add: Proof.context -> conv,
    5.27         mul: Proof.context -> conv,
    5.28         neg: Proof.context -> conv,
    5.29 @@ -327,7 +327,7 @@
    5.30       end
    5.31     | _ => (TrueI, true_tm, true_tm));
    5.32  
    5.33 -in fn variable_order =>
    5.34 +in fn variable_ord =>
    5.35   let
    5.36  
    5.37  (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
    5.38 @@ -438,7 +438,7 @@
    5.39      else
    5.40       if x aconvc one_tm then ~1
    5.41       else if y aconvc one_tm then 1
    5.42 -      else if variable_order x y then ~1 else 1
    5.43 +      else if is_less (variable_ord (x, y)) then ~1 else 1
    5.44     fun monomial_mul tm l r =
    5.45      ((let val (lx,ly) = dest_mul l val vl = powvar lx
    5.46        in
    5.47 @@ -594,8 +594,8 @@
    5.48    | (_ ,[]) => ~1
    5.49    | ([], _) => 1
    5.50    | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
    5.51 -     if variable_order x1 x2 then 1
    5.52 -     else if variable_order x2 x1 then ~1
    5.53 +     if is_less (variable_ord (x1, x2)) then 1
    5.54 +     else if is_less (variable_ord (x2, x1)) then ~1
    5.55       else if n1 < n2 then ~1
    5.56       else if n2 < n1 then 1
    5.57       else lexorder vs1 vs2
    5.58 @@ -851,13 +851,11 @@
    5.59      addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
    5.60      addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
    5.61  
    5.62 -fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
    5.63 -
    5.64  
    5.65  (* various normalizing conversions *)
    5.66  
    5.67  fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
    5.68 -                                     {conv, dest_const, mk_const, is_const}) ord =
    5.69 +                                     {conv, dest_const, mk_const, is_const}) term_ord =
    5.70    let
    5.71      val pow_conv =
    5.72        Conv.arg_conv (Simplifier.rewrite (put_simpset nat_exp_ss ctxt))
    5.73 @@ -865,21 +863,22 @@
    5.74          (put_simpset HOL_basic_ss ctxt addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
    5.75        then_conv conv ctxt
    5.76      val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
    5.77 -  in semiring_normalizers_conv vars semiring ring field dat ord end;
    5.78 +  in semiring_normalizers_conv vars semiring ring field dat term_ord end;
    5.79  
    5.80 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    5.81 +fun semiring_normalize_ord_wrapper ctxt
    5.82 +  ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) term_ord =
    5.83   #main (semiring_normalizers_ord_wrapper ctxt
    5.84    ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},
    5.85 -   {conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord) ctxt;
    5.86 +   {conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) term_ord) ctxt;
    5.87  
    5.88  fun semiring_normalize_wrapper ctxt data =
    5.89 -  semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
    5.90 +  semiring_normalize_ord_wrapper ctxt data Thm.term_ord;
    5.91  
    5.92  fun semiring_normalize_ord_conv ctxt ord tm =
    5.93    (case match ctxt tm of
    5.94      NONE => Thm.reflexive tm
    5.95    | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
    5.96  
    5.97 -fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
    5.98 +fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt Thm.term_ord;
    5.99  
   5.100  end;