src/HOL/Arith.ML
changeset 6059 aa00e235ea27
parent 6055 fdf4638bf726
child 6073 fba734ba6894
     1.1 --- a/src/HOL/Arith.ML	Mon Jan 04 16:37:04 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Tue Jan 05 17:27:59 1999 +0100
     1.3 @@ -849,26 +849,22 @@
     1.4  val ccontr = ccontr;
     1.5  val conjI = conjI;
     1.6  val lessD = Suc_leI;
     1.7 -val nat_neqE = nat_neqE;
     1.8 +val neqE = nat_neqE;
     1.9  val notI = notI;
    1.10  val not_leD = not_leE RS Suc_leI;
    1.11  val not_lessD = leI;
    1.12  val sym = sym;
    1.13  
    1.14 -val nat = Type("nat",[]);
    1.15 -val boolT = Type("bool",[]);
    1.16 -
    1.17 -fun nnb T = T = ([nat,nat] ---> boolT);
    1.18 -
    1.19  (* Turn term into list of summand * multiplicity plus a constant *)
    1.20  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.21 -  | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
    1.22 -      poly(s,poly(t,pi))
    1.23 +  | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
    1.24    | poly(t,(p,i)) =
    1.25 -      if t = Const("0",nat) then (p,i)
    1.26 +      if t = Const("0",HOLogic.natT) then (p,i)
    1.27        else (case assoc(p,t) of None => ((t,1)::p,i)
    1.28              | Some m => (overwrite(p,(t,m+1)), i))
    1.29  
    1.30 +fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
    1.31 +
    1.32  fun decomp2(rel,T,lhs,rhs) =
    1.33    if not(nnb T) then None else
    1.34    let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
    1.35 @@ -908,12 +904,12 @@
    1.36  
    1.37  fun is_False thm =
    1.38    let val _ $ t = #prop(rep_thm thm)
    1.39 -  in t = Const("False",boolT) end;
    1.40 +  in t = Const("False",HOLogic.boolT) end;
    1.41  
    1.42 -fun is_nat(t) = fastype_of1 t = nat;
    1.43 +fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    1.44  
    1.45  fun mk_nat_thm sg t =
    1.46 -  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),nat))
    1.47 +  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
    1.48    in instantiate ([],[(cn,ct)]) le0 end;
    1.49  
    1.50  end;