# HG changeset patch # User kuncar # Date 1477829714 -3600 # Node ID ae53f4d901a36c7a7eadb5ddebebd6ea11a968c1 # Parent 1d85ac286c72237f245dcc2b2ba8a2bf7e858d41 types to sets: initial commit diff -r 1d85ac286c72 -r ae53f4d901a3 src/HOL/Library/Types_To_Sets.thy --- /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 \From Types to Sets\ + +text \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.\ + +theory Types_To_Sets + imports Main +begin + +subsection \Rules\ + +text\The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\ +ML_file "Types_To_Sets/local_typedef.ML" + +text\The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\ +ML_file "Types_To_Sets/unoverloading.ML" + +text\The following file implements a derived rule that internalizes type class annotations.\ +ML_file "Types_To_Sets/internalize_sort.ML" + +end \ No newline at end of file diff -r 1d85ac286c72 -r ae53f4d901a3 src/HOL/Library/Types_To_Sets/internalize_sort.ML --- /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. +*) + + +(* + \['a::{c_1, ..., c_n} / 'a] +--------------------------------------------------------------------- + class.c_1 ops_1 \ ... \ class.c_n ops_n \ \['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 diff -r 1d85ac286c72 -r ae53f4d901a3 src/HOL/Library/Types_To_Sets/local_typedef.ML --- /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) + + \ \ (\(Rep::\ \ \) Abs. type_definition Rep Abs A) \ \ +------------------------------------------------------------- [\ not in \, \, A; + \ \ A \ \ \ \ sort(\)=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 "\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 diff -r 1d85ac286c72 -r ae53f4d901a3 src/HOL/Library/Types_To_Sets/unoverloading.ML --- /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) + + \ \[c::\ / x::\] +---------------------------- [no type or constant or type class in \ + \ \x::\. \ depends on c::\; c::\ 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 diff -r 1d85ac286c72 -r ae53f4d901a3 src/HOL/ROOT --- 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