--- a/NEWS Thu Apr 10 11:34:55 2014 +0200
+++ b/NEWS Thu Apr 10 14:40:11 2014 +0200
@@ -25,6 +25,10 @@
supports input methods via ` (backquote), or << and >> (double angle
brackets).
+* The outer syntax categories "text" (for formal comments and document
+markup commands) and "altstring" (for literal fact references) allow
+cartouches as well, in addition to the traditional mix of quotations.
+
* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax. Method arguments should be
processed in the original proof context as far as possible, before
@@ -110,6 +114,9 @@
* Support for Navigator plugin (with toolbar buttons).
+* More support for remote files (e.g. http) using standard Java
+networking operations instead of jEdit virtual file-systems.
+
*** Pure ***
--- a/src/Doc/Implementation/Tactic.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Doc/Implementation/Tactic.thy Thu Apr 10 14:40:11 2014 +0200
@@ -175,7 +175,7 @@
@{index_ML_type tactic: "thm -> thm Seq.seq"} \\
@{index_ML no_tac: tactic} \\
@{index_ML all_tac: tactic} \\
- @{index_ML print_tac: "string -> tactic"} \\[1ex]
+ @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
@{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
@{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
@{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
@@ -200,7 +200,7 @@
\item @{ML all_tac} is a tactic that always succeeds, returning a
singleton sequence with unchanged goal state.
- \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
+ \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
prints a message together with the goal state on the tracing
channel.
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Apr 10 14:40:11 2014 +0200
@@ -265,14 +265,14 @@
text {* Large chunks of plain @{syntax text} are usually given
@{syntax verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
- "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}. For convenience,
- any of the smaller text units conforming to @{syntax nameref} are
- admitted as well. A marginal @{syntax comment} is of the form
- @{verbatim "--"}~@{syntax text}. Any number of these may occur
- within Isabelle/Isar commands.
+ "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}, or as @{syntax
+ cartouche} @{text "\<open>\<dots>\<close>"}. For convenience, any of the smaller text
+ units conforming to @{syntax nameref} are admitted as well. A
+ marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax
+ text}. Any number of these may occur within Isabelle/Isar commands.
@{rail \<open>
- @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
+ @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
;
@{syntax_def comment}: '--' @{syntax text}
\<close>}
@@ -424,9 +424,9 @@
\item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
- \item literal fact propositions using @{syntax_ref altstring} syntax
- @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
- @{method_ref fact}).
+ \item literal fact propositions using token syntax @{syntax_ref altstring}
+ @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
+ @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
\end{enumerate}
@@ -451,7 +451,8 @@
@{syntax_def thmdef}: thmbind '='
;
@{syntax_def thmref}:
- (@{syntax nameref} selection? | @{syntax altstring}) @{syntax attributes}? |
+ (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
+ @{syntax attributes}? |
'[' @{syntax attributes} ']'
;
@{syntax_def thmrefs}: @{syntax thmref} +
--- a/src/HOL/HOLCF/Domain_Aux.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy Thu Apr 10 14:40:11 2014 +0200
@@ -350,6 +350,4 @@
ML_file "Tools/Domain/domain_constructors.ML"
ML_file "Tools/Domain/domain_induction.ML"
-setup Domain_Take_Proofs.setup
-
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Apr 10 14:40:11 2014 +0200
@@ -61,7 +61,6 @@
val get_deflation_thms : theory -> thm list
val map_ID_add : attribute
val get_map_ID_thms : theory -> thm list
- val setup : theory -> theory
end
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
@@ -148,7 +147,7 @@
val map_ID_add = Map_Id_Data.add
val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
-val setup = DeflMapData.setup #> Map_Id_Data.setup
+val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
(******************************************************************************)
(************************** building types and terms **************************)
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Apr 10 14:40:11 2014 +0200
@@ -81,9 +81,9 @@
val weak_congs = [@{thm "if_weak_cong"}]
(* debugging *)
-fun DEBUG_tac (msg,tac) =
- CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]);
-fun NO_DEBUG_tac (_,tac) = CHANGED tac;
+fun DEBUG ctxt (msg,tac) =
+ CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]);
+fun NO_DEBUG _ (_,tac) = CHANGED tac;
(* simproc that deals with instances of permutations in front *)
@@ -170,8 +170,8 @@
(* main simplification tactics for permutations *)
-fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (perm_simp stac ctxt i));
-fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (eqvt_simp stac ctxt i));
+fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
+fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i));
val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac
val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac
@@ -253,12 +253,12 @@
let fun perm_extend_simp_tac_aux tactical ctxt n =
if n=0 then K all_tac
else DETERM o
- (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
- fn i => tactical (perm_simp asm_full_simp_tac ctxt i),
- fn i => tactical (perm_compose_tac ctxt i),
- fn i => tactical (apply_cong_tac i),
- fn i => tactical (unfold_perm_fun_def_tac i),
- fn i => tactical (ext_fun_tac i)]
+ (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
+ fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
+ fn i => tactical ctxt (perm_compose_tac ctxt i),
+ fn i => tactical ctxt (apply_cong_tac i),
+ fn i => tactical ctxt (unfold_perm_fun_def_tac i),
+ fn i => tactical ctxt (ext_fun_tac i)]
THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
in perm_extend_simp_tac_aux tactical ctxt 10 end;
@@ -270,11 +270,11 @@
let
val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod]
in
- EVERY [tactical ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
- tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
- tactical ("geting rid of the imps ", rtac impI i),
- tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
- tactical ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
+ EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
+ tactical ctxt ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
+ tactical ctxt ("geting rid of the imps ", rtac impI i),
+ tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
+ tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
end;
@@ -314,7 +314,7 @@
val fin_supp = dynamic_thms st ("fin_supp")
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
- (tactical ("guessing of the right supports-set",
+ (tactical ctxt ("guessing of the right supports-set",
EVERY [compose_tac (false, supports_rule'', 2) i,
asm_full_simp_tac ctxt' (i+1),
supports_tac_i tactical ctxt i])) st
@@ -356,7 +356,7 @@
val supports_fresh_rule'' = Drule.cterm_instantiate
[(cert (head_of S), cert s')] supports_fresh_rule'
in
- (tactical ("guessing of the right set that supports the goal",
+ (tactical ctxt ("guessing of the right set that supports the goal",
(EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
asm_full_simp_tac ctxt1 (i+2),
asm_full_simp_tac ctxt2 (i+1),
@@ -364,25 +364,25 @@
end
(* when a term-constructor contains more than one binder, it is useful *)
(* in nominal_primrecs to try whether the goal can be solved by an hammer *)
- | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",
+ | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",
(asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
end
handle General.Subscript => Seq.empty;
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
-val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
+val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG;
-val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG_tac;
-val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac;
-val supports_tac = supports_tac_i NO_DEBUG_tac;
-val finite_guess_tac = finite_guess_tac_i NO_DEBUG_tac;
-val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG_tac;
+val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG;
+val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG;
+val supports_tac = supports_tac_i NO_DEBUG;
+val finite_guess_tac = finite_guess_tac_i NO_DEBUG;
+val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG;
-val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG_tac;
-val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac;
-val dsupports_tac = supports_tac_i DEBUG_tac;
-val dfinite_guess_tac = finite_guess_tac_i DEBUG_tac;
-val dfresh_guess_tac = fresh_guess_tac_i DEBUG_tac;
+val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG;
+val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG;
+val dsupports_tac = supports_tac_i DEBUG;
+val dfinite_guess_tac = finite_guess_tac_i DEBUG;
+val dfresh_guess_tac = fresh_guess_tac_i DEBUG;
(* Code opied from the Simplifer for setting up the perm_simp method *)
(* behaves nearly identical to the simp-method, for example can handle *)
@@ -393,11 +393,11 @@
val asm_lrN = "asm_lr";
val perm_simp_options =
- (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac) ||
- Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac) ||
- Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac) ||
- Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
- Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
+ (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG) ||
+ Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG) ||
+ Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG) ||
+ Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG) ||
+ Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG));
val perm_simp_meth =
Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Apr 10 14:40:11 2014 +0200
@@ -47,7 +47,7 @@
fun tactic ctxt (msg, tac) =
if Config.get ctxt nominal_eqvt_debug
- then tac THEN' (K (print_tac ("after " ^ msg)))
+ then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
else tac
fun prove_eqvt_tac ctxt orig_thm pi pi' =
--- a/src/HOL/Orderings.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Orderings.thy Thu Apr 10 14:40:11 2014 +0200
@@ -344,21 +344,19 @@
subsection {* Reasoning tools setup *}
ML {*
-
signature ORDERS =
sig
val print_structures: Proof.context -> unit
- val attrib_setup: theory -> theory
val order_tac: Proof.context -> thm list -> int -> tactic
end;
structure Orders: ORDERS =
struct
-(** Theory and context data **)
+(* context data *)
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
- (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
+ s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
structure Data = Generic_Data
(
@@ -386,44 +384,52 @@
Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
end;
-
-(** Method **)
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_orders"}
+ "print order structures available to transitivity reasoner"
+ (Scan.succeed (Toplevel.unknown_context o
+ Toplevel.keep (print_structures o Toplevel.context_of)));
-fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
+
+(* tactics *)
+
+fun struct_tac ((s, ops), thms) ctxt facts =
let
+ val [eq, le, less] = ops;
fun decomp thy (@{const Trueprop} $ t) =
- let
- fun excluded t =
- (* exclude numeric types: linear arithmetic subsumes transitivity *)
- let val T = type_of t
- in
- T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
- end;
- fun rel (bin_op $ t1 $ t2) =
- if excluded t1 then NONE
- else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
- else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
- else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
- else NONE
- | rel _ = NONE;
- fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
- of NONE => NONE
- | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
- | dec x = rel x;
- in dec t end
- | decomp thy _ = NONE;
+ let
+ fun excluded t =
+ (* exclude numeric types: linear arithmetic subsumes transitivity *)
+ let val T = type_of t
+ in
+ T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
+ end;
+ fun rel (bin_op $ t1 $ t2) =
+ if excluded t1 then NONE
+ else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
+ else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
+ else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
+ else NONE
+ | rel _ = NONE;
+ fun dec (Const (@{const_name Not}, _) $ t) =
+ (case rel t of NONE =>
+ NONE
+ | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
+ | dec x = rel x;
+ in dec t end
+ | decomp _ _ = NONE;
in
- case s of
- "order" => Order_Tac.partial_tac decomp thms ctxt prems
- | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
- | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
+ (case s of
+ "order" => Order_Tac.partial_tac decomp thms ctxt facts
+ | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
+ | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
end
-fun order_tac ctxt prems =
- FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
+fun order_tac ctxt facts =
+ FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
-(** Attribute **)
+(* attributes *)
fun add_struct_thm s tag =
Thm.declaration_attribute
@@ -432,30 +438,19 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attrib_setup =
- Attrib.setup @{binding order}
- (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
- Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts)))
- "theorems controlling transitivity reasoner";
-
-
-(** Diagnostic command **)
-
val _ =
- Outer_Syntax.improper_command @{command_spec "print_orders"}
- "print order structures available to transitivity reasoner"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (print_structures o Toplevel.context_of)));
+ Theory.setup
+ (Attrib.setup @{binding order}
+ (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+ Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+ | ((NONE, n), ts) => del_struct (n, ts)))
+ "theorems controlling transitivity reasoner");
end;
-
*}
-setup Orders.attrib_setup
-
method_setup order = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
*} "transitivity reasoner"
@@ -546,64 +541,64 @@
end
-
setup {*
-let
-
-fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *)
+ map_theory_simpset (fn ctxt0 => ctxt0 addSolver
+ mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
+ (*Adding the transitivity reasoners also as safe solvers showed a slight
+ speed up, but the reasoning strength appears to be not higher (at least
+ no breaking of additional proofs in the entire HOL distribution, as
+ of 5 March 2004, was observed).*)
+*}
-fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) =
- let val prems = Simplifier.prems_of ctxt;
- val less = Const (@{const_name less}, T);
- val t = HOLogic.mk_Trueprop(le $ s $ r);
- in case find_first (prp t) prems of
- NONE =>
- let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
- in case find_first (prp t) prems of
- NONE => NONE
- | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
- end
- | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
- end
- handle THM _ => NONE;
+ML {*
+local
+ fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *)
+in
-fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) =
- let val prems = Simplifier.prems_of ctxt;
- val le = Const (@{const_name less_eq}, T);
- val t = HOLogic.mk_Trueprop(le $ r $ s);
- in case find_first (prp t) prems of
- NONE =>
- let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
- in case find_first (prp t) prems of
- NONE => NONE
- | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
- end
- | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
- end
- handle THM _ => NONE;
+fun antisym_le_simproc ctxt ct =
+ (case term_of ct of
+ (le as Const (_, T)) $ r $ s =>
+ (let
+ val prems = Simplifier.prems_of ctxt;
+ val less = Const (@{const_name less}, T);
+ val t = HOLogic.mk_Trueprop(le $ s $ r);
+ in
+ (case find_first (prp t) prems of
+ NONE =>
+ let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
+ (case find_first (prp t) prems of
+ NONE => NONE
+ | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})))
+ end
+ | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
+ end handle THM _ => NONE)
+ | _ => NONE);
-fun add_simprocs procs thy =
- map_theory_simpset (fn ctxt => ctxt
- addsimprocs (map (fn (name, raw_ts, proc) =>
- Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
-
-fun add_solver name tac =
- map_theory_simpset (fn ctxt0 => ctxt0 addSolver
- mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt)));
+fun antisym_less_simproc ctxt ct =
+ (case term_of ct of
+ NotC $ ((less as Const(_,T)) $ r $ s) =>
+ (let
+ val prems = Simplifier.prems_of ctxt;
+ val le = Const (@{const_name less_eq}, T);
+ val t = HOLogic.mk_Trueprop(le $ r $ s);
+ in
+ (case find_first (prp t) prems of
+ NONE =>
+ let val t = HOLogic.mk_Trueprop (NotC $ (less $ s $ r)) in
+ (case find_first (prp t) prems of
+ NONE => NONE
+ | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
+ end
+ | SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2})))
+ end handle THM _ => NONE)
+ | _ => NONE);
-in
- add_simprocs [
- ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
- ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
- ]
- #> add_solver "Transitivity" Orders.order_tac
- (* Adding the transitivity reasoners also as safe solvers showed a slight
- speed up, but the reasoning strength appears to be not higher (at least
- no breaking of additional proofs in the entire HOL distribution, as
- of 5 March 2004, was observed). *)
-end
+end;
*}
+simproc_setup antisym_le ("(x::'a::order) \<le> y") = "K antisym_le_simproc"
+simproc_setup antisym_less ("\<not> (x::'a::linorder) < y") = "K antisym_less_simproc"
+
subsection {* Bounded quantifiers *}
--- a/src/HOL/Probability/measurable.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Probability/measurable.ML Thu Apr 10 14:40:11 2014 +0200
@@ -95,7 +95,7 @@
fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
-fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
+fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
fun nth_hol_goal thm i =
HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
--- a/src/HOL/Product_Type.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Product_Type.thy Thu Apr 10 14:40:11 2014 +0200
@@ -1219,8 +1219,37 @@
subsection {* Inductively defined sets *}
+(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
+simproc_setup Collect_mem ("Collect t") = {*
+ fn _ => fn ctxt => fn ct =>
+ (case term_of ct of
+ S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t =>
+ let val (u, _, ps) = HOLogic.strip_psplits t in
+ (case u of
+ (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
+ (case try (HOLogic.strip_ptuple ps) q of
+ NONE => NONE
+ | SOME ts =>
+ if not (Term.is_open S') andalso
+ ts = map Bound (length ps downto 0)
+ then
+ let val simp =
+ full_simp_tac (put_simpset HOL_basic_ss ctxt
+ addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
+ in
+ SOME (Goal.prove ctxt [] []
+ (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
+ (K (EVERY
+ [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
+ rtac subsetI 1, dtac CollectD 1, simp,
+ rtac subsetI 1, rtac CollectI 1, simp])))
+ end
+ else NONE)
+ | _ => NONE)
+ end
+ | _ => NONE)
+*}
ML_file "Tools/inductive_set.ML"
-setup Inductive_Set.setup
subsection {* Legacy theorem bindings and duplicates *}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Apr 10 14:40:11 2014 +0200
@@ -25,20 +25,11 @@
(* debug stuff *)
-fun print_tac options s =
- if show_proof_trace options then Tactical.print_tac s else Seq.single;
-
-
-(** auxiliary **)
+fun trace_tac ctxt options s =
+ if show_proof_trace options then print_tac ctxt s else Seq.single;
-datatype assertion = Max_number_of_subgoals of int
-
-fun assert_tac (Max_number_of_subgoals i) st =
- if (nprems_of st <= i) then Seq.single st
- else
- raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :\n" ^
- Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals_without_context st)))
+fun assert_tac ctxt pos pred =
+ COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac);
(** special setup for simpset **)
@@ -75,7 +66,7 @@
@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
| Free _ =>
- Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
@@ -84,9 +75,9 @@
| Abs _ => raise Fail "prove_param: No valid parameter term")
in
REPEAT_DETERM (rtac @{thm ext} 1)
- THEN print_tac options "prove_param"
- THEN f_tac
- THEN print_tac options "after prove_param"
+ THEN trace_tac ctxt options "prove_param"
+ THEN f_tac
+ THEN trace_tac ctxt options "after prove_param"
THEN (REPEAT_DETERM (atac 1))
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
THEN REPEAT_DETERM (rtac @{thm refl} 1)
@@ -101,20 +92,20 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
- print_tac options "before intro rule:"
+ trace_tac ctxt options "before intro rule:"
THEN rtac introrule 1
- THEN print_tac options "after intro rule"
+ THEN trace_tac ctxt options "after intro rule"
(* for the right assumption in first position *)
THEN rotate_tac premposition 1
THEN atac 1
- THEN print_tac options "parameter goal"
+ THEN trace_tac ctxt options "parameter goal"
(* work with parameter arguments *)
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
THEN (REPEAT_DETERM (atac 1))
end
| (Free _, _) =>
- print_tac options "proving parameter call.."
- THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+ trace_tac ctxt options "proving parameter call.."
+ THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} =>
let
val param_prem = nth prems premposition
val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -129,14 +120,14 @@
in
rtac param_prem' 1
end) ctxt 1
- THEN print_tac options "after prove parameter call")
+ THEN trace_tac ctxt options "after prove parameter call")
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st
fun prove_match options ctxt nargs out_ts =
let
val eval_if_P =
- @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
+ @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
fun get_case_rewrite t =
if is_constructor ctxt t then
let
@@ -151,13 +142,13 @@
in
(* make this simpset better! *)
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
- THEN print_tac options "after prove_match:"
- THEN (DETERM (TRY
+ THEN trace_tac ctxt options "after prove_match:"
+ THEN (DETERM (TRY
(rtac eval_if_P 1
- THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} =>
+ THEN (SUBPROOF (fn {prems, ...} =>
(REPEAT_DETERM (rtac @{thm conjI} 1
THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
- THEN print_tac options "if condition to be solved:"
+ THEN trace_tac ctxt options "if condition to be solved:"
THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
THEN TRY (
let
@@ -167,8 +158,8 @@
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
THEN REPEAT_DETERM (rtac @{thm refl} 1))
- THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
- THEN print_tac options "after if simplification"
+ THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
+ THEN trace_tac ctxt options "after if simplification"
end;
@@ -187,7 +178,7 @@
(fn (pred, T) => predfun_definition_of ctxt pred
(all_input_of T))
preds
- in
+ in
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
(* need better control here! *)
@@ -198,11 +189,11 @@
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems out_ts [] =
(prove_match options ctxt nargs out_ts)
- THEN print_tac options "before simplifying assumptions"
+ THEN trace_tac ctxt options "before simplifying assumptions"
THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
- THEN print_tac options "before single intro rule"
+ THEN trace_tac ctxt options "before single intro rule"
THEN Subgoal.FOCUS_PREMS
- (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+ (fn {context = ctxt', prems, ...} =>
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
@@ -221,11 +212,11 @@
val (_, out_ts''') = split_mode mode us
val rec_tac = prove_prems out_ts''' ps
in
- print_tac options "before clause:"
+ trace_tac ctxt options "before clause:"
(*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
- THEN print_tac options "before prove_expr:"
+ THEN trace_tac ctxt options "before prove_expr:"
THEN prove_expr options ctxt nargs premposition (t, deriv)
- THEN print_tac options "after prove_expr:"
+ THEN trace_tac ctxt options "after prove_expr:"
THEN rec_tac
end
| Negprem t =>
@@ -240,17 +231,16 @@
val param_derivations = param_derivations_of deriv
val params = ho_args_of mode args
in
- print_tac options "before prove_neg_expr:"
+ trace_tac ctxt options "before prove_neg_expr:"
THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
[@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
THEN (if (is_some name) then
- print_tac options "before applying not introduction rule"
- THEN Subgoal.FOCUS_PREMS
- (fn {context, params = params, prems, asms, concl, schematics} =>
- rtac (the neg_intro_rule) 1
- THEN rtac (nth prems premposition) 1) ctxt 1
- THEN print_tac options "after applying not introduction rule"
+ trace_tac ctxt options "before applying not introduction rule"
+ THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
+ rtac (the neg_intro_rule) 1
+ THEN rtac (nth prems premposition) 1) ctxt 1
+ THEN trace_tac ctxt options "after applying not introduction rule"
THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
THEN (REPEAT_DETERM (atac 1))
else
@@ -265,16 +255,16 @@
end
| Sidecond t =>
rtac @{thm if_predI} 1
- THEN print_tac options "before sidecond:"
+ THEN trace_tac ctxt options "before sidecond:"
THEN prove_sidecond ctxt t
- THEN print_tac options "after sidecond:"
+ THEN trace_tac ctxt options "after sidecond:"
THEN prove_prems [] ps)
in (prove_match options ctxt nargs out_ts)
THEN rest_tac
end
val prems_tac = prove_prems in_ts moded_ps
in
- print_tac options "Proving clause..."
+ trace_tac ctxt options "Proving clause..."
THEN rtac @{thm bindI} 1
THEN rtac @{thm singleI} 1
THEN prems_tac
@@ -291,15 +281,15 @@
val pred_case_rule = the_elim_of ctxt pred
in
REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
- THEN print_tac options "before applying elim rule"
+ THEN trace_tac ctxt options "before applying elim rule"
THEN etac (predfun_elim_of ctxt pred mode) 1
THEN etac pred_case_rule 1
- THEN print_tac options "after applying elim rule"
+ THEN trace_tac ctxt options "after applying elim rule"
THEN (EVERY (map
- (fn i => EVERY' (select_sup (length moded_clauses) i) i)
+ (fn i => EVERY' (select_sup (length moded_clauses) i) i)
(1 upto (length moded_clauses))))
THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
- THEN print_tac options "proved one direction"
+ THEN trace_tac ctxt options "proved one direction"
end
@@ -316,15 +306,15 @@
val num_of_constrs = length case_thms
val (_, ts) = strip_comb t
in
- print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
+ trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
" splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
THEN TRY (Splitter.split_asm_tac [split_asm] 1
- THEN (print_tac options "after splitting with split_asm rules")
+ THEN (trace_tac ctxt options "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
THEN (REPEAT_DETERM_N (num_of_constrs - 1)
(etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
- THEN (assert_tac (Max_number_of_subgoals 2))
+ THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
THEN (EVERY (map split_term_tac ts))
end
else all_tac
@@ -334,7 +324,7 @@
THEN (etac @{thm botE} 2))))
end
-(* VERY LARGE SIMILIRATIY to function prove_param
+(* VERY LARGE SIMILIRATIY to function prove_param
-- join both functions
*)
(* TODO: remove function *)
@@ -347,19 +337,19 @@
val ho_args = ho_args_of mode args
val f_tac =
(case f of
- Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+ Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
(@{thm eval_pred}::(predfun_definition_of ctxt name mode)
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term")
in
- print_tac options "before simplification in prove_args:"
+ trace_tac ctxt options "before simplification in prove_args:"
THEN f_tac
- THEN print_tac options "after simplification in prove_args"
+ THEN trace_tac ctxt options "after simplification in prove_args"
THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
end
-fun prove_expr2 options ctxt (t, deriv) =
+fun prove_expr2 options ctxt (t, deriv) =
(case strip_comb t of
(Const (name, _), args) =>
let
@@ -369,11 +359,11 @@
in
etac @{thm bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
- THEN print_tac options "prove_expr2-before"
+ THEN trace_tac ctxt options "prove_expr2-before"
THEN etac (predfun_elim_of ctxt name mode) 1
- THEN print_tac options "prove_expr2"
+ THEN trace_tac ctxt options "prove_expr2"
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
- THEN print_tac options "finished prove_expr2"
+ THEN trace_tac ctxt options "finished prove_expr2"
end
| _ => etac @{thm bindE} 1)
@@ -387,16 +377,16 @@
| _ => nameTs)
val preds = preds_of t []
val defs = map
- (fn (pred, T) => predfun_definition_of ctxt pred
+ (fn (pred, T) => predfun_definition_of ctxt pred
(all_input_of T))
preds
in
(* only simplify the one assumption *)
- full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
+ full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
(* need better control here! *)
- THEN print_tac options "after sidecond2 simplification"
+ THEN trace_tac ctxt options "after sidecond2 simplification"
end
-
+
fun prove_clause2 options ctxt pred mode (ts, ps) i =
let
val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
@@ -406,23 +396,23 @@
addsimps [@{thm split_eta}, @{thm split_beta},
@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
fun prove_prems2 out_ts [] =
- print_tac options "before prove_match2 - last call:"
+ trace_tac ctxt options "before prove_match2 - last call:"
THEN prove_match2 options ctxt out_ts
- THEN print_tac options "after prove_match2 - last call:"
+ THEN trace_tac ctxt options "after prove_match2 - last call:"
THEN (etac @{thm singleE} 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
THEN TRY (
(REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
-
- THEN SOLVED (print_tac options "state before applying intro rule:"
+
+ THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
THEN (rtac pred_intro_rule
(* How to handle equality correctly? *)
- THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+ THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac)))
- THEN' (K (print_tac options "state after pre-simplification:"))
- THEN' (K (print_tac options "state after assumption matching:")))) 1))
+ THEN' (K (trace_tac ctxt options "state after pre-simplification:"))
+ THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
@@ -445,7 +435,7 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
- print_tac options "before neg prem 2"
+ trace_tac ctxt options "before neg prem 2"
THEN etac @{thm bindE} 1
THEN (if is_some name then
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
@@ -456,28 +446,28 @@
else
etac @{thm not_predE'} 1)
THEN rec_tac
- end
+ end
| Sidecond t =>
etac @{thm bindE} 1
THEN etac @{thm if_predE} 1
THEN prove_sidecond2 options ctxt t
THEN prove_prems2 [] ps)
in
- print_tac options "before prove_match2:"
+ trace_tac ctxt options "before prove_match2:"
THEN prove_match2 options ctxt out_ts
- THEN print_tac options "after prove_match2:"
+ THEN trace_tac ctxt options "after prove_match2:"
THEN rest_tac
end
- val prems_tac = prove_prems2 in_ts ps
+ val prems_tac = prove_prems2 in_ts ps
in
- print_tac options "starting prove_clause2"
+ trace_tac ctxt options "starting prove_clause2"
THEN etac @{thm bindE} 1
THEN (etac @{thm singleE'} 1)
THEN (TRY (etac @{thm Pair_inject} 1))
- THEN print_tac options "after singleE':"
+ THEN trace_tac ctxt options "after singleE':"
THEN prems_tac
end;
-
+
fun prove_other_direction options ctxt pred mode moded_clauses =
let
fun prove_clause clause i =
@@ -505,11 +495,11 @@
(if not (skip_proof options) then
(fn _ =>
rtac @{thm pred_iffI} 1
- THEN print_tac options "after pred_iffI"
+ THEN trace_tac ctxt options "after pred_iffI"
THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
- THEN print_tac options "proved one direction"
+ THEN trace_tac ctxt options "proved one direction"
THEN prove_other_direction options ctxt pred mode moded_clauses
- THEN print_tac options "proved other direction")
+ THEN trace_tac ctxt options "proved other direction")
else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
end
--- a/src/HOL/Tools/cnf.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/cnf.ML Thu Apr 10 14:40:11 2014 +0200
@@ -207,9 +207,9 @@
in
make_nnf_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
+ | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
make_nnf_not_false
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
+ | make_nnf_thm _ (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
make_nnf_not_true
| make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
let
--- a/src/HOL/Tools/inductive_set.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Apr 10 14:40:11 2014 +0200
@@ -25,42 +25,11 @@
val mono_add: attribute
val mono_del: attribute
val codegen_preproc: theory -> thm list -> thm list
- val setup: theory -> theory
end;
structure Inductive_Set: INDUCTIVE_SET =
struct
-(**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
-
-val collect_mem_simproc =
- Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn ctxt =>
- fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
- let val (u, _, ps) = HOLogic.strip_psplits t
- in case u of
- (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
- (case try (HOLogic.strip_ptuple ps) q of
- NONE => NONE
- | SOME ts =>
- if not (Term.is_open S') andalso
- ts = map Bound (length ps downto 0)
- then
- let val simp =
- full_simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
- in
- SOME (Goal.prove ctxt [] []
- (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
- (K (EVERY
- [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
- rtac subsetI 1, dtac CollectD 1, simp,
- rtac subsetI 1, rtac CollectI 1, simp])))
- end
- else NONE)
- | _ => NONE
- end
- | _ => NONE);
-
(***********************************************************************************)
(* simplifies (%x y. (x, y) : S & P x y) to (%x y. (x, y) : S Int {(x, y). P x y}) *)
(* and (%x y. (x, y) : S | P x y) to (%x y. (x, y) : S Un {(x, y). P x y}) *)
@@ -206,7 +175,7 @@
(swap #> Pattern.matches thy) (f #> fst) (op aconv) rules;
fun infer_arities thy arities (optf, t) fs = case strip_comb t of
- (Abs (s, T, u), []) => infer_arities thy arities (NONE, u) fs
+ (Abs (_, _, u), []) => infer_arities thy arities (NONE, u) fs
| (Abs _, _) => infer_arities thy arities (NONE, Envir.beta_norm t) fs
| (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
SOME (SOME (_, (arity, _))) =>
@@ -266,7 +235,7 @@
end)
in
Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
- addsimprocs [collect_mem_simproc]) thm'' |>
+ addsimprocs [@{simproc Collect_mem}]) thm'' |>
zero_var_indexes |> eta_contract_thm (equal p)
end;
@@ -397,7 +366,7 @@
thm |>
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
- addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
+ addsimprocs [strong_ind_simproc pred_arities, @{simproc Collect_mem}]) |>
Rule_Cases.save thm
end;
@@ -425,8 +394,6 @@
else thm
in map preproc end;
-fun code_ind_att optmod = to_pred_att [];
-
(**** definition of inductive sets ****)
@@ -569,21 +536,21 @@
(** package setup **)
-(* setup theory *)
+(* attributes *)
-val setup =
- Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
- "declare rules for converting between predicate and set notation" #>
- Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
- "convert rule to set notation" #>
- Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
- "convert rule to predicate notation" #>
- Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
- "declaration of monotonicity rule for set operators" #>
- map_theory_simpset (fn ctxt => ctxt addsimprocs [collect_mem_simproc]);
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+ "declare rules for converting between predicate and set notation" #>
+ Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
+ "convert rule to set notation" #>
+ Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
+ "convert rule to predicate notation" #>
+ Attrib.setup @{binding mono_set} (Attrib.add_del mono_add mono_del)
+ "declare of monotonicity rule for set operators");
-(* outer syntax *)
+(* commands *)
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
--- a/src/HOL/Tools/record.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/Tools/record.ML Thu Apr 10 14:40:11 2014 +0200
@@ -1066,7 +1066,7 @@
subrecord.
*)
val simproc =
- Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record" ["x"]
(fn ctxt => fn t =>
let val thy = Proof_Context.theory_of ctxt in
(case t of
@@ -1142,7 +1142,7 @@
we omit considering further updates if doing so would introduce
both a more update and an update to a field within it.*)
val upd_simproc =
- Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record_upd" ["x"]
(fn ctxt => fn t =>
let
val thy = Proof_Context.theory_of ctxt;
@@ -1263,7 +1263,7 @@
Complexity: #components * #updates #updates
*)
val eq_simproc =
- Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
+ Simplifier.simproc_global @{theory HOL} "record_eq" ["r = s"]
(fn ctxt => fn t =>
(case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
(case rec_id ~1 T of
@@ -1283,7 +1283,7 @@
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
fun split_simproc P =
- Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record_split" ["x"]
(fn ctxt => fn t =>
(case t of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1311,7 +1311,7 @@
| _ => NONE));
val ex_sel_eq_simproc =
- Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
+ Simplifier.simproc_global @{theory HOL} "ex_sel_eq" ["Ex t"]
(fn ctxt => fn t =>
let
val thy = Proof_Context.theory_of ctxt;
--- a/src/HOL/ex/Cartouche_Examples.thy Thu Apr 10 11:34:55 2014 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Thu Apr 10 14:40:11 2014 +0200
@@ -7,6 +7,32 @@
"text_cartouche" :: thy_decl
begin
+subsection {* Regular outer syntax *}
+
+text \<open>Text cartouches may be used in the outer syntax category "text",
+ as alternative to the traditional "verbatim" tokens. An example is
+ this text block.\<close> -- \<open>The same works for small side-comments.\<close>
+
+notepad
+begin
+ txt \<open>Moreover, cartouches work as additional syntax in the
+ "altstring" category, for literal fact references. For example:\<close>
+
+ fix x y :: 'a
+ assume "x = y"
+ note \<open>x = y\<close>
+ have "x = y" by (rule \<open>x = y\<close>)
+ from \<open>x = y\<close> have "x = y" .
+
+ txt \<open>Of course, this can be nested inside formal comments and
+ antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
+ [OF \<open>x = y\<close>]}.\<close>
+
+ have "x = y"
+ by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>) -- \<open>more cartouches involving ML\<close>
+end
+
+
subsection {* Outer syntax: cartouche within command syntax *}
ML {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/url.scala Thu Apr 10 14:40:11 2014 +0200
@@ -0,0 +1,36 @@
+/* Title: Pure/General/url.scala
+ Author: Makarius
+
+Basic URL operations.
+*/
+
+package isabelle
+
+
+import java.net.{URL, MalformedURLException}
+
+
+object Url
+{
+ def apply(name: String): URL =
+ {
+ try { new URL(name) }
+ catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
+ }
+
+ def is_wellformed(name: String): Boolean =
+ try { Url(name); true }
+ catch { case ERROR(_) => false }
+
+ def is_readable(name: String): Boolean =
+ try { Url(name).openStream.close; true }
+ catch { case ERROR(_) => false }
+
+ def read(name: String): String =
+ {
+ val stream = Url(name).openStream
+ try { File.read_stream(stream) }
+ finally { stream.close }
+ }
+}
+
--- a/src/Pure/Isar/args.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/args.ML Thu Apr 10 14:40:11 2014 +0200
@@ -33,6 +33,8 @@
val maybe: 'a parser -> 'a option parser
val cartouche_inner_syntax: string parser
val cartouche_source_position: Symbol_Pos.source parser
+ val text_source_position: Symbol_Pos.source parser
+ val text: string parser
val name_inner_syntax: string parser
val name_source_position: Symbol_Pos.source parser
val name: string parser
@@ -151,8 +153,8 @@
(Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
Parse.type_ident || Parse.type_var || Parse.number);
-val string = Parse.token (Parse.string || Parse.verbatim);
-val alt_string = Parse.token Parse.alt_string;
+val string = Parse.token Parse.string;
+val alt_string = Parse.token (Parse.alt_string || Parse.cartouche);
val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
fun $$$ x =
@@ -163,7 +165,6 @@
else Scan.fail
end);
-
val named = ident || string;
val add = $$$ "add";
@@ -183,6 +184,10 @@
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_source_position = cartouche >> Token.source_position_of;
+val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
+val text_source_position = text_token >> Token.source_position_of;
+val text = text_token >> Token.content_of;
+
val name_inner_syntax = named >> Token.inner_syntax_of;
val name_source_position = named >> Token.source_position_of;
--- a/src/Pure/Isar/method.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/method.ML Thu Apr 10 14:40:11 2014 +0200
@@ -513,9 +513,9 @@
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
"rotate assumptions of goal" #>
- setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
+ setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic)
"ML tactic as proof method" #>
- setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
+ setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic)
"ML tactic as raw proof method");
--- a/src/Pure/Isar/parse.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/Isar/parse.ML Thu Apr 10 14:40:11 2014 +0200
@@ -275,7 +275,7 @@
(short_ident || long_ident || sym_ident || string || number);
val text = group (fn () => "text")
- (short_ident || long_ident || sym_ident || string || number || verbatim);
+ (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
val path = group (fn () => "file name/path specification") name;
@@ -386,7 +386,7 @@
val const = inner_syntax (group (fn () => "constant") xname);
-val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
+val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
(* patterns *)
--- a/src/Pure/PIDE/command.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/command.ML Thu Apr 10 14:40:11 2014 +0200
@@ -89,9 +89,17 @@
type blob =
(string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*)
-fun read_file master_dir pos src_path =
+fun read_file_node file_node master_dir pos src_path =
let
val _ = Position.report pos Markup.language_path;
+ val _ =
+ (case try Url.explode file_node of
+ NONE => ()
+ | SOME (Url.File _) => ()
+ | _ =>
+ (Position.report pos (Markup.path file_node);
+ error ("Prover cannot load remote file " ^
+ Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
val full_path = File.check_file (File.full_path master_dir src_path);
val _ = Position.report pos (Markup.path (Path.implode full_path));
val text = File.read full_path;
@@ -99,6 +107,8 @@
val digest = SHA1.digest text;
in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
+val read_file = read_file_node "";
+
local
fun blob_file src_path lines digest file_node =
@@ -115,8 +125,9 @@
[span] => span
|> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
let
- fun make_file src_path (Exn.Res (_, NONE)) =
- Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
+ fun make_file src_path (Exn.Res (file_node, NONE)) =
+ Exn.interruptible_capture (fn () =>
+ read_file_node file_node master_dir pos src_path) ()
| make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
(Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
Exn.Res (blob_file src_path lines digest file_node))
--- a/src/Pure/PIDE/command.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/command.scala Thu Apr 10 14:40:11 2014 +0200
@@ -75,6 +75,8 @@
final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
{
+ def is_empty: Boolean = rep.isEmpty
+
def apply(index: Markup_Index): Markup_Tree =
rep.getOrElse(index, Markup_Tree.empty)
@@ -86,11 +88,14 @@
yield id
def redirect(other_id: Document_ID.Generic): Markups =
- new Markups(
+ {
+ val rep1 =
(for {
(Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
if other_id == id
- } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+ } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
+ if (rep1.isEmpty) Markups.empty else new Markups(rep1)
+ }
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
@@ -135,9 +140,12 @@
def markup(index: Markup_Index): Markup_Tree = markups(index)
- def redirect(other_command: Command): State =
- new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
-
+ def redirect(other_command: Command): Option[State] =
+ {
+ val markups1 = markups.redirect(other_command.id)
+ if (markups1.is_empty) None
+ else Some(new State(other_command, Nil, Results.empty, markups1))
+ }
def eq_content(other: State): Boolean =
command.source == other.command.source &&
@@ -199,11 +207,7 @@
case None => bad(); state
}
case None =>
- chunk_name match {
- // FIXME workaround for static positions stemming from batch build
- case Text.Chunk.File(name) if name.endsWith(".thy") =>
- case _ => bad()
- }
+ // silently ignore excessive reports
state
}
--- a/src/Pure/PIDE/document.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/document.scala Thu Apr 10 14:40:11 2014 +0200
@@ -536,9 +536,11 @@
id == st.command.id ||
(execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
- private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+ private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
+ /* FIXME
(execs.get(id) orElse commands.get(id)).map(st =>
((Text.Chunk.Id(st.command.id), st.command.chunk)))
+ */
private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
(commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
@@ -688,7 +690,7 @@
} yield (id, st)).toMap.valuesIterator.toList
}
else Nil
- self.map(_._2) ::: others.map(_.redirect(command))
+ self.map(_._2) ::: others.flatMap(_.redirect(command))
}
def command_results(version: Version, command: Command): Command.Results =
--- a/src/Pure/PIDE/editor.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/editor.scala Thu Apr 10 14:40:11 2014 +0200
@@ -22,7 +22,10 @@
def insert_overlay(command: Command, fn: String, args: List[String]): Unit
def remove_overlay(command: Command, fn: String, args: List[String]): Unit
- abstract class Hyperlink { def follow(context: Context): Unit }
+ abstract class Hyperlink {
+ def external: Boolean
+ def follow(context: Context): Unit
+ }
def hyperlink_command(
snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
}
--- a/src/Pure/PIDE/protocol.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Apr 10 14:40:11 2014 +0200
@@ -214,9 +214,6 @@
/* specific messages */
- def is_inlined(msg: XML.Tree): Boolean =
- !(is_result(msg) || is_tracing(msg) || is_state(msg))
-
def is_result(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -239,8 +236,14 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
- def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+ def is_warning_markup(msg: XML.Tree, name: String): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WARNING, _),
+ List(XML.Elem(markup, _))) => markup.name == name
+ case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
+ List(XML.Elem(markup, _))) => markup.name == name
+ case _ => false
+ }
def is_warning(msg: XML.Tree): Boolean =
msg match {
@@ -256,6 +259,13 @@
case _ => false
}
+ def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
+ def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+ def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
+
+ def is_inlined(msg: XML.Tree): Boolean =
+ !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
/* dialogs */
--- a/src/Pure/System/isabelle_system.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/System/isabelle_system.ML Thu Apr 10 14:40:11 2014 +0200
@@ -67,7 +67,7 @@
else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
-(* unique tmp files *)
+(* tmp files *)
fun create_tmp_path name ext =
let
@@ -80,6 +80,9 @@
let val path = create_tmp_path name ext
in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
+
+(* tmp dirs *)
+
fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
fun with_tmp_dir name f =
--- a/src/Pure/build-jars Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/build-jars Thu Apr 10 14:40:11 2014 +0200
@@ -31,6 +31,7 @@
General/symbol.scala
General/time.scala
General/timing.scala
+ General/url.scala
General/xz_file.scala
GUI/color_value.scala
GUI/gui.scala
--- a/src/Pure/goal_display.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/goal_display.ML Thu Apr 10 14:40:11 2014 +0200
@@ -15,7 +15,6 @@
val show_consts: bool Config.T
val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
- val pretty_goals_without_context: thm -> Pretty.T list
val pretty_goal: Proof.context -> thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
end;
@@ -131,11 +130,6 @@
(if show_sorts0 then pretty_varsT prop else [])
end;
-fun pretty_goals_without_context th =
- let val ctxt =
- Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
- in pretty_goals ctxt th end;
-
val pretty_goal = Pretty.chunks oo pretty_goals;
val string_of_goal = Pretty.string_of oo pretty_goal;
--- a/src/Pure/simplifier.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/simplifier.ML Thu Apr 10 14:40:11 2014 +0200
@@ -29,6 +29,19 @@
sig
include BASIC_SIMPLIFIER
val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
+ val attrib: (thm -> Proof.context -> Proof.context) -> attribute
+ val simp_add: attribute
+ val simp_del: attribute
+ val cong_add: attribute
+ val cong_del: attribute
+ val check_simproc: Proof.context -> xstring * Position.T -> string
+ val the_simproc: Proof.context -> string -> simproc
+ val def_simproc: {name: binding, lhss: term list,
+ proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
+ local_theory -> local_theory
+ val def_simproc_cmd: {name: binding, lhss: string list,
+ proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
+ local_theory -> local_theory
val pretty_simpset: Proof.context -> Pretty.T
val default_mk_sym: Proof.context -> thm -> thm option
val prems_of: Proof.context -> thm list
@@ -57,19 +70,6 @@
val full_rewrite: Proof.context -> conv
val asm_lr_rewrite: Proof.context -> conv
val asm_full_rewrite: Proof.context -> conv
- val attrib: (thm -> Proof.context -> Proof.context) -> attribute
- val simp_add: attribute
- val simp_del: attribute
- val cong_add: attribute
- val cong_del: attribute
- val check_simproc: Proof.context -> xstring * Position.T -> string
- val the_simproc: Proof.context -> string -> simproc
- val def_simproc: {name: binding, lhss: term list,
- proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
- local_theory -> local_theory
- val def_simproc_cmd: {name: binding, lhss: string list,
- proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
- local_theory -> local_theory
val cong_modifiers: Method.modifier parser list
val simp_modifiers': Method.modifier parser list
val simp_modifiers: Method.modifier parser list
@@ -83,36 +83,6 @@
open Raw_Simplifier;
-(** pretty printing **)
-
-fun pretty_simpset ctxt =
- let
- val pretty_term = Syntax.pretty_term ctxt;
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thm_item = Display.pretty_thm_item ctxt;
-
- fun pretty_proc (name, lhss) =
- Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
-
- fun pretty_cong_name (const, name) =
- pretty_term ((if const then Const else Free) (name, dummyT));
- fun pretty_cong (name, thm) =
- Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
-
- val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
- dest_ss (simpset_of ctxt);
- in
- [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
- Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
- Pretty.big_list "congruences:" (map pretty_cong congs),
- Pretty.strs ("loopers:" :: map quote loopers),
- Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
- Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
- |> Pretty.chunks
- end;
-
-
-
(** declarations **)
(* attributes *)
@@ -187,6 +157,40 @@
+(** pretty_simpset **)
+
+fun pretty_simpset ctxt =
+ let
+ val pretty_term = Syntax.pretty_term ctxt;
+ val pretty_thm = Display.pretty_thm ctxt;
+ val pretty_thm_item = Display.pretty_thm_item ctxt;
+
+ fun pretty_simproc (name, lhss) =
+ Pretty.block
+ (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
+ Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss));
+
+ fun pretty_cong_name (const, name) =
+ pretty_term ((if const then Const else Free) (name, dummyT));
+ fun pretty_cong (name, thm) =
+ Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
+
+ val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
+ dest_ss (simpset_of ctxt);
+ val simprocs =
+ Name_Space.markup_entries ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
+ in
+ [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
+ Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
+ Pretty.big_list "congruences:" (map pretty_cong congs),
+ Pretty.strs ("loopers:" :: map quote loopers),
+ Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
+ Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
+ |> Pretty.chunks
+ end;
+
+
+
(** simplification tactics and rules **)
fun solve_all_tac solvers ctxt =
--- a/src/Pure/tactical.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Pure/tactical.ML Thu Apr 10 14:40:11 2014 +0200
@@ -30,7 +30,7 @@
val FIRST': ('a -> tactic) list -> 'a -> tactic
val FIRST1: (int -> tactic) list -> tactic
val RANGE: (int -> tactic) list -> int -> tactic
- val print_tac: string -> tactic
+ val print_tac: Proof.context -> string -> tactic
val pause_tac: tactic
val trace_REPEAT: bool Unsynchronized.ref
val suppress_tracing: bool Unsynchronized.ref
@@ -182,9 +182,8 @@
(*** Tracing tactics ***)
(*Print the current proof state and pass it on.*)
-fun print_tac msg st =
- (tracing (msg ^ "\n" ^
- Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st)));
+fun print_tac ctxt msg st =
+ (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
Seq.single st);
(*Pause until a line is typed -- if non-empty then fail. *)
@@ -223,7 +222,7 @@
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing) then
(tracing (Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals_without_context st @
+ (Goal_Display.pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm st)) st @
[Pretty.str "** Press RETURN to continue:"])));
exec_trace_command flag (tac, st))
else tac st;
--- a/src/Sequents/prover.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Sequents/prover.ML Thu Apr 10 14:40:11 2014 +0200
@@ -196,7 +196,7 @@
val lastrestac = RESOLVE_THEN unsafes;
fun gtac i =
restac gtac i ORELSE
- (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i
+ (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i
else lastrestac gtac i)
in gtac end;
--- a/src/Tools/induction.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/induction.ML Thu Apr 10 14:40:11 2014 +0200
@@ -17,7 +17,7 @@
| (p as Free _, _) => [p]
| (_, ts) => flat(map preds_of ts))
-fun name_hyps thy (arg as ((cases,consumes),th)) =
+fun name_hyps (arg as ((cases, consumes), th)) =
if not(forall (null o #2 o #1) cases) then arg
else
let
@@ -35,7 +35,7 @@
(take n cases ~~ take n hnamess)
in ((cases',consumes),th) end
-val induction_tac = Induct.gen_induct_tac name_hyps
+val induction_tac = Induct.gen_induct_tac (K name_hyps)
val setup = Induct.gen_induct_setup @{binding induction} induction_tac
--- a/src/Tools/jEdit/src/Isabelle.props Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Thu Apr 10 14:40:11 2014 +0200
@@ -4,7 +4,7 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
-plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Markus Kaiser, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Lars Hupel, Markus Kaiser, Makarius Wenzel
plugin.isabelle.jedit.Plugin.version=1.0.0
plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
--- a/src/Tools/jEdit/src/document_view.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Thu Apr 10 14:40:11 2014 +0200
@@ -144,7 +144,7 @@
val line_range = Text.Range(start(i), end(i))
// gutter icons
- rendering.gutter_message(line_range) match {
+ rendering.gutter_icon(line_range) match {
case Some(icon) =>
val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Apr 10 14:40:11 2014 +0200
@@ -161,6 +161,7 @@
def hyperlink_url(name: String): Hyperlink =
new Hyperlink {
+ val external = true
def follow(view: View) =
default_thread_pool.submit(() =>
try { Isabelle_System.open(name) }
@@ -173,6 +174,7 @@
def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
new Hyperlink {
+ val external = false
def follow(view: View) = goto_file(view, name, line, column)
override def toString: String = "file " + quote(name)
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Apr 10 14:40:11 2014 +0200
@@ -10,10 +10,10 @@
import isabelle._
-import java.io.{File => JFile, IOException, ByteArrayOutputStream}
+import java.io.{File => JFile, ByteArrayOutputStream}
import javax.swing.text.Segment
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.bufferio.BufferIORequest
@@ -45,6 +45,7 @@
{
val path = source_path.expand
if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+ else if (path.is_current) dir
else {
val vfs = VFSManager.getVFSForPath(dir)
if (vfs.isInstanceOf[FileVFS])
@@ -54,42 +55,32 @@
}
}
- override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+ override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
{
Swing_Thread.now {
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
JEdit_Lib.buffer_lock(buffer) {
- Some(f(buffer.getSegment(0, buffer.getLength)))
+ Some(consume(buffer.getSegment(0, buffer.getLength)))
}
case None => None
}
} getOrElse {
- val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?)
- if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
- f(File.read(file))
+ if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
+ else {
+ val file = new JFile(name.node)
+ if (file.isFile) consume(File.read(file))
+ else error("No such file: " + quote(file.toString))
+ }
}
}
- def check_file(view: View, path: String): Boolean =
- {
- val vfs = VFSManager.getVFSForPath(path)
- val session = vfs.createVFSSession(path, view)
-
+ def check_file(view: View, file: String): Boolean =
try {
- session != null && {
- try {
- val file = vfs._getFile(session, path, view)
- file != null && file.isReadable && file.getType == VFSFile.FILE
- }
- catch { case _: IOException => false }
- }
+ if (Url.is_wellformed(file)) Url.is_readable(file)
+ else (new JFile(file)).isFile
}
- finally {
- try { vfs._endVFSSession(session, view) }
- catch { case _: IOException => }
- }
- }
+ catch { case ERROR(_) => false }
/* file content */
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Apr 10 14:40:11 2014 +0200
@@ -36,6 +36,9 @@
else None
}
+ private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
+ Swing_Thread.require { stack.find(tip => tip.original_parent == parent) }
+
def apply(
view: View,
parent: JComponent,
@@ -60,7 +63,7 @@
old.foreach(_.hide_popup)
val loc = SwingUtilities.convertPoint(parent, location, layered)
- val tip = new Pretty_Tooltip(view, layered, loc, rendering, results, info)
+ val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
stack = tip :: rest
tip.show_popup
}
@@ -142,6 +145,9 @@
}
}
+ def dismiss_descendant(parent: JComponent): Unit =
+ descendant(parent).foreach(dismiss(_))
+
def dismissed_all(): Boolean =
{
deactivate()
@@ -159,6 +165,7 @@
class Pretty_Tooltip private(
view: View,
layered: JLayeredPane,
+ val original_parent: JComponent,
location: Point,
rendering: Rendering,
private val results: Command.Results,
--- a/src/Tools/jEdit/src/rendering.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Thu Apr 10 14:40:11 2014 +0200
@@ -495,7 +495,14 @@
lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
- /* gutter icons */
+ /* gutter */
+
+ private def gutter_message_pri(msg: XML.Tree): Int =
+ if (Protocol.is_error(msg)) Rendering.error_pri
+ else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
+ else if (Protocol.is_warning(msg)) Rendering.warning_pri
+ else if (Protocol.is_information(msg)) Rendering.information_pri
+ else 0
private lazy val gutter_icons = Map(
Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
@@ -503,27 +510,17 @@
Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
- def gutter_message(range: Text.Range): Option[Icon] =
+ def gutter_icon(range: Text.Range): Option[Icon] =
{
- val results =
+ val pris =
snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
{
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
- Some(pri max Rendering.information_pri)
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
- body match {
- case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
- Some(pri max Rendering.legacy_pri)
- case _ =>
- Some(pri max Rendering.warning_pri)
- }
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
- Some(pri max Rendering.error_pri)
+ case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
+ Some(pri max gutter_message_pri(msg))
case _ => None
- })
- val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
- gutter_icons.get(pri)
+ }).map(_.info)
+
+ gutter_icons.get((0 /: pris)(_ max _))
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 10 11:34:55 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 10 14:40:11 2014 +0200
@@ -168,12 +168,14 @@
robust_body(()) {
hyperlink_area.info match {
case Some(Text.Info(range, link)) =>
- try { text_area.moveCaretPosition(range.start) }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
+ if (!link.external) {
+ try { text_area.moveCaretPosition(range.start) }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+ text_area.requestFocus
}
- text_area.requestFocus
link.follow(view)
case None =>
}
@@ -200,7 +202,8 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseDragged(evt: MouseEvent) {
robust_body(()) {
- PIDE.dismissed_popups(view)
+ Completion_Popup.Text_Area.dismissed(text_area)
+ Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
}
}
@@ -245,7 +248,7 @@
case Some(tip) =>
val painter = text_area.getPainter
val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
- val results = rendering.command_results(range)
+ val results = rendering.command_results(tip.range)
Pretty_Tooltip(view, painter, loc, rendering, results, tip)
}
}
--- a/src/ZF/Tools/inductive_package.ML Thu Apr 10 11:34:55 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Apr 10 14:40:11 2014 +0200
@@ -226,13 +226,13 @@
rewrite_goals_tac ctxt con_defs,
REPEAT (rtac @{thm refl} 2),
(*Typechecking; this can fail*)
- if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
+ if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
else all_tac,
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
type_elims)
ORELSE' hyp_subst_tac ctxt1)),
- if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
+ if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
else all_tac,
DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];