src/HOL/Types_To_Sets/unoverloading.ML
changeset 64551 79e9587dbcca
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/unoverloading.ML	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,140 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/unoverloading.ML
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +
     1.7 +The Unoverloading Rule (extension of the logic).
     1.8 +*)
     1.9 +
    1.10 +signature UNOVERLOADING =
    1.11 +sig
    1.12 +  val unoverload: cterm -> thm -> thm
    1.13 +  val unoverload_attr: cterm -> attribute
    1.14 +end;
    1.15 +
    1.16 +structure Unoverloading : UNOVERLOADING =
    1.17 +struct
    1.18 +
    1.19 +(*
    1.20 +Unoverloading Rule (UO)
    1.21 +
    1.22 +      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
    1.23 +---------------------------- [no type or constant or type class in \<phi>
    1.24 +        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
    1.25 +*)
    1.26 +
    1.27 +(* The following functions match_args, reduction and entries_of were
    1.28 +   cloned from defs.ML and theory.ML because the functions are not public.
    1.29 +   Notice that these functions already belong to the critical code.
    1.30 +*)
    1.31 +
    1.32 +(* >= *)
    1.33 +fun match_args (Ts, Us) =
    1.34 +  if Type.could_matches (Ts, Us) then
    1.35 +    Option.map Envir.subst_type
    1.36 +      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
    1.37 +  else NONE;
    1.38 +
    1.39 +fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
    1.40 +  let
    1.41 +    fun reduct Us (Ts, rhs) =
    1.42 +      (case match_args (Ts, Us) of
    1.43 +        NONE => NONE
    1.44 +      | SOME subst => SOME (map (apsnd (map subst)) rhs));
    1.45 +    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
    1.46 +
    1.47 +    val reds = map (`reducts) deps;
    1.48 +    val deps' =
    1.49 +      if forall (is_none o #1) reds then NONE
    1.50 +      else SOME (fold_rev
    1.51 +        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
    1.52 +  in deps' end;
    1.53 +
    1.54 +fun const_and_typ_entries_of thy tm =
    1.55 + let
    1.56 +   val consts =
    1.57 +     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
    1.58 +   val types =
    1.59 +     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
    1.60 + in
    1.61 +   consts @ types
    1.62 + end;
    1.63 +
    1.64 +
    1.65 +(* The actual implementation *)
    1.66 +
    1.67 +(** BEGINNING OF THE CRITICAL CODE **)
    1.68 +
    1.69 +fun fold_atyps_classes f =
    1.70 +  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
    1.71 +    | T as TVar (_, S) => fold (pair T #> f) S
    1.72 +    (* just to avoid a warning about incomplete patterns *)
    1.73 +    | _ => raise TERM ("fold_atyps_classes", []));
    1.74 +
    1.75 +fun class_entries_of thy tm =
    1.76 +  let
    1.77 +    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
    1.78 +  in
    1.79 +    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
    1.80 +  end;
    1.81 +
    1.82 +fun unoverload_impl cconst thm =
    1.83 +  let
    1.84 +    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
    1.85 +
    1.86 +    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
    1.87 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
    1.88 +
    1.89 +    val prop = Thm.prop_of thm;
    1.90 +    val prop_tfrees = rev (Term.add_tfree_names prop []);
    1.91 +    val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
    1.92 +      ^ commas_quote prop_tfrees);
    1.93 +
    1.94 +    val const = Thm.term_of cconst;
    1.95 +    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
    1.96 +    val const_tfrees = rev (Term.add_tfree_names const []);
    1.97 +    val _ = null const_tfrees orelse err ("the constant contains free type variables "
    1.98 +      ^ commas_quote const_tfrees);
    1.99 +
   1.100 +    val thy = Thm.theory_of_thm thm;
   1.101 +    val defs = Theory.defs_of thy;
   1.102 +
   1.103 +    val const_entry = Theory.const_dep thy (Term.dest_Const const);
   1.104 +
   1.105 +    val Uss = Defs.specifications_of defs (fst const_entry);
   1.106 +    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
   1.107 +      orelse err "the constant instance has already a specification";
   1.108 +
   1.109 +    val context = Defs.global_context thy;
   1.110 +    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
   1.111 +
   1.112 +    fun dep_err (c, Ts) (d, Us) =
   1.113 +      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
   1.114 +    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
   1.115 +    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
   1.116 +      orelse dep_err prop_entry const_entry;
   1.117 +    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
   1.118 +    val _ = forall not_depends_on_const prop_entries;
   1.119 +  in
   1.120 +    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
   1.121 +  end;
   1.122 +
   1.123 +(** END OF THE CRITICAL CODE **)
   1.124 +
   1.125 +val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
   1.126 +  (Thm.add_oracle (@{binding unoverload},
   1.127 +  fn (const, thm) => unoverload_impl const  thm)));
   1.128 +
   1.129 +fun unoverload const thm = unoverload_oracle (const, thm);
   1.130 +
   1.131 +fun unoverload_attr const =
   1.132 +  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
   1.133 +
   1.134 +val const = Args.context -- Args.term  >>
   1.135 +  (fn (ctxt, tm) =>
   1.136 +    if not (Term.is_Const tm)
   1.137 +    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
   1.138 +    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
   1.139 +
   1.140 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
   1.141 +  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
   1.142 +
   1.143 +end;