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