src/HOL/Tools/datatype_package.ML
changeset 25537 55017c8b0a24
parent 25495 98f3596bec44
child 25677 8b2ddc6e7be1
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Dec 05 14:15:51 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 05 14:15:59 2007 +0100
     1.3 @@ -61,9 +61,9 @@
     1.4    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
     1.5    val get_datatype : theory -> string -> DatatypeAux.datatype_info option
     1.6    val the_datatype : theory -> string -> DatatypeAux.datatype_info
     1.7 +  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
     1.8    val datatype_of_constr : theory -> string -> DatatypeAux.datatype_info option
     1.9    val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
    1.10 -  val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
    1.11    val get_datatype_constrs : theory -> string -> (string * typ) list option
    1.12    val interpretation: (string list -> theory -> theory) -> theory -> theory
    1.13    val print_datatypes : theory -> unit
    1.14 @@ -137,10 +137,9 @@
    1.15    |> Option.map (fn info as { descr, index, ... } =>
    1.16         (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
    1.17  
    1.18 -fun get_datatype_spec thy dtco =
    1.19 +fun the_datatype_spec thy dtco =
    1.20    let
    1.21 -    fun mk_cons typ_of_dtyp (co, tys) =
    1.22 -      (co, map typ_of_dtyp tys);
    1.23 +    fun mk_cons typ_of_dtyp (co, tys) = (co, map typ_of_dtyp tys);
    1.24      fun mk_dtyp ({ sorts = raw_sorts, descr, ... } : DatatypeAux.datatype_info, (dtys, cos)) =
    1.25        let
    1.26          val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
    1.27 @@ -148,10 +147,10 @@
    1.28          val typ_of_dtyp = DatatypeAux.typ_of_dtyp descr sorts;
    1.29          val tys = map typ_of_dtyp dtys;
    1.30        in (sorts, map (mk_cons typ_of_dtyp) cos) end;
    1.31 -  in Option.map mk_dtyp (get_datatype_descr thy dtco) end;
    1.32 +  in mk_dtyp (the (get_datatype_descr thy dtco)) end;
    1.33  
    1.34  fun get_datatype_constrs thy dtco =
    1.35 -  case get_datatype_spec thy dtco
    1.36 +  case try (the_datatype_spec thy) dtco
    1.37     of SOME (sorts, cos) =>
    1.38          let
    1.39            fun subst (v, sort) = TVar ((v, 0), sort);
    1.40 @@ -365,6 +364,26 @@
    1.41  
    1.42  exception ConstrDistinct of term;
    1.43  
    1.44 +fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
    1.45 +    QuickAndDirty => Thm.invoke_oracle
    1.46 +      (ThyInfo.the_theory "Datatype" thy) distinctN (thy, ConstrDistinct eq_t)
    1.47 +  | FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.48 +      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.49 +        atac 2, resolve_tac thms 1, etac FalseE 1]))
    1.50 +  | ManyConstrs (thm, simpset) =>
    1.51 +      let
    1.52 +        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    1.53 +          map (get_thm (ThyInfo.the_theory "Datatype" thy) o Name)
    1.54 +            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
    1.55 +      in
    1.56 +        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.57 +        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.58 +          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.59 +          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.60 +          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.61 +          etac FalseE 1]))
    1.62 +      end;
    1.63 +
    1.64  fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
    1.65    (case (stripC (0, t1), stripC (0, t2)) of
    1.66       ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
    1.67 @@ -374,27 +393,8 @@
    1.68                     (case (get_datatype_descr thy) tname1 of
    1.69                        SOME (_, (_, constrs)) => let val cnames = map fst constrs
    1.70                          in if cname1 mem cnames andalso cname2 mem cnames then
    1.71 -                             let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
    1.72 -                                 val eq_ct = cterm_of thy eq_t;
    1.73 -                                 val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    1.74 -                                 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    1.75 -                                   map (get_thm Datatype_thy o Name)
    1.76 -                                     ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
    1.77 -                             in (case (#distinct (the_datatype thy tname1)) of
    1.78 -                                 QuickAndDirty => SOME (Thm.invoke_oracle
    1.79 -                                   Datatype_thy distinctN (thy, ConstrDistinct eq_t))
    1.80 -                               | FewConstrs thms =>
    1.81 -                                   SOME (Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.82 -                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.83 -                                       atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.84 -                               | ManyConstrs (thm, simpset) =>
    1.85 -                                   SOME (Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.86 -                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.87 -                                      full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.88 -                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.89 -                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.90 -                                      etac FalseE 1]))))
    1.91 -                             end
    1.92 +                             SOME (distinct_rule thy ss tname1
    1.93 +                               (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
    1.94                             else NONE
    1.95                          end
    1.96                      | NONE => NONE)