Transitivity reasoner ignores types amenable to linear arithmetic.
authorballarin
Thu Mar 24 16:34:15 2005 +0100 (2005-03-24 ago)
changeset 156224723248c982b
parent 15621 4c964b85df5c
child 15623 8b40f741597c
Transitivity reasoner ignores types amenable to linear arithmetic.
These are currently nat, int, real.

Fixed IsaMakefile.
src/HOL/IsaMakefile
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Mar 24 10:59:21 2005 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 24 16:34:15 2005 +0100
     1.3 @@ -96,7 +96,8 @@
     1.4    Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
     1.5    Refute.thy ROOT.ML \
     1.6    Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
     1.7 -  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
     1.8 +  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \
     1.9 +  Orderings.ML Orderings.thy Ring_and_Field.thy\
    1.10    Set.ML Set.thy SetInterval.thy \
    1.11    Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    1.12    Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
     2.1 --- a/src/HOL/Orderings.thy	Thu Mar 24 10:59:21 2005 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Thu Mar 24 16:34:15 2005 +0100
     2.3 @@ -287,7 +287,10 @@
     2.4     Quasi_Tac.quasi_tac are not of much use. *)
     2.5  
     2.6  fun decomp_gen sort sign (Trueprop $ t) =
     2.7 -  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
     2.8 +  let fun of_sort t = let val T = type_of t in
     2.9 +        (* exclude numeric types: linear arithmetic subsumes transitivity *)
    2.10 +        T <> HOLogic.natT andalso T <> HOLogic.intT andalso
    2.11 +        T <> HOLogic.realT andalso Sign.of_sort sign (T, sort) end
    2.12    fun dec (Const ("Not", _) $ t) = (
    2.13  	  case dec t of
    2.14  	    NONE => NONE