merged
authorwenzelm
Mon Dec 12 17:40:06 2016 +0100 (23 months ago)
changeset 64555628b271c5b8b
parent 64546 134ae7da2ccf
parent 64554 5d2cef77373c
child 64556 851ae0e7b09c
merged
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
     1.1 --- a/.hgtags	Sat Dec 10 17:22:47 2016 +0100
     1.2 +++ b/.hgtags	Mon Dec 12 17:40:06 2016 +0100
     1.3 @@ -32,8 +32,4 @@
     1.4  8f4a332500e41bb67efc3e141608829473606a72 Isabelle2014
     1.5  5ae2a2e74c93eafeb00b1ddeef0404256745ebba Isabelle2015
     1.6  d3996d5873ddcf1115ec8d3d511a0bb5dbd1cfc4 Isabelle2016
     1.7 -666c7475f4f7e9ba46c59170026230787c504ca7 Isabelle2016-1-RC0
     1.8 -9ee2480d10b7404683aa7f4c3a30d44cbb6a21b9 Isabelle2016-1-RC1
     1.9 -2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4 Isabelle2016-1-RC2
    1.10 -51be997d0698583bf2d3f5a99f37381a146d3a6c Isabelle2016-1-RC3
    1.11 -49708cffb98dc6ced89f66b10662e6af2808bebd Isabelle2016-1-RC4
    1.12 +7aa3c52f27aade2cada22206cf0477b30a25f781 Isabelle2016-1
     2.1 --- a/ANNOUNCE	Sat Dec 10 17:22:47 2016 +0100
     2.2 +++ b/ANNOUNCE	Mon Dec 12 17:40:06 2016 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  Isabelle2016-1 is now available.
     2.5  
     2.6  This version introduces significant changes over Isabelle2016: see the NEWS
     2.7 -file for further details. Some notable changes:
     2.8 +file for further details. Some notable points:
     2.9  
    2.10  * Improved Isabelle/jEdit Prover IDE: more support for formal text structure,
    2.11    more visual feedback.
     3.1 --- a/CONTRIBUTORS	Sat Dec 10 17:22:47 2016 +0100
     3.2 +++ b/CONTRIBUTORS	Mon Dec 12 17:40:06 2016 +0100
     3.3 @@ -10,6 +10,10 @@
     3.4  Contributions to Isabelle2016-1
     3.5  -------------------------------
     3.6  
     3.7 +* December 2016: Ondřej Kunčar, TUM
     3.8 +  Types_To_Sets: experimental extension of Higher-Order Logic to allow
     3.9 +  translation of types to sets.
    3.10 +
    3.11  * October 2016: Jasmin Blanchette
    3.12    Integration of Nunchaku model finder.
    3.13  
     4.1 --- a/NEWS	Sat Dec 10 17:22:47 2016 +0100
     4.2 +++ b/NEWS	Mon Dec 12 17:40:06 2016 +0100
     4.3 @@ -949,6 +949,9 @@
     4.4  * Session Old_Number_Theory has been removed, after porting remaining
     4.5  theories.
     4.6  
     4.7 +* Session HOL-Types_To_Sets provides an experimental extension of
     4.8 +Higher-Order Logic to allow translation of types to sets.
     4.9 +
    4.10  
    4.11  *** ML ***
    4.12  
     5.1 --- a/src/Doc/JEdit/JEdit.thy	Sat Dec 10 17:22:47 2016 +0100
     5.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Dec 12 17:40:06 2016 +0100
     5.3 @@ -723,6 +723,11 @@
     5.4  
     5.5    The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
     5.6    Isabelle / General\<close>.
     5.7 +
     5.8 +  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
     5.9 +  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
    5.10 +  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
    5.11 +  aggressive options to trim whitespace on buffer-save.
    5.12  \<close>
    5.13  
    5.14  
     6.1 --- a/src/HOL/Decision_Procs/approximation.ML	Sat Dec 10 17:22:47 2016 +0100
     6.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Dec 12 17:40:06 2016 +0100
     6.3 @@ -43,7 +43,7 @@
     6.4    end
     6.5  
     6.6  fun approximation_conv ctxt ct =
     6.7 -  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
     6.8 +  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct);
     6.9  
    6.10  fun approximate ctxt t =
    6.11    approximation_oracle (Proof_Context.theory_of ctxt, t)
     7.1 --- a/src/HOL/Library/Types_To_Sets.thy	Sat Dec 10 17:22:47 2016 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,27 +0,0 @@
     7.4 -(*  Title:      HOL/Library/Types_To_Sets.thy
     7.5 -    Author:     Ondřej Kunčar, TU München
     7.6 -*)
     7.7 -
     7.8 -section \<open>From Types to Sets\<close>
     7.9 -
    7.10 -text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
    7.11 -  to allow translation of types to sets as described in 
    7.12 -  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
    7.13 -  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
    7.14 -
    7.15 -theory Types_To_Sets
    7.16 -  imports Main
    7.17 -begin
    7.18 -
    7.19 -subsection \<open>Rules\<close>
    7.20 -
    7.21 -text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
    7.22 -ML_file "Types_To_Sets/local_typedef.ML"
    7.23 -
    7.24 -text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
    7.25 -ML_file "Types_To_Sets/unoverloading.ML"
    7.26 -
    7.27 -text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
    7.28 -ML_file "Types_To_Sets/internalize_sort.ML"
    7.29 -
    7.30 -end
    7.31 \ No newline at end of file
     8.1 --- a/src/HOL/Library/Types_To_Sets/internalize_sort.ML	Sat Dec 10 17:22:47 2016 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,68 +0,0 @@
     8.4 -(*  Title:      internalize_sort.ML
     8.5 -    Author:     Ondřej Kunčar, TU München
     8.6 -
     8.7 -    Implements a derived rule (by using Thm.unconstrainT) that internalizes
     8.8 -    type class annotations.
     8.9 -*)
    8.10 -
    8.11 -
    8.12 -(*
    8.13 -                     \<phi>['a::{c_1, ..., c_n} / 'a]
    8.14 ----------------------------------------------------------------------
    8.15 -  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
    8.16 -
    8.17 -where class.c is the locale predicate associated with type class c and
    8.18 -ops are operations associated with type class c. For example:
    8.19 -If c = semigroup_add, then ops = op-, op+, 0, uminus.
    8.20 -If c = finite, then ops = TYPE('a::type).
    8.21 -*)
    8.22 -
    8.23 -signature INTERNALIZE_SORT =
    8.24 -sig
    8.25 -  val internalize_sort:  ctyp -> thm -> typ * thm
    8.26 -  val internalize_sort_attr: typ -> attribute
    8.27 -end;
    8.28 -
    8.29 -structure Internalize_Sort : INTERNALIZE_SORT =
    8.30 -struct
    8.31 -
    8.32 -fun internalize_sort ctvar thm =
    8.33 -  let
    8.34 -    val thy = Thm.theory_of_thm thm;
    8.35 -    val tvar = Thm.typ_of ctvar;
    8.36 -    
    8.37 -    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
    8.38 -
    8.39 -    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
    8.40 -    fun reduce_to_non_proper_sort (TVar (name, sort)) = 
    8.41 -        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
    8.42 -      | reduce_to_non_proper_sort _ = error "not supported";
    8.43 -
    8.44 -    val data = (map fst classes) ~~ assms;
    8.45 -    
    8.46 -    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' 
    8.47 -      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
    8.48 -      |> the_default tvar;
    8.49 -
    8.50 -    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
    8.51 -
    8.52 -    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
    8.53 -
    8.54 -    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' 
    8.55 -      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
    8.56 -      else discharge_of_class ren_tvar class) data;
    8.57 -  in
    8.58 -    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
    8.59 -  end;
    8.60 -
    8.61 -val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v 
    8.62 -  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
    8.63 -
    8.64 -fun internalize_sort_attr tvar = 
    8.65 -  Thm.rule_attribute [] (fn context => fn thm => 
    8.66 -    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
    8.67 -
    8.68 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort} 
    8.69 -  (tvar >> internalize_sort_attr) "internalize a sort"));
    8.70 -
    8.71 -end;
    8.72 \ No newline at end of file
     9.1 --- a/src/HOL/Library/Types_To_Sets/local_typedef.ML	Sat Dec 10 17:22:47 2016 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,84 +0,0 @@
     9.4 -(*  Title:      local_typedef.ML
     9.5 -    Author:     Ondřej Kunčar, TU München
     9.6 -
     9.7 -    Implements the Local Typedef Rule and extends the logic by the rule.
     9.8 -*)
     9.9 -
    9.10 -signature LOCAL_TYPEDEF =
    9.11 -sig
    9.12 -  val cancel_type_definition: thm -> thm
    9.13 -  val cancel_type_definition_attr: attribute
    9.14 -end;
    9.15 -
    9.16 -structure Local_Typedef : LOCAL_TYPEDEF =
    9.17 -struct
    9.18 -
    9.19 -(*
    9.20 -Local Typedef Rule (LT)
    9.21 -
    9.22 -  \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
    9.23 -------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
    9.24 -                       \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi>                        sort(\<beta>)=HOL.type]
    9.25 -*)
    9.26 -
    9.27 -(** BEGINNING OF THE CRITICAL CODE **)
    9.28 -
    9.29 -fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _, 
    9.30 -      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,  
    9.31 -      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) = 
    9.32 -    (Abs_type, set)
    9.33 -   | dest_typedef t = raise TERM ("dest_typedef", [t]);
    9.34 -  
    9.35 -fun cancel_type_definition_cterm thm =
    9.36 -  let
    9.37 -    fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
    9.38 -
    9.39 -    val thy = Thm.theory_of_thm thm;
    9.40 -    val prop = Thm.prop_of thm;
    9.41 -    val hyps = Thm.hyps_of thm;
    9.42 -
    9.43 -    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
    9.44 -
    9.45 -    val (typedef_assm, phi) = Logic.dest_implies prop
    9.46 -      handle TERM _ => err "the theorem is not an implication";
    9.47 -    val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
    9.48 -      handle TERM _ => err ("the assumption is not of the form " 
    9.49 -        ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
    9.50 -
    9.51 -    val (repT, absT) = Term.dest_funT abs_type;
    9.52 -    val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
    9.53 -    val (absT_name, sorts) = Term.dest_TVar absT;
    9.54 -    
    9.55 -    val typeS = Sign.defaultS thy;
    9.56 -    val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort " 
    9.57 -      ^ quote (Syntax.string_of_sort_global thy typeS));
    9.58 -     
    9.59 -    fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
    9.60 -    fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type " 
    9.61 -      ^ quote (fst absT_name));
    9.62 -    val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
    9.63 -    val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
    9.64 -    (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
    9.65 -    val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
    9.66 -
    9.67 -    val not_empty_assm = HOLogic.mk_Trueprop
    9.68 -      (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
    9.69 -    val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
    9.70 -  in
    9.71 -    Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
    9.72 -  end;
    9.73 -
    9.74 -(** END OF THE CRITICAL CODE **)
    9.75 -
    9.76 -val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
    9.77 -  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
    9.78 -
    9.79 -fun cancel_type_definition thm =  
    9.80 -  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
    9.81 -
    9.82 -val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
    9.83 -
    9.84 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition} 
    9.85 -  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
    9.86 -
    9.87 -end;
    9.88 \ No newline at end of file
    10.1 --- a/src/HOL/Library/Types_To_Sets/unoverloading.ML	Sat Dec 10 17:22:47 2016 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,139 +0,0 @@
    10.4 -(*  Title:      unoverloading.ML
    10.5 -    Author:     Ondřej Kunčar, TU München
    10.6 -
    10.7 -    Implements the Unoverloading Rule and extends the logic by the rule.
    10.8 -*)
    10.9 -
   10.10 -signature UNOVERLOADING =
   10.11 -sig
   10.12 -  val unoverload: cterm -> thm -> thm
   10.13 -  val unoverload_attr: cterm -> attribute
   10.14 -end;
   10.15 -
   10.16 -structure Unoverloading : UNOVERLOADING =
   10.17 -struct
   10.18 -
   10.19 -(*
   10.20 -Unoverloading Rule (UO)
   10.21 -
   10.22 -      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
   10.23 ----------------------------- [no type or constant or type class in \<phi> 
   10.24 -        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
   10.25 -*)
   10.26 -
   10.27 -(* The following functions match_args, reduction and entries_of were 
   10.28 -   cloned from defs.ML and theory.ML because the functions are not public.
   10.29 -   Notice that these functions already belong to the critical code.
   10.30 -*)
   10.31 -
   10.32 -(* >= *)
   10.33 -fun match_args (Ts, Us) =
   10.34 -  if Type.could_matches (Ts, Us) then
   10.35 -    Option.map Envir.subst_type
   10.36 -      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
   10.37 -  else NONE;
   10.38 -
   10.39 -fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
   10.40 -  let
   10.41 -    fun reduct Us (Ts, rhs) =
   10.42 -      (case match_args (Ts, Us) of
   10.43 -        NONE => NONE
   10.44 -      | SOME subst => SOME (map (apsnd (map subst)) rhs));
   10.45 -    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
   10.46 -
   10.47 -    val reds = map (`reducts) deps;
   10.48 -    val deps' =
   10.49 -      if forall (is_none o #1) reds then NONE
   10.50 -      else SOME (fold_rev
   10.51 -        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   10.52 -  in deps' end;
   10.53 -
   10.54 -fun const_and_typ_entries_of thy tm =
   10.55 - let
   10.56 -   val consts =
   10.57 -     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
   10.58 -   val types =
   10.59 -     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
   10.60 - in
   10.61 -   consts @ types
   10.62 - end;
   10.63 -
   10.64 -(* The actual implementation *)
   10.65 -
   10.66 -(** BEGINNING OF THE CRITICAL CODE **)
   10.67 -
   10.68 -fun fold_atyps_classes f =
   10.69 -  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S 
   10.70 -    | T as TVar (_, S) => fold (pair T #> f) S 
   10.71 -    (* just to avoid a warning about incomplete patterns *)
   10.72 -    | _ => raise TERM ("fold_atyps_classes", [])); 
   10.73 -
   10.74 -fun class_entries_of thy tm =
   10.75 -  let
   10.76 -    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
   10.77 -  in
   10.78 -    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
   10.79 -  end;
   10.80 -
   10.81 -fun unoverload_impl cconst thm =
   10.82 -  let
   10.83 -    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
   10.84 -
   10.85 -    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
   10.86 -    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
   10.87 -    
   10.88 -    val prop = Thm.prop_of thm;
   10.89 -    val prop_tfrees = rev (Term.add_tfree_names prop []);
   10.90 -    val _ = null prop_tfrees orelse err ("the theorem contains free type variables " 
   10.91 -      ^ commas_quote prop_tfrees);
   10.92 -
   10.93 -    val const = Thm.term_of cconst;
   10.94 -    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
   10.95 -    val const_tfrees = rev (Term.add_tfree_names const []);
   10.96 -    val _ = null const_tfrees orelse err ("the constant contains free type variables " 
   10.97 -      ^ commas_quote const_tfrees);
   10.98 -
   10.99 -    val thy = Thm.theory_of_thm thm;
  10.100 -    val defs = Theory.defs_of thy;
  10.101 -
  10.102 -    val const_entry = Theory.const_dep thy (Term.dest_Const const);
  10.103 -
  10.104 -    val Uss = Defs.specifications_of defs (fst const_entry);
  10.105 -    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss 
  10.106 -      orelse err "the constant instance has already a specification";
  10.107 -
  10.108 -    val context = Defs.global_context thy;
  10.109 -    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
  10.110 -    
  10.111 -    fun dep_err (c, Ts) (d, Us) =
  10.112 -      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
  10.113 -    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
  10.114 -    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
  10.115 -      orelse dep_err prop_entry const_entry;
  10.116 -    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
  10.117 -    val _ = forall not_depends_on_const prop_entries;
  10.118 -  in
  10.119 -    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
  10.120 -  end;
  10.121 -
  10.122 -(** END OF THE CRITICAL CODE **)
  10.123 -
  10.124 -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
  10.125 -  (Thm.add_oracle (@{binding unoverload},
  10.126 -  fn (const, thm) => unoverload_impl const  thm)));
  10.127 -
  10.128 -fun unoverload const thm = unoverload_oracle (const, thm);
  10.129 -
  10.130 -fun unoverload_attr const = 
  10.131 -  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
  10.132 -
  10.133 -val const = Args.context -- Args.term  >>
  10.134 -  (fn (ctxt, tm) => 
  10.135 -    if not (Term.is_Const tm) 
  10.136 -    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
  10.137 -    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
  10.138 -
  10.139 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload} 
  10.140 -  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
  10.141 -
  10.142 -end;
  10.143 \ No newline at end of file
    11.1 --- a/src/HOL/ROOT	Sat Dec 10 17:22:47 2016 +0100
    11.2 +++ b/src/HOL/ROOT	Mon Dec 12 17:40:06 2016 +0100
    11.3 @@ -38,7 +38,6 @@
    11.4      Predicate_Compile_Quickcheck
    11.5      Prefix_Order
    11.6      Rewrite
    11.7 -    Types_To_Sets
    11.8      (*conflicting type class instantiations*)
    11.9      List_lexord
   11.10      Sublist_Order
   11.11 @@ -1018,6 +1017,17 @@
   11.12    theories [condition = ISABELLE_SWIPL, quick_and_dirty]
   11.13      Reg_Exp_Example
   11.14  
   11.15 +session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   11.16 +  description {*
   11.17 +    Experimental extension of Higher-Order Logic to allow translation of types to sets.
   11.18 +  *}
   11.19 +  options [document = false]
   11.20 +  theories
   11.21 +    Types_To_Sets
   11.22 +    "Examples/Prerequisites"
   11.23 +    "Examples/Finite"
   11.24 +    "Examples/T2_Spaces"
   11.25 +
   11.26  session HOLCF (main timing) in HOLCF = HOL +
   11.27    description {*
   11.28      Author:     Franz Regensburger
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Types_To_Sets/Examples/Finite.thy	Mon Dec 12 17:40:06 2016 +0100
    12.3 @@ -0,0 +1,90 @@
    12.4 +(*  Title:      HOL/Types_To_Sets/Examples/Finite.thy
    12.5 +    Author:     Ondřej Kunčar, TU München
    12.6 +*)
    12.7 +
    12.8 +theory Finite
    12.9 +  imports "../Types_To_Sets" Prerequisites
   12.10 +begin
   12.11 +
   12.12 +section \<open>The Type-Based Theorem\<close>
   12.13 +
   12.14 +text\<open>This example file shows how we perform the relativization in presence of axiomatic
   12.15 +  type classes: we internalize them.\<close>
   12.16 +
   12.17 +definition injective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   12.18 +  where "injective f \<equiv> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
   12.19 +
   12.20 +text\<open>We want to relativize the following type-based theorem using the type class finite.\<close>
   12.21 +
   12.22 +lemma type_based: "\<exists>f :: 'a::finite \<Rightarrow> nat. injective f"
   12.23 +  unfolding injective_def
   12.24 +  using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto
   12.25 +
   12.26 +section \<open>Definitions and Setup for The Relativization\<close>
   12.27 +
   12.28 +text\<open>We have to define what being injective on a set means.\<close>
   12.29 +
   12.30 +definition injective_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   12.31 +  where "injective_on A f \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. f x = f y \<longrightarrow> x = y"
   12.32 +
   12.33 +text\<open>The predicate injective_on is the relativization of the predicate injective.\<close>
   12.34 +
   12.35 +lemma injective_transfer[transfer_rule]:
   12.36 +  includes lifting_syntax
   12.37 +  assumes [transfer_rule]: "right_total T"
   12.38 +  assumes [transfer_rule]: "bi_unique T"
   12.39 +  shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective"
   12.40 +  unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
   12.41 +
   12.42 +text\<open>Similarly, we define the relativization of the internalization
   12.43 +     of the type class finite, class.finite\<close>
   12.44 +
   12.45 +definition finite_on :: "'a set => bool" where "finite_on A = finite A"
   12.46 +
   12.47 +lemma class_finite_transfer[transfer_rule]:
   12.48 +  assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
   12.49 +  assumes [transfer_rule]: "bi_unique T"
   12.50 +  shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
   12.51 +  unfolding finite_on_def class.finite_def by transfer_prover
   12.52 +
   12.53 +text\<open>The aforementioned development can be automated. The main part is already automated
   12.54 +     by the transfer_prover.\<close>
   12.55 +
   12.56 +section \<open>The Relativization to The Set-Based Theorem\<close>
   12.57 +
   12.58 +lemmas internalized = type_based[internalize_sort "'a::finite"]
   12.59 +text\<open>We internalized the type class finite and thus reduced the task to the
   12.60 +  original relativization algorithm.\<close>
   12.61 +thm internalized
   12.62 +
   12.63 +text\<open>This is the set-based variant.\<close>
   12.64 +
   12.65 +lemma set_based:
   12.66 +  assumes "(A::'a set) \<noteq> {}"
   12.67 +  shows "finite_on A \<longrightarrow> (\<exists>f :: 'a \<Rightarrow> nat. injective_on A f)"
   12.68 +proof -
   12.69 +  {
   12.70 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
   12.71 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
   12.72 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
   12.73 +      by auto
   12.74 +
   12.75 +    text\<open>Setup for the Transfer tool.\<close>
   12.76 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
   12.77 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
   12.78 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
   12.79 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
   12.80 +
   12.81 +    have ?thesis
   12.82 +      text\<open>Relativization by the Transfer tool.\<close>
   12.83 +      using internalized[where 'a = 'b, untransferred, simplified]
   12.84 +      by blast
   12.85 +  } note * = this[cancel_type_definition, OF assms] text\<open>We removed the definition of 'b.\<close>
   12.86 +
   12.87 +  show ?thesis by (rule *)
   12.88 +qed
   12.89 +
   12.90 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
   12.91 +thm type_based set_based
   12.92 +
   12.93 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Mon Dec 12 17:40:06 2016 +0100
    13.3 @@ -0,0 +1,25 @@
    13.4 +(*  Title:      HOL/Types_To_Sets/Examples/Prerequisites.thy
    13.5 +    Author:     Ondřej Kunčar, TU München
    13.6 +*)
    13.7 +
    13.8 +theory Prerequisites
    13.9 +  imports Main
   13.10 +begin
   13.11 +
   13.12 +context
   13.13 +  fixes Rep Abs A T
   13.14 +  assumes type: "type_definition Rep Abs A"
   13.15 +  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   13.16 +begin
   13.17 +
   13.18 +lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
   13.19 +proof -
   13.20 +  interpret type_definition Rep Abs A by(rule type)
   13.21 +  show ?thesis
   13.22 +    unfolding Domainp_iff[abs_def] T_def fun_eq_iff
   13.23 +    by (metis Abs_inverse Rep)
   13.24 +qed
   13.25 +
   13.26 +end
   13.27 +
   13.28 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Mon Dec 12 17:40:06 2016 +0100
    14.3 @@ -0,0 +1,162 @@
    14.4 +(*  Title:      HOL/Types_To_Sets/Examples/T2_Spaces.thy
    14.5 +    Author:     Ondřej Kunčar, TU München
    14.6 +*)
    14.7 +
    14.8 +theory T2_Spaces
    14.9 +  imports Complex_Main "../Types_To_Sets" Prerequisites
   14.10 +begin
   14.11 +
   14.12 +section \<open>The Type-Based Theorem\<close>
   14.13 +
   14.14 +text\<open>We relativize a theorem that contains a type class with an associated (overloaded) operation.
   14.15 +     The key technique is to compile out the overloaded operation by the dictionary construction
   14.16 +     using the Unoverloading rule.\<close>
   14.17 +
   14.18 +text\<open>This is the type-based statement that we want to relativize.\<close>
   14.19 +thm compact_imp_closed
   14.20 +text\<open>The type is class a T2 typological space.\<close>
   14.21 +typ "'a :: t2_space"
   14.22 +text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close>
   14.23 +term "open"
   14.24 +
   14.25 +section \<open>Definitions and Setup for The Relativization\<close>
   14.26 +
   14.27 +text\<open>We gradually define relativization of topological spaces, t2 spaces, compact and closed
   14.28 +     predicates and prove that they are indeed the relativization of the original predicates.\<close>
   14.29 +
   14.30 +definition topological_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
   14.31 +  where "topological_space_on_with A \<equiv> \<lambda>open. open A \<and>
   14.32 +    (\<forall>S \<subseteq> A. \<forall>T \<subseteq> A. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T))
   14.33 +    \<and> (\<forall>K \<subseteq> Pow A. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union>K))"
   14.34 +
   14.35 +lemma topological_space_transfer[transfer_rule]:
   14.36 +  includes lifting_syntax
   14.37 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   14.38 +  shows "((rel_set T ===> op=) ===> op=) (topological_space_on_with (Collect (Domainp T)))
   14.39 +    class.topological_space"
   14.40 +  unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
   14.41 +  apply transfer_prover_start
   14.42 +  apply transfer_step+
   14.43 +  unfolding Pow_def Ball_Collect[symmetric]
   14.44 +  by blast
   14.45 +
   14.46 +definition t2_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
   14.47 +  where "t2_space_on_with A \<equiv> \<lambda>open. topological_space_on_with A open \<and>
   14.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 = {}))"
   14.49 +
   14.50 +lemma t2_space_transfer[transfer_rule]:
   14.51 +  includes lifting_syntax
   14.52 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   14.53 +  shows "((rel_set T ===> op=) ===> op=) (t2_space_on_with (Collect (Domainp T))) class.t2_space"
   14.54 +  unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def]
   14.55 +    class.t2_space_axioms_def[abs_def]
   14.56 +  apply transfer_prover_start
   14.57 +  apply transfer_step+
   14.58 +  unfolding Ball_Collect[symmetric]
   14.59 +  by blast
   14.60 +
   14.61 +definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   14.62 +  where "closed_with \<equiv> \<lambda>open S. open (- S)"
   14.63 +
   14.64 +lemma closed_closed_with: "closed s = closed_with open s"
   14.65 +  unfolding closed_with_def closed_def[abs_def] ..
   14.66 +
   14.67 +definition closed_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   14.68 +  where "closed_on_with A \<equiv> \<lambda>open S. open (-S \<inter> A)"
   14.69 +
   14.70 +lemma closed_with_transfer[transfer_rule]:
   14.71 +  includes lifting_syntax
   14.72 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   14.73 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (closed_on_with (Collect (Domainp T)))
   14.74 +    closed_with"
   14.75 +  unfolding closed_with_def closed_on_with_def by transfer_prover
   14.76 +
   14.77 +definition compact_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   14.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))"
   14.79 +
   14.80 +lemma compact_compact_with: "compact s = compact_with open s"
   14.81 +  unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
   14.82 +
   14.83 +definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   14.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>
   14.85 +    (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
   14.86 +
   14.87 +lemma compact_on_with_subset_trans: "(\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
   14.88 +  (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)) =
   14.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)))"
   14.90 +  by (meson subset_trans)
   14.91 +
   14.92 +lemma compact_with_transfer[transfer_rule]:
   14.93 +  includes lifting_syntax
   14.94 +  assumes [transfer_rule]: "right_total T" "bi_unique T"
   14.95 +  shows "((rel_set T ===> op=) ===> rel_set T===> op=) (compact_on_with (Collect (Domainp T)))
   14.96 +    compact_with"
   14.97 +  unfolding compact_with_def compact_on_with_def
   14.98 +  apply transfer_prover_start
   14.99 +  apply transfer_step+
  14.100 +  unfolding compact_on_with_subset_trans
  14.101 +  unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq
  14.102 +  by blast
  14.103 +
  14.104 +setup \<open>Sign.add_const_constraint
  14.105 +  (@{const_name "open"}, SOME @{typ "'a set \<Rightarrow> bool"})\<close>
  14.106 +
  14.107 +text\<open>The aforementioned development can be automated. The main part is already automated
  14.108 +     by the transfer_prover.\<close>
  14.109 +
  14.110 +section \<open>The Relativization to The Set-Based Theorem\<close>
  14.111 +
  14.112 +text\<open>The first step of the dictionary construction.\<close>
  14.113 +lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
  14.114 +thm dictionary_first_step
  14.115 +
  14.116 +text\<open>Internalization of the type class t2_space.\<close>
  14.117 +lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
  14.118 +thm internalized_sort
  14.119 +
  14.120 +text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close>
  14.121 +lemmas dictionary_second_step =  internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"]
  14.122 +text\<open>The theorem with internalized type classes and compiled out operations is the starting point
  14.123 +     for the original relativization algorithm.\<close>
  14.124 +thm dictionary_second_step
  14.125 +
  14.126 +
  14.127 +text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
  14.128 +lemma compact_imp_closed_set_based:
  14.129 +  assumes "(A::'a set) \<noteq> {}"
  14.130 +  shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow>
  14.131 +    closed_on_with A open S)"
  14.132 +proof -
  14.133 +  {
  14.134 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
  14.135 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
  14.136 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
  14.137 +      by auto
  14.138 +
  14.139 +    text\<open>Setup for the Transfer tool.\<close>
  14.140 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
  14.141 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
  14.142 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
  14.143 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
  14.144 +
  14.145 +    have ?thesis
  14.146 +      text\<open>Relativization by the Transfer tool.\<close>
  14.147 +      using dictionary_second_step[where 'a = 'b, untransferred, simplified]
  14.148 +      by blast
  14.149 +
  14.150 +  } note * = this[cancel_type_definition, OF assms]
  14.151 +
  14.152 +  show ?thesis by (rule *)
  14.153 +qed
  14.154 +
  14.155 +setup \<open>Sign.add_const_constraint
  14.156 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
  14.157 +
  14.158 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
  14.159 +thm compact_imp_closed compact_imp_closed_set_based
  14.160 +
  14.161 +declare [[show_sorts]]
  14.162 +text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close>
  14.163 +thm compact_imp_closed compact_imp_closed_set_based
  14.164 +
  14.165 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Mon Dec 12 17:40:06 2016 +0100
    15.3 @@ -0,0 +1,27 @@
    15.4 +(*  Title:      HOL/Types_To_Sets/Types_To_Sets.thy
    15.5 +    Author:     Ondřej Kunčar, TU München
    15.6 +*)
    15.7 +
    15.8 +section \<open>From Types to Sets\<close>
    15.9 +
   15.10 +text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
   15.11 +  to allow translation of types to sets as described in
   15.12 +  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
   15.13 +  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
   15.14 +
   15.15 +theory Types_To_Sets
   15.16 +  imports Main
   15.17 +begin
   15.18 +
   15.19 +subsection \<open>Rules\<close>
   15.20 +
   15.21 +text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
   15.22 +ML_file "local_typedef.ML"
   15.23 +
   15.24 +text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
   15.25 +ML_file "unoverloading.ML"
   15.26 +
   15.27 +text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
   15.28 +ML_file "internalize_sort.ML"
   15.29 +
   15.30 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Dec 12 17:40:06 2016 +0100
    16.3 @@ -0,0 +1,68 @@
    16.4 +(*  Title:      HOL/Types_To_Sets/internalize_sort.ML
    16.5 +    Author:     Ondřej Kunčar, TU München
    16.6 +
    16.7 +A derived rule (by using Thm.unconstrainT) that internalizes
    16.8 +type class annotations.
    16.9 +*)
   16.10 +
   16.11 +
   16.12 +(*
   16.13 +                     \<phi>['a::{c_1, ..., c_n} / 'a]
   16.14 +---------------------------------------------------------------------
   16.15 +  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
   16.16 +
   16.17 +where class.c is the locale predicate associated with type class c and
   16.18 +ops are operations associated with type class c. For example:
   16.19 +If c = semigroup_add, then ops = op-, op+, 0, uminus.
   16.20 +If c = finite, then ops = TYPE('a::type).
   16.21 +*)
   16.22 +
   16.23 +signature INTERNALIZE_SORT =
   16.24 +sig
   16.25 +  val internalize_sort:  ctyp -> thm -> typ * thm
   16.26 +  val internalize_sort_attr: typ -> attribute
   16.27 +end;
   16.28 +
   16.29 +structure Internalize_Sort : INTERNALIZE_SORT =
   16.30 +struct
   16.31 +
   16.32 +fun internalize_sort ctvar thm =
   16.33 +  let
   16.34 +    val thy = Thm.theory_of_thm thm;
   16.35 +    val tvar = Thm.typ_of ctvar;
   16.36 +
   16.37 +    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
   16.38 +
   16.39 +    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
   16.40 +    fun reduce_to_non_proper_sort (TVar (name, sort)) =
   16.41 +        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
   16.42 +      | reduce_to_non_proper_sort _ = error "not supported";
   16.43 +
   16.44 +    val data = (map fst classes) ~~ assms;
   16.45 +
   16.46 +    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
   16.47 +      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
   16.48 +      |> the_default tvar;
   16.49 +
   16.50 +    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
   16.51 +
   16.52 +    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
   16.53 +
   16.54 +    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
   16.55 +      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
   16.56 +      else discharge_of_class ren_tvar class) data;
   16.57 +  in
   16.58 +    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
   16.59 +  end;
   16.60 +
   16.61 +val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
   16.62 +  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
   16.63 +
   16.64 +fun internalize_sort_attr tvar =
   16.65 +  Thm.rule_attribute [] (fn context => fn thm =>
   16.66 +    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
   16.67 +
   16.68 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
   16.69 +  (tvar >> internalize_sort_attr) "internalize a sort"));
   16.70 +
   16.71 +end;
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Types_To_Sets/local_typedef.ML	Mon Dec 12 17:40:06 2016 +0100
    17.3 @@ -0,0 +1,84 @@
    17.4 +(*  Title:      HOL/Types_To_Sets/local_typedef.ML
    17.5 +    Author:     Ondřej Kunčar, TU München
    17.6 +
    17.7 +The Local Typedef Rule (extension of the logic).
    17.8 +*)
    17.9 +
   17.10 +signature LOCAL_TYPEDEF =
   17.11 +sig
   17.12 +  val cancel_type_definition: thm -> thm
   17.13 +  val cancel_type_definition_attr: attribute
   17.14 +end;
   17.15 +
   17.16 +structure Local_Typedef : LOCAL_TYPEDEF =
   17.17 +struct
   17.18 +
   17.19 +(*
   17.20 +Local Typedef Rule (LT)
   17.21 +
   17.22 +  \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
   17.23 +------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
   17.24 +                       \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi>                        sort(\<beta>)=HOL.type]
   17.25 +*)
   17.26 +
   17.27 +(** BEGINNING OF THE CRITICAL CODE **)
   17.28 +
   17.29 +fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
   17.30 +      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
   17.31 +      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
   17.32 +    (Abs_type, set)
   17.33 +   | dest_typedef t = raise TERM ("dest_typedef", [t]);
   17.34 +
   17.35 +fun cancel_type_definition_cterm thm =
   17.36 +  let
   17.37 +    fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
   17.38 +
   17.39 +    val thy = Thm.theory_of_thm thm;
   17.40 +    val prop = Thm.prop_of thm;
   17.41 +    val hyps = Thm.hyps_of thm;
   17.42 +
   17.43 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
   17.44 +
   17.45 +    val (typedef_assm, phi) = Logic.dest_implies prop
   17.46 +      handle TERM _ => err "the theorem is not an implication";
   17.47 +    val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
   17.48 +      handle TERM _ => err ("the assumption is not of the form "
   17.49 +        ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
   17.50 +
   17.51 +    val (repT, absT) = Term.dest_funT abs_type;
   17.52 +    val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
   17.53 +    val (absT_name, sorts) = Term.dest_TVar absT;
   17.54 +
   17.55 +    val typeS = Sign.defaultS thy;
   17.56 +    val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
   17.57 +      ^ quote (Syntax.string_of_sort_global thy typeS));
   17.58 +
   17.59 +    fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
   17.60 +    fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
   17.61 +      ^ quote (fst absT_name));
   17.62 +    val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
   17.63 +    val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
   17.64 +    (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
   17.65 +    val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
   17.66 +
   17.67 +    val not_empty_assm = HOLogic.mk_Trueprop
   17.68 +      (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
   17.69 +    val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
   17.70 +  in
   17.71 +    Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
   17.72 +  end;
   17.73 +
   17.74 +(** END OF THE CRITICAL CODE **)
   17.75 +
   17.76 +val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
   17.77 +  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
   17.78 +
   17.79 +fun cancel_type_definition thm =
   17.80 +  Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
   17.81 +
   17.82 +val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
   17.83 +
   17.84 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
   17.85 +  (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
   17.86 +
   17.87 +end;
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Types_To_Sets/unoverloading.ML	Mon Dec 12 17:40:06 2016 +0100
    18.3 @@ -0,0 +1,140 @@
    18.4 +(*  Title:      HOL/Types_To_Sets/unoverloading.ML
    18.5 +    Author:     Ondřej Kunčar, TU München
    18.6 +
    18.7 +The Unoverloading Rule (extension of the logic).
    18.8 +*)
    18.9 +
   18.10 +signature UNOVERLOADING =
   18.11 +sig
   18.12 +  val unoverload: cterm -> thm -> thm
   18.13 +  val unoverload_attr: cterm -> attribute
   18.14 +end;
   18.15 +
   18.16 +structure Unoverloading : UNOVERLOADING =
   18.17 +struct
   18.18 +
   18.19 +(*
   18.20 +Unoverloading Rule (UO)
   18.21 +
   18.22 +      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
   18.23 +---------------------------- [no type or constant or type class in \<phi>
   18.24 +        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
   18.25 +*)
   18.26 +
   18.27 +(* The following functions match_args, reduction and entries_of were
   18.28 +   cloned from defs.ML and theory.ML because the functions are not public.
   18.29 +   Notice that these functions already belong to the critical code.
   18.30 +*)
   18.31 +
   18.32 +(* >= *)
   18.33 +fun match_args (Ts, Us) =
   18.34 +  if Type.could_matches (Ts, Us) then
   18.35 +    Option.map Envir.subst_type
   18.36 +      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
   18.37 +  else NONE;
   18.38 +
   18.39 +fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
   18.40 +  let
   18.41 +    fun reduct Us (Ts, rhs) =
   18.42 +      (case match_args (Ts, Us) of
   18.43 +        NONE => NONE
   18.44 +      | SOME subst => SOME (map (apsnd (map subst)) rhs));
   18.45 +    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
   18.46 +
   18.47 +    val reds = map (`reducts) deps;
   18.48 +    val deps' =
   18.49 +      if forall (is_none o #1) reds then NONE
   18.50 +      else SOME (fold_rev
   18.51 +        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   18.52 +  in deps' end;
   18.53 +
   18.54 +fun const_and_typ_entries_of thy tm =
   18.55 + let
   18.56 +   val consts =
   18.57 +     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
   18.58 +   val types =
   18.59 +     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
   18.60 + in
   18.61 +   consts @ types
   18.62 + end;
   18.63 +
   18.64 +
   18.65 +(* The actual implementation *)
   18.66 +
   18.67 +(** BEGINNING OF THE CRITICAL CODE **)
   18.68 +
   18.69 +fun fold_atyps_classes f =
   18.70 +  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
   18.71 +    | T as TVar (_, S) => fold (pair T #> f) S
   18.72 +    (* just to avoid a warning about incomplete patterns *)
   18.73 +    | _ => raise TERM ("fold_atyps_classes", []));
   18.74 +
   18.75 +fun class_entries_of thy tm =
   18.76 +  let
   18.77 +    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
   18.78 +  in
   18.79 +    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
   18.80 +  end;
   18.81 +
   18.82 +fun unoverload_impl cconst thm =
   18.83 +  let
   18.84 +    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
   18.85 +
   18.86 +    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
   18.87 +    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
   18.88 +
   18.89 +    val prop = Thm.prop_of thm;
   18.90 +    val prop_tfrees = rev (Term.add_tfree_names prop []);
   18.91 +    val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
   18.92 +      ^ commas_quote prop_tfrees);
   18.93 +
   18.94 +    val const = Thm.term_of cconst;
   18.95 +    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
   18.96 +    val const_tfrees = rev (Term.add_tfree_names const []);
   18.97 +    val _ = null const_tfrees orelse err ("the constant contains free type variables "
   18.98 +      ^ commas_quote const_tfrees);
   18.99 +
  18.100 +    val thy = Thm.theory_of_thm thm;
  18.101 +    val defs = Theory.defs_of thy;
  18.102 +
  18.103 +    val const_entry = Theory.const_dep thy (Term.dest_Const const);
  18.104 +
  18.105 +    val Uss = Defs.specifications_of defs (fst const_entry);
  18.106 +    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
  18.107 +      orelse err "the constant instance has already a specification";
  18.108 +
  18.109 +    val context = Defs.global_context thy;
  18.110 +    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
  18.111 +
  18.112 +    fun dep_err (c, Ts) (d, Us) =
  18.113 +      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
  18.114 +    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
  18.115 +    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
  18.116 +      orelse dep_err prop_entry const_entry;
  18.117 +    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
  18.118 +    val _ = forall not_depends_on_const prop_entries;
  18.119 +  in
  18.120 +    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
  18.121 +  end;
  18.122 +
  18.123 +(** END OF THE CRITICAL CODE **)
  18.124 +
  18.125 +val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
  18.126 +  (Thm.add_oracle (@{binding unoverload},
  18.127 +  fn (const, thm) => unoverload_impl const  thm)));
  18.128 +
  18.129 +fun unoverload const thm = unoverload_oracle (const, thm);
  18.130 +
  18.131 +fun unoverload_attr const =
  18.132 +  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
  18.133 +
  18.134 +val const = Args.context -- Args.term  >>
  18.135 +  (fn (ctxt, tm) =>
  18.136 +    if not (Term.is_Const tm)
  18.137 +    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
  18.138 +    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
  18.139 +
  18.140 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
  18.141 +  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
  18.142 +
  18.143 +end;
    19.1 --- a/src/Tools/misc_legacy.ML	Sat Dec 10 17:22:47 2016 +0100
    19.2 +++ b/src/Tools/misc_legacy.ML	Mon Dec 12 17:40:06 2016 +0100
    19.3 @@ -201,26 +201,10 @@
    19.4            (false, relift st, Thm.nprems_of st) gno state
    19.5    in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
    19.6  
    19.7 -fun print_vars_terms ctxt n thm =
    19.8 -  let
    19.9 -    fun typed s ty = "  " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty;
   19.10 -    fun find_vars (Const (c, ty)) =
   19.11 -          if null (Term.add_tvarsT ty []) then I
   19.12 -          else insert (op =) (typed c ty)
   19.13 -      | find_vars (Var (xi, ty)) =
   19.14 -          insert (op =) (typed (Term.string_of_vname xi) ty)
   19.15 -      | find_vars (Free _) = I
   19.16 -      | find_vars (Bound _) = I
   19.17 -      | find_vars (Abs (_, _, t)) = find_vars t
   19.18 -      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
   19.19 -    val prem = Logic.nth_prem (n, Thm.prop_of thm)
   19.20 -    val tms = find_vars prem []
   19.21 -  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
   19.22 -
   19.23  in
   19.24  
   19.25  fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm
   19.26 -  handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty)
   19.27 +  handle THM ("assume: variables", _, _) => Seq.empty
   19.28  
   19.29  end;
   19.30