--- a/CONTRIBUTORS Thu Dec 08 15:11:20 2016 +0100
+++ b/CONTRIBUTORS Mon Dec 12 11:33:14 2016 +0100
@@ -6,6 +6,10 @@
Contributions to Isabelle2016-1
-------------------------------
+* December 2016: Ondřej Kunčar, TUM
+ Types_To_Sets: experimental extension of Higher-Order Logic to allow
+ translation of types to sets.
+
* October 2016: Jasmin Blanchette
Integration of Nunchaku model finder.
--- a/NEWS Thu Dec 08 15:11:20 2016 +0100
+++ b/NEWS Mon Dec 12 11:33:14 2016 +0100
@@ -938,6 +938,9 @@
* Session Old_Number_Theory has been removed, after porting remaining
theories.
+* Session HOL-Types_To_Sets provides an experimental extension of
+Higher-Order Logic to allow translation of types to sets.
+
*** ML ***
--- a/src/HOL/Library/Types_To_Sets.thy Thu Dec 08 15:11:20 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: HOL/Library/Types_To_Sets.thy
- Author: Ondřej Kunčar, TU München
-*)
-
-section \<open>From Types to Sets\<close>
-
-text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
- to allow translation of types to sets as described in
- O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
- available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
-
-theory Types_To_Sets
- imports Main
-begin
-
-subsection \<open>Rules\<close>
-
-text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
-ML_file "Types_To_Sets/local_typedef.ML"
-
-text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
-ML_file "Types_To_Sets/unoverloading.ML"
-
-text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
-ML_file "Types_To_Sets/internalize_sort.ML"
-
-end
\ No newline at end of file
--- a/src/HOL/Library/Types_To_Sets/internalize_sort.ML Thu Dec 08 15:11:20 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title: internalize_sort.ML
- Author: Ondřej Kunčar, TU München
-
- Implements a derived rule (by using Thm.unconstrainT) that internalizes
- type class annotations.
-*)
-
-
-(*
- \<phi>['a::{c_1, ..., c_n} / 'a]
----------------------------------------------------------------------
- class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
-
-where class.c is the locale predicate associated with type class c and
-ops are operations associated with type class c. For example:
-If c = semigroup_add, then ops = op-, op+, 0, uminus.
-If c = finite, then ops = TYPE('a::type).
-*)
-
-signature INTERNALIZE_SORT =
-sig
- val internalize_sort: ctyp -> thm -> typ * thm
- val internalize_sort_attr: typ -> attribute
-end;
-
-structure Internalize_Sort : INTERNALIZE_SORT =
-struct
-
-fun internalize_sort ctvar thm =
- let
- val thy = Thm.theory_of_thm thm;
- val tvar = Thm.typ_of ctvar;
-
- val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
-
- fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
- fun reduce_to_non_proper_sort (TVar (name, sort)) =
- TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
- | reduce_to_non_proper_sort _ = error "not supported";
-
- val data = (map fst classes) ~~ assms;
-
- val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
- then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
- |> the_default tvar;
-
- fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
-
- fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
-
- val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
- then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
- else discharge_of_class ren_tvar class) data;
- in
- (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
- end;
-
-val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
- | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
-
-fun internalize_sort_attr tvar =
- Thm.rule_attribute [] (fn context => fn thm =>
- (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
-
-val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
- (tvar >> internalize_sort_attr) "internalize a sort"));
-
-end;
\ No newline at end of file
--- a/src/HOL/Library/Types_To_Sets/local_typedef.ML Thu Dec 08 15:11:20 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(* Title: local_typedef.ML
- Author: Ondřej Kunčar, TU München
-
- Implements the Local Typedef Rule and extends the logic by the rule.
-*)
-
-signature LOCAL_TYPEDEF =
-sig
- val cancel_type_definition: thm -> thm
- val cancel_type_definition_attr: attribute
-end;
-
-structure Local_Typedef : LOCAL_TYPEDEF =
-struct
-
-(*
-Local Typedef Rule (LT)
-
- \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
-------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
- \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi> sort(\<beta>)=HOL.type]
-*)
-
-(** BEGINNING OF THE CRITICAL CODE **)
-
-fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
- (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
- (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
- (Abs_type, set)
- | dest_typedef t = raise TERM ("dest_typedef", [t]);
-
-fun cancel_type_definition_cterm thm =
- let
- fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
-
- val thy = Thm.theory_of_thm thm;
- val prop = Thm.prop_of thm;
- val hyps = Thm.hyps_of thm;
-
- val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
-
- val (typedef_assm, phi) = Logic.dest_implies prop
- handle TERM _ => err "the theorem is not an implication";
- val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
- handle TERM _ => err ("the assumption is not of the form "
- ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
-
- val (repT, absT) = Term.dest_funT abs_type;
- val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
- val (absT_name, sorts) = Term.dest_TVar absT;
-
- val typeS = Sign.defaultS thy;
- val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
- ^ quote (Syntax.string_of_sort_global thy typeS));
-
- fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
- fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
- ^ quote (fst absT_name));
- val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
- val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
- (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
- val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
-
- val not_empty_assm = HOLogic.mk_Trueprop
- (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
- val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
- in
- Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
- end;
-
-(** END OF THE CRITICAL CODE **)
-
-val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
-
-fun cancel_type_definition thm =
- Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
-
-val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
-
-val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
- (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
-
-end;
\ No newline at end of file
--- a/src/HOL/Library/Types_To_Sets/unoverloading.ML Thu Dec 08 15:11:20 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-(* Title: unoverloading.ML
- Author: Ondřej Kunčar, TU München
-
- Implements the Unoverloading Rule and extends the logic by the rule.
-*)
-
-signature UNOVERLOADING =
-sig
- val unoverload: cterm -> thm -> thm
- val unoverload_attr: cterm -> attribute
-end;
-
-structure Unoverloading : UNOVERLOADING =
-struct
-
-(*
-Unoverloading Rule (UO)
-
- \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
----------------------------- [no type or constant or type class in \<phi>
- \<turnstile> \<And>x::\<sigma>. \<phi> depends on c::\<sigma>; c::\<sigma> is undefined]
-*)
-
-(* The following functions match_args, reduction and entries_of were
- cloned from defs.ML and theory.ML because the functions are not public.
- Notice that these functions already belong to the critical code.
-*)
-
-(* >= *)
-fun match_args (Ts, Us) =
- if Type.could_matches (Ts, Us) then
- Option.map Envir.subst_type
- (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
- else NONE;
-
-fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
- let
- fun reduct Us (Ts, rhs) =
- (case match_args (Ts, Us) of
- NONE => NONE
- | SOME subst => SOME (map (apsnd (map subst)) rhs));
- fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
-
- val reds = map (`reducts) deps;
- val deps' =
- if forall (is_none o #1) reds then NONE
- else SOME (fold_rev
- (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
- in deps' end;
-
-fun const_and_typ_entries_of thy tm =
- let
- val consts =
- fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
- val types =
- (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
- in
- consts @ types
- end;
-
-(* The actual implementation *)
-
-(** BEGINNING OF THE CRITICAL CODE **)
-
-fun fold_atyps_classes f =
- fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
- | T as TVar (_, S) => fold (pair T #> f) S
- (* just to avoid a warning about incomplete patterns *)
- | _ => raise TERM ("fold_atyps_classes", []));
-
-fun class_entries_of thy tm =
- let
- val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
- in
- map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
- end;
-
-fun unoverload_impl cconst thm =
- let
- fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
-
- val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
- val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
-
- val prop = Thm.prop_of thm;
- val prop_tfrees = rev (Term.add_tfree_names prop []);
- val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
- ^ commas_quote prop_tfrees);
-
- val const = Thm.term_of cconst;
- val _ = Term.is_Const const orelse err "the parameter is is not a constant";
- val const_tfrees = rev (Term.add_tfree_names const []);
- val _ = null const_tfrees orelse err ("the constant contains free type variables "
- ^ commas_quote const_tfrees);
-
- val thy = Thm.theory_of_thm thm;
- val defs = Theory.defs_of thy;
-
- val const_entry = Theory.const_dep thy (Term.dest_Const const);
-
- val Uss = Defs.specifications_of defs (fst const_entry);
- val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
- orelse err "the constant instance has already a specification";
-
- val context = Defs.global_context thy;
- val prt_entry = Pretty.string_of o Defs.pretty_entry context;
-
- fun dep_err (c, Ts) (d, Us) =
- err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
- fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
- fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
- orelse dep_err prop_entry const_entry;
- val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
- val _ = forall not_depends_on_const prop_entries;
- in
- Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
- end;
-
-(** END OF THE CRITICAL CODE **)
-
-val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (@{binding unoverload},
- fn (const, thm) => unoverload_impl const thm)));
-
-fun unoverload const thm = unoverload_oracle (const, thm);
-
-fun unoverload_attr const =
- Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
-
-val const = Args.context -- Args.term >>
- (fn (ctxt, tm) =>
- if not (Term.is_Const tm)
- then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
- else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
-
-val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
- (const >> unoverload_attr) "unoverload an uninterpreted constant"));
-
-end;
\ No newline at end of file
--- a/src/HOL/ROOT Thu Dec 08 15:11:20 2016 +0100
+++ b/src/HOL/ROOT Mon Dec 12 11:33:14 2016 +0100
@@ -38,7 +38,6 @@
Predicate_Compile_Quickcheck
Prefix_Order
Rewrite
- Types_To_Sets
(*conflicting type class instantiations*)
List_lexord
Sublist_Order
@@ -1021,6 +1020,17 @@
theories [condition = ISABELLE_SWIPL, quick_and_dirty]
Reg_Exp_Example
+session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
+ description {*
+ Experimental extension of Higher-Order Logic to allow translation of types to sets.
+ *}
+ options [document = false]
+ theories
+ Types_To_Sets
+ "Examples/Prerequisites"
+ "Examples/Finite"
+ "Examples/T2_Spaces"
+
session HOLCF (main timing) in HOLCF = HOL +
description {*
Author: Franz Regensburger
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Finite.thy Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,90 @@
+(* Title: HOL/Types_To_Sets/Examples/Finite.thy
+ Author: Ondřej Kunčar, TU München
+*)
+
+theory Finite
+ imports "../Types_To_Sets" Prerequisites
+begin
+
+section \<open>The Type-Based Theorem\<close>
+
+text\<open>This example file shows how we perform the relativization in presence of axiomatic
+ type classes: we internalize them.\<close>
+
+definition injective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ where "injective f \<equiv> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
+
+text\<open>We want to relativize the following type-based theorem using the type class finite.\<close>
+
+lemma type_based: "\<exists>f :: 'a::finite \<Rightarrow> nat. injective f"
+ unfolding injective_def
+ using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto
+
+section \<open>Definitions and Setup for The Relativization\<close>
+
+text\<open>We have to define what being injective on a set means.\<close>
+
+definition injective_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ where "injective_on A f \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. f x = f y \<longrightarrow> x = y"
+
+text\<open>The predicate injective_on is the relativization of the predicate injective.\<close>
+
+lemma injective_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total T"
+ assumes [transfer_rule]: "bi_unique T"
+ shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective"
+ unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
+
+text\<open>Similarly, we define the relativization of the internalization
+ of the type class finite, class.finite\<close>
+
+definition finite_on :: "'a set => bool" where "finite_on A = finite A"
+
+lemma class_finite_transfer[transfer_rule]:
+ assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
+ assumes [transfer_rule]: "bi_unique T"
+ shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
+ unfolding finite_on_def class.finite_def by transfer_prover
+
+text\<open>The aforementioned development can be automated. The main part is already automated
+ by the transfer_prover.\<close>
+
+section \<open>The Relativization to The Set-Based Theorem\<close>
+
+lemmas internalized = type_based[internalize_sort "'a::finite"]
+text\<open>We internalized the type class finite and thus reduced the task to the
+ original relativization algorithm.\<close>
+thm internalized
+
+text\<open>This is the set-based variant.\<close>
+
+lemma set_based:
+ assumes "(A::'a set) \<noteq> {}"
+ shows "finite_on A \<longrightarrow> (\<exists>f :: 'a \<Rightarrow> nat. injective_on A f)"
+proof -
+ {
+ text\<open>We define the type 'b to be isomorphic to A.\<close>
+ assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
+ from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
+ by auto
+
+ text\<open>Setup for the Transfer tool.\<close>
+ define cr_b where "cr_b == \<lambda>r a. r = rep a"
+ note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
+ note typedef_right_total[OF t cr_b_def, transfer_rule]
+ note typedef_bi_unique[OF t cr_b_def, transfer_rule]
+
+ have ?thesis
+ text\<open>Relativization by the Transfer tool.\<close>
+ using internalized[where 'a = 'b, untransferred, simplified]
+ by blast
+ } note * = this[cancel_type_definition, OF assms] text\<open>We removed the definition of 'b.\<close>
+
+ show ?thesis by (rule *)
+qed
+
+text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
+thm type_based set_based
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,25 @@
+(* Title: HOL/Types_To_Sets/Examples/Prerequisites.thy
+ Author: Ondřej Kunčar, TU München
+*)
+
+theory Prerequisites
+ imports Main
+begin
+
+context
+ fixes Rep Abs A T
+ assumes type: "type_definition Rep Abs A"
+ assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
+begin
+
+lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
+proof -
+ interpret type_definition Rep Abs A by(rule type)
+ show ?thesis
+ unfolding Domainp_iff[abs_def] T_def fun_eq_iff
+ by (metis Abs_inverse Rep)
+qed
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,162 @@
+(* Title: HOL/Types_To_Sets/Examples/T2_Spaces.thy
+ Author: Ondřej Kunčar, TU München
+*)
+
+theory T2_Spaces
+ imports Complex_Main "../Types_To_Sets" Prerequisites
+begin
+
+section \<open>The Type-Based Theorem\<close>
+
+text\<open>We relativize a theorem that contains a type class with an associated (overloaded) operation.
+ The key technique is to compile out the overloaded operation by the dictionary construction
+ using the Unoverloading rule.\<close>
+
+text\<open>This is the type-based statement that we want to relativize.\<close>
+thm compact_imp_closed
+text\<open>The type is class a T2 typological space.\<close>
+typ "'a :: t2_space"
+text\<open>The associated operation is the predicate open that determines the open sets in the T2 space.\<close>
+term "open"
+
+section \<open>Definitions and Setup for The Relativization\<close>
+
+text\<open>We gradually define relativization of topological spaces, t2 spaces, compact and closed
+ predicates and prove that they are indeed the relativization of the original predicates.\<close>
+
+definition topological_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
+ where "topological_space_on_with A \<equiv> \<lambda>open. open A \<and>
+ (\<forall>S \<subseteq> A. \<forall>T \<subseteq> A. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T))
+ \<and> (\<forall>K \<subseteq> Pow A. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union>K))"
+
+lemma topological_space_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total T" "bi_unique T"
+ shows "((rel_set T ===> op=) ===> op=) (topological_space_on_with (Collect (Domainp T)))
+ class.topological_space"
+ unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
+ apply transfer_prover_start
+ apply transfer_step+
+ unfolding Pow_def Ball_Collect[symmetric]
+ by blast
+
+definition t2_space_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> bool"
+ where "t2_space_on_with A \<equiv> \<lambda>open. topological_space_on_with A open \<and>
+ (\<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 = {}))"
+
+lemma t2_space_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total T" "bi_unique T"
+ shows "((rel_set T ===> op=) ===> op=) (t2_space_on_with (Collect (Domainp T))) class.t2_space"
+ unfolding t2_space_on_with_def[abs_def] class.t2_space_def[abs_def]
+ class.t2_space_axioms_def[abs_def]
+ apply transfer_prover_start
+ apply transfer_step+
+ unfolding Ball_Collect[symmetric]
+ by blast
+
+definition closed_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+ where "closed_with \<equiv> \<lambda>open S. open (- S)"
+
+lemma closed_closed_with: "closed s = closed_with open s"
+ unfolding closed_with_def closed_def[abs_def] ..
+
+definition closed_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+ where "closed_on_with A \<equiv> \<lambda>open S. open (-S \<inter> A)"
+
+lemma closed_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total T" "bi_unique T"
+ shows "((rel_set T ===> op=) ===> rel_set T===> op=) (closed_on_with (Collect (Domainp T)))
+ closed_with"
+ unfolding closed_with_def closed_on_with_def by transfer_prover
+
+definition compact_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+ 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))"
+
+lemma compact_compact_with: "compact s = compact_with open s"
+ unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
+
+definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+ 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>
+ (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
+
+lemma compact_on_with_subset_trans: "(\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open' c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
+ (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)) =
+ ((\<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)))"
+ by (meson subset_trans)
+
+lemma compact_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total T" "bi_unique T"
+ shows "((rel_set T ===> op=) ===> rel_set T===> op=) (compact_on_with (Collect (Domainp T)))
+ compact_with"
+ unfolding compact_with_def compact_on_with_def
+ apply transfer_prover_start
+ apply transfer_step+
+ unfolding compact_on_with_subset_trans
+ unfolding Pow_def Ball_Collect[symmetric] Ball_def Bex_def mem_Collect_eq
+ by blast
+
+setup \<open>Sign.add_const_constraint
+ (@{const_name "open"}, SOME @{typ "'a set \<Rightarrow> bool"})\<close>
+
+text\<open>The aforementioned development can be automated. The main part is already automated
+ by the transfer_prover.\<close>
+
+section \<open>The Relativization to The Set-Based Theorem\<close>
+
+text\<open>The first step of the dictionary construction.\<close>
+lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with]
+thm dictionary_first_step
+
+text\<open>Internalization of the type class t2_space.\<close>
+lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"]
+thm internalized_sort
+
+text\<open>We unoverload the overloaded constant open and thus finish compiling out of it.\<close>
+lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"]
+text\<open>The theorem with internalized type classes and compiled out operations is the starting point
+ for the original relativization algorithm.\<close>
+thm dictionary_second_step
+
+
+text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
+lemma compact_imp_closed_set_based:
+ assumes "(A::'a set) \<noteq> {}"
+ shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow>
+ closed_on_with A open S)"
+proof -
+ {
+ text\<open>We define the type 'b to be isomorphic to A.\<close>
+ assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
+ from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
+ by auto
+
+ text\<open>Setup for the Transfer tool.\<close>
+ define cr_b where "cr_b == \<lambda>r a. r = rep a"
+ note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
+ note typedef_right_total[OF t cr_b_def, transfer_rule]
+ note typedef_bi_unique[OF t cr_b_def, transfer_rule]
+
+ have ?thesis
+ text\<open>Relativization by the Transfer tool.\<close>
+ using dictionary_second_step[where 'a = 'b, untransferred, simplified]
+ by blast
+
+ } note * = this[cancel_type_definition, OF assms]
+
+ show ?thesis by (rule *)
+qed
+
+setup \<open>Sign.add_const_constraint
+ (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
+
+text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
+thm compact_imp_closed compact_imp_closed_set_based
+
+declare [[show_sorts]]
+text\<open>The Final Result. This time with explicitly shown type-class annotations.\<close>
+thm compact_imp_closed compact_imp_closed_set_based
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,27 @@
+(* Title: HOL/Types_To_Sets/Types_To_Sets.thy
+ Author: Ondřej Kunčar, TU München
+*)
+
+section \<open>From Types to Sets\<close>
+
+text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
+ to allow translation of types to sets as described in
+ O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
+ available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
+
+theory Types_To_Sets
+ imports Main
+begin
+
+subsection \<open>Rules\<close>
+
+text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
+ML_file "local_typedef.ML"
+
+text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
+ML_file "unoverloading.ML"
+
+text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
+ML_file "internalize_sort.ML"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,68 @@
+(* Title: HOL/Types_To_Sets/internalize_sort.ML
+ Author: Ondřej Kunčar, TU München
+
+A derived rule (by using Thm.unconstrainT) that internalizes
+type class annotations.
+*)
+
+
+(*
+ \<phi>['a::{c_1, ..., c_n} / 'a]
+---------------------------------------------------------------------
+ class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
+
+where class.c is the locale predicate associated with type class c and
+ops are operations associated with type class c. For example:
+If c = semigroup_add, then ops = op-, op+, 0, uminus.
+If c = finite, then ops = TYPE('a::type).
+*)
+
+signature INTERNALIZE_SORT =
+sig
+ val internalize_sort: ctyp -> thm -> typ * thm
+ val internalize_sort_attr: typ -> attribute
+end;
+
+structure Internalize_Sort : INTERNALIZE_SORT =
+struct
+
+fun internalize_sort ctvar thm =
+ let
+ val thy = Thm.theory_of_thm thm;
+ val tvar = Thm.typ_of ctvar;
+
+ val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
+
+ fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
+ fun reduce_to_non_proper_sort (TVar (name, sort)) =
+ TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
+ | reduce_to_non_proper_sort _ = error "not supported";
+
+ val data = (map fst classes) ~~ assms;
+
+ val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
+ then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
+ |> the_default tvar;
+
+ fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
+
+ fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
+
+ val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
+ then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
+ else discharge_of_class ren_tvar class) data;
+ in
+ (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
+ end;
+
+val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
+ | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
+
+fun internalize_sort_attr tvar =
+ Thm.rule_attribute [] (fn context => fn thm =>
+ (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
+ (tvar >> internalize_sort_attr) "internalize a sort"));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/local_typedef.ML Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,84 @@
+(* Title: HOL/Types_To_Sets/local_typedef.ML
+ Author: Ondřej Kunčar, TU München
+
+The Local Typedef Rule (extension of the logic).
+*)
+
+signature LOCAL_TYPEDEF =
+sig
+ val cancel_type_definition: thm -> thm
+ val cancel_type_definition_attr: attribute
+end;
+
+structure Local_Typedef : LOCAL_TYPEDEF =
+struct
+
+(*
+Local Typedef Rule (LT)
+
+ \<Gamma> \<turnstile> (\<exists>(Rep::\<beta> \<Rightarrow> \<tau>) Abs. type_definition Rep Abs A) \<Longrightarrow> \<phi>
+------------------------------------------------------------- [\<beta> not in \<phi>, \<Gamma>, A;
+ \<Gamma> \<turnstile> A \<noteq> \<emptyset> \<Longrightarrow> \<phi> sort(\<beta>)=HOL.type]
+*)
+
+(** BEGINNING OF THE CRITICAL CODE **)
+
+fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
+ (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
+ (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
+ (Abs_type, set)
+ | dest_typedef t = raise TERM ("dest_typedef", [t]);
+
+fun cancel_type_definition_cterm thm =
+ let
+ fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]);
+
+ val thy = Thm.theory_of_thm thm;
+ val prop = Thm.prop_of thm;
+ val hyps = Thm.hyps_of thm;
+
+ val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs";
+
+ val (typedef_assm, phi) = Logic.dest_implies prop
+ handle TERM _ => err "the theorem is not an implication";
+ val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef
+ handle TERM _ => err ("the assumption is not of the form "
+ ^ quote "\<exists>Rep Abs. type_definition Rep Abs A");
+
+ val (repT, absT) = Term.dest_funT abs_type;
+ val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable";
+ val (absT_name, sorts) = Term.dest_TVar absT;
+
+ val typeS = Sign.defaultS thy;
+ val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort "
+ ^ quote (Syntax.string_of_sort_global thy typeS));
+
+ fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts);
+ fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type "
+ ^ quote (fst absT_name));
+ val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion";
+ val _ = not (contains_absT set) orelse err_contains_absT_in "the set term";
+ (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *)
+ val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses";
+
+ val not_empty_assm = HOLogic.mk_Trueprop
+ (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT [])));
+ val prop = Logic.list_implies (hyps @ [not_empty_assm], phi);
+ in
+ Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm)
+ end;
+
+(** END OF THE CRITICAL CODE **)
+
+val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
+
+fun cancel_type_definition thm =
+ Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
+
+val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
+ (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/unoverloading.ML Mon Dec 12 11:33:14 2016 +0100
@@ -0,0 +1,140 @@
+(* Title: HOL/Types_To_Sets/unoverloading.ML
+ Author: Ondřej Kunčar, TU München
+
+The Unoverloading Rule (extension of the logic).
+*)
+
+signature UNOVERLOADING =
+sig
+ val unoverload: cterm -> thm -> thm
+ val unoverload_attr: cterm -> attribute
+end;
+
+structure Unoverloading : UNOVERLOADING =
+struct
+
+(*
+Unoverloading Rule (UO)
+
+ \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
+---------------------------- [no type or constant or type class in \<phi>
+ \<turnstile> \<And>x::\<sigma>. \<phi> depends on c::\<sigma>; c::\<sigma> is undefined]
+*)
+
+(* The following functions match_args, reduction and entries_of were
+ cloned from defs.ML and theory.ML because the functions are not public.
+ Notice that these functions already belong to the critical code.
+*)
+
+(* >= *)
+fun match_args (Ts, Us) =
+ if Type.could_matches (Ts, Us) then
+ Option.map Envir.subst_type
+ (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+ else NONE;
+
+fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
+ let
+ fun reduct Us (Ts, rhs) =
+ (case match_args (Ts, Us) of
+ NONE => NONE
+ | SOME subst => SOME (map (apsnd (map subst)) rhs));
+ fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
+
+ val reds = map (`reducts) deps;
+ val deps' =
+ if forall (is_none o #1) reds then NONE
+ else SOME (fold_rev
+ (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
+ in deps' end;
+
+fun const_and_typ_entries_of thy tm =
+ let
+ val consts =
+ fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
+ val types =
+ (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
+ in
+ consts @ types
+ end;
+
+
+(* The actual implementation *)
+
+(** BEGINNING OF THE CRITICAL CODE **)
+
+fun fold_atyps_classes f =
+ fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
+ | T as TVar (_, S) => fold (pair T #> f) S
+ (* just to avoid a warning about incomplete patterns *)
+ | _ => raise TERM ("fold_atyps_classes", []));
+
+fun class_entries_of thy tm =
+ let
+ val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
+ in
+ map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
+ end;
+
+fun unoverload_impl cconst thm =
+ let
+ fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
+
+ val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
+ val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
+
+ val prop = Thm.prop_of thm;
+ val prop_tfrees = rev (Term.add_tfree_names prop []);
+ val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
+ ^ commas_quote prop_tfrees);
+
+ val const = Thm.term_of cconst;
+ val _ = Term.is_Const const orelse err "the parameter is is not a constant";
+ val const_tfrees = rev (Term.add_tfree_names const []);
+ val _ = null const_tfrees orelse err ("the constant contains free type variables "
+ ^ commas_quote const_tfrees);
+
+ val thy = Thm.theory_of_thm thm;
+ val defs = Theory.defs_of thy;
+
+ val const_entry = Theory.const_dep thy (Term.dest_Const const);
+
+ val Uss = Defs.specifications_of defs (fst const_entry);
+ val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
+ orelse err "the constant instance has already a specification";
+
+ val context = Defs.global_context thy;
+ val prt_entry = Pretty.string_of o Defs.pretty_entry context;
+
+ fun dep_err (c, Ts) (d, Us) =
+ err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
+ fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
+ fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
+ orelse dep_err prop_entry const_entry;
+ val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
+ val _ = forall not_depends_on_const prop_entries;
+ in
+ Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
+ end;
+
+(** END OF THE CRITICAL CODE **)
+
+val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (@{binding unoverload},
+ fn (const, thm) => unoverload_impl const thm)));
+
+fun unoverload const thm = unoverload_oracle (const, thm);
+
+fun unoverload_attr const =
+ Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
+
+val const = Args.context -- Args.term >>
+ (fn (ctxt, tm) =>
+ if not (Term.is_Const tm)
+ then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
+ else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload}
+ (const >> unoverload_attr) "unoverload an uninterpreted constant"));
+
+end;