proper session HOL-Types_To_Sets;
authorwenzelm
Mon Dec 12 11:33:14 2016 +0100 (13 months ago)
changeset 6455179e9587dbcca
parent 64550 3e20defb1e3c
child 64552 7aa3c52f27aa
proper session HOL-Types_To_Sets;
NEWS;
CONTRIBUTORS;
tuned whitespace;
CONTRIBUTORS
NEWS
src/HOL/Library/Types_To_Sets.thy
src/HOL/Library/Types_To_Sets/internalize_sort.ML
src/HOL/Library/Types_To_Sets/local_typedef.ML
src/HOL/Library/Types_To_Sets/unoverloading.ML
src/HOL/ROOT
src/HOL/Types_To_Sets/Examples/Finite.thy
src/HOL/Types_To_Sets/Examples/Prerequisites.thy
src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
src/HOL/Types_To_Sets/Types_To_Sets.thy
src/HOL/Types_To_Sets/internalize_sort.ML
src/HOL/Types_To_Sets/local_typedef.ML
src/HOL/Types_To_Sets/unoverloading.ML
     1.1 --- a/CONTRIBUTORS	Thu Dec 08 15:11:20 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to Isabelle2016-1
     1.5  -------------------------------
     1.6  
     1.7 +* December 2016: Ondřej Kunčar, TUM
     1.8 +  Types_To_Sets: experimental extension of Higher-Order Logic to allow
     1.9 +  translation of types to sets.
    1.10 +
    1.11  * October 2016: Jasmin Blanchette
    1.12    Integration of Nunchaku model finder.
    1.13  
     2.1 --- a/NEWS	Thu Dec 08 15:11:20 2016 +0100
     2.2 +++ b/NEWS	Mon Dec 12 11:33:14 2016 +0100
     2.3 @@ -938,6 +938,9 @@
     2.4  * Session Old_Number_Theory has been removed, after porting remaining
     2.5  theories.
     2.6  
     2.7 +* Session HOL-Types_To_Sets provides an experimental extension of
     2.8 +Higher-Order Logic to allow translation of types to sets.
     2.9 +
    2.10  
    2.11  *** ML ***
    2.12  
     3.1 --- a/src/HOL/Library/Types_To_Sets.thy	Thu Dec 08 15:11:20 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,27 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Types_To_Sets.thy
     3.5 -    Author:     Ondřej Kunčar, TU München
     3.6 -*)
     3.7 -
     3.8 -section \<open>From Types to Sets\<close>
     3.9 -
    3.10 -text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
    3.11 -  to allow translation of types to sets as described in 
    3.12 -  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
    3.13 -  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
    3.14 -
    3.15 -theory Types_To_Sets
    3.16 -  imports Main
    3.17 -begin
    3.18 -
    3.19 -subsection \<open>Rules\<close>
    3.20 -
    3.21 -text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
    3.22 -ML_file "Types_To_Sets/local_typedef.ML"
    3.23 -
    3.24 -text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
    3.25 -ML_file "Types_To_Sets/unoverloading.ML"
    3.26 -
    3.27 -text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
    3.28 -ML_file "Types_To_Sets/internalize_sort.ML"
    3.29 -
    3.30 -end
    3.31 \ No newline at end of file
     4.1 --- a/src/HOL/Library/Types_To_Sets/internalize_sort.ML	Thu Dec 08 15:11:20 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,68 +0,0 @@
     4.4 -(*  Title:      internalize_sort.ML
     4.5 -    Author:     Ondřej Kunčar, TU München
     4.6 -
     4.7 -    Implements a derived rule (by using Thm.unconstrainT) that internalizes
     4.8 -    type class annotations.
     4.9 -*)
    4.10 -
    4.11 -
    4.12 -(*
    4.13 -                     \<phi>['a::{c_1, ..., c_n} / 'a]
    4.14 ----------------------------------------------------------------------
    4.15 -  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
    4.16 -
    4.17 -where class.c is the locale predicate associated with type class c and
    4.18 -ops are operations associated with type class c. For example:
    4.19 -If c = semigroup_add, then ops = op-, op+, 0, uminus.
    4.20 -If c = finite, then ops = TYPE('a::type).
    4.21 -*)
    4.22 -
    4.23 -signature INTERNALIZE_SORT =
    4.24 -sig
    4.25 -  val internalize_sort:  ctyp -> thm -> typ * thm
    4.26 -  val internalize_sort_attr: typ -> attribute
    4.27 -end;
    4.28 -
    4.29 -structure Internalize_Sort : INTERNALIZE_SORT =
    4.30 -struct
    4.31 -
    4.32 -fun internalize_sort ctvar thm =
    4.33 -  let
    4.34 -    val thy = Thm.theory_of_thm thm;
    4.35 -    val tvar = Thm.typ_of ctvar;
    4.36 -    
    4.37 -    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
    4.38 -
    4.39 -    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
    4.40 -    fun reduce_to_non_proper_sort (TVar (name, sort)) = 
    4.41 -        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
    4.42 -      | reduce_to_non_proper_sort _ = error "not supported";
    4.43 -
    4.44 -    val data = (map fst classes) ~~ assms;
    4.45 -    
    4.46 -    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' 
    4.47 -      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
    4.48 -      |> the_default tvar;
    4.49 -
    4.50 -    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
    4.51 -
    4.52 -    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
    4.53 -
    4.54 -    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' 
    4.55 -      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
    4.56 -      else discharge_of_class ren_tvar class) data;
    4.57 -  in
    4.58 -    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
    4.59 -  end;
    4.60 -
    4.61 -val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v 
    4.62 -  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
    4.63 -
    4.64 -fun internalize_sort_attr tvar = 
    4.65 -  Thm.rule_attribute [] (fn context => fn thm => 
    4.66 -    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
    4.67 -
    4.68 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort} 
    4.69 -  (tvar >> internalize_sort_attr) "internalize a sort"));
    4.70 -
    4.71 -end;
    4.72 \ No newline at end of file
     5.1 --- a/src/HOL/Library/Types_To_Sets/local_typedef.ML	Thu Dec 08 15:11:20 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,84 +0,0 @@
     5.4 -(*  Title:      local_typedef.ML
     5.5 -    Author:     Ondřej Kunčar, TU München
     5.6 -
     5.7 -    Implements the Local Typedef Rule and extends the logic by the rule.
     5.8 -*)
     5.9 -
    5.10 -signature LOCAL_TYPEDEF =
    5.11 -sig
    5.12 -  val cancel_type_definition: thm -> thm
    5.13 -  val cancel_type_definition_attr: attribute
    5.14 -end;
    5.15 -
    5.16 -structure Local_Typedef : LOCAL_TYPEDEF =
    5.17 -struct
    5.18 -
    5.19 -(*
    5.20 -Local Typedef Rule (LT)
    5.21 -
    5.22 -  \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
    5.23 -------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
    5.24 -                       \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi>                        sort(\<beta>)=HOL.type]
    5.25 -*)
    5.26 -
    5.27 -(** BEGINNING OF THE CRITICAL CODE **)
    5.28 -
    5.29 -fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _, 
    5.30 -      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,  
    5.31 -      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) = 
    5.32 -    (Abs_type, set)
    5.33 -   | dest_typedef t = raise TERM ("dest_typedef", [t]);
    5.34 -  
    5.35 -fun cancel_type_definition_cterm thm =
    5.36 -  let
    5.37 -    fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
    5.38 -
    5.39 -    val thy = Thm.theory_of_thm thm;
    5.40 -    val prop = Thm.prop_of thm;
    5.41 -    val hyps = Thm.hyps_of thm;
    5.42 -
    5.43 -    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
    5.44 -
    5.45 -    val (typedef_assm, phi) = Logic.dest_implies prop
    5.46 -      handle TERM _ => err "the theorem is not an implication";
    5.47 -    val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
    5.48 -      handle TERM _ => err ("the assumption is not of the form " 
    5.49 -        ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
    5.50 -
    5.51 -    val (repT, absT) = Term.dest_funT abs_type;
    5.52 -    val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
    5.53 -    val (absT_name, sorts) = Term.dest_TVar absT;
    5.54 -    
    5.55 -    val typeS = Sign.defaultS thy;
    5.56 -    val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort " 
    5.57 -      ^ quote (Syntax.string_of_sort_global thy typeS));
    5.58 -     
    5.59 -    fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
    5.60 -    fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type " 
    5.61 -      ^ quote (fst absT_name));
    5.62 -    val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
    5.63 -    val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
    5.64 -    (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
    5.65 -    val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
    5.66 -
    5.67 -    val not_empty_assm = HOLogic.mk_Trueprop
    5.68 -      (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
    5.69 -    val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
    5.70 -  in
    5.71 -    Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
    5.72 -  end;
    5.73 -
    5.74 -(** END OF THE CRITICAL CODE **)
    5.75 -
    5.76 -val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
    5.77 -  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
    5.78 -
    5.79 -fun cancel_type_definition thm =  
    5.80 -  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
    5.81 -
    5.82 -val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
    5.83 -
    5.84 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition} 
    5.85 -  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
    5.86 -
    5.87 -end;
    5.88 \ No newline at end of file
     6.1 --- a/src/HOL/Library/Types_To_Sets/unoverloading.ML	Thu Dec 08 15:11:20 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,139 +0,0 @@
     6.4 -(*  Title:      unoverloading.ML
     6.5 -    Author:     Ondřej Kunčar, TU München
     6.6 -
     6.7 -    Implements the Unoverloading Rule and extends the logic by the rule.
     6.8 -*)
     6.9 -
    6.10 -signature UNOVERLOADING =
    6.11 -sig
    6.12 -  val unoverload: cterm -> thm -> thm
    6.13 -  val unoverload_attr: cterm -> attribute
    6.14 -end;
    6.15 -
    6.16 -structure Unoverloading : UNOVERLOADING =
    6.17 -struct
    6.18 -
    6.19 -(*
    6.20 -Unoverloading Rule (UO)
    6.21 -
    6.22 -      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
    6.23 ----------------------------- [no type or constant or type class in \<phi> 
    6.24 -        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
    6.25 -*)
    6.26 -
    6.27 -(* The following functions match_args, reduction and entries_of were 
    6.28 -   cloned from defs.ML and theory.ML because the functions are not public.
    6.29 -   Notice that these functions already belong to the critical code.
    6.30 -*)
    6.31 -
    6.32 -(* >= *)
    6.33 -fun match_args (Ts, Us) =
    6.34 -  if Type.could_matches (Ts, Us) then
    6.35 -    Option.map Envir.subst_type
    6.36 -      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
    6.37 -  else NONE;
    6.38 -
    6.39 -fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
    6.40 -  let
    6.41 -    fun reduct Us (Ts, rhs) =
    6.42 -      (case match_args (Ts, Us) of
    6.43 -        NONE => NONE
    6.44 -      | SOME subst => SOME (map (apsnd (map subst)) rhs));
    6.45 -    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
    6.46 -
    6.47 -    val reds = map (`reducts) deps;
    6.48 -    val deps' =
    6.49 -      if forall (is_none o #1) reds then NONE
    6.50 -      else SOME (fold_rev
    6.51 -        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
    6.52 -  in deps' end;
    6.53 -
    6.54 -fun const_and_typ_entries_of thy tm =
    6.55 - let
    6.56 -   val consts =
    6.57 -     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
    6.58 -   val types =
    6.59 -     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
    6.60 - in
    6.61 -   consts @ types
    6.62 - end;
    6.63 -
    6.64 -(* The actual implementation *)
    6.65 -
    6.66 -(** BEGINNING OF THE CRITICAL CODE **)
    6.67 -
    6.68 -fun fold_atyps_classes f =
    6.69 -  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S 
    6.70 -    | T as TVar (_, S) => fold (pair T #> f) S 
    6.71 -    (* just to avoid a warning about incomplete patterns *)
    6.72 -    | _ => raise TERM ("fold_atyps_classes", [])); 
    6.73 -
    6.74 -fun class_entries_of thy tm =
    6.75 -  let
    6.76 -    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
    6.77 -  in
    6.78 -    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
    6.79 -  end;
    6.80 -
    6.81 -fun unoverload_impl cconst thm =
    6.82 -  let
    6.83 -    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
    6.84 -
    6.85 -    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
    6.86 -    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
    6.87 -    
    6.88 -    val prop = Thm.prop_of thm;
    6.89 -    val prop_tfrees = rev (Term.add_tfree_names prop []);
    6.90 -    val _ = null prop_tfrees orelse err ("the theorem contains free type variables " 
    6.91 -      ^ commas_quote prop_tfrees);
    6.92 -
    6.93 -    val const = Thm.term_of cconst;
    6.94 -    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
    6.95 -    val const_tfrees = rev (Term.add_tfree_names const []);
    6.96 -    val _ = null const_tfrees orelse err ("the constant contains free type variables " 
    6.97 -      ^ commas_quote const_tfrees);
    6.98 -
    6.99 -    val thy = Thm.theory_of_thm thm;
   6.100 -    val defs = Theory.defs_of thy;
   6.101 -
   6.102 -    val const_entry = Theory.const_dep thy (Term.dest_Const const);
   6.103 -
   6.104 -    val Uss = Defs.specifications_of defs (fst const_entry);
   6.105 -    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss 
   6.106 -      orelse err "the constant instance has already a specification";
   6.107 -
   6.108 -    val context = Defs.global_context thy;
   6.109 -    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
   6.110 -    
   6.111 -    fun dep_err (c, Ts) (d, Us) =
   6.112 -      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
   6.113 -    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
   6.114 -    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
   6.115 -      orelse dep_err prop_entry const_entry;
   6.116 -    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
   6.117 -    val _ = forall not_depends_on_const prop_entries;
   6.118 -  in
   6.119 -    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
   6.120 -  end;
   6.121 -
   6.122 -(** END OF THE CRITICAL CODE **)
   6.123 -
   6.124 -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
   6.125 -  (Thm.add_oracle (@{binding unoverload},
   6.126 -  fn (const, thm) => unoverload_impl const  thm)));
   6.127 -
   6.128 -fun unoverload const thm = unoverload_oracle (const, thm);
   6.129 -
   6.130 -fun unoverload_attr const = 
   6.131 -  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
   6.132 -
   6.133 -val const = Args.context -- Args.term  >>
   6.134 -  (fn (ctxt, tm) => 
   6.135 -    if not (Term.is_Const tm) 
   6.136 -    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
   6.137 -    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
   6.138 -
   6.139 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload} 
   6.140 -  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
   6.141 -
   6.142 -end;
   6.143 \ No newline at end of file
     7.1 --- a/src/HOL/ROOT	Thu Dec 08 15:11:20 2016 +0100
     7.2 +++ b/src/HOL/ROOT	Mon Dec 12 11:33:14 2016 +0100
     7.3 @@ -38,7 +38,6 @@
     7.4      Predicate_Compile_Quickcheck
     7.5      Prefix_Order
     7.6      Rewrite
     7.7 -    Types_To_Sets
     7.8      (*conflicting type class instantiations*)
     7.9      List_lexord
    7.10      Sublist_Order
    7.11 @@ -1021,6 +1020,17 @@
    7.12    theories [condition = ISABELLE_SWIPL, quick_and_dirty]
    7.13      Reg_Exp_Example
    7.14  
    7.15 +session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
    7.16 +  description {*
    7.17 +    Experimental extension of Higher-Order Logic to allow translation of types to sets.
    7.18 +  *}
    7.19 +  options [document = false]
    7.20 +  theories
    7.21 +    Types_To_Sets
    7.22 +    "Examples/Prerequisites"
    7.23 +    "Examples/Finite"
    7.24 +    "Examples/T2_Spaces"
    7.25 +
    7.26  session HOLCF (main timing) in HOLCF = HOL +
    7.27    description {*
    7.28      Author:     Franz Regensburger
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Types_To_Sets/Examples/Finite.thy	Mon Dec 12 11:33:14 2016 +0100
     8.3 @@ -0,0 +1,90 @@
     8.4 +(*  Title:      HOL/Types_To_Sets/Examples/Finite.thy
     8.5 +    Author:     Ondřej Kunčar, TU München
     8.6 +*)
     8.7 +
     8.8 +theory Finite
     8.9 +  imports "../Types_To_Sets" Prerequisites
    8.10 +begin
    8.11 +
    8.12 +section \<open>The Type-Based Theorem\<close>
    8.13 +
    8.14 +text\<open>This example file shows how we perform the relativization in presence of axiomatic
    8.15 +  type classes: we internalize them.\<close>
    8.16 +
    8.17 +definition injective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    8.18 +  where "injective f \<equiv> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
    8.19 +
    8.20 +text\<open>We want to relativize the following type-based theorem using the type class finite.\<close>
    8.21 +
    8.22 +lemma type_based: "\<exists>f :: 'a::finite \<Rightarrow> nat. injective f"
    8.23 +  unfolding injective_def
    8.24 +  using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto
    8.25 +
    8.26 +section \<open>Definitions and Setup for The Relativization\<close>
    8.27 +
    8.28 +text\<open>We have to define what being injective on a set means.\<close>
    8.29 +
    8.30 +definition injective_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    8.31 +  where "injective_on A f \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. f x = f y \<longrightarrow> x = y"
    8.32 +
    8.33 +text\<open>The predicate injective_on is the relativization of the predicate injective.\<close>
    8.34 +
    8.35 +lemma injective_transfer[transfer_rule]:
    8.36 +  includes lifting_syntax
    8.37 +  assumes [transfer_rule]: "right_total T"
    8.38 +  assumes [transfer_rule]: "bi_unique T"
    8.39 +  shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective"
    8.40 +  unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
    8.41 +
    8.42 +text\<open>Similarly, we define the relativization of the internalization
    8.43 +     of the type class finite, class.finite\<close>
    8.44 +
    8.45 +definition finite_on :: "'a set => bool" where "finite_on A = finite A"
    8.46 +
    8.47 +lemma class_finite_transfer[transfer_rule]:
    8.48 +  assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
    8.49 +  assumes [transfer_rule]: "bi_unique T"
    8.50 +  shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
    8.51 +  unfolding finite_on_def class.finite_def by transfer_prover
    8.52 +
    8.53 +text\<open>The aforementioned development can be automated. The main part is already automated
    8.54 +     by the transfer_prover.\<close>
    8.55 +
    8.56 +section \<open>The Relativization to The Set-Based Theorem\<close>
    8.57 +
    8.58 +lemmas internalized = type_based[internalize_sort "'a::finite"]
    8.59 +text\<open>We internalized the type class finite and thus reduced the task to the
    8.60 +  original relativization algorithm.\<close>
    8.61 +thm internalized
    8.62 +
    8.63 +text\<open>This is the set-based variant.\<close>
    8.64 +
    8.65 +lemma set_based:
    8.66 +  assumes "(A::'a set) \<noteq> {}"
    8.67 +  shows "finite_on A \<longrightarrow> (\<exists>f :: 'a \<Rightarrow> nat. injective_on A f)"
    8.68 +proof -
    8.69 +  {
    8.70 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
    8.71 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
    8.72 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
    8.73 +      by auto
    8.74 +
    8.75 +    text\<open>Setup for the Transfer tool.\<close>
    8.76 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
    8.77 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
    8.78 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
    8.79 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
    8.80 +
    8.81 +    have ?thesis
    8.82 +      text\<open>Relativization by the Transfer tool.\<close>
    8.83 +      using internalized[where 'a = 'b, untransferred, simplified]
    8.84 +      by blast
    8.85 +  } note * = this[cancel_type_definition, OF assms] text\<open>We removed the definition of 'b.\<close>
    8.86 +
    8.87 +  show ?thesis by (rule *)
    8.88 +qed
    8.89 +
    8.90 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
    8.91 +thm type_based set_based
    8.92 +
    8.93 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Mon Dec 12 11:33:14 2016 +0100
     9.3 @@ -0,0 +1,25 @@
     9.4 +(*  Title:      HOL/Types_To_Sets/Examples/Prerequisites.thy
     9.5 +    Author:     Ondřej Kunčar, TU München
     9.6 +*)
     9.7 +
     9.8 +theory Prerequisites
     9.9 +  imports Main
    9.10 +begin
    9.11 +
    9.12 +context
    9.13 +  fixes Rep Abs A T
    9.14 +  assumes type: "type_definition Rep Abs A"
    9.15 +  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
    9.16 +begin
    9.17 +
    9.18 +lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
    9.19 +proof -
    9.20 +  interpret type_definition Rep Abs A by(rule type)
    9.21 +  show ?thesis
    9.22 +    unfolding Domainp_iff[abs_def] T_def fun_eq_iff
    9.23 +    by (metis Abs_inverse Rep)
    9.24 +qed
    9.25 +
    9.26 +end
    9.27 +
    9.28 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Mon Dec 12 11:33:14 2016 +0100
    10.3 @@ -0,0 +1,162 @@
    10.4 +(*  Title:      HOL/Types_To_Sets/Examples/T2_Spaces.thy
    10.5 +    Author:     Ondřej Kunčar, TU München
    10.6 +*)
    10.7 +
    10.8 +theory T2_Spaces
    10.9 +  imports Complex_Main "../Types_To_Sets" Prerequisites
   10.10 +begin
   10.11 +
   10.12 +section \<open>The Type-Based Theorem\<close>
   10.13 +
   10.14 +text\<open>We relativize a theorem that contains a type class with an associated (overloaded) operation.
   10.15 +     The key technique is to compile out the overloaded operation by the dictionary construction
   10.16 +     using the Unoverloading rule.\<close>
   10.17 +
   10.18 +text\<open>This is the type-based statement that we want to relativize.\<close>
   10.19 +thm compact_imp_closed
   10.20 +text\<open>The type is class a T2 typological space.\<close>
   10.21 +typ "'a :: t2_space"
   10.22 +text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close>
   10.23 +term "open"
   10.24 +
   10.25 +section \<open>Definitions and Setup for The Relativization\<close>
   10.26 +
   10.27 +text\<open>We gradually define relativization of topological spaces, t2 spaces, compact and closed
   10.28 +     predicates and prove that they are indeed the relativization of the original predicates.\<close>
   10.29 +
   10.30 +definition topological_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
   10.31 +  where "topological_space_on_with A \<equiv> \<lambda>open. open A \<and>
   10.32 +    (\<forall>S \<subseteq> A. \<forall>T \<subseteq> A. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T))
   10.33 +    \<and> (\<forall>K \<subseteq> Pow A. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union>K))"
   10.34 +
   10.35 +lemma topological_space_transfer[transfer_rule]:
   10.36 +  includes lifting_syntax
   10.37 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   10.38 +  shows "((rel_set T ===> op=) ===> op=) (topological_space_on_with (Collect (Domainp T)))
   10.39 +    class.topological_space"
   10.40 +  unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
   10.41 +  apply transfer_prover_start
   10.42 +  apply transfer_step+
   10.43 +  unfolding Pow_def Ball_Collect[symmetric]
   10.44 +  by blast
   10.45 +
   10.46 +definition t2_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
   10.47 +  where "t2_space_on_with A \<equiv> \<lambda>open. topological_space_on_with A open \<and>
   10.48 +  (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> (\<exists>U\<subseteq>A. \<exists>V\<subseteq>A. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}))"
   10.49 +
   10.50 +lemma t2_space_transfer[transfer_rule]:
   10.51 +  includes lifting_syntax
   10.52 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   10.53 +  shows "((rel_set T ===> op=) ===> op=) (t2_space_on_with (Collect (Domainp T))) class.t2_space"
   10.54 +  unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def]
   10.55 +    class.t2_space_axioms_def[abs_def]
   10.56 +  apply transfer_prover_start
   10.57 +  apply transfer_step+
   10.58 +  unfolding Ball_Collect[symmetric]
   10.59 +  by blast
   10.60 +
   10.61 +definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   10.62 +  where "closed_with \<equiv> \<lambda>open S. open (- S)"
   10.63 +
   10.64 +lemma closed_closed_with: "closed s = closed_with open s"
   10.65 +  unfolding closed_with_def closed_def[abs_def] ..
   10.66 +
   10.67 +definition closed_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   10.68 +  where "closed_on_with A \<equiv> \<lambda>open S. open (-S \<inter> A)"
   10.69 +
   10.70 +lemma closed_with_transfer[transfer_rule]:
   10.71 +  includes lifting_syntax
   10.72 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   10.73 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (closed_on_with (Collect (Domainp T)))
   10.74 +    closed_with"
   10.75 +  unfolding closed_with_def closed_on_with_def by transfer_prover
   10.76 +
   10.77 +definition compact_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   10.78 +  where "compact_with \<equiv> \<lambda>open S. (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
   10.79 +
   10.80 +lemma compact_compact_with: "compact s = compact_with open s"
   10.81 +  unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
   10.82 +
   10.83 +definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   10.84 +  where "compact_on_with A \<equiv> \<lambda>open S. (\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
   10.85 +    (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
   10.86 +
   10.87 +lemma compact_on_with_subset_trans: "(\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
   10.88 +  (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)) =
   10.89 +  ((\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>Pow A. D\<subseteq>C \<and> finite D \<and> S \<subseteq> \<Union>D)))"
   10.90 +  by (meson subset_trans)
   10.91 +
   10.92 +lemma compact_with_transfer[transfer_rule]:
   10.93 +  includes lifting_syntax
   10.94 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   10.95 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (compact_on_with (Collect (Domainp T)))
   10.96 +    compact_with"
   10.97 +  unfolding compact_with_def compact_on_with_def
   10.98 +  apply transfer_prover_start
   10.99 +  apply transfer_step+
  10.100 +  unfolding compact_on_with_subset_trans
  10.101 +  unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq
  10.102 +  by blast
  10.103 +
  10.104 +setup \<open>Sign.add_const_constraint
  10.105 +  (@{const_name "open"}, SOME @{typ "'a set \<Rightarrow> bool"})\<close>
  10.106 +
  10.107 +text\<open>The aforementioned development can be automated. The main part is already automated
  10.108 +     by the transfer_prover.\<close>
  10.109 +
  10.110 +section \<open>The Relativization to The Set-Based Theorem\<close>
  10.111 +
  10.112 +text\<open>The first step of the dictionary construction.\<close>
  10.113 +lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
  10.114 +thm dictionary_first_step
  10.115 +
  10.116 +text\<open>Internalization of the type class t2_space.\<close>
  10.117 +lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
  10.118 +thm internalized_sort
  10.119 +
  10.120 +text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close>
  10.121 +lemmas dictionary_second_step =  internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"]
  10.122 +text\<open>The theorem with internalized type classes and compiled out operations is the starting point
  10.123 +     for the original relativization algorithm.\<close>
  10.124 +thm dictionary_second_step
  10.125 +
  10.126 +
  10.127 +text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
  10.128 +lemma compact_imp_closed_set_based:
  10.129 +  assumes "(A::'a set) \<noteq> {}"
  10.130 +  shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow>
  10.131 +    closed_on_with A open S)"
  10.132 +proof -
  10.133 +  {
  10.134 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
  10.135 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
  10.136 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
  10.137 +      by auto
  10.138 +
  10.139 +    text\<open>Setup for the Transfer tool.\<close>
  10.140 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
  10.141 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
  10.142 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
  10.143 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
  10.144 +
  10.145 +    have ?thesis
  10.146 +      text\<open>Relativization by the Transfer tool.\<close>
  10.147 +      using dictionary_second_step[where 'a = 'b, untransferred, simplified]
  10.148 +      by blast
  10.149 +
  10.150 +  } note * = this[cancel_type_definition, OF assms]
  10.151 +
  10.152 +  show ?thesis by (rule *)
  10.153 +qed
  10.154 +
  10.155 +setup \<open>Sign.add_const_constraint
  10.156 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
  10.157 +
  10.158 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
  10.159 +thm compact_imp_closed compact_imp_closed_set_based
  10.160 +
  10.161 +declare [[show_sorts]]
  10.162 +text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close>
  10.163 +thm compact_imp_closed compact_imp_closed_set_based
  10.164 +
  10.165 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Mon Dec 12 11:33:14 2016 +0100
    11.3 @@ -0,0 +1,27 @@
    11.4 +(*  Title:      HOL/Types_To_Sets/Types_To_Sets.thy
    11.5 +    Author:     Ondřej Kunčar, TU München
    11.6 +*)
    11.7 +
    11.8 +section \<open>From Types to Sets\<close>
    11.9 +
   11.10 +text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
   11.11 +  to allow translation of types to sets as described in
   11.12 +  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
   11.13 +  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
   11.14 +
   11.15 +theory Types_To_Sets
   11.16 +  imports Main
   11.17 +begin
   11.18 +
   11.19 +subsection \<open>Rules\<close>
   11.20 +
   11.21 +text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
   11.22 +ML_file "local_typedef.ML"
   11.23 +
   11.24 +text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
   11.25 +ML_file "unoverloading.ML"
   11.26 +
   11.27 +text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
   11.28 +ML_file "internalize_sort.ML"
   11.29 +
   11.30 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Dec 12 11:33:14 2016 +0100
    12.3 @@ -0,0 +1,68 @@
    12.4 +(*  Title:      HOL/Types_To_Sets/internalize_sort.ML
    12.5 +    Author:     Ondřej Kunčar, TU München
    12.6 +
    12.7 +A derived rule (by using Thm.unconstrainT) that internalizes
    12.8 +type class annotations.
    12.9 +*)
   12.10 +
   12.11 +
   12.12 +(*
   12.13 +                     \<phi>['a::{c_1, ..., c_n} / 'a]
   12.14 +---------------------------------------------------------------------
   12.15 +  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
   12.16 +
   12.17 +where class.c is the locale predicate associated with type class c and
   12.18 +ops are operations associated with type class c. For example:
   12.19 +If c = semigroup_add, then ops = op-, op+, 0, uminus.
   12.20 +If c = finite, then ops = TYPE('a::type).
   12.21 +*)
   12.22 +
   12.23 +signature INTERNALIZE_SORT =
   12.24 +sig
   12.25 +  val internalize_sort:  ctyp -> thm -> typ * thm
   12.26 +  val internalize_sort_attr: typ -> attribute
   12.27 +end;
   12.28 +
   12.29 +structure Internalize_Sort : INTERNALIZE_SORT =
   12.30 +struct
   12.31 +
   12.32 +fun internalize_sort ctvar thm =
   12.33 +  let
   12.34 +    val thy = Thm.theory_of_thm thm;
   12.35 +    val tvar = Thm.typ_of ctvar;
   12.36 +
   12.37 +    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
   12.38 +
   12.39 +    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
   12.40 +    fun reduce_to_non_proper_sort (TVar (name, sort)) =
   12.41 +        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
   12.42 +      | reduce_to_non_proper_sort _ = error "not supported";
   12.43 +
   12.44 +    val data = (map fst classes) ~~ assms;
   12.45 +
   12.46 +    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
   12.47 +      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
   12.48 +      |> the_default tvar;
   12.49 +
   12.50 +    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
   12.51 +
   12.52 +    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
   12.53 +
   12.54 +    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
   12.55 +      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
   12.56 +      else discharge_of_class ren_tvar class) data;
   12.57 +  in
   12.58 +    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
   12.59 +  end;
   12.60 +
   12.61 +val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
   12.62 +  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
   12.63 +
   12.64 +fun internalize_sort_attr tvar =
   12.65 +  Thm.rule_attribute [] (fn context => fn thm =>
   12.66 +    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
   12.67 +
   12.68 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
   12.69 +  (tvar >> internalize_sort_attr) "internalize a sort"));
   12.70 +
   12.71 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Types_To_Sets/local_typedef.ML	Mon Dec 12 11:33:14 2016 +0100
    13.3 @@ -0,0 +1,84 @@
    13.4 +(*  Title:      HOL/Types_To_Sets/local_typedef.ML
    13.5 +    Author:     Ondřej Kunčar, TU München
    13.6 +
    13.7 +The Local Typedef Rule (extension of the logic).
    13.8 +*)
    13.9 +
   13.10 +signature LOCAL_TYPEDEF =
   13.11 +sig
   13.12 +  val cancel_type_definition: thm -> thm
   13.13 +  val cancel_type_definition_attr: attribute
   13.14 +end;
   13.15 +
   13.16 +structure Local_Typedef : LOCAL_TYPEDEF =
   13.17 +struct
   13.18 +
   13.19 +(*
   13.20 +Local Typedef Rule (LT)
   13.21 +
   13.22 +  \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
   13.23 +------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
   13.24 +                       \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi>                        sort(\<beta>)=HOL.type]
   13.25 +*)
   13.26 +
   13.27 +(** BEGINNING OF THE CRITICAL CODE **)
   13.28 +
   13.29 +fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
   13.30 +      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
   13.31 +      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
   13.32 +    (Abs_type, set)
   13.33 +   | dest_typedef t = raise TERM ("dest_typedef", [t]);
   13.34 +
   13.35 +fun cancel_type_definition_cterm thm =
   13.36 +  let
   13.37 +    fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
   13.38 +
   13.39 +    val thy = Thm.theory_of_thm thm;
   13.40 +    val prop = Thm.prop_of thm;
   13.41 +    val hyps = Thm.hyps_of thm;
   13.42 +
   13.43 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
   13.44 +
   13.45 +    val (typedef_assm, phi) = Logic.dest_implies prop
   13.46 +      handle TERM _ => err "the theorem is not an implication";
   13.47 +    val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
   13.48 +      handle TERM _ => err ("the assumption is not of the form "
   13.49 +        ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
   13.50 +
   13.51 +    val (repT, absT) = Term.dest_funT abs_type;
   13.52 +    val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
   13.53 +    val (absT_name, sorts) = Term.dest_TVar absT;
   13.54 +
   13.55 +    val typeS = Sign.defaultS thy;
   13.56 +    val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
   13.57 +      ^ quote (Syntax.string_of_sort_global thy typeS));
   13.58 +
   13.59 +    fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
   13.60 +    fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
   13.61 +      ^ quote (fst absT_name));
   13.62 +    val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
   13.63 +    val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
   13.64 +    (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
   13.65 +    val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
   13.66 +
   13.67 +    val not_empty_assm = HOLogic.mk_Trueprop
   13.68 +      (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
   13.69 +    val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
   13.70 +  in
   13.71 +    Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
   13.72 +  end;
   13.73 +
   13.74 +(** END OF THE CRITICAL CODE **)
   13.75 +
   13.76 +val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
   13.77 +  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
   13.78 +
   13.79 +fun cancel_type_definition thm =
   13.80 +  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
   13.81 +
   13.82 +val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
   13.83 +
   13.84 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
   13.85 +  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
   13.86 +
   13.87 +end;
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Types_To_Sets/unoverloading.ML	Mon Dec 12 11:33:14 2016 +0100
    14.3 @@ -0,0 +1,140 @@
    14.4 +(*  Title:      HOL/Types_To_Sets/unoverloading.ML
    14.5 +    Author:     Ondřej Kunčar, TU München
    14.6 +
    14.7 +The Unoverloading Rule (extension of the logic).
    14.8 +*)
    14.9 +
   14.10 +signature UNOVERLOADING =
   14.11 +sig
   14.12 +  val unoverload: cterm -> thm -> thm
   14.13 +  val unoverload_attr: cterm -> attribute
   14.14 +end;
   14.15 +
   14.16 +structure Unoverloading : UNOVERLOADING =
   14.17 +struct
   14.18 +
   14.19 +(*
   14.20 +Unoverloading Rule (UO)
   14.21 +
   14.22 +      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
   14.23 +---------------------------- [no type or constant or type class in \<phi>
   14.24 +        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
   14.25 +*)
   14.26 +
   14.27 +(* The following functions match_args, reduction and entries_of were
   14.28 +   cloned from defs.ML and theory.ML because the functions are not public.
   14.29 +   Notice that these functions already belong to the critical code.
   14.30 +*)
   14.31 +
   14.32 +(* >= *)
   14.33 +fun match_args (Ts, Us) =
   14.34 +  if Type.could_matches (Ts, Us) then
   14.35 +    Option.map Envir.subst_type
   14.36 +      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
   14.37 +  else NONE;
   14.38 +
   14.39 +fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
   14.40 +  let
   14.41 +    fun reduct Us (Ts, rhs) =
   14.42 +      (case match_args (Ts, Us) of
   14.43 +        NONE => NONE
   14.44 +      | SOME subst => SOME (map (apsnd (map subst)) rhs));
   14.45 +    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
   14.46 +
   14.47 +    val reds = map (`reducts) deps;
   14.48 +    val deps' =
   14.49 +      if forall (is_none o #1) reds then NONE
   14.50 +      else SOME (fold_rev
   14.51 +        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   14.52 +  in deps' end;
   14.53 +
   14.54 +fun const_and_typ_entries_of thy tm =
   14.55 + let
   14.56 +   val consts =
   14.57 +     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
   14.58 +   val types =
   14.59 +     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
   14.60 + in
   14.61 +   consts @ types
   14.62 + end;
   14.63 +
   14.64 +
   14.65 +(* The actual implementation *)
   14.66 +
   14.67 +(** BEGINNING OF THE CRITICAL CODE **)
   14.68 +
   14.69 +fun fold_atyps_classes f =
   14.70 +  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
   14.71 +    | T as TVar (_, S) => fold (pair T #> f) S
   14.72 +    (* just to avoid a warning about incomplete patterns *)
   14.73 +    | _ => raise TERM ("fold_atyps_classes", []));
   14.74 +
   14.75 +fun class_entries_of thy tm =
   14.76 +  let
   14.77 +    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
   14.78 +  in
   14.79 +    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
   14.80 +  end;
   14.81 +
   14.82 +fun unoverload_impl cconst thm =
   14.83 +  let
   14.84 +    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
   14.85 +
   14.86 +    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
   14.87 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
   14.88 +
   14.89 +    val prop = Thm.prop_of thm;
   14.90 +    val prop_tfrees = rev (Term.add_tfree_names prop []);
   14.91 +    val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
   14.92 +      ^ commas_quote prop_tfrees);
   14.93 +
   14.94 +    val const = Thm.term_of cconst;
   14.95 +    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
   14.96 +    val const_tfrees = rev (Term.add_tfree_names const []);
   14.97 +    val _ = null const_tfrees orelse err ("the constant contains free type variables "
   14.98 +      ^ commas_quote const_tfrees);
   14.99 +
  14.100 +    val thy = Thm.theory_of_thm thm;
  14.101 +    val defs = Theory.defs_of thy;
  14.102 +
  14.103 +    val const_entry = Theory.const_dep thy (Term.dest_Const const);
  14.104 +
  14.105 +    val Uss = Defs.specifications_of defs (fst const_entry);
  14.106 +    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
  14.107 +      orelse err "the constant instance has already a specification";
  14.108 +
  14.109 +    val context = Defs.global_context thy;
  14.110 +    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
  14.111 +
  14.112 +    fun dep_err (c, Ts) (d, Us) =
  14.113 +      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
  14.114 +    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
  14.115 +    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
  14.116 +      orelse dep_err prop_entry const_entry;
  14.117 +    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
  14.118 +    val _ = forall not_depends_on_const prop_entries;
  14.119 +  in
  14.120 +    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
  14.121 +  end;
  14.122 +
  14.123 +(** END OF THE CRITICAL CODE **)
  14.124 +
  14.125 +val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
  14.126 +  (Thm.add_oracle (@{binding unoverload},
  14.127 +  fn (const, thm) => unoverload_impl const  thm)));
  14.128 +
  14.129 +fun unoverload const thm = unoverload_oracle (const, thm);
  14.130 +
  14.131 +fun unoverload_attr const =
  14.132 +  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
  14.133 +
  14.134 +val const = Args.context -- Args.term  >>
  14.135 +  (fn (ctxt, tm) =>
  14.136 +    if not (Term.is_Const tm)
  14.137 +    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
  14.138 +    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
  14.139 +
  14.140 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
  14.141 +  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
  14.142 +
  14.143 +end;