src/HOL/Tools/refute.ML
changeset 37388 793618618f78
parent 37254 3625d37a0079
child 37391 476270a6c2dc
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -657,14 +657,14 @@
     1.4        (* other optimizations *)
     1.5        | Const (@{const_name Finite_Set.card}, _) => t
     1.6        | Const (@{const_name Finite_Set.finite}, _) => t
     1.7 -      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
     1.8 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
     1.9 -      | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
    1.10 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.11 -      | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
    1.12 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.13 -      | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
    1.14 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.15 +      | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
    1.16 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
    1.17 +      | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
    1.18 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
    1.19 +      | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
    1.20 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
    1.21 +      | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
    1.22 +        Type ("fun", [@{typ nat}, @{typ nat}])])) => t
    1.23        | Const (@{const_name List.append}, _) => t
    1.24  (* UNSOUND
    1.25        | Const (@{const_name lfp}, _) => t
    1.26 @@ -834,17 +834,17 @@
    1.27        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
    1.28        | Const (@{const_name Finite_Set.finite}, T) =>
    1.29          collect_type_axioms T axs
    1.30 -      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
    1.31 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.32 +      | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
    1.33 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
    1.34            collect_type_axioms T axs
    1.35 -      | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
    1.36 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.37 +      | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
    1.38 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.39            collect_type_axioms T axs
    1.40 -      | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
    1.41 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.42 +      | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
    1.43 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.44            collect_type_axioms T axs
    1.45 -      | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []),
    1.46 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.47 +      | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
    1.48 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.49            collect_type_axioms T axs
    1.50        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
    1.51  (* UNSOUND
    1.52 @@ -2654,7 +2654,7 @@
    1.53      case t of
    1.54        Const (@{const_name Finite_Set.card},
    1.55          Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
    1.56 -                      Type ("nat", [])])) =>
    1.57 +                      @{typ nat}])) =>
    1.58        let
    1.59          (* interpretation -> int *)
    1.60          fun number_of_elements (Node xs) =
    1.61 @@ -2670,7 +2670,7 @@
    1.62            | number_of_elements (Leaf _) =
    1.63            raise REFUTE ("Finite_Set_card_interpreter",
    1.64              "interpretation for set type is a leaf")
    1.65 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.66 +        val size_of_nat = size_of_type thy model (@{typ nat})
    1.67          (* takes an interpretation for a set and returns an interpretation *)
    1.68          (* for a 'nat' denoting the set's cardinality                      *)
    1.69          (* interpretation -> interpretation *)
    1.70 @@ -2730,10 +2730,10 @@
    1.71  
    1.72    fun Nat_less_interpreter thy model args t =
    1.73      case t of
    1.74 -      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    1.75 -        Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.76 +      Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
    1.77 +        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
    1.78        let
    1.79 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.80 +        val size_of_nat = size_of_type thy model (@{typ nat})
    1.81          (* the 'n'-th nat is not less than the first 'n' nats, while it *)
    1.82          (* is less than the remaining 'size_of_nat - n' nats            *)
    1.83          (* int -> interpretation *)
    1.84 @@ -2753,10 +2753,10 @@
    1.85  
    1.86    fun Nat_plus_interpreter thy model args t =
    1.87      case t of
    1.88 -      Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
    1.89 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.90 +      Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
    1.91 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.92        let
    1.93 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.94 +        val size_of_nat = size_of_type thy model (@{typ nat})
    1.95          (* int -> int -> interpretation *)
    1.96          fun plus m n =
    1.97            let
    1.98 @@ -2784,10 +2784,10 @@
    1.99  
   1.100    fun Nat_minus_interpreter thy model args t =
   1.101      case t of
   1.102 -      Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
   1.103 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.104 +      Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
   1.105 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.106        let
   1.107 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
   1.108 +        val size_of_nat = size_of_type thy model (@{typ nat})
   1.109          (* int -> int -> interpretation *)
   1.110          fun minus m n =
   1.111            let
   1.112 @@ -2812,10 +2812,10 @@
   1.113  
   1.114    fun Nat_times_interpreter thy model args t =
   1.115      case t of
   1.116 -      Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
   1.117 -        Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.118 +      Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
   1.119 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.120        let
   1.121 -        val size_of_nat = size_of_type thy model (Type ("nat", []))
   1.122 +        val size_of_nat = size_of_type thy model (@{typ nat})
   1.123          (* nat -> nat -> interpretation *)
   1.124          fun mult m n =
   1.125            let