src/HOL/Library/Types_To_Sets/unoverloading.ML
changeset 64551 79e9587dbcca
parent 64550 3e20defb1e3c
child 64552 7aa3c52f27aa
     1.1 --- a/src/HOL/Library/Types_To_Sets/unoverloading.ML	Thu Dec 08 15:11:20 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,139 +0,0 @@
     1.4 -(*  Title:      unoverloading.ML
     1.5 -    Author:     Ondřej Kunčar, TU München
     1.6 -
     1.7 -    Implements the Unoverloading Rule and extends the logic by the rule.
     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 -(* The actual implementation *)
    1.65 -
    1.66 -(** BEGINNING OF THE CRITICAL CODE **)
    1.67 -
    1.68 -fun fold_atyps_classes f =
    1.69 -  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S 
    1.70 -    | T as TVar (_, S) => fold (pair T #> f) S 
    1.71 -    (* just to avoid a warning about incomplete patterns *)
    1.72 -    | _ => raise TERM ("fold_atyps_classes", [])); 
    1.73 -
    1.74 -fun class_entries_of thy tm =
    1.75 -  let
    1.76 -    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
    1.77 -  in
    1.78 -    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
    1.79 -  end;
    1.80 -
    1.81 -fun unoverload_impl cconst thm =
    1.82 -  let
    1.83 -    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
    1.84 -
    1.85 -    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
    1.86 -    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
    1.87 -    
    1.88 -    val prop = Thm.prop_of thm;
    1.89 -    val prop_tfrees = rev (Term.add_tfree_names prop []);
    1.90 -    val _ = null prop_tfrees orelse err ("the theorem contains free type variables " 
    1.91 -      ^ commas_quote prop_tfrees);
    1.92 -
    1.93 -    val const = Thm.term_of cconst;
    1.94 -    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
    1.95 -    val const_tfrees = rev (Term.add_tfree_names const []);
    1.96 -    val _ = null const_tfrees orelse err ("the constant contains free type variables " 
    1.97 -      ^ commas_quote const_tfrees);
    1.98 -
    1.99 -    val thy = Thm.theory_of_thm thm;
   1.100 -    val defs = Theory.defs_of thy;
   1.101 -
   1.102 -    val const_entry = Theory.const_dep thy (Term.dest_Const const);
   1.103 -
   1.104 -    val Uss = Defs.specifications_of defs (fst const_entry);
   1.105 -    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss 
   1.106 -      orelse err "the constant instance has already a specification";
   1.107 -
   1.108 -    val context = Defs.global_context thy;
   1.109 -    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
   1.110 -    
   1.111 -    fun dep_err (c, Ts) (d, Us) =
   1.112 -      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
   1.113 -    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
   1.114 -    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
   1.115 -      orelse dep_err prop_entry const_entry;
   1.116 -    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
   1.117 -    val _ = forall not_depends_on_const prop_entries;
   1.118 -  in
   1.119 -    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
   1.120 -  end;
   1.121 -
   1.122 -(** END OF THE CRITICAL CODE **)
   1.123 -
   1.124 -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
   1.125 -  (Thm.add_oracle (@{binding unoverload},
   1.126 -  fn (const, thm) => unoverload_impl const  thm)));
   1.127 -
   1.128 -fun unoverload const thm = unoverload_oracle (const, thm);
   1.129 -
   1.130 -fun unoverload_attr const = 
   1.131 -  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
   1.132 -
   1.133 -val const = Args.context -- Args.term  >>
   1.134 -  (fn (ctxt, tm) => 
   1.135 -    if not (Term.is_Const tm) 
   1.136 -    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
   1.137 -    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
   1.138 -
   1.139 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload} 
   1.140 -  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
   1.141 -
   1.142 -end;
   1.143 \ No newline at end of file