# HG changeset patch # User wenzelm # Date 1481560806 -3600 # Node ID 628b271c5b8bc8843cf43b6a36cac870ff4be167 # Parent 134ae7da2ccf29c1a6cb4008163868bc3d4ccb52# Parent 5d2cef77373c064ea204a15799e2e46be04eed3b merged diff -r 134ae7da2ccf -r 628b271c5b8b .hgtags --- a/.hgtags Sat Dec 10 17:22:47 2016 +0100 +++ b/.hgtags Mon Dec 12 17:40:06 2016 +0100 @@ -32,8 +32,4 @@ 8f4a332500e41bb67efc3e141608829473606a72 Isabelle2014 5ae2a2e74c93eafeb00b1ddeef0404256745ebba Isabelle2015 d3996d5873ddcf1115ec8d3d511a0bb5dbd1cfc4 Isabelle2016 -666c7475f4f7e9ba46c59170026230787c504ca7 Isabelle2016-1-RC0 -9ee2480d10b7404683aa7f4c3a30d44cbb6a21b9 Isabelle2016-1-RC1 -2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4 Isabelle2016-1-RC2 -51be997d0698583bf2d3f5a99f37381a146d3a6c Isabelle2016-1-RC3 -49708cffb98dc6ced89f66b10662e6af2808bebd Isabelle2016-1-RC4 +7aa3c52f27aade2cada22206cf0477b30a25f781 Isabelle2016-1 diff -r 134ae7da2ccf -r 628b271c5b8b ANNOUNCE --- a/ANNOUNCE Sat Dec 10 17:22:47 2016 +0100 +++ b/ANNOUNCE Mon Dec 12 17:40:06 2016 +0100 @@ -4,7 +4,7 @@ Isabelle2016-1 is now available. This version introduces significant changes over Isabelle2016: see the NEWS -file for further details. Some notable changes: +file for further details. Some notable points: * Improved Isabelle/jEdit Prover IDE: more support for formal text structure, more visual feedback. diff -r 134ae7da2ccf -r 628b271c5b8b CONTRIBUTORS --- a/CONTRIBUTORS Sat Dec 10 17:22:47 2016 +0100 +++ b/CONTRIBUTORS Mon Dec 12 17:40:06 2016 +0100 @@ -10,6 +10,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. diff -r 134ae7da2ccf -r 628b271c5b8b NEWS --- a/NEWS Sat Dec 10 17:22:47 2016 +0100 +++ b/NEWS Mon Dec 12 17:40:06 2016 +0100 @@ -949,6 +949,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 *** diff -r 134ae7da2ccf -r 628b271c5b8b src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Dec 10 17:22:47 2016 +0100 +++ b/src/Doc/JEdit/JEdit.thy Mon Dec 12 17:40:06 2016 +0100 @@ -723,6 +723,11 @@ The above options are accessible in the menu \<^emph>\Plugins / Plugin Options / Isabelle / General\. + + \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That + can be purged manually with the jEdit action @{action "remove-trailing-ws"} + (shortcut \<^verbatim>\C+e r\). Moreover, the \<^emph>\WhiteSpace\ plugin provides some + aggressive options to trim whitespace on buffer-save. \ diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Sat Dec 10 17:22:47 2016 +0100 +++ b/src/HOL/Decision_Procs/approximation.ML Mon Dec 12 17:40:06 2016 +0100 @@ -43,7 +43,7 @@ end fun approximation_conv ctxt ct = - approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); + approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct); fun approximate ctxt t = approximation_oracle (Proof_Context.theory_of ctxt, t) diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Library/Types_To_Sets.thy --- a/src/HOL/Library/Types_To_Sets.thy Sat Dec 10 17:22:47 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 \From Types to Sets\ - -text \This theory extends Isabelle/HOL's logic by two new inference rules - to allow translation of types to sets as described in - O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic - available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\ - -theory Types_To_Sets - imports Main -begin - -subsection \Rules\ - -text\The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\ -ML_file "Types_To_Sets/local_typedef.ML" - -text\The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\ -ML_file "Types_To_Sets/unoverloading.ML" - -text\The following file implements a derived rule that internalizes type class annotations.\ -ML_file "Types_To_Sets/internalize_sort.ML" - -end \ No newline at end of file diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Library/Types_To_Sets/internalize_sort.ML --- a/src/HOL/Library/Types_To_Sets/internalize_sort.ML Sat Dec 10 17:22:47 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. -*) - - -(* - \['a::{c_1, ..., c_n} / 'a] ---------------------------------------------------------------------- - class.c_1 ops_1 \ ... \ class.c_n ops_n \ \['a::type / 'a] - -where class.c is the locale predicate associated with type class c and -ops are operations associated with type class c. For example: -If c = semigroup_add, then ops = op-, op+, 0, uminus. -If c = finite, then ops = TYPE('a::type). -*) - -signature INTERNALIZE_SORT = -sig - val internalize_sort: ctyp -> thm -> typ * thm - val internalize_sort_attr: typ -> attribute -end; - -structure Internalize_Sort : INTERNALIZE_SORT = -struct - -fun internalize_sort ctvar thm = - let - val thy = Thm.theory_of_thm thm; - val tvar = Thm.typ_of ctvar; - - val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm); - - fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) - fun reduce_to_non_proper_sort (TVar (name, sort)) = - TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort))) - | reduce_to_non_proper_sort _ = error "not supported"; - - val data = (map fst classes) ~~ assms; - - val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' - then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data - |> the_default tvar; - - fun localify class = Class.rules thy class |> snd |> Thm.transfer thy; - - fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class); - - val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' - then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class) - else discharge_of_class ren_tvar class) data; - in - (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes) - end; - -val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v - | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t)); - -fun internalize_sort_attr tvar = - Thm.rule_attribute [] (fn context => fn thm => - (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm))); - -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort} - (tvar >> internalize_sort_attr) "internalize a sort")); - -end; \ No newline at end of file diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Library/Types_To_Sets/local_typedef.ML --- a/src/HOL/Library/Types_To_Sets/local_typedef.ML Sat Dec 10 17:22:47 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) - - \ \ (\(Rep::\ \ \) Abs. type_definition Rep Abs A) \ \ -------------------------------------------------------------- [\ not in \, \, A; - \ \ A \ \ \ \ sort(\)=HOL.type] -*) - -(** BEGINNING OF THE CRITICAL CODE **) - -fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _, - (Const (@{const_name Ex}, _) $ Abs (_, Abs_type, - (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) = - (Abs_type, set) - | dest_typedef t = raise TERM ("dest_typedef", [t]); - -fun cancel_type_definition_cterm thm = - let - fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]); - - val thy = Thm.theory_of_thm thm; - val prop = Thm.prop_of thm; - val hyps = Thm.hyps_of thm; - - val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs"; - - val (typedef_assm, phi) = Logic.dest_implies prop - handle TERM _ => err "the theorem is not an implication"; - val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef - handle TERM _ => err ("the assumption is not of the form " - ^ quote "\Rep Abs. type_definition Rep Abs A"); - - val (repT, absT) = Term.dest_funT abs_type; - val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable"; - val (absT_name, sorts) = Term.dest_TVar absT; - - val typeS = Sign.defaultS thy; - val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort " - ^ quote (Syntax.string_of_sort_global thy typeS)); - - fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts); - fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type " - ^ quote (fst absT_name)); - val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion"; - val _ = not (contains_absT set) orelse err_contains_absT_in "the set term"; - (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *) - val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses"; - - val not_empty_assm = HOLogic.mk_Trueprop - (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT []))); - val prop = Logic.list_implies (hyps @ [not_empty_assm], phi); - in - Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm) - end; - -(** END OF THE CRITICAL CODE **) - -val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm))); - -fun cancel_type_definition thm = - Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm)); - -val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition); - -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition} - (Scan.succeed cancel_type_definition_attr) "cancel a local type definition")); - -end; \ No newline at end of file diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Library/Types_To_Sets/unoverloading.ML --- a/src/HOL/Library/Types_To_Sets/unoverloading.ML Sat Dec 10 17:22:47 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) - - \ \[c::\ / x::\] ----------------------------- [no type or constant or type class in \ - \ \x::\. \ depends on c::\; c::\ is undefined] -*) - -(* The following functions match_args, reduction and entries_of were - cloned from defs.ML and theory.ML because the functions are not public. - Notice that these functions already belong to the critical code. -*) - -(* >= *) -fun match_args (Ts, Us) = - if Type.could_matches (Ts, Us) then - Option.map Envir.subst_type - (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE) - else NONE; - -fun reduction defs (deps : Defs.entry list) : Defs.entry list option = - let - fun reduct Us (Ts, rhs) = - (case match_args (Ts, Us) of - NONE => NONE - | SOME subst => SOME (map (apsnd (map subst)) rhs)); - fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d); - - val reds = map (`reducts) deps; - val deps' = - if forall (is_none o #1) reds then NONE - else SOME (fold_rev - (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); - in deps' end; - -fun const_and_typ_entries_of thy tm = - let - val consts = - fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm []; - val types = - (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm []; - in - consts @ types - end; - -(* The actual implementation *) - -(** BEGINNING OF THE CRITICAL CODE **) - -fun fold_atyps_classes f = - fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S - | T as TVar (_, S) => fold (pair T #> f) S - (* just to avoid a warning about incomplete patterns *) - | _ => raise TERM ("fold_atyps_classes", [])); - -fun class_entries_of thy tm = - let - val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm []; - in - map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes - end; - -fun unoverload_impl cconst thm = - let - fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]); - - val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses"; - val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs"; - - val prop = Thm.prop_of thm; - val prop_tfrees = rev (Term.add_tfree_names prop []); - val _ = null prop_tfrees orelse err ("the theorem contains free type variables " - ^ commas_quote prop_tfrees); - - val const = Thm.term_of cconst; - val _ = Term.is_Const const orelse err "the parameter is is not a constant"; - val const_tfrees = rev (Term.add_tfree_names const []); - val _ = null const_tfrees orelse err ("the constant contains free type variables " - ^ commas_quote const_tfrees); - - val thy = Thm.theory_of_thm thm; - val defs = Theory.defs_of thy; - - val const_entry = Theory.const_dep thy (Term.dest_Const const); - - val Uss = Defs.specifications_of defs (fst const_entry); - val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss - orelse err "the constant instance has already a specification"; - - val context = Defs.global_context thy; - val prt_entry = Pretty.string_of o Defs.pretty_entry context; - - fun dep_err (c, Ts) (d, Us) = - err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us)); - fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these; - fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry) - orelse dep_err prop_entry const_entry; - val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop; - val _ = forall not_depends_on_const prop_entries; - in - Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm) - end; - -(** END OF THE CRITICAL CODE **) - -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (@{binding unoverload}, - fn (const, thm) => unoverload_impl const thm))); - -fun unoverload const thm = unoverload_oracle (const, thm); - -fun unoverload_attr const = - Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm)); - -val const = Args.context -- Args.term >> - (fn (ctxt, tm) => - if not (Term.is_Const tm) - then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm) - else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt); - -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload} - (const >> unoverload_attr) "unoverload an uninterpreted constant")); - -end; \ No newline at end of file diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/ROOT --- a/src/HOL/ROOT Sat Dec 10 17:22:47 2016 +0100 +++ b/src/HOL/ROOT Mon Dec 12 17:40:06 2016 +0100 @@ -38,7 +38,6 @@ Predicate_Compile_Quickcheck Prefix_Order Rewrite - Types_To_Sets (*conflicting type class instantiations*) List_lexord Sublist_Order @@ -1018,6 +1017,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 diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/Examples/Finite.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/Examples/Finite.thy Mon Dec 12 17:40:06 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 \The Type-Based Theorem\ + +text\This example file shows how we perform the relativization in presence of axiomatic + type classes: we internalize them.\ + +definition injective :: "('a \ 'b) \ bool" + where "injective f \ (\x y. f x = f y \ x = y)" + +text\We want to relativize the following type-based theorem using the type class finite.\ + +lemma type_based: "\f :: 'a::finite \ nat. injective f" + unfolding injective_def + using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto + +section \Definitions and Setup for The Relativization\ + +text\We have to define what being injective on a set means.\ + +definition injective_on :: "'a set \ ('a \ 'b) \ bool" + where "injective_on A f \ \x \ A. \y \ A. f x = f y \ x = y" + +text\The predicate injective_on is the relativization of the predicate injective.\ + +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\Similarly, we define the relativization of the internalization + of the type class finite, class.finite\ + +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\'b\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\The aforementioned development can be automated. The main part is already automated + by the transfer_prover.\ + +section \The Relativization to The Set-Based Theorem\ + +lemmas internalized = type_based[internalize_sort "'a::finite"] +text\We internalized the type class finite and thus reduced the task to the + original relativization algorithm.\ +thm internalized + +text\This is the set-based variant.\ + +lemma set_based: + assumes "(A::'a set) \ {}" + shows "finite_on A \ (\f :: 'a \ nat. injective_on A f)" +proof - + { + text\We define the type 'b to be isomorphic to A.\ + assume T: "\(Rep :: 'b \ 'a) Abs. type_definition Rep Abs A" + from T obtain rep :: "'b \ 'a" and abs :: "'a \ 'b" where t: "type_definition rep abs A" + by auto + + text\Setup for the Transfer tool.\ + define cr_b where "cr_b == \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\Relativization by the Transfer tool.\ + using internalized[where 'a = 'b, untransferred, simplified] + by blast + } note * = this[cancel_type_definition, OF assms] text\We removed the definition of 'b.\ + + show ?thesis by (rule *) +qed + +text\The Final Result. We can compare the type-based and the set-based statement.\ +thm type_based set_based + +end diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/Examples/Prerequisites.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Mon Dec 12 17:40:06 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 \ (\(x::'a) (y::'b). x = Rep y)" +begin + +lemma type_definition_Domainp: "Domainp T = (\x. x \ 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 diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/Examples/T2_Spaces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Mon Dec 12 17:40:06 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 \The Type-Based Theorem\ + +text\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.\ + +text\This is the type-based statement that we want to relativize.\ +thm compact_imp_closed +text\The type is class a T2 typological space.\ +typ "'a :: t2_space" +text\The associated operation is the predicate open that determines the open sets in the T2 space.\ +term "open" + +section \Definitions and Setup for The Relativization\ + +text\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.\ + +definition topological_space_on_with :: "'a set \ ('a set \ bool) \ bool" + where "topological_space_on_with A \ \open. open A \ + (\S \ A. \T \ A. open S \ open T \ open (S \ T)) + \ (\K \ Pow A. (\S\K. open S) \ open (\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 \ ('a set \ bool) \ bool" + where "t2_space_on_with A \ \open. topological_space_on_with A open \ + (\x \ A. \y \ A. x \ y \ (\U\A. \V\A. open U \ open V \ x \ U \ y \ V \ U \ 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 \ bool) \ 'a set \ bool" + where "closed_with \ \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 \ ('a set \ bool) \ 'a set \ bool" + where "closed_on_with A \ \open S. open (-S \ 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 \ bool) \ 'a set \ bool" + where "compact_with \ \open S. (\C. (\c\C. open c) \ S \ \C \ (\D\C. finite D \ S \ \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 \ ('a set \ bool) \ 'a set \ bool" + where "compact_on_with A \ \open S. (\C\Pow A. (\c\C. open c) \ S \ \C \ + (\D\C. finite D \ S \ \D))" + +lemma compact_on_with_subset_trans: "(\C\Pow A. (\c\C. open' c) \ S \ \C \ + (\D\C. finite D \ S \ \D)) = + ((\C\Pow A. (\c\C. open' c) \ S \ \C \ (\D\Pow A. D\C \ finite D \ S \ \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 \Sign.add_const_constraint + (@{const_name "open"}, SOME @{typ "'a set \ bool"})\ + +text\The aforementioned development can be automated. The main part is already automated + by the transfer_prover.\ + +section \The Relativization to The Set-Based Theorem\ + +text\The first step of the dictionary construction.\ +lemmas dictionary_first_step = compact_imp_closed[unfolded compact_compact_with closed_closed_with] +thm dictionary_first_step + +text\Internalization of the type class t2_space.\ +lemmas internalized_sort = dictionary_first_step[internalize_sort "'a::t2_space"] +thm internalized_sort + +text\We unoverload the overloaded constant open and thus finish compiling out of it.\ +lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \ bool"] +text\The theorem with internalized type classes and compiled out operations is the starting point + for the original relativization algorithm.\ +thm dictionary_second_step + + +text\This is the set-based variant of the theorem compact_imp_closed.\ +lemma compact_imp_closed_set_based: + assumes "(A::'a set) \ {}" + shows "\open. t2_space_on_with A open \ (\S\A. compact_on_with A open S \ + closed_on_with A open S)" +proof - + { + text\We define the type 'b to be isomorphic to A.\ + assume T: "\(Rep :: 'b \ 'a) Abs. type_definition Rep Abs A" + from T obtain rep :: "'b \ 'a" and abs :: "'a \ 'b" where t: "type_definition rep abs A" + by auto + + text\Setup for the Transfer tool.\ + define cr_b where "cr_b == \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\Relativization by the Transfer tool.\ + using dictionary_second_step[where 'a = 'b, untransferred, simplified] + by blast + + } note * = this[cancel_type_definition, OF assms] + + show ?thesis by (rule *) +qed + +setup \Sign.add_const_constraint + (@{const_name "open"}, SOME @{typ "'a::topological_space set \ bool"})\ + +text\The Final Result. We can compare the type-based and the set-based statement.\ +thm compact_imp_closed compact_imp_closed_set_based + +declare [[show_sorts]] +text\The Final Result. This time with explicitly shown type-class annotations.\ +thm compact_imp_closed compact_imp_closed_set_based + +end diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/Types_To_Sets.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Mon Dec 12 17:40:06 2016 +0100 @@ -0,0 +1,27 @@ +(* Title: HOL/Types_To_Sets/Types_To_Sets.thy + Author: Ondřej Kunčar, TU München +*) + +section \From Types to Sets\ + +text \This theory extends Isabelle/HOL's logic by two new inference rules + to allow translation of types to sets as described in + O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic + available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\ + +theory Types_To_Sets + imports Main +begin + +subsection \Rules\ + +text\The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\ +ML_file "local_typedef.ML" + +text\The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\ +ML_file "unoverloading.ML" + +text\The following file implements a derived rule that internalizes type class annotations.\ +ML_file "internalize_sort.ML" + +end diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/internalize_sort.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML Mon Dec 12 17:40:06 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. +*) + + +(* + \['a::{c_1, ..., c_n} / 'a] +--------------------------------------------------------------------- + class.c_1 ops_1 \ ... \ class.c_n ops_n \ \['a::type / 'a] + +where class.c is the locale predicate associated with type class c and +ops are operations associated with type class c. For example: +If c = semigroup_add, then ops = op-, op+, 0, uminus. +If c = finite, then ops = TYPE('a::type). +*) + +signature INTERNALIZE_SORT = +sig + val internalize_sort: ctyp -> thm -> typ * thm + val internalize_sort_attr: typ -> attribute +end; + +structure Internalize_Sort : INTERNALIZE_SORT = +struct + +fun internalize_sort ctvar thm = + let + val thy = Thm.theory_of_thm thm; + val tvar = Thm.typ_of ctvar; + + val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm); + + fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) + fun reduce_to_non_proper_sort (TVar (name, sort)) = + TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort))) + | reduce_to_non_proper_sort _ = error "not supported"; + + val data = (map fst classes) ~~ assms; + + val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' + then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data + |> the_default tvar; + + fun localify class = Class.rules thy class |> snd |> Thm.transfer thy; + + fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class); + + val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' + then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class) + else discharge_of_class ren_tvar class) data; + in + (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes) + end; + +val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v + | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t)); + +fun internalize_sort_attr tvar = + Thm.rule_attribute [] (fn context => fn thm => + (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm))); + +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort} + (tvar >> internalize_sort_attr) "internalize a sort")); + +end; diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/local_typedef.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/local_typedef.ML Mon Dec 12 17:40:06 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) + + \ \ (\(Rep::\ \ \) Abs. type_definition Rep Abs A) \ \ +------------------------------------------------------------- [\ not in \, \, A; + \ \ A \ \ \ \ sort(\)=HOL.type] +*) + +(** BEGINNING OF THE CRITICAL CODE **) + +fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _, + (Const (@{const_name Ex}, _) $ Abs (_, Abs_type, + (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) = + (Abs_type, set) + | dest_typedef t = raise TERM ("dest_typedef", [t]); + +fun cancel_type_definition_cterm thm = + let + fun err msg = raise THM ("cancel_type_definition: " ^ msg, 0, [thm]); + + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; + val hyps = Thm.hyps_of thm; + + val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unsolved flex-flex pairs"; + + val (typedef_assm, phi) = Logic.dest_implies prop + handle TERM _ => err "the theorem is not an implication"; + val (abs_type, set) = typedef_assm |> HOLogic.dest_Trueprop |> dest_typedef + handle TERM _ => err ("the assumption is not of the form " + ^ quote "\Rep Abs. type_definition Rep Abs A"); + + val (repT, absT) = Term.dest_funT abs_type; + val _ = Term.is_TVar absT orelse err "the abstract type is not a schematic type variable"; + val (absT_name, sorts) = Term.dest_TVar absT; + + val typeS = Sign.defaultS thy; + val _ = sorts = typeS orelse err ("the type " ^ quote (fst absT_name) ^ " is not of the sort " + ^ quote (Syntax.string_of_sort_global thy typeS)); + + fun contains_absT tm = member (op=) (Term.add_tvars tm []) (absT_name, sorts); + fun err_contains_absT_in msg = err (msg ^ " contains the forbidden type " + ^ quote (fst absT_name)); + val _ = not (contains_absT phi) orelse err_contains_absT_in "the conclusion"; + val _ = not (contains_absT set) orelse err_contains_absT_in "the set term"; + (* the following test is superfluous; the meta hypotheses cannot currently contain TVars *) + val _ = not (exists contains_absT hyps) orelse err_contains_absT_in "one of the hypotheses"; + + val not_empty_assm = HOLogic.mk_Trueprop + (HOLogic.mk_not (HOLogic.mk_eq (set, HOLogic.mk_set repT []))); + val prop = Logic.list_implies (hyps @ [not_empty_assm], phi); + in + Thm.global_cterm_of thy prop |> Thm.weaken_sorts (Thm.shyps_of thm) + end; + +(** END OF THE CRITICAL CODE **) + +val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result + (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm))); + +fun cancel_type_definition thm = + Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm)); + +val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition); + +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition} + (Scan.succeed cancel_type_definition_attr) "cancel a local type definition")); + +end; diff -r 134ae7da2ccf -r 628b271c5b8b src/HOL/Types_To_Sets/unoverloading.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Types_To_Sets/unoverloading.ML Mon Dec 12 17:40:06 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) + + \ \[c::\ / x::\] +---------------------------- [no type or constant or type class in \ + \ \x::\. \ depends on c::\; c::\ is undefined] +*) + +(* The following functions match_args, reduction and entries_of were + cloned from defs.ML and theory.ML because the functions are not public. + Notice that these functions already belong to the critical code. +*) + +(* >= *) +fun match_args (Ts, Us) = + if Type.could_matches (Ts, Us) then + Option.map Envir.subst_type + (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE) + else NONE; + +fun reduction defs (deps : Defs.entry list) : Defs.entry list option = + let + fun reduct Us (Ts, rhs) = + (case match_args (Ts, Us) of + NONE => NONE + | SOME subst => SOME (map (apsnd (map subst)) rhs)); + fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d); + + val reds = map (`reducts) deps; + val deps' = + if forall (is_none o #1) reds then NONE + else SOME (fold_rev + (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); + in deps' end; + +fun const_and_typ_entries_of thy tm = + let + val consts = + fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm []; + val types = + (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm []; + in + consts @ types + end; + + +(* The actual implementation *) + +(** BEGINNING OF THE CRITICAL CODE **) + +fun fold_atyps_classes f = + fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S + | T as TVar (_, S) => fold (pair T #> f) S + (* just to avoid a warning about incomplete patterns *) + | _ => raise TERM ("fold_atyps_classes", [])); + +fun class_entries_of thy tm = + let + val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm []; + in + map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes + end; + +fun unoverload_impl cconst thm = + let + fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]); + + val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses"; + val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs"; + + val prop = Thm.prop_of thm; + val prop_tfrees = rev (Term.add_tfree_names prop []); + val _ = null prop_tfrees orelse err ("the theorem contains free type variables " + ^ commas_quote prop_tfrees); + + val const = Thm.term_of cconst; + val _ = Term.is_Const const orelse err "the parameter is is not a constant"; + val const_tfrees = rev (Term.add_tfree_names const []); + val _ = null const_tfrees orelse err ("the constant contains free type variables " + ^ commas_quote const_tfrees); + + val thy = Thm.theory_of_thm thm; + val defs = Theory.defs_of thy; + + val const_entry = Theory.const_dep thy (Term.dest_Const const); + + val Uss = Defs.specifications_of defs (fst const_entry); + val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss + orelse err "the constant instance has already a specification"; + + val context = Defs.global_context thy; + val prt_entry = Pretty.string_of o Defs.pretty_entry context; + + fun dep_err (c, Ts) (d, Us) = + err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us)); + fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these; + fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry) + orelse dep_err prop_entry const_entry; + val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop; + val _ = forall not_depends_on_const prop_entries; + in + Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm) + end; + +(** END OF THE CRITICAL CODE **) + +val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result + (Thm.add_oracle (@{binding unoverload}, + fn (const, thm) => unoverload_impl const thm))); + +fun unoverload const thm = unoverload_oracle (const, thm); + +fun unoverload_attr const = + Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm)); + +val const = Args.context -- Args.term >> + (fn (ctxt, tm) => + if not (Term.is_Const tm) + then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm) + else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt); + +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload} + (const >> unoverload_attr) "unoverload an uninterpreted constant")); + +end; diff -r 134ae7da2ccf -r 628b271c5b8b src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Sat Dec 10 17:22:47 2016 +0100 +++ b/src/Tools/misc_legacy.ML Mon Dec 12 17:40:06 2016 +0100 @@ -201,26 +201,10 @@ (false, relift st, Thm.nprems_of st) gno state in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; -fun print_vars_terms ctxt n thm = - let - fun typed s ty = " " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty; - fun find_vars (Const (c, ty)) = - if null (Term.add_tvarsT ty []) then I - else insert (op =) (typed c ty) - | find_vars (Var (xi, ty)) = - insert (op =) (typed (Term.string_of_vname xi) ty) - | find_vars (Free _) = I - | find_vars (Bound _) = I - | find_vars (Abs (_, _, t)) = find_vars t - | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2; - val prem = Logic.nth_prem (n, Thm.prop_of thm) - val tms = find_vars prem [] - in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; - in fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm - handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty) + handle THM ("assume: variables", _, _) => Seq.empty end;