src/HOL/Tools/SMT/smt_normalize.ML
changeset 39483 9f0e5684f04b
parent 38864 4abe644fcea5
child 40161 539d07b00e5f
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 08:41:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 10:52:35 2010 +0200
     1.3 @@ -9,14 +9,16 @@
     1.4    * embed natural numbers into integers,
     1.5    * add extra rules specifying types and constants which occur frequently,
     1.6    * fully translate into object logic, add universal closure,
     1.7 +  * monomorphize (create instances of schematic rules),
     1.8    * lift lambda terms,
     1.9    * make applications explicit for functions with varying number of arguments.
    1.10 +  * add (hypothetical definitions for) missing datatype selectors,
    1.11  *)
    1.12  
    1.13  signature SMT_NORMALIZE =
    1.14  sig
    1.15    type extra_norm = thm list -> Proof.context -> thm list * Proof.context
    1.16 -  val normalize: extra_norm -> thm list -> Proof.context ->
    1.17 +  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
    1.18      thm list * Proof.context
    1.19    val atomize_conv: Proof.context -> conv
    1.20    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.21 @@ -427,13 +429,60 @@
    1.22  
    1.23  
    1.24  
    1.25 +(* add missing datatype selectors via hypothetical definitions *)
    1.26 +
    1.27 +local
    1.28 +  val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I)
    1.29 +
    1.30 +  fun collect t =
    1.31 +    (case Term.strip_comb t of
    1.32 +      (Abs (_, T, t), _) => add T #> collect t
    1.33 +    | (Const (_, T), ts) => collects T ts
    1.34 +    | (Free (_, T), ts) => collects T ts
    1.35 +    | _ => I)
    1.36 +  and collects T ts =
    1.37 +    let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts))
    1.38 +    in fold add Ts #> add (Us ---> U) #> fold collect ts end
    1.39 +
    1.40 +  fun add_constructors thy n =
    1.41 +    (case Datatype.get_info thy n of
    1.42 +      NONE => I
    1.43 +    | SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) =>
    1.44 +        fold (insert (op =) o pair n) (1 upto length ds)) cs) descr)
    1.45 +
    1.46 +  fun add_selector (c as (n, i)) ctxt =
    1.47 +    (case Datatype_Selectors.lookup_selector ctxt c of
    1.48 +      SOME _ => ctxt
    1.49 +    | NONE =>
    1.50 +        let
    1.51 +          val T = Sign.the_const_type (ProofContext.theory_of ctxt) n
    1.52 +          val U = Term.body_type T --> nth (Term.binder_types T) (i-1)
    1.53 +        in
    1.54 +          ctxt
    1.55 +          |> yield_singleton Variable.variant_fixes Name.uu
    1.56 +          |>> pair ((n, T), i) o rpair U
    1.57 +          |-> Context.proof_map o Datatype_Selectors.add_selector
    1.58 +        end)
    1.59 +in
    1.60 +
    1.61 +fun datatype_selectors thms ctxt =
    1.62 +  let
    1.63 +    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
    1.64 +    val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
    1.65 +  in (thms, fold add_selector cs ctxt) end
    1.66 +    (* FIXME: also generate hypothetical definitions for the selectors *)
    1.67 +
    1.68 +end
    1.69 +
    1.70 +
    1.71 +
    1.72  (* combined normalization *)
    1.73  
    1.74  type extra_norm = thm list -> Proof.context -> thm list * Proof.context
    1.75  
    1.76  fun with_context f thms ctxt = (f ctxt thms, ctxt)
    1.77  
    1.78 -fun normalize extra_norm thms ctxt =
    1.79 +fun normalize extra_norm with_datatypes thms ctxt =
    1.80    thms
    1.81    |> trivial_distinct ctxt
    1.82    |> rewrite_bool_cases ctxt
    1.83 @@ -445,5 +494,6 @@
    1.84    |-> SMT_Monomorph.monomorph
    1.85    |-> lift_lambdas
    1.86    |-> with_context explicit_application
    1.87 +  |-> (if with_datatypes then datatype_selectors else pair)
    1.88  
    1.89  end