--- a/doc-src/IsarRef/Thy/Generic.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Tue Feb 28 11:45:40 2012 +0100
@@ -329,11 +329,11 @@
\cite{isabelle-implementation}).
\item @{method cut_tac} inserts facts into the proof state as
- assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
- \cite{isabelle-implementation}. Note that the scope of schematic
- variables is spread over the main goal statement. Instantiations
- may be given as well, see also ML tactic @{ML cut_inst_tac} in
- \cite{isabelle-implementation}.
+ assumption of a subgoal; instantiations may be given as well. Note
+ that the scope of schematic variables is spread over the main goal
+ statement and rule premises are turned into new subgoals. This is
+ in contrast to the regular method @{method insert} which inserts
+ closed rule statements.
\item @{method thin_tac}~@{text \<phi>} deletes the specified premise
from a subgoal. Note that @{text \<phi>} may contain schematic
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue Feb 28 11:10:09 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue Feb 28 11:45:40 2012 +0100
@@ -531,11 +531,11 @@
\cite{isabelle-implementation}).
\item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}} inserts facts into the proof state as
- assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
- \cite{isabelle-implementation}. Note that the scope of schematic
- variables is spread over the main goal statement. Instantiations
- may be given as well, see also ML tactic \verb|cut_inst_tac| in
- \cite{isabelle-implementation}.
+ assumption of a subgoal; instantiations may be given as well. Note
+ that the scope of schematic variables is spread over the main goal
+ statement and rule premises are turned into new subgoals. This is
+ in contrast to the regular method \hyperlink{method.insert}{\mbox{\isa{insert}}} which inserts
+ closed rule statements.
\item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} deletes the specified premise
from a subgoal. Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Feb 28 11:10:09 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Feb 28 11:45:40 2012 +0100
@@ -2207,7 +2207,7 @@
\begin{matharray}{rcl}
\indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
\end{matharray}
@@ -2217,7 +2217,7 @@
\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
\rail@end
\rail@begin{6}{}
-\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}[]
+\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
@@ -2304,13 +2304,13 @@
subgoals can be solved directly by an existing theorem. Duplicate
lemmas can be detected in this way.
- \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}} attempts to prove a subgoal
+ \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}} attempts to prove a subgoal
using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}},
\hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, etc.). Additional facts supplied
via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof methods.
\item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
- using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
+ using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
\item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal
using external automatic provers (resolution provers and SMT
--- a/src/HOL/Algebra/Coset.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Feb 28 11:45:40 2012 +0100
@@ -232,7 +232,7 @@
also from carr
have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
also from carr
- have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
+ have "\<dots> = x' \<otimes> \<one>" by simp
also from carr
have "\<dots> = x'" by simp
finally
@@ -520,8 +520,7 @@
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed
- r_one subgroup.subset [THEN subsetD])
+apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
done
@@ -612,7 +611,7 @@
fix x y
assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
and "inv x \<otimes> y \<in> H"
- hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
+ hence "inv (inv x \<otimes> y) \<in> H" by simp
thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
qed
next
@@ -722,7 +721,7 @@
assume abrcong: "(a, b) \<in> rcong H"
and ccarr: "c \<in> carrier G"
- from ccarr have "c \<in> Units G" by (simp add: Units_eq)
+ from ccarr have "c \<in> Units G" by simp
hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
from abrcong
--- a/src/HOL/Algebra/FiniteProduct.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Tue Feb 28 11:45:40 2012 +0100
@@ -190,7 +190,7 @@
lemma (in LCD) foldD_closed [simp]:
"[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
proof (induct set: finite)
- case empty then show ?case by (simp add: foldD_empty)
+ case empty then show ?case by simp
next
case insert then show ?case by (simp add: foldD_insert)
qed
@@ -328,7 +328,7 @@
apply fast
apply fast
apply assumption
- apply (fastforce intro: m_closed)
+ apply fastforce
apply simp+
apply fast
apply (auto simp add: finprod_def)
@@ -372,14 +372,13 @@
finprod G g A \<otimes> finprod G g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
proof (induct set: finite)
- case empty then show ?case by (simp add: finprod_closed)
+ case empty then show ?case by simp
next
case (insert a A)
then have a: "g a \<in> carrier G" by fast
from insert have A: "g \<in> A -> carrier G" by fast
from insert A a show ?case
- by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
- Int_mono2)
+ by (simp add: m_ac Int_insert_left insert_absorb Int_mono2)
qed
lemma finprod_Un_disjoint:
@@ -387,7 +386,7 @@
g \<in> A -> carrier G; g \<in> B -> carrier G |]
==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
apply (subst finprod_Un_Int [symmetric])
- apply (auto simp add: finprod_closed)
+ apply auto
done
lemma finprod_multf:
@@ -498,9 +497,8 @@
assumes fin: "finite A"
shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
- using fin apply induct
- apply (auto simp add: finprod_insert Pi_def)
-done
+ using fin
+ by induct (auto simp add: Pi_def)
lemma finprod_const:
assumes fin [simp]: "finite A"
@@ -512,7 +510,7 @@
apply auto
apply (subst m_comm)
apply auto
-done
+ done
(* The following lemma was contributed by Jesus Aransay. *)
--- a/src/HOL/Algebra/Ring.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Algebra/Ring.thy Tue Feb 28 11:45:40 2012 +0100
@@ -259,16 +259,12 @@
context ring begin
-lemma is_abelian_group:
- "abelian_group R"
- ..
+lemma is_abelian_group: "abelian_group R" ..
-lemma is_monoid:
- "monoid R"
+lemma is_monoid: "monoid R"
by (auto intro!: monoidI m_assoc)
-lemma is_ring:
- "ring R"
+lemma is_ring: "ring R"
by (rule ring_axioms)
end
@@ -444,12 +440,13 @@
show "\<one> = \<zero>" by simp
qed
-lemma carrier_one_zero:
- shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
- by (rule, erule one_zeroI, erule one_zeroD)
+lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
+ apply rule
+ apply (erule one_zeroI)
+ apply (erule one_zeroD)
+ done
-lemma carrier_one_not_zero:
- shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
+lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
by (simp add: carrier_one_zero)
end
@@ -571,7 +568,7 @@
from bcarr
have "b = \<one> \<otimes> b" by algebra
also from aUnit acarr
- have "... = (inv a \<otimes> a) \<otimes> b" by (simp add: Units_l_inv)
+ have "... = (inv a \<otimes> a) \<otimes> b" by simp
also from acarr bcarr aUnit[THEN Units_inv_closed]
have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
also from ab and acarr bcarr aUnit
--- a/src/HOL/Bali/AxCompl.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/AxCompl.thy Tue Feb 28 11:45:40 2012 +0100
@@ -1299,7 +1299,7 @@
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Jmp [THEN conseq1])
- apply (auto intro: eval.Jmp simp add: abupd_def2)
+ apply (auto intro: eval.Jmp)
done
next
case (Throw e)
--- a/src/HOL/Bali/AxSound.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/AxSound.thy Tue Feb 28 11:45:40 2012 +0100
@@ -78,8 +78,7 @@
done
lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
-apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
-done
+by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2)
lemma Methd_triple_valid2_SucI:
"\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk>
@@ -992,7 +991,7 @@
from da obtain V where
da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
- from eval obtain w upd where
+ from eval obtain upd where
eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_var P valid_A conf_s0 eval_var wt_var da_var
@@ -1408,7 +1407,7 @@
by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
with normal_s1 normal_s2 eval_args
have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
- by (auto dest: eval_gext intro: conf_gext)
+ by (auto dest: eval_gext)
from evaln_args wt_args da_args' conf_s1 wf
have conf_args: "list_all2 (conf G (store s2)) vs pTs"
by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
@@ -1491,7 +1490,7 @@
apply (rule dynM')
apply (force dest: ty_expr_is_type)
apply (rule invC_widen)
- apply (force intro: conf_gext dest: eval_gext)
+ apply (force dest: eval_gext)
apply simp
apply simp
apply (simp add: invC)
--- a/src/HOL/Bali/DeclConcepts.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Feb 28 11:45:40 2012 +0100
@@ -2241,7 +2241,7 @@
\<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
apply (simp only: accfield_def Let_def)
apply (rule table_of_remap_SomeD)
-apply (auto dest: filter_tab_SomeD)
+apply auto
done
--- a/src/HOL/Bali/Evaln.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/Evaln.thy Tue Feb 28 11:45:40 2012 +0100
@@ -233,7 +233,6 @@
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<midarrow>n\<rightarrow> (v, s')"
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')"
- "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')"
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
@@ -575,7 +574,6 @@
apply -
apply (rule evaln.Loop)
apply (iprover intro: evaln_nonstrict intro: le_maxI1)
-
apply (auto intro: evaln_nonstrict intro: le_maxI2)
done
then show ?case ..
--- a/src/HOL/Bali/Example.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/Example.thy Tue Feb 28 11:45:40 2012 +0100
@@ -975,7 +975,6 @@
done
declare mhead_resTy_simp [simp add]
-declare member_is_static_simp [simp add]
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
--- a/src/HOL/Bali/TypeSafe.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Tue Feb 28 11:45:40 2012 +0100
@@ -28,7 +28,7 @@
next
case New
then show ?case
- by (auto split: split_if_asm)
+ by auto
qed
with eqs
show ?thesis
@@ -68,19 +68,18 @@
\<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
apply (cases s)
apply (auto simp add: check_method_access_def Let_def error_free_def
- abrupt_if_def
- split: split_if_asm)
+ abrupt_if_def)
done
lemma error_free_FVar_lemma:
"error_free s
\<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
- by (case_tac s) (auto split: split_if)
+ by (case_tac s) auto
lemma error_free_init_lvars [simp,intro]:
"error_free s \<Longrightarrow>
error_free (init_lvars G C sig mode a pvs s)"
-by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
+by (cases s) (auto simp add: init_lvars_def Let_def)
lemma error_free_LVar_lemma:
"error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
@@ -362,12 +361,12 @@
case CInst
with modeIntVir obj_props
show ?thesis
- by (auto dest!: widen_Array2 split add: split_if)
+ by (auto dest!: widen_Array2)
next
case Arr
- from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
+ from Arr obtain T where "obj_ty obj = T.[]" by blast
moreover from Arr have "obj_class obj = Object"
- by (blast dest: obj_class_Arr1)
+ by blast
moreover note modeIntVir obj_props wf
ultimately show ?thesis by (auto dest!: widen_Array )
qed
@@ -411,8 +410,7 @@
dynimethd_def dynmethd_C_C
intro: dynmethd_declclass
dest!: wf_imethdsD
- dest: table_of_map_SomeI
- split: split_if_asm)
+ dest: table_of_map_SomeI)
next
case SuperM
with not_SuperM show ?thesis ..
@@ -421,8 +419,7 @@
with wf dynlookup IfaceT invC_prop show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
DynT_prop_def
- intro: methd_declclass dynmethd_declclass
- split: split_if_asm)
+ intro: methd_declclass dynmethd_declclass)
qed
next
case ClassT
@@ -1851,7 +1848,7 @@
(*
wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
- by (rule wt_elim_cases) (auto split add: split_if)
+ by (rule wt_elim_cases) auto
from If.prems obtain E C where
da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state)))
\<guillemotright>In1l e\<guillemotright> E" and
@@ -3978,7 +3975,7 @@
obtain
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
- by (elim wt_elim_cases) (auto split add: split_if)
+ by (elim wt_elim_cases) auto
from If.prems obtain E C where
da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state)))
\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
--- a/src/HOL/Bali/WellType.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Bali/WellType.thy Tue Feb 28 11:45:40 2012 +0100
@@ -546,7 +546,7 @@
then show ?thesis by blast
next
case False then show ?thesis
- by (auto simp add: invmode_def split: split_if_asm)
+ by (auto simp add: invmode_def)
qed
qed
--- a/src/HOL/Big_Operators.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Big_Operators.thy Tue Feb 28 11:45:40 2012 +0100
@@ -523,6 +523,25 @@
case insert thus ?case by (auto simp: add_strict_mono)
qed
+lemma setsum_strict_mono_ex1:
+fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
+assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
+shows "setsum f A < setsum g A"
+proof-
+ from assms(3) obtain a where a: "a:A" "f a < g a" by blast
+ have "setsum f A = setsum f ((A-{a}) \<union> {a})"
+ by(simp add:insert_absorb[OF `a:A`])
+ also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
+ using `finite A` by(subst setsum_Un_disjoint) auto
+ also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
+ by(rule setsum_mono)(simp add: assms(2))
+ also have "setsum f {a} < setsum g {a}" using a by simp
+ also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
+ using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
+ also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
+ finally show ?thesis by (metis add_right_mono add_strict_left_mono)
+qed
+
lemma setsum_negf:
"setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
proof (cases "finite A")
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Tue Feb 28 11:45:40 2012 +0100
@@ -93,7 +93,7 @@
val norm_eq_th =
simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
in
- cut_rules_tac [norm_eq_th] i
+ cut_tac norm_eq_th i
THEN (simp_tac cring_ss i)
THEN (simp_tac cring_ss i)
end);
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Feb 28 11:45:40 2012 +0100
@@ -732,7 +732,7 @@
val tac =
EVERY
[rtac @{thm trans} 1, rtac map_ID_thm 2,
- cut_facts_tac [lub_take_lemma] 1,
+ cut_tac lub_take_lemma 1,
REPEAT (etac @{thm Pair_inject} 1), atac 1]
val lub_take_thm = Goal.prove_global thy [] [] goal (K tac)
in
--- a/src/HOL/IsaMakefile Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 28 11:45:40 2012 +0100
@@ -61,7 +61,6 @@
HOL-Nitpick_Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
- HOL-Quickcheck_Examples \
HOL-Quotient_Examples \
HOL-Predicate_Compile_Examples \
HOL-Prolog \
@@ -96,7 +95,7 @@
HOL-Nominal-Examples
all: test-no-smlnj test images-no-smlnj images
-full: all benchmark
+full: all benchmark HOL-Quickcheck_Examples
smlnj: test images
@@ -964,11 +963,10 @@
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
-$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL \
- MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \
- MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \
- MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \
- MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \
+$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
+ MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy \
+ MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy \
+ MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy \
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \
MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
@@ -985,7 +983,8 @@
MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \
MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \
MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \
- MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy \
+ MicroJava/DFA/Semilattices.thy \
+ MicroJava/DFA/Typing_Framework_err.thy \
MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \
MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy \
MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \
--- a/src/HOL/List.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/List.thy Tue Feb 28 11:45:40 2012 +0100
@@ -960,6 +960,8 @@
subsubsection {* @{text set} *}
+declare set.simps [code_post] --"pretty output"
+
lemma finite_set [iff]: "finite (set xs)"
by (induct xs) auto
--- a/src/HOL/Matrix/Matrix.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Matrix/Matrix.thy Tue Feb 28 11:45:40 2012 +0100
@@ -849,7 +849,7 @@
"singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where
- "move_matrix A y x == Abs_matrix(% j i. if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
+ "move_matrix A y x == Abs_matrix(% j i. if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
"take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
@@ -930,7 +930,7 @@
lemma Rep_move_matrix[simp]:
"Rep_matrix (move_matrix A y x) j i =
- (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
+ (if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
apply (simp add: move_matrix_def)
apply (auto)
by (subst RepAbs_matrix,
@@ -959,8 +959,8 @@
apply (case_tac "j + int u < 0")
apply (simp, arith)
apply (case_tac "i + int v < 0")
- apply (simp add: neg_def, arith)
- apply (simp add: neg_def)
+ apply (simp, arith)
+ apply simp
apply arith
done
@@ -1016,7 +1016,6 @@
apply (subst foldseq_almostzero[of _ j])
apply (simp add: assms)+
apply (auto)
- apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
done
lemma mult_matrix_ext:
@@ -1440,19 +1439,19 @@
done
lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
lemma move_matrix_le_move_matrix_iff[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
--- a/src/HOL/Matrix/SparseMatrix.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy Tue Feb 28 11:45:40 2012 +0100
@@ -97,7 +97,7 @@
apply (auto)
apply (frule sorted_spvec_cons2, simp)
apply (frule sorted_spvec_cons3, simp)
- apply (simp add: sparse_row_matrix_cons neg_def)
+ apply (simp add: sparse_row_matrix_cons)
done
primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
@@ -273,7 +273,6 @@
apply (simp add: algebra_simps sparse_row_matrix_cons)
apply (simplesubst Rep_matrix_zero_imp_mult_zero)
apply (simp)
- apply (intro strip)
apply (rule disjI2)
apply (intro strip)
apply (subst nrows)
@@ -284,7 +283,6 @@
apply (case_tac "k <= j")
apply (rule_tac m1 = k and n1 = i and a1 = a in ssubst[OF sorted_sparse_row_vector_zero])
apply (simp_all)
- apply (rule impI)
apply (rule disjI2)
apply (rule nrows)
apply (rule order_trans[of _ 1])
@@ -297,7 +295,7 @@
apply (simp)
apply (rule disjI2)
apply (intro strip)
- apply (simp add: sparse_row_matrix_cons neg_def)
+ apply (simp add: sparse_row_matrix_cons)
apply (case_tac "i <= j")
apply (erule sorted_sparse_row_matrix_zero)
apply (simp_all)
@@ -315,7 +313,6 @@
apply (auto)
apply (rule_tac m=k and n = j and a = a and arr=arr in sorted_sparse_row_vector_zero)
apply (simp_all)
- apply (simp add: neg_def)
apply (drule nrows_notzero)
apply (drule nrows_helper)
apply (arith)
@@ -647,7 +644,7 @@
lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]:
"j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
- apply (auto simp add: neg_def disj_matrices_def)
+ apply (auto simp add: disj_matrices_def)
apply (drule nrows_notzero)
apply (drule less_le_trans[OF _ nrows_spvec])
apply (subgoal_tac "ja = j")
@@ -664,7 +661,7 @@
lemma disj_move_sparse_row_vector_twice:
"j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
- apply (auto simp add: neg_def disj_matrices_def)
+ apply (auto simp add: disj_matrices_def)
apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
done
@@ -783,7 +780,7 @@
apply (simplesubst sorted_sparse_row_matrix_zero)
apply auto
apply (simplesubst Rep_sparse_row_vector_zero)
- apply (simp_all add: neg_def)
+ apply simp_all
done
lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"
--- a/src/HOL/MicroJava/BV/Effect.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Feb 28 11:45:40 2012 +0100
@@ -217,10 +217,10 @@
{
fix x
assume "length x = Suc 0"
- hence "\<exists> l. x = [l]" by - (cases x, auto)
+ hence "\<exists> l. x = [l]" by (cases x) auto
} note 0 = this
- have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a) (auto dest: 0)
with * show ?thesis by (auto dest: 0)
qed
--- a/src/HOL/MicroJava/Comp/NatCanonify.thy Tue Feb 28 11:10:09 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: HOL/MicroJava/Comp/NatCanonify.thy
- Author: Martin Strecker
-*)
-
-theory NatCanonify imports Main begin
-
-(************************************************************************)
- (* Canonizer for converting nat to int *)
-(************************************************************************)
-
-lemma nat_add_canonify: "(n1::nat) + n2 = nat ((int n1) + (int n2))"
-by (simp add: nat_add_distrib)
-
-lemma nat_mult_canonify: "(n1::nat) * n2 = nat ((int n1) * (int n2))"
-by (simp add: nat_mult_distrib)
-
-lemma nat_diff_canonify: "(n1::nat) - n2 =
- nat (if (int n1) \<le> (int n2) then 0 else (int n1) - (int n2))"
-by (simp add: zdiff_int nat_int)
-
-lemma nat_le_canonify: "((n1::nat) \<le> n2) = ((int n1) \<le> (int n2))"
-by arith
-
-lemma nat_less_canonify: "((n1::nat) < n2) = ((int n1) < (int n2))"
-by arith
-
-lemma nat_eq_canonify: "((n1::nat) = n2) = ((int n1) = (int n2))"
-by arith
-
-lemma nat_if_canonify: "(if b then (n1::nat) else n2) =
- nat (if b then (int n1) else (int n2))"
-by simp
-
-lemma int_nat_canonify: "(int (nat n)) = (if 0 \<le> n then n else 0)"
-by simp
-
-lemmas nat_canonify =
- nat_add_canonify nat_mult_canonify nat_diff_canonify
- nat_le_canonify nat_less_canonify nat_eq_canonify nat_if_canonify
- int_nat_canonify nat_int
-
-end
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Feb 28 11:45:40 2012 +0100
@@ -169,7 +169,7 @@
lemma (in lbv) top_le_conv [simp]:
"\<top> <=_r x = (x = \<top>)"
- by (insert semilat) (simp add: top top_le_conv)
+ using semilat by (simp add: top)
lemma (in lbv) neq_top [simp, elim]:
"\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"
--- a/src/HOL/Mutabelle/Mutabelle.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Mutabelle/Mutabelle.thy Tue Feb 28 11:45:40 2012 +0100
@@ -1,3 +1,5 @@
+(* FIXME dead code!?!? *)
+
theory Mutabelle
imports Main
uses "mutabelle.ML"
@@ -26,7 +28,7 @@
[@{const_name nibble_pair_of_char}];
fun is_forbidden s th =
- exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
+ exists (fn s' => s' mem Long_Name.explode s) forbidden_thms orelse
exists (fn s' => s' mem (Term.add_const_names (prop_of th) [])) forbidden_consts;
fun test j = List.app (fn i =>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 28 11:45:40 2012 +0100
@@ -235,13 +235,13 @@
fun is_forbidden_theorem (s, th) =
let val consts = Term.add_const_names (prop_of th) [] in
- exists (member (op =) (space_explode "." s)) forbidden_thms orelse
+ exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
exists (member (op =) forbidden_consts) consts orelse
- length (space_explode "." s) <> 2 orelse
- String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
+ length (Long_Name.explode s) <> 2 orelse
+ String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
String.isSuffix "_def" s orelse
String.isSuffix "_raw" s orelse
- String.isPrefix "term_of" (List.last (space_explode "." s))
+ String.isPrefix "term_of" (List.last (Long_Name.explode s))
end
val forbidden_mutant_constnames =
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 28 11:45:40 2012 +0100
@@ -154,9 +154,9 @@
end
fun is_forbidden_theorem name =
- length (space_explode "." name) <> 2 orelse
- String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse
- String.isPrefix "arity_" (List.last (space_explode "." name)) orelse
+ length (Long_Name.explode name) <> 2 orelse
+ String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
+ String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
String.isSuffix "_def" name orelse
String.isSuffix "_raw" name
--- a/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Tue Feb 28 11:45:40 2012 +0100
@@ -25,4 +25,4 @@
find_unused_assms List
find_unused_assms Map
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/etc/settings Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/TPTP/etc/settings Tue Feb 28 11:45:40 2012 +0100
@@ -2,4 +2,4 @@
TPTP_HOME="$COMPONENT"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$TPTP_HOME/lib/Tools"
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Feb 28 11:45:40 2012 +0100
@@ -493,7 +493,7 @@
fun new_skolem_const_name s num_T_args =
[new_skolem_const_prefix, s, string_of_int num_T_args]
- |> space_implode Long_Name.separator
+ |> Long_Name.implode
fun robust_const_type thy s =
if s = app_op_name then
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 28 11:45:40 2012 +0100
@@ -360,7 +360,7 @@
constant name. *)
fun num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
- s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ s |> Long_Name.explode |> List.last |> Int.fromString |> the
else if String.isPrefix lam_lifted_prefix s then
if String.isPrefix lam_lifted_poly_prefix s then 2 else 0
else
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Feb 28 11:45:40 2012 +0100
@@ -102,7 +102,7 @@
val unyxml = XML.content_of o YXML.parse_body
-val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
+val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode
fun maybe_quote y =
let val s = unyxml y in
y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Tue Feb 28 11:45:40 2012 +0100
@@ -433,7 +433,7 @@
let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
EVERY [
simp_tac (HOL_ss addsimps [hd prems]) 1,
- cut_facts_tac [nchotomy''] 1,
+ cut_tac nchotomy'' 1,
REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
end)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Feb 28 11:45:40 2012 +0100
@@ -437,7 +437,7 @@
val prems = prems0 |> map normalize_literal
|> distinct Term.aconv_untyped
val goal = Logic.list_implies (prems, concl)
- val tac = cut_rules_tac [th] 1
+ val tac = cut_tac th 1
THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
THEN ALLGOALS assume_tac
in
@@ -730,7 +730,7 @@
cat_lines (map string_for_subst_info substs))
*)
fun cut_and_ex_tac axiom =
- cut_rules_tac [axiom] 1
+ cut_tac axiom 1
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
fun rotation_for_subgoal i =
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 28 11:45:40 2012 +0100
@@ -94,7 +94,7 @@
exception NOT_SUPPORTED of string
exception SAME of unit
-val nitpick_prefix = "Nitpick."
+val nitpick_prefix = "Nitpick" ^ Long_Name.separator
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Feb 28 11:45:40 2012 +0100
@@ -41,7 +41,7 @@
val ctxt' = ctxt
|> Config.put Quickcheck.abort_potential true
|> Config.put Quickcheck.quiet true
- val all_thms = filter (fn (s, _) => length (space_explode "." s) = 2)
+ val all_thms = filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *)
(thms_of (Proof_Context.theory_of ctxt) thy_name)
fun check_single conjecture =
case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
@@ -84,7 +84,6 @@
fun print_unused_assms ctxt opt_thy_name =
let
- val start = Timing.start ()
val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
val results = find_unused_assms ctxt thy_name
val total = length results
@@ -97,7 +96,6 @@
val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
^ " in the theory " ^ quote thy_name
^ " with a total of " ^ string_of_int total ^ " theorem(s)"
- ^ " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
in
([Pretty.str (msg ^ ":"), Pretty.str ""] @
map pretty_thm with_superfluous_assumptions
--- a/src/HOL/Tools/inductive.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Feb 28 11:45:40 2012 +0100
@@ -432,7 +432,7 @@
in
(Skip_Proof.prove ctxt'' [] prems P
(fn {prems, ...} => EVERY
- [cut_facts_tac [hd prems] 1,
+ [cut_tac (hd prems) 1,
rewrite_goals_tac rec_preds_defs,
dtac (unfold RS iffD1) 1,
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
--- a/src/HOL/Tools/inductive_realizer.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Feb 28 11:45:40 2012 +0100
@@ -456,7 +456,7 @@
val rews = map mk_meta_eq case_thms;
val thm = Goal.prove_global thy []
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
- [cut_facts_tac [hd prems] 1,
+ [cut_tac (hd prems) 1,
etac elimR 1,
ALLGOALS (asm_simp_tac HOL_basic_ss),
rewrite_goals_tac rews,
--- a/src/HOL/Tools/lin_arith.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/lin_arith.ML Tue Feb 28 11:45:40 2012 +0100
@@ -901,7 +901,7 @@
val setup =
init_arith_data #>
Simplifier.map_ss (fn ss => ss
- addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
+ addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac)));
val global_setup =
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
--- a/src/HOL/Tools/record.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/Tools/record.ML Tue Feb 28 11:45:40 2012 +0100
@@ -1623,7 +1623,7 @@
let val (assm, concl) = induct_prop in
Skip_Proof.prove_global defs_thy [] [assm] concl
(fn {prems, ...} =>
- cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
+ cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
resolve_tac prems 2 THEN
asm_simp_tac HOL_ss 1)
end);
--- a/src/HOL/ex/Meson_Test.thy Tue Feb 28 11:10:09 2012 +0100
+++ b/src/HOL/ex/Meson_Test.thy Tue Feb 28 11:45:40 2012 +0100
@@ -28,7 +28,7 @@
val nnf25 = Meson.make_nnf @{context} prem25;
val xsko25 = Meson.skolemize @{context} nnf25;
*}
- apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *})
+ apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
val clauses25 = Meson.make_clauses @{context} [sko25]; (*7 clauses*)
@@ -49,7 +49,7 @@
val nnf26 = Meson.make_nnf @{context} prem26;
val xsko26 = Meson.skolemize @{context} nnf26;
*}
- apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *})
+ apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
val clauses26 = Meson.make_clauses @{context} [sko26]; (*9 clauses*)
@@ -71,7 +71,7 @@
val nnf43 = Meson.make_nnf @{context} prem43;
val xsko43 = Meson.skolemize @{context} nnf43;
*}
- apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *})
+ apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
val clauses43 = Meson.make_clauses @{context} [sko43]; (*6*)
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Feb 28 11:45:40 2012 +0100
@@ -1,9 +1,7 @@
(* Title: Provers/Arith/fast_lin_arith.ML
Author: Tobias Nipkow and Tjark Weber and Sascha Boehme
-A generic linear arithmetic package. It provides two tactics
-(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
-(lin_arith_simproc).
+A generic linear arithmetic package.
Only take premises and conclusions into account that are already
(negated) (in)equations. lin_arith_simproc tries to prove or disprove
@@ -88,7 +86,7 @@
signature FAST_LIN_ARITH =
sig
- val cut_lin_arith_tac: simpset -> int -> tactic
+ val prems_lin_arith_tac: simpset -> int -> tactic
val lin_arith_tac: Proof.context -> bool -> int -> tactic
val lin_arith_simproc: simpset -> term -> thm option
val map_data:
@@ -846,8 +844,8 @@
refute_tac ss (i, split_neq, js))
end);
-fun cut_lin_arith_tac ss =
- cut_facts_tac (Simplifier.prems_of ss) THEN'
+fun prems_lin_arith_tac ss =
+ Method.insert_tac (Simplifier.prems_of ss) THEN'
simpset_lin_arith_tac ss false;
fun lin_arith_tac ctxt =
--- a/src/Provers/blast.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Provers/blast.ML Tue Feb 28 11:45:40 2012 +0100
@@ -1251,7 +1251,7 @@
NONE => (writeln ("PROOF FAILED for depth " ^
string_of_int lim);
backtrack trace choices)
- | cell => (if (trace orelse stats)
+ | cell => (if trace orelse stats
then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
else ();
Seq.make(fn()=> cell))
--- a/src/Pure/Concurrent/counter.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Concurrent/counter.scala Tue Feb 28 11:45:40 2012 +0100
@@ -16,7 +16,7 @@
def apply(): Counter = new Counter
}
-class Counter private
+final class Counter private
{
private var count: Counter.ID = 0
--- a/src/Pure/Concurrent/volatile.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Concurrent/volatile.scala Tue Feb 28 11:45:40 2012 +0100
@@ -14,7 +14,7 @@
}
-class Volatile[A] private(init: A)
+final class Volatile[A] private(init: A)
{
@volatile private var state: A = init
def apply(): A = state
--- a/src/Pure/General/graph.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/General/graph.scala Tue Feb 28 11:45:40 2012 +0100
@@ -27,7 +27,7 @@
}
-class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
+final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
{
type Keys = SortedSet[Key]
type Entry = (A, (Keys, Keys))
--- a/src/Pure/General/linear_set.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/General/linear_set.scala Tue Feb 28 11:45:40 2012 +0100
@@ -26,7 +26,7 @@
}
-class Linear_Set[A] private(
+final class Linear_Set[A] private(
start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
extends scala.collection.immutable.Set[A]
with GenericSetTemplate[A, Linear_Set]
--- a/src/Pure/General/path.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/General/path.scala Tue Feb 28 11:45:40 2012 +0100
@@ -98,7 +98,7 @@
}
-class Path private(private val elems: List[Path.Elem]) // reversed elements
+final class Path private(private val elems: List[Path.Elem]) // reversed elements
{
def is_current: Boolean = elems.isEmpty
def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
--- a/src/Pure/General/scan.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/General/scan.scala Tue Feb 28 11:45:40 2012 +0100
@@ -40,7 +40,7 @@
def apply(elems: String*): Lexicon = empty ++ elems
}
- class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
+ final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
{
import Lexicon.Tree
--- a/src/Pure/General/time.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/General/time.scala Tue Feb 28 11:45:40 2012 +0100
@@ -14,7 +14,7 @@
def ms(m: Long): Time = new Time(m)
}
-class Time private(val ms: Long)
+final class Time private(val ms: Long)
{
def seconds: Double = ms / 1000.0
--- a/src/Pure/Isar/outer_syntax.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Feb 28 11:45:40 2012 +0100
@@ -37,7 +37,7 @@
def init(): Outer_Syntax = new Outer_Syntax()
}
-class Outer_Syntax private(
+final class Outer_Syntax private(
keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.init())
--- a/src/Pure/PIDE/command.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/PIDE/command.scala Tue Feb 28 11:45:40 2012 +0100
@@ -121,7 +121,7 @@
}
-class Command private(
+final class Command private(
val id: Document.Command_ID,
val node_name: Document.Node.Name,
val span: List[Token],
--- a/src/Pure/PIDE/document.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/PIDE/document.scala Tue Feb 28 11:45:40 2012 +0100
@@ -29,7 +29,7 @@
/** document structure **/
- /* named nodes -- development graph */
+ /* individual nodes */
type Edit[A, B] = (Node.Name, Node.Edit[A, B])
type Edit_Text = Edit[Text.Edit, Text.Perspective]
@@ -49,6 +49,11 @@
val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
Name(node, dir, theory)
}
+
+ object Ordering extends scala.math.Ordering[Name]
+ {
+ def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
+ }
}
sealed case class Name(node: String, dir: String, theory: String)
{
@@ -98,7 +103,7 @@
val empty: Node = new Node()
}
- class Node private(
+ final class Node private(
val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
val perspective: Command.Perspective = Command.Perspective.empty,
val blobs: Map[String, Blob] = Map.empty,
@@ -169,13 +174,50 @@
}
+ /* development graph */
+
+ object Nodes
+ {
+ val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
+ }
+
+ final class Nodes private(graph: Graph[Node.Name, Node])
+ {
+ def get_name(s: String): Option[Node.Name] =
+ graph.keys.find(name => name.node == s)
+
+ def apply(name: Node.Name): Node =
+ graph.default_node(name, Node.empty).get_node(name)
+
+ def + (entry: (Node.Name, Node)): Nodes =
+ {
+ val (name, node) = entry
+ val parents =
+ node.header match {
+ case Exn.Res(header) =>
+ // FIXME official names of yet unknown nodes!?
+ for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
+ case _ => Nil
+ }
+ val graph1 =
+ (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
+ val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
+ val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
+ new Nodes(graph3.map_node(name, _ => node))
+ }
+
+ def entries: Iterator[(Node.Name, Node)] =
+ graph.entries.map({ case (name, (node, _)) => (name, node) })
+
+ def topological_order: List[Node.Name] = graph.topological_order
+ }
+
+
/** versioning **/
/* particular document versions */
- type Nodes = Map[Node.Name, Node]
-
object Version
{
val init: Version = new Version()
@@ -183,22 +225,9 @@
def make(nodes: Nodes): Version = new Version(new_id(), nodes)
}
- class Version private(
+ final class Version private(
val id: Version_ID = no_id,
- val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
- {
- def topological_order: List[Node.Name] =
- {
- val names = nodes.map({ case (name, node) => (name.node -> name) })
- def next(x: Node.Name): List[Node.Name] =
- nodes(x).header match {
- case Exn.Res(header) =>
- for (imp <- header.imports; name <- names.get(imp)) yield(name)
- case Exn.Exn(_) => Nil
- }
- Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
- }
- }
+ val nodes: Nodes = Nodes.empty)
/* changes of plain text, eventually resulting in document edits */
@@ -211,7 +240,7 @@
new Change(Some(previous), edits, version)
}
- class Change private(
+ final class Change private(
val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
val edits: List[Edit_Text] = Nil,
val version: Future[Version] = Future.value(Version.init))
@@ -231,7 +260,7 @@
val init: History = new History()
}
- class History private(
+ final class History private(
val undo_list: List[Change] = List(Change.init)) // non-empty list
{
def tip: Change = undo_list.head
@@ -282,7 +311,7 @@
val init: Assignment = new Assignment()
}
- class Assignment private(
+ final class Assignment private(
val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
val last_execs: Map[String, Option[Command_ID]] = Map.empty,
val is_finished: Boolean = false)
@@ -307,7 +336,7 @@
State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
}
- sealed case class State private(
+ final case class State private(
val versions: Map[Version_ID, Version] = Map.empty,
val commands: Map[Command_ID, Command.State] = Map.empty, // static markup from define_command
val execs: Map[Exec_ID, Command.State] = Map.empty, // dynamic markup from execution
@@ -440,7 +469,7 @@
for {
(version_id, version) <- versions1.iterator
val command_execs = assignments1(version_id).command_execs
- (_, node) <- version.nodes.iterator
+ (_, node) <- version.nodes.entries
command <- node.commands.iterator
} {
val id = command.id
--- a/src/Pure/PIDE/markup_tree.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Tue Feb 28 11:45:40 2012 +0100
@@ -45,7 +45,7 @@
}
-class Markup_Tree private(branches: Markup_Tree.Branches.T)
+final class Markup_Tree private(branches: Markup_Tree.Branches.T)
{
private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
this(branches + (entry.range -> entry))
--- a/src/Pure/PIDE/text.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/PIDE/text.scala Tue Feb 28 11:45:40 2012 +0100
@@ -98,7 +98,8 @@
}
}
- class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
+ final class Perspective private(
+ val ranges: List[Range]) // visible text partitioning in canonical order
{
def is_empty: Boolean = ranges.isEmpty
def range: Range =
@@ -134,7 +135,7 @@
def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
}
- class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
+ final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
{
override def toString =
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Feb 28 11:45:40 2012 +0100
@@ -642,7 +642,7 @@
fun splitthy id =
let val comps = Long_Name.explode id
in case comps of
- (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
+ (thy::(rest as _::_)) => (Thy_Info.get_theory thy, Long_Name.implode rest)
| [plainid] => (topthy(),plainid)
| _ => raise Toplevel.UNDEF (* assert false *)
end
--- a/src/Pure/Thy/completion.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Thy/completion.scala Tue Feb 28 11:45:40 2012 +0100
@@ -40,7 +40,7 @@
}
}
-class Completion private(
+final class Completion private(
words_lex: Scan.Lexicon = Scan.Lexicon.empty,
words_map: Map[String, String] = Map.empty,
abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
--- a/src/Pure/Tools/find_consts.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Tools/find_consts.ML Tue Feb 28 11:45:40 2012 +0100
@@ -69,8 +69,6 @@
fun find_consts ctxt raw_criteria =
let
- val start = Timing.start ();
-
val thy = Proof_Context.theory_of ctxt;
val low_ranking = 10000;
@@ -113,15 +111,13 @@
|> map_filter I
|> sort (rev_order o int_ord o pairself snd)
|> map (apsnd fst o fst);
-
- val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
in
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
Pretty.str "" ::
Pretty.str
(if null matches
- then "nothing found" ^ end_msg
- else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
+ then "nothing found"
+ else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
Pretty.str "" ::
map (pretty_const ctxt) matches
end |> Pretty.chunks |> Pretty.writeln;
--- a/src/Pure/Tools/find_theorems.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML Tue Feb 28 11:45:40 2012 +0100
@@ -1,5 +1,6 @@
(* Title: Pure/Tools/find_theorems.ML
Author: Rafal Kolanski and Gerwin Klein, NICTA
+ Author: Lars Noschinski and Alexander Krauss, TU Muenchen
Retrieve theorems from proof context.
*)
@@ -7,8 +8,7 @@
signature FIND_THEOREMS =
sig
datatype 'term criterion =
- Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
- Pattern of 'term
+ Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
datatype theorem =
Internal of Facts.ref * thm | External of Facts.ref * term
@@ -52,8 +52,7 @@
(** search criteria **)
datatype 'term criterion =
- Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
- Pattern of 'term;
+ Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
fun apply_dummies tm =
let
@@ -76,7 +75,6 @@
fun read_criterion _ (Name name) = Name name
| read_criterion _ Intro = Intro
- | read_criterion _ IntroIff = IntroIff
| read_criterion _ Elim = Elim
| read_criterion _ Dest = Dest
| read_criterion _ Solves = Solves
@@ -90,7 +88,6 @@
(case c of
Name name => Pretty.str (prfx "name: " ^ quote name)
| Intro => Pretty.str (prfx "intro")
- | IntroIff => Pretty.str (prfx "introiff")
| Elim => Pretty.str (prfx "elim")
| Dest => Pretty.str (prfx "dest")
| Solves => Pretty.str (prfx "solves")
@@ -112,11 +109,10 @@
};
fun map_criteria f {goal, limit, rem_dups, criteria} =
- {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
+ {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
| xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
- | xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , [])
| xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
| xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
| xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
@@ -125,7 +121,6 @@
fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
| criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
- | criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff
| criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
| criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
| criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
@@ -133,7 +128,7 @@
| criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
| criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
-fun xml_of_query {goal=NONE, limit, rem_dups, criteria} =
+fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
let
val properties = []
|> (if rem_dups then cons ("rem_dups", "") else I)
@@ -152,7 +147,7 @@
XML.Decode.list (XML.Decode.pair XML.Decode.bool
(criterion_of_xml o the_single)) body;
in
- {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
+ {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
end
| query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
@@ -178,8 +173,9 @@
let
val name = the (Properties.get properties "name");
val pos = Position.of_properties properties;
- val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
- (Properties.get properties "index");
+ val intvs_opt =
+ Option.map (single o Facts.Single o Markup.parse_int)
+ (Properties.get properties "index");
in
External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
end
@@ -234,32 +230,17 @@
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
-(*educated guesses on HOL*) (* FIXME utterly broken *)
-val boolT = Type ("bool", []);
-val iff_const = Const ("op =", boolT --> boolT --> boolT);
-
(*extract terms from term_src, refine them to the parts that concern us,
if po try match them against obj else vice versa.
trivial matches are ignored.
returns: smallest substitution size*)
-fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
+fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
let
val thy = Proof_Context.theory_of ctxt;
- fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun matches pat =
- let
- val jpat = Object_Logic.drop_judgment thy pat;
- val c = Term.head_of jpat;
- val pats =
- if Term.is_Const c
- then
- if doiff andalso c = iff_const then
- (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
- |> filter (is_nontrivial thy)
- else [pat]
- else [];
- in filter check_match pats end;
+ is_nontrivial thy pat andalso
+ Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun substsize pat =
let val (_, subst) =
@@ -271,8 +252,7 @@
val match_thm = matches o refine_term;
in
- maps match_thm (extract_terms term_src)
- |> map substsize
+ map (substsize o refine_term) (filter match_thm (extract_terms term_src))
|> bestmatch
end;
@@ -293,7 +273,7 @@
hd o Logic.strip_imp_prems);
val prems = Logic.prems_of_goal goal 1;
- fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem;
+ fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
val successful = prems |> map_filter try_subst;
in
(*if possible, keep best substitution (one with smallest size)*)
@@ -303,11 +283,11 @@
then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
end;
-fun filter_intro doiff ctxt goal theorem =
+fun filter_intro ctxt goal theorem =
let
val extract_intro = (single o prop_of, Logic.strip_imp_concl);
val concl = Logic.concl_of_goal goal 1;
- val ss = is_matching_thm doiff extract_intro ctxt true concl theorem;
+ val ss = is_matching_thm extract_intro ctxt true concl theorem;
in
if is_some ss then SOME (nprems_of theorem, the ss) else NONE
end;
@@ -323,8 +303,7 @@
fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
val rule_tree = combine rule_mp rule_concl;
fun goal_tree prem = combine prem goal_concl;
- fun try_subst prem =
- is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
+ fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
val successful = prems |> map_filter try_subst;
in
(*elim rules always have assumptions, so an elim with one
@@ -333,7 +312,7 @@
andalso not (null successful)
then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
end
- else NONE
+ else NONE;
val tac_limit = Unsynchronized.ref 5;
@@ -358,7 +337,7 @@
val mksimps = Simplifier.mksimps (simpset_of ctxt);
val extract_simp =
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
- val ss = is_matching_thm false extract_simp ctxt false t thm;
+ val ss = is_matching_thm extract_simp ctxt false t thm;
in
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
end
@@ -403,12 +382,10 @@
fun filter_crit _ _ (Name name) = apfst (filter_name name)
| filter_crit _ NONE Intro = err_no_goal "intro"
- | filter_crit _ NONE IntroIff = err_no_goal "introiff"
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
| filter_crit _ NONE Solves = err_no_goal "solves"
- | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal))
- | filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
@@ -448,7 +425,6 @@
fun lazy_filter filters =
let
fun lazy_match thms = Seq.make (fn () => first_match thms)
-
and first_match [] = NONE
| first_match (thm :: thms) =
(case app_filters thm (SOME (0, 0), NONE, filters) of
@@ -489,7 +465,7 @@
fun nicer_shortest ctxt =
let
- (* FIXME global name space!? *)
+ (* FIXME Why global name space!?? *)
val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
val shorten =
@@ -532,7 +508,7 @@
fun filter_theorems ctxt theorems query =
let
- val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query
+ val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
val filters = map (filter_criterion ctxt opt_goal) criteria;
fun find_all theorems =
@@ -555,8 +531,8 @@
in find theorems end;
-fun filter_theorems_cmd ctxt theorems raw_query =
- filter_theorems ctxt theorems (map_criteria
+fun filter_theorems_cmd ctxt theorems raw_query =
+ filter_theorems ctxt theorems (map_criteria
(map (apsnd (read_criterion ctxt))) raw_query);
fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
@@ -567,8 +543,8 @@
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
val opt_goal' = Option.map add_prems opt_goal;
in
- filter ctxt (map Internal (all_facts_of ctxt))
- {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria}
+ filter ctxt (map Internal (all_facts_of ctxt))
+ {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
|> apsnd (map (fn Internal f => f))
end;
@@ -586,11 +562,9 @@
fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
let
- val start = Timing.start ();
-
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (foundo, theorems) = find
- {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
+ {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;
val tally_msg =
@@ -601,14 +575,12 @@
(if returned < found
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
-
- val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
Pretty.str "" ::
- (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
+ (if null theorems then [Pretty.str "nothing found"]
else
- [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
+ [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
map (pretty_theorem ctxt) theorems)
end |> Pretty.chunks |> Pretty.writeln;
@@ -616,6 +588,7 @@
gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
+
(** command syntax **)
local
@@ -623,7 +596,6 @@
val criterion =
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
Parse.reserved "intro" >> K Intro ||
- Parse.reserved "introiff" >> K IntroIff ||
Parse.reserved "elim" >> K Elim ||
Parse.reserved "dest" >> K Dest ||
Parse.reserved "solves" >> K Solves ||
--- a/src/Pure/library.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/library.scala Tue Feb 28 11:45:40 2012 +0100
@@ -128,26 +128,6 @@
}
- /* graph traversal */
-
- def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] =
- {
- type Reached = (List[A], Set[A])
- def reach(reached: Reached, x: A): Reached =
- {
- val (rs, r_set) = reached
- if (r_set(x)) reached
- else {
- val (rs1, r_set1) = reachs((rs, r_set + x), next(x))
- (x :: rs1, r_set1)
- }
- }
- def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach)
-
- reachs((Nil, Set.empty), starts)._1.reverse
- }
-
-
/* simple dialogs */
private def simple_dialog(kind: Int, default_title: String)
--- a/src/Pure/raw_simplifier.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Feb 28 11:45:40 2012 +0100
@@ -1309,9 +1309,7 @@
(global_context (Thm.theory_of_thm st) ss) i st
end;
-(*Prunes all redundant parameters from the proof state by rewriting.
- DOES NOT rewrite main goal, where quantification over an unused bound
- variable is sometimes done to avoid the need for cut_facts_tac.*)
+(*Prunes all redundant parameters from the proof state by rewriting.*)
val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
--- a/src/Pure/tactic.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Pure/tactic.ML Tue Feb 28 11:45:40 2012 +0100
@@ -31,7 +31,7 @@
val flexflex_tac: tactic
val distinct_subgoal_tac: int -> tactic
val distinct_subgoals_tac: tactic
- val metacut_tac: thm -> int -> tactic
+ val cut_tac: thm -> int -> tactic
val cut_rules_tac: thm list -> int -> tactic
val cut_facts_tac: thm list -> int -> tactic
val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
@@ -181,11 +181,11 @@
(*The conclusion of the rule gets assumed in subgoal i,
while subgoal i+1,... are the premises of the rule.*)
-fun metacut_tac rule i = resolve_tac [cut_rl] i THEN biresolve_tac [(false, rule)] (i+1);
+fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
(*"Cut" a list of rules into the goal. Their premises will become new
subgoals.*)
-fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
+fun cut_rules_tac ths i = EVERY (map (fn th => cut_tac th i) ths);
(*As above, but inserts only facts (unconditional theorems);
generates no additional subgoals. *)
--- a/src/Tools/WWW_Find/html_templates.ML Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Tools/WWW_Find/html_templates.ML Tue Feb 28 11:45:40 2012 +0100
@@ -93,14 +93,14 @@
fun show_criterion (b, c) =
let
- fun prfx s = let
+ fun prfx s =
+ let
val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
in span (class c, v) end;
in
(case c of
Find_Theorems.Name name => prfx ("name: " ^ quote name)
| Find_Theorems.Intro => prfx "intro"
- | Find_Theorems.IntroIff => prfx "introiff"
| Find_Theorems.Elim => prfx "elim"
| Find_Theorems.Dest => prfx "dest"
| Find_Theorems.Solves => prfx "solves"
@@ -133,7 +133,7 @@
[ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
end
-(*FIXME!?!*)
+(* FIXME!?! *)
fun is_sorry thm =
Thm.proof_of thm
|> Proofterm.approximate_proof_body
--- a/src/Tools/jEdit/src/session_dockable.scala Tue Feb 28 11:10:09 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue Feb 28 11:45:40 2012 +0100
@@ -147,18 +147,20 @@
{
Swing_Thread.now {
val snapshot = Isabelle.session.snapshot()
- val names = restriction getOrElse snapshot.version.nodes.keySet
+ val iterator =
+ restriction match {
+ case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+ case None => snapshot.version.nodes.entries
+ }
val nodes_status1 =
- (nodes_status /: names)((status, name) => {
- val node = snapshot.version.nodes(name)
- status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
- })
+ (nodes_status /: iterator)({ case (status, (name, node)) =>
+ status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
if (nodes_status != nodes_status1) {
nodes_status = nodes_status1
status.listData =
- snapshot.version.topological_order.filter(
+ snapshot.version.nodes.topological_order.filter(
(name: Document.Node.Name) => nodes_status.isDefinedAt(name))
}
}