src/HOL/Library/refute.ML
changeset 58120 a14b8d77b15a
parent 58109 6d4695335d41
child 58129 3ec65a7f2b50
     1.1 --- a/src/HOL/Library/refute.ML	Mon Sep 01 16:17:47 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Sep 01 16:17:47 2014 +0200
     1.3 @@ -367,11 +367,11 @@
     1.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
     1.8 -    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
     1.9 -  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
    1.10 +fun typ_of_dtyp _ typ_assoc (Old_Datatype_Aux.DtTFree a) =
    1.11 +    the (AList.lookup (op =) typ_assoc (Old_Datatype_Aux.DtTFree a))
    1.12 +  | typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtType (s, Us)) =
    1.13      Type (s, map (typ_of_dtyp descr typ_assoc) Us)
    1.14 -  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
    1.15 +  | typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtRec i) =
    1.16      let val (s, ds, _) = the (AList.lookup (op =) descr i) in
    1.17        Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.18      end
    1.19 @@ -402,7 +402,7 @@
    1.20  fun is_IDT_constructor thy (s, T) =
    1.21    (case body_type T of
    1.22      Type (s', _) =>
    1.23 -      (case Datatype.get_constrs thy s' of
    1.24 +      (case Old_Datatype_Data.get_constrs thy s' of
    1.25          SOME constrs =>
    1.26            List.exists (fn (cname, cty) =>
    1.27              cname = s andalso Sign.typ_instance thy (T, cty)) constrs
    1.28 @@ -417,7 +417,7 @@
    1.29  fun is_IDT_recursor thy (s, _) =
    1.30    let
    1.31      val rec_names = Symtab.fold (append o #rec_names o snd)
    1.32 -      (Datatype.get_all thy) []
    1.33 +      (Old_Datatype_Data.get_all thy) []
    1.34    in
    1.35      (* I'm not quite sure if checking the name 's' is sufficient, *)
    1.36      (* or if we should also check the type 'T'.                   *)
    1.37 @@ -691,7 +691,7 @@
    1.38        (* axiomatic type classes *)
    1.39        | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    1.40        | Type (s, Ts) =>
    1.41 -        (case Datatype.get_info thy s of
    1.42 +        (case Old_Datatype_Data.get_info thy s of
    1.43            SOME _ =>  (* inductive datatype *)
    1.44              (* only collect relevant type axioms for the argument types *)
    1.45              fold collect_type_axioms Ts axs
    1.46 @@ -820,7 +820,7 @@
    1.47        | Type (@{type_name prop}, []) => acc
    1.48        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    1.49        | Type (s, Ts) =>
    1.50 -          (case Datatype.get_info thy s of
    1.51 +          (case Old_Datatype_Data.get_info thy s of
    1.52              SOME info =>  (* inductive datatype *)
    1.53                let
    1.54                  val index = #index info
    1.55 @@ -830,7 +830,7 @@
    1.56                  (* sanity check: every element in 'dtyps' must be a *)
    1.57                  (* 'DtTFree'                                        *)
    1.58                  val _ = if Library.exists (fn d =>
    1.59 -                  case d of Datatype.DtTFree _ => false | _ => true) typs then
    1.60 +                  case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) typs then
    1.61                    raise REFUTE ("ground_types", "datatype argument (for type "
    1.62                      ^ Syntax.string_of_typ ctxt T ^ ") is not a variable")
    1.63                  else ()
    1.64 @@ -842,11 +842,11 @@
    1.65                      val dT = typ_of_dtyp descr typ_assoc d
    1.66                    in
    1.67                      case d of
    1.68 -                      Datatype.DtTFree _ =>
    1.69 +                      Old_Datatype_Aux.DtTFree _ =>
    1.70                        collect_types dT acc
    1.71 -                    | Datatype.DtType (_, ds) =>
    1.72 +                    | Old_Datatype_Aux.DtType (_, ds) =>
    1.73                        collect_types dT (fold_rev collect_dtyp ds acc)
    1.74 -                    | Datatype.DtRec i =>
    1.75 +                    | Old_Datatype_Aux.DtRec i =>
    1.76                        if member (op =) acc dT then
    1.77                          acc  (* prevent infinite recursion *)
    1.78                        else
    1.79 @@ -855,7 +855,7 @@
    1.80                            (* if the current type is a recursive IDT (i.e. a depth *)
    1.81                            (* is required), add it to 'acc'                        *)
    1.82                            val acc_dT = if Library.exists (fn (_, ds) =>
    1.83 -                            Library.exists Datatype_Aux.is_rec_type ds) dconstrs then
    1.84 +                            Library.exists Old_Datatype_Aux.is_rec_type ds) dconstrs then
    1.85                                insert (op =) dT acc
    1.86                              else acc
    1.87                            (* collect argument types *)
    1.88 @@ -869,7 +869,7 @@
    1.89                in
    1.90                  (* argument types 'Ts' could be added here, but they are also *)
    1.91                  (* added by 'collect_dtyp' automatically                      *)
    1.92 -                collect_dtyp (Datatype.DtRec index) acc
    1.93 +                collect_dtyp (Old_Datatype_Aux.DtRec index) acc
    1.94                end
    1.95            | NONE =>
    1.96              (* not an inductive datatype, e.g. defined via "typedef" or *)
    1.97 @@ -1015,7 +1015,7 @@
    1.98          (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    1.99          val maybe_spurious = Library.exists (fn
   1.100              Type (s, _) =>
   1.101 -              (case Datatype.get_info thy s of
   1.102 +              (case Old_Datatype_Data.get_info thy s of
   1.103                  SOME info =>  (* inductive datatype *)
   1.104                    let
   1.105                      val index           = #index info
   1.106 @@ -1024,7 +1024,7 @@
   1.107                    in
   1.108                      (* recursive datatype? *)
   1.109                      Library.exists (fn (_, ds) =>
   1.110 -                      Library.exists Datatype_Aux.is_rec_type ds) constrs
   1.111 +                      Library.exists Old_Datatype_Aux.is_rec_type ds) constrs
   1.112                    end
   1.113                | NONE => false)
   1.114            | _ => false) types
   1.115 @@ -1741,7 +1741,7 @@
   1.116      val thy = Proof_Context.theory_of ctxt
   1.117      val (typs, terms) = model
   1.118      fun interpret_term (Type (s, Ts)) =
   1.119 -          (case Datatype.get_info thy s of
   1.120 +          (case Old_Datatype_Data.get_info thy s of
   1.121              SOME info =>  (* inductive datatype *)
   1.122                let
   1.123                  (* only recursive IDTs have an associated depth *)
   1.124 @@ -1767,7 +1767,7 @@
   1.125                      (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.126                      val _ =
   1.127                        if Library.exists (fn d =>
   1.128 -                        case d of Datatype.DtTFree _ => false | _ => true) dtyps
   1.129 +                        case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) dtyps
   1.130                        then
   1.131                          raise REFUTE ("IDT_interpreter",
   1.132                            "datatype argument (for type "
   1.133 @@ -1866,7 +1866,7 @@
   1.134                  HOLogic_empty_set) pairss
   1.135              end
   1.136        | Type (s, Ts) =>
   1.137 -          (case Datatype.get_info thy s of
   1.138 +          (case Old_Datatype_Data.get_info thy s of
   1.139              SOME info =>
   1.140                (case AList.lookup (op =) typs T of
   1.141                  SOME 0 =>
   1.142 @@ -1881,7 +1881,7 @@
   1.143                    (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.144                    val _ =
   1.145                      if Library.exists (fn d =>
   1.146 -                      case d of Datatype.DtTFree _ => false | _ => true) dtyps
   1.147 +                      case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) dtyps
   1.148                      then
   1.149                        raise REFUTE ("IDT_constructor_interpreter",
   1.150                          "datatype argument (for type "
   1.151 @@ -1932,7 +1932,7 @@
   1.152            Const (s, T) =>
   1.153              (case body_type T of
   1.154                Type (s', Ts') =>
   1.155 -                (case Datatype.get_info thy s' of
   1.156 +                (case Old_Datatype_Data.get_info thy s' of
   1.157                    SOME info =>  (* body type is an inductive datatype *)
   1.158                      let
   1.159                        val index               = #index info
   1.160 @@ -1941,7 +1941,7 @@
   1.161                        val typ_assoc           = dtyps ~~ Ts'
   1.162                        (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.163                        val _ = if Library.exists (fn d =>
   1.164 -                          case d of Datatype.DtTFree _ => false | _ => true) dtyps
   1.165 +                          case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) dtyps
   1.166                          then
   1.167                            raise REFUTE ("IDT_constructor_interpreter",
   1.168                              "datatype argument (for type "
   1.169 @@ -2153,7 +2153,7 @@
   1.170                        (*               'DtTFree'                          *)
   1.171                        val _ =
   1.172                          if Library.exists (fn d =>
   1.173 -                          case d of Datatype.DtTFree _ => false
   1.174 +                          case d of Old_Datatype_Aux.DtTFree _ => false
   1.175                                    | _ => true) dtyps
   1.176                          then
   1.177                            raise REFUTE ("IDT_recursion_interpreter",
   1.178 @@ -2174,10 +2174,10 @@
   1.179                              (case AList.lookup op= acc d of
   1.180                                NONE =>
   1.181                                  (case d of
   1.182 -                                  Datatype.DtTFree _ =>
   1.183 +                                  Old_Datatype_Aux.DtTFree _ =>
   1.184                                    (* add the association, proceed *)
   1.185                                    rec_typ_assoc ((d, T)::acc) xs
   1.186 -                                | Datatype.DtType (s, ds) =>
   1.187 +                                | Old_Datatype_Aux.DtType (s, ds) =>
   1.188                                      let
   1.189                                        val (s', Ts) = dest_Type T
   1.190                                      in
   1.191 @@ -2187,7 +2187,7 @@
   1.192                                          raise REFUTE ("IDT_recursion_interpreter",
   1.193                                            "DtType/Type mismatch")
   1.194                                      end
   1.195 -                                | Datatype.DtRec i =>
   1.196 +                                | Old_Datatype_Aux.DtRec i =>
   1.197                                      let
   1.198                                        val (_, ds, _) = the (AList.lookup (op =) descr i)
   1.199                                        val (_, Ts)    = dest_Type T
   1.200 @@ -2203,7 +2203,7 @@
   1.201                                    raise REFUTE ("IDT_recursion_interpreter",
   1.202                                      "different type associations for the same dtyp"))
   1.203                        val typ_assoc = filter
   1.204 -                        (fn (Datatype.DtTFree _, _) => true | (_, _) => false)
   1.205 +                        (fn (Old_Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
   1.206                          (rec_typ_assoc []
   1.207                            (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
   1.208                        (* sanity check: typ_assoc must associate types to the   *)
   1.209 @@ -2220,7 +2220,7 @@
   1.210                        val mc_intrs = map (fn (idx, (_, _, cs)) =>
   1.211                          let
   1.212                            val c_return_typ = typ_of_dtyp descr typ_assoc
   1.213 -                            (Datatype.DtRec idx)
   1.214 +                            (Old_Datatype_Aux.DtRec idx)
   1.215                          in
   1.216                            (idx, map (fn (cname, cargs) =>
   1.217                              (#1 o interpret ctxt (typs, []) {maxvars=0,
   1.218 @@ -2272,7 +2272,7 @@
   1.219                        val _ = map (fn (idx, intrs) =>
   1.220                          let
   1.221                            val T = typ_of_dtyp descr typ_assoc
   1.222 -                            (Datatype.DtRec idx)
   1.223 +                            (Old_Datatype_Aux.DtRec idx)
   1.224                          in
   1.225                            if length intrs <> size_of_type ctxt (typs, []) T then
   1.226                              raise REFUTE ("IDT_recursion_interpreter",
   1.227 @@ -2346,7 +2346,7 @@
   1.228                                val (_, _, constrs) = the (AList.lookup (op =) descr idx)
   1.229                                val (_, dtyps) = nth constrs c
   1.230                                val rec_dtyps_args = filter
   1.231 -                                (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
   1.232 +                                (Old_Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
   1.233                                (* map those indices to interpretations *)
   1.234                                val rec_dtyps_intrs = map (fn (dtyp, arg) =>
   1.235                                  let
   1.236 @@ -2359,17 +2359,17 @@
   1.237                                (* takes the dtyp and interpretation of an element, *)
   1.238                                (* and computes the interpretation for the          *)
   1.239                                (* corresponding recursive argument                 *)
   1.240 -                              fun rec_intr (Datatype.DtRec i) (Leaf xs) =
   1.241 +                              fun rec_intr (Old_Datatype_Aux.DtRec i) (Leaf xs) =
   1.242                                      (* recursive argument is "rec_i params elem" *)
   1.243                                      compute_array_entry i (find_index (fn x => x = True) xs)
   1.244 -                                | rec_intr (Datatype.DtRec _) (Node _) =
   1.245 +                                | rec_intr (Old_Datatype_Aux.DtRec _) (Node _) =
   1.246                                      raise REFUTE ("IDT_recursion_interpreter",
   1.247                                        "interpretation for IDT is a node")
   1.248 -                                | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) =
   1.249 +                                | rec_intr (Old_Datatype_Aux.DtType ("fun", [_, dt2])) (Node xs) =
   1.250                                      (* recursive argument is something like     *)
   1.251                                      (* "\<lambda>x::dt1. rec_? params (elem x)" *)
   1.252                                      Node (map (rec_intr dt2) xs)
   1.253 -                                | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) =
   1.254 +                                | rec_intr (Old_Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) =
   1.255                                      raise REFUTE ("IDT_recursion_interpreter",
   1.256                                        "interpretation for function dtyp is a leaf")
   1.257                                  | rec_intr _ _ =
   1.258 @@ -2404,7 +2404,7 @@
   1.259                  end
   1.260                else
   1.261                  NONE  (* not a recursion operator of this datatype *)
   1.262 -          ) (Datatype.get_all thy) NONE
   1.263 +          ) (Old_Datatype_Data.get_all thy) NONE
   1.264      | _ =>  (* head of term is not a constant *)
   1.265        NONE
   1.266    end;
   1.267 @@ -2838,7 +2838,7 @@
   1.268    in
   1.269      (case T of
   1.270        Type (s, Ts) =>
   1.271 -        (case Datatype.get_info thy s of
   1.272 +        (case Old_Datatype_Data.get_info thy s of
   1.273            SOME info =>  (* inductive datatype *)
   1.274              let
   1.275                val (typs, _)           = model
   1.276 @@ -2849,7 +2849,7 @@
   1.277                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.278                val _ =
   1.279                  if Library.exists (fn d =>
   1.280 -                  case d of Datatype.DtTFree _ => false | _ => true) dtyps
   1.281 +                  case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) dtyps
   1.282                  then
   1.283                    raise REFUTE ("IDT_printer", "datatype argument (for type " ^
   1.284                      Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable")