# HG changeset patch # User wenzelm # Date 1530303273 -7200 # Node ID 549a4992222f71f7cf7f8777cd50199ae5cadfca # Parent 4d09df93d1a23383b323b59c13e332b7ce35a77f# Parent 34d732a83767a39885716955af00946d9418d9f8 merged; diff -r 4d09df93d1a2 -r 549a4992222f ANNOUNCE --- a/ANNOUNCE Fri Jun 29 15:22:30 2018 +0100 +++ b/ANNOUNCE Fri Jun 29 22:14:33 2018 +0200 @@ -4,9 +4,25 @@ Isabelle2018 is now available. This version introduces many changes over Isabelle2017: see the NEWS -file for further details. Some notable points: +file for further details. Here are the main points: + +* Improved infix notation within terms. + +* Improved syntax for formal comments, within terms and other languages. + +* Improved management of ROOT files and session-qualified theories. + +* Various improvements of document preparation. -* FIXME. +* Many Isabelle/jEdit improvements, including semantic IDE for Bibtex. + +* Numerous HOL library improvements, including HOL-Algebra. + +* Substantial additions to HOL-Analysis. + +* Isabelle server for reactive communication with other programs. + +* More uniform 64-bit platform support: smaller Isabelle application. You may get Isabelle2018 from the following mirror sites: diff -r 4d09df93d1a2 -r 549a4992222f Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Fri Jun 29 15:22:30 2018 +0100 +++ b/Admin/Release/CHECKLIST Fri Jun 29 22:14:33 2018 +0200 @@ -5,6 +5,14 @@ - check Admin/components; +- test "isabelle dump -l Pure ZF"; + +- test "isabelle -o export_theory -f ZF"; + +- test "isabelle server" according to "system" manual; + +- test Isabelle/VSCode; + - test Isabelle/jEdit: print buffer - test "#!/usr/bin/env isabelle_scala_script"; diff -r 4d09df93d1a2 -r 549a4992222f CONTRIBUTORS --- a/CONTRIBUTORS Fri Jun 29 15:22:30 2018 +0100 +++ b/CONTRIBUTORS Fri Jun 29 22:14:33 2018 +0200 @@ -15,6 +15,10 @@ * June 2018: Wenda Li New/strengthened results involving analysis, topology, etc. +* May/June 2018: Makarius Wenzel + System infrastructure to export blobs as theory presentation, and to dump + PIDE database content in batch mode. + * May 2018: Manuel Eberl Landau symbols and asymptotic equivalence (moved from the AFP). diff -r 4d09df93d1a2 -r 549a4992222f NEWS --- a/NEWS Fri Jun 29 15:22:30 2018 +0100 +++ b/NEWS Fri Jun 29 22:14:33 2018 +0200 @@ -19,6 +19,11 @@ FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". +* Global facts need to be closed: no free variables, no hypotheses, no +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be +allowed via "declare [[pending_shyps]]" in the global theory context, +but it should be reset to false afterwards. + * Marginal comments need to be written exclusively in the new-style form "\ \text\", old ASCII variants like "-- {* ... *}" are no longer supported. INCOMPATIBILITY, use the command-line tool "isabelle @@ -31,13 +36,13 @@ * The "op " syntax for infix operators has been replaced by "()". If begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. -INCOMPATIBILITY. -There is an Isabelle tool "update_op" that converts theory and ML files -to the new syntax. Because it is based on regular expression matching, -the result may need a bit of manual postprocessing. Invoking "isabelle -update_op" converts all files in the current directory (recursively). -In case you want to exclude conversion of ML files (because the tool -frequently also converts ML's "op" syntax), use option "-m". +INCOMPATIBILITY, use the command-line tool "isabelle update_op" to +convert theory and ML files to the new syntax. Because it is based on +regular expression matching, the result may need a bit of manual +postprocessing. Invoking "isabelle update_op" converts all files in the +current directory (recursively). In case you want to exclude conversion +of ML files (because the tool frequently also converts ML's "op" +syntax), use option "-m". * Theory header 'abbrevs' specifications need to be separated by 'and'. INCOMPATIBILITY. @@ -80,11 +85,15 @@ - option -A specifies an alternative ancestor session for options -R and -S + - option -i includes additional sessions into the name-space of + theories + Examples: isabelle jedit -R HOL-Number_Theory isabelle jedit -R HOL-Number_Theory -A HOL isabelle jedit -d '$AFP' -S Formal_SSA -A HOL isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis + isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL * PIDE markup for session ROOT files: allows to complete session names, follow links to theories and document files etc. @@ -119,14 +128,14 @@ plain-text document draft. Both are available via the menu "Plugins / Isabelle". -* Bibtex database files (.bib) are semantically checked. - * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle is only used if there is no conflict with existing Unicode sequences in the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle symbols remain in literal \ form. This avoids accidental loss of Unicode content when saving the file. +* Bibtex database files (.bib) are semantically checked. + * Update to jedit-5.5.0, the latest release. @@ -198,6 +207,12 @@ Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with object-logic equality or equivalence. + +*** Pure *** + +* The inner syntax category "sort" now includes notation "_" for the +dummy sort: it is effectively ignored in type-inference. + * Rewrites clauses (keyword 'rewrites') were moved into the locale expression syntax, where they are part of locale instances. In interpretation commands rewrites clauses now need to occur before 'for' @@ -209,17 +224,11 @@ locale instances where the qualifier's sole purpose is avoiding duplicate constant declarations. -* Proof method 'simp' now supports a new modifier 'flip:' followed by a list -of theorems. Each of these theorems is removed from the simpset -(without warning if it is not there) and the symmetric version of the theorem -(i.e. lhs and rhs exchanged) is added to the simpset. -For 'auto' and friends the modifier is "simp flip:". - - -*** Pure *** - -* The inner syntax category "sort" now includes notation "_" for the -dummy sort: it is effectively ignored in type-inference. +* Proof method "simp" now supports a new modifier "flip:" followed by a +list of theorems. Each of these theorems is removed from the simpset +(without warning if it is not there) and the symmetric version of the +theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" +and friends the modifier is "simp flip:". *** HOL *** @@ -382,12 +391,12 @@ * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new infix/prefix notation. -* Session HOL-Algebra: Revamped with much new material. -The set of isomorphisms between two groups is now denoted iso rather than iso_set. -INCOMPATIBILITY. - -* Session HOL-Analysis: the Arg function now respects the same interval as -Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. +* Session HOL-Algebra: revamped with much new material. The set of +isomorphisms between two groups is now denoted iso rather than iso_set. +INCOMPATIBILITY. + +* Session HOL-Analysis: the Arg function now respects the same interval +as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. INCOMPATIBILITY. * Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined. @@ -398,10 +407,9 @@ Riemann mapping theorem, the Vitali covering theorem, change-of-variables results for integration and measures. -* Session HOL-Types_To_Sets: more tool support -(unoverload_type combines internalize_sorts and unoverload) and larger -experimental application (type based linear algebra transferred to linear -algebra on subspaces). +* Session HOL-Types_To_Sets: more tool support (unoverload_type combines +internalize_sorts and unoverload) and larger experimental application +(type based linear algebra transferred to linear algebra on subspaces). *** ML *** diff -r 4d09df93d1a2 -r 549a4992222f src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Doc/Implementation/Logic.thy Fri Jun 29 22:14:33 2018 +0200 @@ -862,9 +862,13 @@ class empty = assumes bad: "\(x::'a) y. x \ y" +declare [[pending_shyps]] + theorem (in empty) false: False using bad by blast +declare [[pending_shyps = false]] + ML_val \@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\ text \ diff -r 4d09df93d1a2 -r 549a4992222f src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Doc/JEdit/JEdit.thy Fri Jun 29 22:14:33 2018 +0200 @@ -237,6 +237,7 @@ -b build only -d DIR include session directory -f fresh build + -i NAME include session in name-space of theories -j OPTION add jEdit runtime option (default $JEDIT_OPTIONS) -l NAME logic image name @@ -266,6 +267,9 @@ ancestor session for options \<^verbatim>\-R\ and \<^verbatim>\-S\: this allows to restructure the hierarchy of session images on the spot. + The \<^verbatim>\-i\ option includes additional sessions into the name-space of + theories: multiple occurrences are possible. + The \<^verbatim>\-m\ option specifies additional print modes for the prover process. Note that the system option @{system_option_ref jedit_print_mode} allows to do the same persistently (e.g.\ via the \<^emph>\Plugin Options\ dialog of diff -r 4d09df93d1a2 -r 549a4992222f src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Doc/System/Environment.thy Fri Jun 29 22:14:33 2018 +0200 @@ -407,6 +407,7 @@ Options are: -d DIR include session directory + -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC) -m MODE add print mode for output -n no build of session image on startup @@ -421,6 +422,9 @@ Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is checked and built on demand, but the option \<^verbatim>\-n\ skips that. + Option \<^verbatim>\-i\ includes additional sessions into the name-space of theories: + multiple occurrences are possible. + Option \<^verbatim>\-r\ indicates a bootstrap from the raw Poly/ML system, which is relevant for Isabelle/Pure development. diff -r 4d09df93d1a2 -r 549a4992222f src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/FOL/ex/Miniscope.thy Fri Jun 29 22:14:33 2018 +0200 @@ -17,14 +17,19 @@ subsubsection \de Morgan laws\ -lemma demorgans: +lemma demorgans1: "\ (P \ Q) \ \ P \ \ Q" "\ (P \ Q) \ \ P \ \ Q" "\ \ P \ P" + by blast+ + +lemma demorgans2: "\P. \ (\x. P(x)) \ (\x. \ P(x))" "\P. \ (\x. P(x)) \ (\x. \ P(x))" by blast+ +lemmas demorgans = demorgans1 demorgans2 + (*** Removal of --> and <-> (positive and negative occurrences) ***) (*Last one is important for computing a compact CNF*) lemma nnf_simps: diff -r 4d09df93d1a2 -r 549a4992222f src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Euclidean_Division.thy Fri Jun 29 22:14:33 2018 +0200 @@ -1638,7 +1638,7 @@ by (simp only: *, simp only: l q divide_int_unfold) (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le) qed -qed (use mult_le_mono2 [of 1] in \auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\) +qed (use mult_le_mono2 [of 1] in \auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\) end diff -r 4d09df93d1a2 -r 549a4992222f src/HOL/Fields.thy --- a/src/HOL/Fields.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Fields.thy Fri Jun 29 22:14:33 2018 +0200 @@ -843,10 +843,6 @@ of positivity/negativity needed for \field_simps\. Have not added \sign_simps\ to \field_simps\ because the former can lead to case explosions.\ -lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff - -lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff - (* Only works once linear arithmetic is installed: text{*An example:*} lemma fixes a b c d e f :: "'a::linordered_field" diff -r 4d09df93d1a2 -r 549a4992222f src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Metis_Examples/Big_O.thy Fri Jun 29 22:14:33 2018 +0200 @@ -457,7 +457,7 @@ hence "\(v::'a) (u::'a) SKF\<^sub>7::'a \ 'b. \inverse c\ * \g (SKF\<^sub>7 (u * v))\ \ u * (v * \f (SKF\<^sub>7 (u * v))\)" by (metis mult_left_mono) then show "\ca::'a. \x::'b. inverse \c\ * \g x\ \ ca * \f x\" - using A2 F4 by (metis F1 \0 < \inverse c\\ linordered_field_class.sign_simps(23) mult_le_cancel_left_pos) + using A2 F4 by (metis F1 \0 < \inverse c\\ mult.assoc mult_le_cancel_left_pos) qed lemma bigo_const_mult6 [intro]: "(\x. c) *o O(f) <= O(f)" diff -r 4d09df93d1a2 -r 549a4992222f src/HOL/Num.thy --- a/src/HOL/Num.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Num.thy Fri Jun 29 22:14:33 2018 +0200 @@ -1282,14 +1282,20 @@ numeral for 1 reduces the number of special cases. \ -lemma mult_1s: +lemma mult_1s_semiring_numeral: "Numeral1 * a = a" "a * Numeral1 = a" + for a :: "'a::semiring_numeral" + by simp_all + +lemma mult_1s_ring_1: "- Numeral1 * b = - b" "b * - Numeral1 = - b" - for a :: "'a::semiring_numeral" and b :: "'b::ring_1" + for b :: "'a::ring_1" by simp_all +lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1 + setup \ Reorient_Proc.add (fn Const (@{const_name numeral}, _) $ _ => true @@ -1385,13 +1391,20 @@ "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)" by (simp_all add: add.assoc [symmetric]) -lemma mult_numeral_left [simp]: +lemma mult_numeral_left_semiring_numeral: "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)" - "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)" - "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)" - "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)" + by (simp add: mult.assoc [symmetric]) + +lemma mult_numeral_left_ring_1: + "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)" + "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)" + "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)" by (simp_all add: mult.assoc [symmetric]) +lemmas mult_numeral_left [simp] = + mult_numeral_left_semiring_numeral + mult_numeral_left_ring_1 + hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec diff -r 4d09df93d1a2 -r 549a4992222f src/HOL/Rat.thy --- a/src/HOL/Rat.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Rat.thy Fri Jun 29 22:14:33 2018 +0200 @@ -529,6 +529,10 @@ end +lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff +lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff + + instantiation rat :: distrib_lattice begin diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Jun 29 22:14:33 2018 +0200 @@ -591,6 +591,7 @@ register_config ML_Options.exception_trace_raw #> register_config ML_Options.exception_debugger_raw #> register_config ML_Options.debugger_raw #> + register_config Global_Theory.pending_shyps_raw #> register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/ML/ml_console.scala Fri Jun 29 22:14:33 2018 +0200 @@ -15,6 +15,7 @@ { Command_Line.tool { var dirs: List[Path] = Nil + var include_sessions: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var no_build = false @@ -27,6 +28,7 @@ Options are: -d DIR include session directory + -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -n no build of session image on startup @@ -39,6 +41,7 @@ quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. """, "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "n" -> (arg => no_build = true), @@ -69,7 +72,8 @@ store = Some(Sessions.store(options, system_mode)), session_base = if (raw_ml_system) None - else Some(Sessions.base_info(options, logic, dirs = dirs).check_base)) + else Some(Sessions.base_info( + options, logic, dirs = dirs, include_sessions = include_sessions).check_base)) val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _)) val process_result = Future.thread[Int]("process_result") { diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/PIDE/document.ML Fri Jun 29 22:14:33 2018 +0200 @@ -735,8 +735,9 @@ segments = segments}; in fn _ => - (Thy_Info.apply_presentation presentation_context thy; - commit_consolidated node) + Exn.release + (Exn.capture (Thy_Info.apply_presentation presentation_context) thy + before commit_consolidated node) end else fn _ => commit_consolidated node; diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/Thy/export_theory.ML Fri Jun 29 22:14:33 2018 +0200 @@ -102,6 +102,12 @@ (* axioms and facts *) + val standard_prop_of = + Thm.transfer thy #> + Thm.check_hyps (Context.Theory thy) #> + Drule.sort_constraint_intr_shyps #> + Thm.full_prop_of; + val encode_props = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) (list term) end; @@ -114,7 +120,7 @@ in encode_props (typargs, args, props') end; val export_axiom = export_props o single; - val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of; + val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of; val _ = export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Jun 29 22:14:33 2018 +0200 @@ -461,7 +461,11 @@ { val sel_sessions1 = session1 :: session :: include_sessions val select_sessions1 = - if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1 + if (session_focus) { + full_sessions1.check_sessions(sel_sessions1) + full_sessions1.imports_descendants(sel_sessions1) + } + else sel_sessions1 full_sessions1.selection(Selection(sessions = select_sessions1)) } @@ -679,13 +683,16 @@ } }) + def check_sessions(names: List[String]) + { + val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList + if (bad_sessions.nonEmpty) + error("Undefined session(s): " + commas_quote(bad_sessions)) + } + def selection(sel: Selection): Structure = { - val bad_sessions = - SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions). - filterNot(defined(_)): _*).toList - if (bad_sessions.nonEmpty) - error("Undefined session(s): " + commas_quote(bad_sessions)) + check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions) val excluded = sel.excluded(build_graph).toSet diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/Tools/dump.scala Fri Jun 29 22:14:33 2018 +0200 @@ -93,8 +93,8 @@ system_mode: Boolean = false, selection: Sessions.Selection = Sessions.Selection.empty): Process_Result = { - if (Build.build_logic(options, logic, progress = progress, dirs = dirs, - system_mode = system_mode) != 0) error(logic + " FAILED") + if (Build.build_logic(options, logic, build_heap = true, progress = progress, + dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED") val dump_options = make_options(options, aspects) diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/drule.ML Fri Jun 29 22:14:33 2018 +0200 @@ -98,6 +98,8 @@ val is_sort_constraint: term -> bool val sort_constraintI: thm val sort_constraint_eq: thm + val sort_constraint_intr: indexname * sort -> thm -> thm + val sort_constraint_intr_shyps: thm -> thm val with_subgoal: int -> (thm -> thm) -> thm -> thm val comp_no_flatten: thm * int -> int -> thm -> thm val rename_bvars: (string * string) list -> thm -> thm @@ -647,6 +649,26 @@ (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); +val sort_constraint_eq' = Thm.symmetric sort_constraint_eq; + +fun sort_constraint_intr tvar thm = + Thm.equal_elim + (Thm.instantiate + ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))], + [((("A", 0), propT), Thm.cprop_of thm)]) + sort_constraint_eq') thm; + +fun sort_constraint_intr_shyps raw_thm = + let val thm = Thm.strip_shyps raw_thm in + (case Thm.extra_shyps thm of + [] => thm + | shyps => + let + val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm [])); + val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps; + in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end) + end; + end; diff -r 4d09df93d1a2 -r 549a4992222f src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Pure/global_theory.ML Fri Jun 29 22:14:33 2018 +0200 @@ -24,6 +24,8 @@ val name_thm: bool -> bool -> string -> thm -> thm val name_thms: bool -> bool -> string -> thm list -> thm list val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list + val pending_shyps_raw: Config.raw + val pending_shyps: bool Config.T val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory val store_thm: binding * thm -> theory -> thm * theory val store_thm_open: binding * thm -> theory -> thm * theory @@ -128,16 +130,35 @@ fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); +val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false)); +val pending_shyps = Config.bool pending_shyps_raw; + fun add_facts (b, fact) thy = let val full_name = Sign.full_name thy b; val pos = Binding.pos_of b; - fun err msg = - error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg); - fun check thm = - ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm))) - handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; - val arg = (b, Lazy.map_finished (tap (List.app check)) fact); + fun check fact = + fact |> map_index (fn (i, thm) => + let + fun err msg = + error ("Malformed global fact " ^ + quote (full_name ^ + (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^ + Position.here pos ^ "\n" ^ msg); + val prop = Thm.plain_prop_of thm + handle THM _ => + thm + |> not (Config.get_global thy pending_shyps) ? + Thm.check_shyps (Proof_Context.init_global thy) + |> Thm.check_hyps (Context.Theory thy) + |> Thm.full_prop_of; + in + ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop)) + handle TYPE (msg, _, _) => err msg + | TERM (msg, _) => err msg + | ERROR msg => err msg + end); + val arg = (b, Lazy.map_finished (tap check) fact); in thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2) end; diff -r 4d09df93d1a2 -r 549a4992222f src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Tools/VSCode/extension/README.md Fri Jun 29 22:14:33 2018 +0200 @@ -1,14 +1,15 @@ # Isabelle Prover IDE support This extension connects VSCode to the Isabelle Prover IDE infrastructure: it -requires a repository version of Isabelle. +requires Isabelle2018. The implementation is centered around the VSCode Language Server protocol, but with many add-ons that are specific to VSCode and Isabelle/PIDE. See also: - * + * + * * @@ -58,8 +59,8 @@ ### Isabelle/VSCode Installation - * Download a recent Isabelle development snapshot from - + * Download Isabelle2018 from + or any of its mirror sites. * Unpack and run the main Isabelle/jEdit application as usual, to ensure that the logic image is built properly and Isabelle works as expected. @@ -68,7 +69,7 @@ * Open the VSCode *Extensions* view and install the following: - + *Isabelle*. + + *Isabelle2018* (needs to fit to the underlying Isabelle release). + *Prettify Symbols Mode* (important for display of Isabelle symbols). @@ -89,17 +90,17 @@ + Linux: ``` - "isabelle.home": "/home/makarius/Isabelle" + "isabelle.home": "/home/makarius/Isabelle2018" ``` + Mac OS X: ``` - "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle" + "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018" ``` + Windows: ``` - "isabelle.home": "C:\\Users\\makarius\\Isabelle" + "isabelle.home": "C:\\Users\\makarius\\Isabelle2018" ``` * Restart the VSCode application to ensure that all extensions are properly diff -r 4d09df93d1a2 -r 549a4992222f src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Tools/VSCode/extension/package.json Fri Jun 29 22:14:33 2018 +0200 @@ -1,6 +1,6 @@ { - "name": "isabelle", - "displayName": "Isabelle", + "name": "Isabelle2018", + "displayName": "Isabelle2018", "description": "Isabelle Prover IDE", "keywords": [ "theorem prover", diff -r 4d09df93d1a2 -r 549a4992222f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 22:14:33 2018 +0200 @@ -106,6 +106,7 @@ echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" + echo " -i NAME include session in name-space of theories" echo " -j OPTION add jEdit runtime option" echo " (default $JEDIT_OPTIONS)" echo " -l NAME logic session name" @@ -142,6 +143,7 @@ JEDIT_LOGIC_ANCESTOR="" JEDIT_LOGIC_REQUIREMENTS="" JEDIT_LOGIC_FOCUS="" +JEDIT_INCLUDE_SESSIONS="" JEDIT_SESSION_DIRS="" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" @@ -150,7 +152,7 @@ function getoptions() { OPTIND=1 - while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT + while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT do case "$OPT" in A) @@ -181,6 +183,13 @@ JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" fi ;; + i) + if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then + JEDIT_INCLUDE_SESSIONS="$OPTARG" + else + JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG" + fi + ;; f) BUILD_JARS="jars_fresh" ;; @@ -413,7 +422,7 @@ if [ "$BUILD_ONLY" = false ] then export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ - JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE + JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" classpath "$JEDIT_HOME/dist/jedit.jar" exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" diff -r 4d09df93d1a2 -r 549a4992222f src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 29 15:22:30 2018 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 29 22:14:33 2018 +0200 @@ -42,6 +42,8 @@ def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true" + def logic_include_sessions: List[String] = + space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = try { @@ -108,6 +110,7 @@ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs(), + include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements,