# HG changeset patch # User berghofe # Date 1330425940 -3600 # Node ID 49cbc06af3e54f7be22ddca58e6989f8364aa166 # Parent 54ea872b60eaee2f9334b153683c47d0b02ea2b6# Parent d34ec0512dfbf763b683e950f8f3b08c7be4d30d merged diff -r d34ec0512dfb -r 49cbc06af3e5 doc-src/IsarRef/Thy/Generic.thy --- 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 \} deletes the specified premise from a subgoal. Note that @{text \} may contain schematic diff -r d34ec0512dfb -r 49cbc06af3e5 doc-src/IsarRef/Thy/document/Generic.tex --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Algebra/Coset.thy --- 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 "\ = x' \ ((inv x) \ x)" by (simp add: m_assoc) also from carr - have "\ = x' \ \" by (simp add: l_inv) + have "\ = x' \ \" by simp also from carr have "\ = 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 _ "\"]) -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 \ carrier G" "y \ carrier G" and "inv x \ y \ H" - hence "inv (inv x \ y) \ H" by (simp add: m_inv_closed) + hence "inv (inv x \ y) \ H" by simp thus "inv y \ x \ H" by (simp add: inv_mult_group) qed next @@ -722,7 +721,7 @@ assume abrcong: "(a, b) \ rcong H" and ccarr: "c \ carrier G" - from ccarr have "c \ Units G" by (simp add: Units_eq) + from ccarr have "c \ Units G" by simp hence cinvc_one: "inv c \ c = \" by (rule Units_l_inv) from abrcong diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Algebra/FiniteProduct.thy --- 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 \ D; A \ B |] ==> foldD D f e A \ 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 \ 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 \ carrier G" by fast from insert have A: "g \ 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 \ A -> carrier G; g \ B -> carrier G |] ==> finprod G g (A Un B) = finprod G g A \ 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) \ carrier G \ 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. *) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Algebra/Ring.thy --- 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 "\ = \" by simp qed -lemma carrier_one_zero: - shows "(carrier R = {\}) = (\ = \)" - by (rule, erule one_zeroI, erule one_zeroD) +lemma carrier_one_zero: "(carrier R = {\}) = (\ = \)" + apply rule + apply (erule one_zeroI) + apply (erule one_zeroD) + done -lemma carrier_one_not_zero: - shows "(carrier R \ {\}) = (\ \ \)" +lemma carrier_one_not_zero: "(carrier R \ {\}) = (\ \ \)" by (simp add: carrier_one_zero) end @@ -571,7 +568,7 @@ from bcarr have "b = \ \ b" by algebra also from aUnit acarr - have "... = (inv a \ a) \ b" by (simp add: Units_l_inv) + have "... = (inv a \ a) \ b" by simp also from acarr bcarr aUnit[THEN Units_inv_closed] have "... = (inv a) \ (a \ b)" by algebra also from ab and acarr bcarr aUnit diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/AxCompl.thy --- 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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/AxSound.thy --- 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\0\{Normal P} Methd C sig-\ {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: "\G\n\{Normal P} body G C sig-\{Q}\ @@ -992,7 +991,7 @@ from da obtain V where da_var: "\prg=G,cls=accC,lcl=L\ \ dom (locals (store s0)) \\var\\<^sub>v\ V" by (cases "\ 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\s0 \var=\(v, upd)\n\ 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\a\\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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/DeclConcepts.thy --- 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 @@ \ 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/Evaln.thy --- 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\Norm s \In2 (e1.[e2]) \\n\ (v, s')" "G\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\n\ (v, s')" "G\Norm s \In1r (Init C) \\n\ (x, s')" - "G\Norm s \In1r (Init C) \\n\ (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 .. diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/Example.thy --- 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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/TypeSafe.thy --- 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 @@ \ (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 \ 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 \ 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 \ error_free (assign (\v. supd lupd(vn\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: "\prg=G, cls=accC, lcl=L\\c1\\" and wt_c2: "\prg=G, cls=accC, lcl=L\\c2\\"*) - 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: "\prg=G,cls=accC,lcl=L\\ dom (locals (store ((Norm s0)::state))) \In1l e\ E" and @@ -3978,7 +3975,7 @@ obtain wt_e: "\prg=G, cls=accC, lcl=L\\e\-PrimT Boolean" and wt_then_else: "\prg=G, cls=accC, lcl=L\\(if the_Bool b then c1 else c2)\\" - 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: "\prg=G,cls=accC,lcl=L\\ dom (locals (store ((Norm s0)::state))) \\e\\<^sub>e\ E" and diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Bali/WellType.thy --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Big_Operators.thy --- 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 \ 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}" +assumes "finite A" and "ALL x:A. f x \ 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}) \ {a})" + by(simp add:insert_absorb[OF `a:A`]) + also have "\ = setsum f (A-{a}) + setsum f {a}" + using `finite A` by(subst setsum_Un_disjoint) auto + also have "setsum f (A-{a}) \ 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}) \ {a})" + using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto + also have "\ = 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") diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Decision_Procs/commutative_ring_tac.ML --- 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); diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/IsaMakefile --- 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 \ diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/List.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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Matrix/Matrix.thy --- 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 \ int \ int \ '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 \ nat \ '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 \ 0 <= i \ (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 \ 0 <= i \ (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 \ 0 <= i \ (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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Matrix/SparseMatrix.thy --- 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 \ '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 \ sorted_spvec((a,c)#as) \ 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 \ u \ 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 \ sorted_spvec (minus_spmat A)" diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/MicroJava/BV/Effect.thy --- 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 "\ l. x = [l]" by - (cases x, auto) + hence "\ l. x = [l]" by (cases x) auto } note 0 = this - have "length a = Suc (Suc 0) \ \l l'. a = [l,l']" by (cases a, auto dest: 0) + have "length a = Suc (Suc 0) \ \l l'. a = [l,l']" by (cases a) (auto dest: 0) with * show ?thesis by (auto dest: 0) qed diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/MicroJava/Comp/NatCanonify.thy --- 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) \ (int n2) then 0 else (int n1) - (int n2))" -by (simp add: zdiff_int nat_int) - -lemma nat_le_canonify: "((n1::nat) \ n2) = ((int n1) \ (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 \ 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/MicroJava/DFA/LBVComplete.thy --- 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]: "\ <=_r x = (x = \)" - by (insert semilat) (simp add: top top_le_conv) + using semilat by (simp add: top) lemma (in lbv) neq_top [simp, elim]: "\ x <=_r y; y \ \ \ \ x \ \" diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Mutabelle/Mutabelle.thy --- 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 => diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Mutabelle/mutabelle_extra.ML --- 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 = diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Quickcheck_Examples/ROOT.ML diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/TPTP/etc/settings --- 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" diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/Datatype/rep_datatype.ML --- 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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/inductive.ML --- 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)), diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/inductive_realizer.ML --- 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, diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/lin_arith.ML --- 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)) diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/Tools/record.ML --- 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); diff -r d34ec0512dfb -r 49cbc06af3e5 src/HOL/ex/Meson_Test.thy --- 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*) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Provers/Arith/fast_lin_arith.ML --- 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 = diff -r d34ec0512dfb -r 49cbc06af3e5 src/Provers/blast.ML --- 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)) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Concurrent/counter.scala --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Concurrent/volatile.scala --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/General/graph.scala --- 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)) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/General/linear_set.scala --- 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] diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/General/path.scala --- 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] diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/General/scan.scala --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/General/time.scala --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Isar/outer_syntax.scala --- 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()) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/PIDE/command.scala --- 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], diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/PIDE/document.scala --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/PIDE/markup_tree.scala --- 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)) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/PIDE/text.scala --- 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 + ")" diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Thy/completion.scala --- 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, diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Tools/find_consts.ML --- 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; diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/Tools/find_theorems.ML --- 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 || diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/library.scala --- 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) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/raw_simplifier.ML --- 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]; diff -r d34ec0512dfb -r 49cbc06af3e5 src/Pure/tactic.ML --- 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. *) diff -r d34ec0512dfb -r 49cbc06af3e5 src/Tools/WWW_Find/html_templates.ML --- 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 diff -r d34ec0512dfb -r 49cbc06af3e5 src/Tools/jEdit/src/session_dockable.scala --- 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)) } }