1(* Title: HOL/Types_To_Sets/unoverloading.ML 2 Author: Ond��ej Kun��ar, TU M��nchen 3 4The Unoverloading Rule (extension of the logic). 5*) 6 7signature UNOVERLOADING = 8sig 9 val unoverload: cterm -> thm -> thm 10 val unoverload_attr: cterm -> attribute 11end; 12 13structure Unoverloading : UNOVERLOADING = 14struct 15 16(* 17Unoverloading 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(* >= *) 30fun 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 36fun 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 51fun 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 66fun 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 72fun 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 79fun 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 122val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result 123 (Thm.add_oracle (\<^binding>\<open>unoverload\<close>, 124 fn (const, thm) => unoverload_impl const thm))); 125 126fun unoverload const thm = unoverload_oracle (const, thm); 127 128fun unoverload_attr const = 129 Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm)); 130 131val 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 137val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload\<close> 138 (const >> unoverload_attr) "unoverload an uninterpreted constant")); 139 140end; 141