src/HOL/Tools/semiring_normalizer.ML
changeset 36945 9bec62c10714
parent 36771 3e08b6789e66
child 37744 3daaf23b9ab4
     1.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4        val semiring = (sr_ops, sr_rules');
     1.5        val ring = (r_ops, r_rules');
     1.6        val field = (f_ops, f_rules');
     1.7 -      val ideal' = map (symmetric o mk_meta) ideal
     1.8 +      val ideal' = map (Thm.symmetric o mk_meta) ideal
     1.9      in
    1.10        AList.delete Thm.eq_thm key #>
    1.11        cons (key, ({vars = vars, semiring = semiring, 
    1.12 @@ -328,16 +328,16 @@
    1.13           ((let val (rx,rn) = dest_pow r
    1.14                 val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
    1.15                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
    1.16 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
    1.17 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
    1.18             handle CTERM _ =>
    1.19              (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
    1.20                   val (tm1,tm2) = Thm.dest_comb(concl th1) in
    1.21 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
    1.22 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
    1.23         handle CTERM _ =>
    1.24             ((let val (rx,rn) = dest_pow r
    1.25                  val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
    1.26                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
    1.27 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
    1.28 +               Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
    1.29             handle CTERM _ => inst_thm [(cx,l)] pthm_32
    1.30  
    1.31  ))
    1.32 @@ -348,7 +348,7 @@
    1.33   fun monomial_deone th =
    1.34         (let val (l,r) = dest_mul(concl th) in
    1.35             if l aconvc one_tm
    1.36 -          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
    1.37 +          then Thm.transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
    1.38         handle CTERM _ => th;
    1.39  
    1.40  (* Conversion for "(monomial)^n", where n is a numeral.                      *)
    1.41 @@ -357,7 +357,7 @@
    1.42    let
    1.43     fun monomial_pow tm bod ntm =
    1.44      if not(is_comb bod)
    1.45 -    then reflexive tm
    1.46 +    then Thm.reflexive tm
    1.47      else
    1.48       if is_semiring_constant bod
    1.49       then semiring_pow_conv tm
    1.50 @@ -365,7 +365,7 @@
    1.51        let
    1.52        val (lopr,r) = Thm.dest_comb bod
    1.53        in if not(is_comb lopr)
    1.54 -         then reflexive tm
    1.55 +         then Thm.reflexive tm
    1.56          else
    1.57            let
    1.58            val (opr,l) = Thm.dest_comb lopr
    1.59 @@ -374,7 +374,7 @@
    1.60            then
    1.61              let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
    1.62                  val (l,r) = Thm.dest_comb(concl th1)
    1.63 -           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
    1.64 +           in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
    1.65             end
    1.66             else
    1.67              if opr aconvc mul_tm
    1.68 @@ -385,9 +385,9 @@
    1.69                val (x,y) = Thm.dest_comb xy
    1.70                val thl = monomial_pow y l ntm
    1.71                val thr = monomial_pow z r ntm
    1.72 -             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
    1.73 +             in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr)
    1.74               end
    1.75 -             else reflexive tm
    1.76 +             else Thm.reflexive tm
    1.77            end
    1.78        end
    1.79    in fn tm =>
    1.80 @@ -436,18 +436,18 @@
    1.81               val (tm1,tm2) = Thm.dest_comb(concl th1)
    1.82               val (tm3,tm4) = Thm.dest_comb tm1
    1.83               val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
    1.84 -             val th3 = transitive th1 th2
    1.85 +             val th3 = Thm.transitive th1 th2
    1.86                val  (tm5,tm6) = Thm.dest_comb(concl th3)
    1.87                val  (tm7,tm8) = Thm.dest_comb tm6
    1.88               val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
    1.89 -         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
    1.90 +         in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4)
    1.91           end
    1.92           else
    1.93            let val th0 = if ord < 0 then pthm_16 else pthm_17
    1.94               val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
    1.95               val (tm1,tm2) = Thm.dest_comb(concl th1)
    1.96               val (tm3,tm4) = Thm.dest_comb tm2
    1.97 -         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
    1.98 +         in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
    1.99           end
   1.100          end)
   1.101         handle CTERM _ =>
   1.102 @@ -459,14 +459,14 @@
   1.103                   val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.104             val (tm3,tm4) = Thm.dest_comb tm1
   1.105             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   1.106 -          in transitive th1 th2
   1.107 +          in Thm.transitive th1 th2
   1.108            end
   1.109            else
   1.110            if ord < 0 then
   1.111              let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   1.112                  val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.113                  val (tm3,tm4) = Thm.dest_comb tm2
   1.114 -           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.115 +           in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.116             end
   1.117             else inst_thm [(ca,l),(cb,r)] pthm_09
   1.118          end)) end)
   1.119 @@ -480,22 +480,22 @@
   1.120                let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   1.121                   val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.122                   val (tm3,tm4) = Thm.dest_comb tm1
   1.123 -             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   1.124 +             in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   1.125               end
   1.126               else if ord > 0 then
   1.127                   let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   1.128                       val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.129                      val (tm3,tm4) = Thm.dest_comb tm2
   1.130 -                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.131 +                in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.132                  end
   1.133 -             else reflexive tm
   1.134 +             else Thm.reflexive tm
   1.135           end)
   1.136          handle CTERM _ =>
   1.137            (let val vr = powvar r
   1.138                 val  ord = vorder vl vr
   1.139            in if ord = 0 then powvar_mul_conv tm
   1.140                else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   1.141 -              else reflexive tm
   1.142 +              else Thm.reflexive tm
   1.143            end)) end))
   1.144    in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   1.145               end
   1.146 @@ -511,8 +511,8 @@
   1.147            val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   1.148            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.149            val (tm3,tm4) = Thm.dest_comb tm1
   1.150 -          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   1.151 -      in transitive th1 th2
   1.152 +          val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   1.153 +      in Thm.transitive th1 th2
   1.154        end)
   1.155       handle CTERM _ => monomial_mul_conv tm)
   1.156     end
   1.157 @@ -537,11 +537,11 @@
   1.158           val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.159           val (tm3,tm4) = Thm.dest_comb tm1
   1.160           val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   1.161 -         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   1.162 +         val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2)
   1.163           val tm5 = concl th3
   1.164        in
   1.165        if (Thm.dest_arg1 tm5) aconvc zero_tm
   1.166 -      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   1.167 +      then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   1.168        else monomial_deone th3
   1.169       end
   1.170   end;
   1.171 @@ -603,9 +603,9 @@
   1.172         val l = Thm.dest_arg lopr
   1.173     in
   1.174      if l aconvc zero_tm
   1.175 -    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   1.176 +    then Thm.transitive th (inst_thm [(ca,r)] pthm_07)   else
   1.177          if r aconvc zero_tm
   1.178 -        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   1.179 +        then Thm.transitive th (inst_thm [(ca,l)] pthm_08)  else th
   1.180     end
   1.181    end
   1.182   fun padd tm =
   1.183 @@ -628,14 +628,14 @@
   1.184              val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.185              val (tm3,tm4) = Thm.dest_comb tm1
   1.186              val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   1.187 -        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   1.188 +        in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2)))
   1.189          end
   1.190         else (* ord <> 0*)
   1.191          let val th1 =
   1.192                  if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.193                  else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.194              val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.195 -        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.196 +        in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.197          end
   1.198        end
   1.199       else (* not (is_add r)*)
   1.200 @@ -646,13 +646,13 @@
   1.201              val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.202              val (tm3,tm4) = Thm.dest_comb tm1
   1.203              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.204 -        in dezero_rule (transitive th1 th2)
   1.205 +        in dezero_rule (Thm.transitive th1 th2)
   1.206          end
   1.207         else (* ord <> 0*)
   1.208          if ord > 0 then
   1.209            let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.210                val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.211 -          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.212 +          in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.213            end
   1.214          else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.215        end
   1.216 @@ -667,21 +667,21 @@
   1.217               val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.218               val (tm3,tm4) = Thm.dest_comb tm1
   1.219               val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.220 -         in dezero_rule (transitive th1 th2)
   1.221 +         in dezero_rule (Thm.transitive th1 th2)
   1.222           end
   1.223         else
   1.224 -        if ord > 0 then reflexive tm
   1.225 +        if ord > 0 then Thm.reflexive tm
   1.226          else
   1.227           let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.228               val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.229 -         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.230 +         in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.231           end
   1.232        end
   1.233      else
   1.234       let val ord = morder l r
   1.235       in
   1.236        if ord = 0 then monomial_add_conv tm
   1.237 -      else if ord > 0 then dezero_rule(reflexive tm)
   1.238 +      else if ord > 0 then dezero_rule(Thm.reflexive tm)
   1.239        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.240       end
   1.241    end
   1.242 @@ -699,7 +699,7 @@
   1.243      else
   1.244       if not(is_add r) then
   1.245        let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   1.246 -      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   1.247 +      in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1))
   1.248        end
   1.249       else
   1.250         let val (a,b) = dest_add l
   1.251 @@ -707,8 +707,8 @@
   1.252             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.253             val (tm3,tm4) = Thm.dest_comb tm1
   1.254             val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   1.255 -           val th3 = transitive th1 (combination th2 (pmul tm2))
   1.256 -       in transitive th3 (polynomial_add_conv (concl th3))
   1.257 +           val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2))
   1.258 +       in Thm.transitive th3 (polynomial_add_conv (concl th3))
   1.259         end
   1.260     end
   1.261   in fn tm =>
   1.262 @@ -740,9 +740,9 @@
   1.263           let val th1 = num_conv n
   1.264               val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   1.265               val (tm1,tm2) = Thm.dest_comb(concl th2)
   1.266 -             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   1.267 -             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   1.268 -         in transitive th4 (polynomial_mul_conv (concl th4))
   1.269 +             val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   1.270 +             val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   1.271 +         in Thm.transitive th4 (polynomial_mul_conv (concl th4))
   1.272           end
   1.273      end
   1.274   in fn tm =>
   1.275 @@ -755,8 +755,8 @@
   1.276     let val (l,r) = Thm.dest_comb tm in
   1.277          if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   1.278          let val th1 = inst_thm [(cx',r)] neg_mul
   1.279 -            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   1.280 -        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   1.281 +            val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   1.282 +        in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2))
   1.283          end
   1.284     end;
   1.285  
   1.286 @@ -767,51 +767,52 @@
   1.287        val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   1.288        val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.289        val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   1.290 -  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   1.291 +  in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2)))
   1.292    end;
   1.293  
   1.294  (* Conversion from HOL term.                                                 *)
   1.295  
   1.296  fun polynomial_conv tm =
   1.297   if is_semiring_constant tm then semiring_add_conv tm
   1.298 - else if not(is_comb tm) then reflexive tm
   1.299 + else if not(is_comb tm) then Thm.reflexive tm
   1.300   else
   1.301    let val (lopr,r) = Thm.dest_comb tm
   1.302    in if lopr aconvc neg_tm then
   1.303         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   1.304 -       in transitive th1 (polynomial_neg_conv (concl th1))
   1.305 +       in Thm.transitive th1 (polynomial_neg_conv (concl th1))
   1.306         end
   1.307       else if lopr aconvc inverse_tm then
   1.308         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   1.309 -       in transitive th1 (semiring_mul_conv (concl th1))
   1.310 +       in Thm.transitive th1 (semiring_mul_conv (concl th1))
   1.311         end
   1.312       else
   1.313 -       if not(is_comb lopr) then reflexive tm
   1.314 +       if not(is_comb lopr) then Thm.reflexive tm
   1.315         else
   1.316           let val (opr,l) = Thm.dest_comb lopr
   1.317           in if opr aconvc pow_tm andalso is_numeral r
   1.318              then
   1.319                let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   1.320 -              in transitive th1 (polynomial_pow_conv (concl th1))
   1.321 +              in Thm.transitive th1 (polynomial_pow_conv (concl th1))
   1.322                end
   1.323           else if opr aconvc divide_tm 
   1.324              then
   1.325 -              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   1.326 +              let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   1.327                                          (polynomial_conv r)
   1.328                    val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
   1.329                                (Thm.rhs_of th1)
   1.330 -              in transitive th1 th2
   1.331 +              in Thm.transitive th1 th2
   1.332                end
   1.333              else
   1.334                if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   1.335                then
   1.336 -               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   1.337 +               let val th1 =
   1.338 +                    Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   1.339                     val f = if opr aconvc add_tm then polynomial_add_conv
   1.340                        else if opr aconvc mul_tm then polynomial_mul_conv
   1.341                        else polynomial_sub_conv
   1.342 -               in transitive th1 (f (concl th1))
   1.343 +               in Thm.transitive th1 (f (concl th1))
   1.344                 end
   1.345 -              else reflexive tm
   1.346 +              else Thm.reflexive tm
   1.347           end
   1.348    end;
   1.349   in
   1.350 @@ -852,7 +853,7 @@
   1.351  
   1.352  fun semiring_normalize_ord_conv ctxt ord tm =
   1.353    (case match ctxt tm of
   1.354 -    NONE => reflexive tm
   1.355 +    NONE => Thm.reflexive tm
   1.356    | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   1.357   
   1.358  fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;