src/HOL/Types_To_Sets/unoverloading.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64551 79e9587dbcca
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
wenzelm@64551
     1
(*  Title:      HOL/Types_To_Sets/unoverloading.ML
wenzelm@64551
     2
    Author:     Ondřej Kunčar, TU München
wenzelm@64551
     3
wenzelm@64551
     4
The Unoverloading Rule (extension of the logic).
wenzelm@64551
     5
*)
wenzelm@64551
     6
wenzelm@64551
     7
signature UNOVERLOADING =
wenzelm@64551
     8
sig
wenzelm@64551
     9
  val unoverload: cterm -> thm -> thm
wenzelm@64551
    10
  val unoverload_attr: cterm -> attribute
wenzelm@64551
    11
end;
wenzelm@64551
    12
wenzelm@64551
    13
structure Unoverloading : UNOVERLOADING =
wenzelm@64551
    14
struct
wenzelm@64551
    15
wenzelm@64551
    16
(*
wenzelm@64551
    17
Unoverloading Rule (UO)
wenzelm@64551
    18
wenzelm@64551
    19
      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
wenzelm@64551
    20
---------------------------- [no type or constant or type class in \<phi>
wenzelm@64551
    21
        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
wenzelm@64551
    22
*)
wenzelm@64551
    23
wenzelm@64551
    24
(* The following functions match_args, reduction and entries_of were
wenzelm@64551
    25
   cloned from defs.ML and theory.ML because the functions are not public.
wenzelm@64551
    26
   Notice that these functions already belong to the critical code.
wenzelm@64551
    27
*)
wenzelm@64551
    28
wenzelm@64551
    29
(* >= *)
wenzelm@64551
    30
fun match_args (Ts, Us) =
wenzelm@64551
    31
  if Type.could_matches (Ts, Us) then
wenzelm@64551
    32
    Option.map Envir.subst_type
wenzelm@64551
    33
      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
wenzelm@64551
    34
  else NONE;
wenzelm@64551
    35
wenzelm@64551
    36
fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
wenzelm@64551
    37
  let
wenzelm@64551
    38
    fun reduct Us (Ts, rhs) =
wenzelm@64551
    39
      (case match_args (Ts, Us) of
wenzelm@64551
    40
        NONE => NONE
wenzelm@64551
    41
      | SOME subst => SOME (map (apsnd (map subst)) rhs));
wenzelm@64551
    42
    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
wenzelm@64551
    43
wenzelm@64551
    44
    val reds = map (`reducts) deps;
wenzelm@64551
    45
    val deps' =
wenzelm@64551
    46
      if forall (is_none o #1) reds then NONE
wenzelm@64551
    47
      else SOME (fold_rev
wenzelm@64551
    48
        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
wenzelm@64551
    49
  in deps' end;
wenzelm@64551
    50
wenzelm@64551
    51
fun const_and_typ_entries_of thy tm =
wenzelm@64551
    52
 let
wenzelm@64551
    53
   val consts =
wenzelm@64551
    54
     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
wenzelm@64551
    55
   val types =
wenzelm@64551
    56
     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
wenzelm@64551
    57
 in
wenzelm@64551
    58
   consts @ types
wenzelm@64551
    59
 end;
wenzelm@64551
    60
wenzelm@64551
    61
wenzelm@64551
    62
(* The actual implementation *)
wenzelm@64551
    63
wenzelm@64551
    64
(** BEGINNING OF THE CRITICAL CODE **)
wenzelm@64551
    65
wenzelm@64551
    66
fun fold_atyps_classes f =
wenzelm@64551
    67
  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
wenzelm@64551
    68
    | T as TVar (_, S) => fold (pair T #> f) S
wenzelm@64551
    69
    (* just to avoid a warning about incomplete patterns *)
wenzelm@64551
    70
    | _ => raise TERM ("fold_atyps_classes", []));
wenzelm@64551
    71
wenzelm@64551
    72
fun class_entries_of thy tm =
wenzelm@64551
    73
  let
wenzelm@64551
    74
    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
wenzelm@64551
    75
  in
wenzelm@64551
    76
    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
wenzelm@64551
    77
  end;
wenzelm@64551
    78
wenzelm@64551
    79
fun unoverload_impl cconst thm =
wenzelm@64551
    80
  let
wenzelm@64551
    81
    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
wenzelm@64551
    82
wenzelm@64551
    83
    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
wenzelm@64551
    84
    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
wenzelm@64551
    85
wenzelm@64551
    86
    val prop = Thm.prop_of thm;
wenzelm@64551
    87
    val prop_tfrees = rev (Term.add_tfree_names prop []);
wenzelm@64551
    88
    val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
wenzelm@64551
    89
      ^ commas_quote prop_tfrees);
wenzelm@64551
    90
wenzelm@64551
    91
    val const = Thm.term_of cconst;
wenzelm@64551
    92
    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
wenzelm@64551
    93
    val const_tfrees = rev (Term.add_tfree_names const []);
wenzelm@64551
    94
    val _ = null const_tfrees orelse err ("the constant contains free type variables "
wenzelm@64551
    95
      ^ commas_quote const_tfrees);
wenzelm@64551
    96
wenzelm@64551
    97
    val thy = Thm.theory_of_thm thm;
wenzelm@64551
    98
    val defs = Theory.defs_of thy;
wenzelm@64551
    99
wenzelm@64551
   100
    val const_entry = Theory.const_dep thy (Term.dest_Const const);
wenzelm@64551
   101
wenzelm@64551
   102
    val Uss = Defs.specifications_of defs (fst const_entry);
wenzelm@64551
   103
    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
wenzelm@64551
   104
      orelse err "the constant instance has already a specification";
wenzelm@64551
   105
wenzelm@64551
   106
    val context = Defs.global_context thy;
wenzelm@64551
   107
    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
wenzelm@64551
   108
wenzelm@64551
   109
    fun dep_err (c, Ts) (d, Us) =
wenzelm@64551
   110
      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
wenzelm@64551
   111
    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
wenzelm@64551
   112
    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
wenzelm@64551
   113
      orelse dep_err prop_entry const_entry;
wenzelm@64551
   114
    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
wenzelm@64551
   115
    val _ = forall not_depends_on_const prop_entries;
wenzelm@64551
   116
  in
wenzelm@64551
   117
    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
wenzelm@64551
   118
  end;
wenzelm@64551
   119
wenzelm@64551
   120
(** END OF THE CRITICAL CODE **)
wenzelm@64551
   121
wenzelm@64551
   122
val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
wenzelm@64551
   123
  (Thm.add_oracle (@{binding unoverload},
wenzelm@64551
   124
  fn (const, thm) => unoverload_impl const  thm)));
wenzelm@64551
   125
wenzelm@64551
   126
fun unoverload const thm = unoverload_oracle (const, thm);
wenzelm@64551
   127
wenzelm@64551
   128
fun unoverload_attr const =
wenzelm@64551
   129
  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
wenzelm@64551
   130
wenzelm@64551
   131
val const = Args.context -- Args.term  >>
wenzelm@64551
   132
  (fn (ctxt, tm) =>
wenzelm@64551
   133
    if not (Term.is_Const tm)
wenzelm@64551
   134
    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
wenzelm@64551
   135
    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
wenzelm@64551
   136
wenzelm@64551
   137
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
wenzelm@64551
   138
  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
wenzelm@64551
   139
wenzelm@64551
   140
end;