--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Types_To_Sets.thy Sun Oct 30 13:15:14 2016 +0100
@@ -0,0 +1,27 @@
+(* Title: HOL/Library/Types_To_Sets.thy
+ Author: Ondřej Kunčar, TU München
+*)
+
+section \<open>From Types to Sets\<close>
+
+text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
+ to allow translation of types to sets as described in
+ O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
+ available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
+
+theory Types_To_Sets
+ imports Main
+begin
+
+subsection \<open>Rules\<close>
+
+text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
+ML_file "Types_To_Sets/local_typedef.ML"
+
+text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
+ML_file "Types_To_Sets/unoverloading.ML"
+
+text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
+ML_file "Types_To_Sets/internalize_sort.ML"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Types_To_Sets/internalize_sort.ML Sun Oct 30 13:15:14 2016 +0100
@@ -0,0 +1,68 @@
+(* Title: internalize_sort.ML
+ Author: Ondřej Kunčar, TU München
+
+ Implements a derived rule (by using Thm.unconstrainT) that internalizes
+ type class annotations.
+*)
+
+
+(*
+ \<phi>['a::{c_1, ..., c_n} / 'a]
+---------------------------------------------------------------------
+ class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
+
+where class.c is the locale predicate associated with type class c and
+ops are operations associated with type class c. For example:
+If c = semigroup_add, then ops = op-, op+, 0, uminus.
+If c = finite, then ops = TYPE('a::type).
+*)
+
+signature INTERNALIZE_SORT =
+sig
+ val internalize_sort: ctyp -> thm -> typ * thm
+ val internalize_sort_attr: typ -> attribute
+end;
+
+structure Internalize_Sort : INTERNALIZE_SORT =
+struct
+
+fun internalize_sort ctvar thm =
+ let
+ val thy = Thm.theory_of_thm thm;
+ val tvar = Thm.typ_of ctvar;
+
+ val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
+
+ fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
+ fun reduce_to_non_proper_sort (TVar (name, sort)) =
+ TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
+ | reduce_to_non_proper_sort _ = error "not supported";
+
+ val data = (map fst classes) ~~ assms;
+
+ val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
+ then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
+ |> the_default tvar;
+
+ fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
+
+ fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
+
+ val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
+ then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
+ else discharge_of_class ren_tvar class) data;
+ in
+ (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
+ end;
+
+val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
+ | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
+
+fun internalize_sort_attr tvar =
+ Thm.rule_attribute [] (fn context => fn thm =>
+ (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
+ (tvar >> internalize_sort_attr) "internalize a sort"));
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Types_To_Sets/local_typedef.ML Sun Oct 30 13:15:14 2016 +0100
@@ -0,0 +1,84 @@
+(* Title: local_typedef.ML
+ Author: Ondřej Kunčar, TU München
+
+ Implements the Local Typedef Rule and extends the logic by the rule.
+*)
+
+signature LOCAL_TYPEDEF =
+sig
+ val cancel_type_definition: thm -> thm
+ val cancel_type_definition_attr: attribute
+end;
+
+structure Local_Typedef : LOCAL_TYPEDEF =
+struct
+
+(*
+Local Typedef Rule (LT)
+
+ \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
+------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
+ \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi> sort(\<beta>)=HOL.type]
+*)
+
+(** BEGINNING OF THE CRITICAL CODE **)
+
+fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
+ (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
+ (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
+ (Abs_type, set)
+ | dest_typedef t = raise TERM ("dest_typedef", [t]);
+
+fun cancel_type_definition_cterm thm =
+ let
+ fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
+
+ val thy = Thm.theory_of_thm thm;
+ val prop = Thm.prop_of thm;
+ val hyps = Thm.hyps_of thm;
+
+ val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
+
+ val (typedef_assm, phi) = Logic.dest_implies prop
+ handle TERM _ => err "the theorem is not an implication";
+ val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
+ handle TERM _ => err ("the assumption is not of the form "
+ ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
+
+ val (repT, absT) = Term.dest_funT abs_type;
+ val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
+ val (absT_name, sorts) = Term.dest_TVar absT;
+
+ val typeS = Sign.defaultS thy;
+ val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
+ ^ quote (Syntax.string_of_sort_global thy typeS));
+
+ fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
+ fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
+ ^ quote (fst absT_name));
+ val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
+ val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
+ (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
+ val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
+
+ val not_empty_assm = HOLogic.mk_Trueprop
+ (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
+ val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
+ in
+ Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
+ end;
+
+(** END OF THE CRITICAL CODE **)
+
+val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
+
+fun cancel_type_definition thm =
+ Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
+
+val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
+ (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Types_To_Sets/unoverloading.ML Sun Oct 30 13:15:14 2016 +0100
@@ -0,0 +1,139 @@
+(* Title: unoverloading.ML
+ Author: Ondřej Kunčar, TU München
+
+ Implements the Unoverloading Rule and extends the logic by the rule.
+*)
+
+signature UNOVERLOADING =
+sig
+ val unoverload: cterm -> thm -> thm
+ val unoverload_attr: cterm -> attribute
+end;
+
+structure Unoverloading : UNOVERLOADING =
+struct
+
+(*
+Unoverloading Rule (UO)
+
+ \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
+---------------------------- [no type or constant or type class in \<phi>
+ \<turnstile> \<And>x::\<sigma>. \<phi> depends on c::\<sigma>; c::\<sigma> is undefined]
+*)
+
+(* The following functions match_args, reduction and entries_of were
+ cloned from defs.ML and theory.ML because the functions are not public.
+ Notice that these functions already belong to the critical code.
+*)
+
+(* >= *)
+fun match_args (Ts, Us) =
+ if Type.could_matches (Ts, Us) then
+ Option.map Envir.subst_type
+ (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+ else NONE;
+
+fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
+ let
+ fun reduct Us (Ts, rhs) =
+ (case match_args (Ts, Us) of
+ NONE => NONE
+ | SOME subst => SOME (map (apsnd (map subst)) rhs));
+ fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
+
+ val reds = map (`reducts) deps;
+ val deps' =
+ if forall (is_none o #1) reds then NONE
+ else SOME (fold_rev
+ (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
+ in deps' end;
+
+fun const_and_typ_entries_of thy tm =
+ let
+ val consts =
+ fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
+ val types =
+ (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
+ in
+ consts @ types
+ end;
+
+(* The actual implementation *)
+
+(** BEGINNING OF THE CRITICAL CODE **)
+
+fun fold_atyps_classes f =
+ fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
+ | T as TVar (_, S) => fold (pair T #> f) S
+ (* just to avoid a warning about incomplete patterns *)
+ | _ => raise TERM ("fold_atyps_classes", []));
+
+fun class_entries_of thy tm =
+ let
+ val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
+ in
+ map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
+ end;
+
+fun unoverload_impl cconst thm =
+ let
+ fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
+
+ val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
+ val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
+
+ val prop = Thm.prop_of thm;
+ val prop_tfrees = rev (Term.add_tfree_names prop []);
+ val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
+ ^ commas_quote prop_tfrees);
+
+ val const = Thm.term_of cconst;
+ val _ = Term.is_Const const orelse err "the parameter is is not a constant";
+ val const_tfrees = rev (Term.add_tfree_names const []);
+ val _ = null const_tfrees orelse err ("the constant contains free type variables "
+ ^ commas_quote const_tfrees);
+
+ val thy = Thm.theory_of_thm thm;
+ val defs = Theory.defs_of thy;
+
+ val const_entry = Theory.const_dep thy (Term.dest_Const const);
+
+ val Uss = Defs.specifications_of defs (fst const_entry);
+ val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
+ orelse err "the constant instance has already a specification";
+
+ val context = Defs.global_context thy;
+ val prt_entry = Pretty.string_of o Defs.pretty_entry context;
+
+ fun dep_err (c, Ts) (d, Us) =
+ err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
+ fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
+ fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
+ orelse dep_err prop_entry const_entry;
+ val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
+ val _ = forall not_depends_on_const prop_entries;
+ in
+ Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
+ end;
+
+(** END OF THE CRITICAL CODE **)
+
+val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding unoverload},
+ fn (const, thm) => unoverload_impl const thm)));
+
+fun unoverload const thm = unoverload_oracle (const, thm);
+
+fun unoverload_attr const =
+ Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
+
+val const = Args.context -- Args.term >>
+ (fn (ctxt, tm) =>
+ if not (Term.is_Const tm)
+ then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
+ else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
+ (const >> unoverload_attr) "unoverload an uninterpreted constant"));
+
+end;
\ No newline at end of file
--- a/src/HOL/ROOT Sat Oct 29 00:39:33 2016 +0200
+++ b/src/HOL/ROOT Sun Oct 30 13:15:14 2016 +0100
@@ -38,6 +38,7 @@
Predicate_Compile_Quickcheck
Prefix_Order
Rewrite
+ Types_To_Sets
(*conflicting type class instantiations*)
List_lexord
Sublist_Order