# HG changeset patch # User wenzelm # Date 1292607513 -3600 # Node ID 4ae674714876fe682b3e7bae3ccf12c2e609fd78 # Parent bb28bf63520262edda9f84dde7ec4acf248aaedf# Parent 1e6d86821718b13597693ae1f8ab13d4c3828c61 merged diff -r bb28bf635202 -r 4ae674714876 NEWS --- a/NEWS Fri Dec 17 18:32:40 2010 +0100 +++ b/NEWS Fri Dec 17 18:38:33 2010 +0100 @@ -83,6 +83,13 @@ *** Pure *** +* Command 'type_synonym' (with single argument) replaces somewhat +outdated 'types', which is still available as legacy feature for some +time. + +* Command 'nonterminal' (with 'and' separated list of arguments) +replaces somewhat outdated 'nonterminals'. INCOMPATIBILITY. + * Command 'notepad' replaces former 'example_proof' for experimentation in Isar without any result. INCOMPATIBILITY. @@ -599,6 +606,9 @@ *** ML *** +* Renamed structure MetaSimplifier to Raw_Simplifier. Note that the +main functionality is provided by structure Simplifier. + * Syntax.pretty_priority (default 0) configures the required priority of pretty-printed output and thus affects insertion of parentheses. diff -r bb28bf635202 -r 4ae674714876 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Dec 17 18:38:33 2010 +0100 @@ -723,7 +723,7 @@ text {* \begin{matharray}{rcl} - @{command_def "nonterminals"} & : & @{text "theory \ theory"} \\ + @{command_def "nonterminal"} & : & @{text "theory \ theory"} \\ @{command_def "syntax"} & : & @{text "theory \ theory"} \\ @{command_def "no_syntax"} & : & @{text "theory \ theory"} \\ @{command_def "translations"} & : & @{text "theory \ theory"} \\ @@ -731,7 +731,7 @@ \end{matharray} \begin{rail} - 'nonterminals' (name +) + 'nonterminal' (name + 'and') ; ('syntax' | 'no_syntax') mode? (constdecl +) ; @@ -746,7 +746,7 @@ \begin{description} - \item @{command "nonterminals"}~@{text c} declares a type + \item @{command "nonterminal"}~@{text c} declares a type constructor @{text c} (without arguments) to act as purely syntactic type: a nonterminal symbol of the inner syntax. diff -r bb28bf635202 -r 4ae674714876 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Fri Dec 17 18:38:33 2010 +0100 @@ -973,13 +973,13 @@ text {* \begin{matharray}{rcll} - @{command_def "types"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "type_synonym"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "typedecl"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} \begin{rail} - 'types' (typespec '=' type mixfix? +) + 'type_synonym' (typespec '=' type mixfix?) ; 'typedecl' typespec mixfix? ; @@ -989,12 +989,12 @@ \begin{description} - \item @{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a - \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the existing type - @{text "\"}. Unlike actual type definitions, as are available in - Isabelle/HOL for example, type synonyms are merely syntactic - abbreviations without any logical significance. Internally, type - synonyms are fully expanded. + \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} + introduces a \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the + existing type @{text "\"}. Unlike actual type definitions, as are + available in Isabelle/HOL for example, type synonyms are merely + syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new type constructor @{text t}. If the object-logic defines a base sort diff -r bb28bf635202 -r 4ae674714876 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Dec 17 18:32:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Dec 17 18:38:33 2010 +0100 @@ -742,7 +742,7 @@ % \begin{isamarkuptext}% \begin{matharray}{rcl} - \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{nonterminal}\hypertarget{command.nonterminal}{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ @@ -750,7 +750,7 @@ \end{matharray} \begin{rail} - 'nonterminals' (name +) + 'nonterminal' (name + 'and') ; ('syntax' | 'no_syntax') mode? (constdecl +) ; @@ -765,7 +765,7 @@ \begin{description} - \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type + \item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type constructor \isa{c} (without arguments) to act as purely syntactic type: a nonterminal symbol of the inner syntax. diff -r bb28bf635202 -r 4ae674714876 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Dec 17 18:32:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Dec 17 18:38:33 2010 +0100 @@ -1010,13 +1010,13 @@ % \begin{isamarkuptext}% \begin{matharray}{rcll} - \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{type\_synonym}\hypertarget{command.type-synonym}{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\ \end{matharray} \begin{rail} - 'types' (typespec '=' type mixfix? +) + 'type_synonym' (typespec '=' type mixfix?) ; 'typedecl' typespec mixfix? ; @@ -1026,12 +1026,12 @@ \begin{description} - \item \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} introduces a - \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the existing type - \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}. Unlike actual type definitions, as are available in - Isabelle/HOL for example, type synonyms are merely syntactic - abbreviations without any logical significance. Internally, type - synonyms are fully expanded. + \item \hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} + introduces a \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the + existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}. Unlike actual type definitions, as are + available in Isabelle/HOL for example, type synonyms are merely + syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} declares a new type constructor \isa{t}. If the object-logic defines a base sort diff -r bb28bf635202 -r 4ae674714876 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri Dec 17 18:32:40 2010 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Dec 17 18:38:33 2010 +0100 @@ -673,7 +673,7 @@ % \isatagproof \isacommand{using}\isamarkupfalse% -\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}trace{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline \isacommand{apply}\isamarkupfalse% \ simp% \endisatagproof diff -r bb28bf635202 -r 4ae674714876 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Fri Dec 17 18:32:40 2010 +0100 +++ b/etc/isar-keywords-ZF.el Fri Dec 17 18:38:33 2010 +0100 @@ -103,7 +103,7 @@ "no_syntax" "no_translations" "no_type_notation" - "nonterminals" + "nonterminal" "notation" "note" "notepad" @@ -189,6 +189,7 @@ "txt_raw" "typ" "type_notation" + "type_synonym" "typed_print_translation" "typedecl" "types" @@ -381,7 +382,7 @@ "no_syntax" "no_translations" "no_type_notation" - "nonterminals" + "nonterminal" "notation" "notepad" "oracle" @@ -403,6 +404,7 @@ "theorems" "translations" "type_notation" + "type_synonym" "typed_print_translation" "typedecl" "types" diff -r bb28bf635202 -r 4ae674714876 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Dec 17 18:32:40 2010 +0100 +++ b/etc/isar-keywords.el Fri Dec 17 18:38:33 2010 +0100 @@ -140,7 +140,7 @@ "nominal_inductive" "nominal_inductive2" "nominal_primrec" - "nonterminals" + "nonterminal" "notation" "note" "notepad" @@ -250,6 +250,7 @@ "typ" "type_lifting" "type_notation" + "type_synonym" "typed_print_translation" "typedecl" "typedef" @@ -487,7 +488,7 @@ "no_translations" "no_type_notation" "nominal_datatype" - "nonterminals" + "nonterminal" "notation" "notepad" "oracle" @@ -516,6 +517,7 @@ "theorems" "translations" "type_notation" + "type_synonym" "typed_print_translation" "typedecl" "types" diff -r bb28bf635202 -r 4ae674714876 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Cube/Cube.thy Fri Dec 17 18:38:33 2010 +0100 @@ -14,8 +14,7 @@ typedecl "context" typedecl typing -nonterminals - context' typing' +nonterminal context' and typing' consts Abs :: "[term, term => term] => term" diff -r bb28bf635202 -r 4ae674714876 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/FOL/IFOL.thy Fri Dec 17 18:38:33 2010 +0100 @@ -754,7 +754,7 @@ subsection {* ``Let'' declarations *} -nonterminals letbinds letbind +nonterminal letbinds and letbind definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where "Let(s, f) == f(s)" diff -r bb28bf635202 -r 4ae674714876 src/HOL/Decision_Procs/langford_data.ML --- a/src/HOL/Decision_Procs/langford_data.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Decision_Procs/langford_data.ML Fri Dec 17 18:38:33 2010 +0100 @@ -36,11 +36,9 @@ Thm.declaration_attribute (fn key => fn context => context |> Data.map (del_data key #> apsnd (cons (key, entry)))); -val add_simp = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) +val add_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.add_simp); -val del_simp = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) +val del_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.del_simp); fun match ctxt tm = let diff -r bb28bf635202 -r 4ae674714876 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Fun.thy Fri Dec 17 18:38:33 2010 +0100 @@ -558,8 +558,8 @@ fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where "fun_upd f a b == % x. if x=a then b else f x" -nonterminals - updbinds updbind +nonterminal updbinds and updbind + syntax "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)") "" :: "updbind => updbinds" ("_") diff -r bb28bf635202 -r 4ae674714876 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/HOL.thy Fri Dec 17 18:38:33 2010 +0100 @@ -103,9 +103,8 @@ notation (xsymbols) iff (infixr "\" 25) -nonterminals - letbinds letbind - case_syn cases_syn +nonterminal letbinds and letbind +nonterminal case_syn and cases_syn syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) diff -r bb28bf635202 -r 4ae674714876 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Dec 17 18:38:33 2010 +0100 @@ -170,7 +170,7 @@ val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef val type_definition_thm = - MetaSimplifier.rewrite_rule + Raw_Simplifier.rewrite_rule (the_list (#set_def (#2 info))) (#type_definition (#2 info)) val typedef_thms = diff -r bb28bf635202 -r 4ae674714876 src/HOL/HOLCF/ex/Letrec.thy --- a/src/HOL/HOLCF/ex/Letrec.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/HOLCF/ex/Letrec.thy Fri Dec 17 18:38:33 2010 +0100 @@ -14,8 +14,7 @@ CLetrec :: "('a \ 'a \ 'b) \ 'b" where "CLetrec = (\ F. snd (F\(\ x. fst (F\x))))" -nonterminals - recbinds recbindt recbind +nonterminal recbinds and recbindt and recbind syntax "_recbind" :: "['a, 'a] \ recbind" ("(2_ =/ _)" 10) diff -r bb28bf635202 -r 4ae674714876 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 17 18:38:33 2010 +0100 @@ -100,8 +100,7 @@ subsection {* Case syntax *} -nonterminals - Case_syn Cases_syn +nonterminal Case_syn and Cases_syn syntax "_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Dec 17 18:38:33 2010 +0100 @@ -56,8 +56,7 @@ "r \c\" \ "r AWAIT CONST True THEN c END" "r WAIT b END" \ "r AWAIT b THEN SKIP END" -nonterminals - prgs +nonterminal prgs syntax "_PAR" :: "prgs \ 'a" ("COBEGIN//_//COEND" [57] 56) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Dec 17 18:38:33 2010 +0100 @@ -27,8 +27,7 @@ "\c\" \ "AWAIT CONST True THEN c END" "WAIT b END" \ "AWAIT b THEN SKIP END" -nonterminals - prgs +nonterminal prgs syntax "_PAR" :: "prgs \ 'a" ("COBEGIN//_//COEND" 60) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Library/Monad_Syntax.thy Fri Dec 17 18:38:33 2010 +0100 @@ -37,8 +37,7 @@ notation (latex output) bind_do (infixr "\" 54) -nonterminals - do_binds do_bind +nonterminal do_binds and do_bind syntax "_do_block" :: "do_binds \ 'a" ("do {//(2 _)//}" [12] 62) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Library/State_Monad.thy Fri Dec 17 18:38:33 2010 +0100 @@ -114,8 +114,7 @@ subsection {* Do-syntax *} -nonterminals - sdo_binds sdo_bind +nonterminal sdo_binds and sdo_bind syntax "_sdo_block" :: "sdo_binds \ 'a" ("exec {//(2 _)//}" [12] 62) diff -r bb28bf635202 -r 4ae674714876 src/HOL/List.thy --- a/src/HOL/List.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/List.thy Fri Dec 17 18:38:33 2010 +0100 @@ -123,7 +123,7 @@ "list_update [] i v = []" | "list_update (x # xs) i v = (case i of 0 \ v # xs | Suc j \ x # list_update xs j v)" -nonterminals lupdbinds lupdbind +nonterminal lupdbinds and lupdbind syntax "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") @@ -346,7 +346,7 @@ @{term"{z. EX x: set xs. EX y:set ys. P x y \ z = f x y}"}. *) -nonterminals lc_qual lc_quals +nonterminal lc_qual and lc_quals syntax "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __") diff -r bb28bf635202 -r 4ae674714876 src/HOL/Map.thy --- a/src/HOL/Map.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Map.thy Fri Dec 17 18:38:33 2010 +0100 @@ -50,8 +50,7 @@ map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\\<^sub>m" 50) where "(m\<^isub>1 \\<^sub>m m\<^isub>2) = (\a \ dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)" -nonterminals - maplets maplet +nonterminal maplets and maplet syntax "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") diff -r bb28bf635202 -r 4ae674714876 src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/NSA/transfer.ML Fri Dec 17 18:38:33 2010 +0100 @@ -58,7 +58,7 @@ val meta = Local_Defs.meta_rewrite_rule ctxt; val ths' = map meta ths; val unfolds' = map meta unfolds and refolds' = map meta refolds; - val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t)) + val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t)) val u = unstar_term consts t' val tac = rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN diff -r bb28bf635202 -r 4ae674714876 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Dec 17 18:38:33 2010 +0100 @@ -19,10 +19,10 @@ val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify []; +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify []; val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) (HOL_basic_ss addsimps inductive_atomize); val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 diff -r bb28bf635202 -r 4ae674714876 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Dec 17 18:38:33 2010 +0100 @@ -20,10 +20,10 @@ val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify}; -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify []; +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify []; val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) (HOL_basic_ss addsimps inductive_atomize); val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 diff -r bb28bf635202 -r 4ae674714876 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Product_Type.thy Fri Dec 17 18:38:33 2010 +0100 @@ -173,8 +173,7 @@ abstractions. *} -nonterminals - tuple_args patterns +nonterminal tuple_args and patterns syntax "_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))") diff -r bb28bf635202 -r 4ae674714876 src/HOL/Record.thy --- a/src/HOL/Record.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Record.thy Fri Dec 17 18:38:33 2010 +0100 @@ -419,8 +419,15 @@ subsection {* Concrete record syntax *} -nonterminals - ident field_type field_types field fields field_update field_updates +nonterminal + ident and + field_type and + field_types and + field and + fields and + field_update and + field_updates + syntax "_constify" :: "id => ident" ("_") "_constify" :: "longid => ident" ("_") diff -r bb28bf635202 -r 4ae674714876 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Statespace/state_fun.ML Fri Dec 17 18:38:33 2010 +0100 @@ -141,8 +141,7 @@ (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s))); val ctxt = Simplifier.the_context ss; val basic_ss = #1 (StateFunData.get (Context.Proof ctxt)); - val ss' = Simplifier.context - (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss; + val ss' = Simplifier.context (Config.put simp_depth_limit 100 ctxt) basic_ss; val thm = Simplifier.rewrite ss' ct; in if (op aconv) (Logic.dest_equals (prop_of thm)) then NONE @@ -232,8 +231,7 @@ end | mk_updterm _ t = init_seed t; - val ctxt = Simplifier.the_context ss |> - Config.put MetaSimplifier.simp_depth_limit 100; + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100; val ss1 = Simplifier.context ctxt ss'; val ss2 = Simplifier.context ctxt (#1 (StateFunData.get (Context.Proof ctxt))); @@ -266,8 +264,7 @@ Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"] (fn thy => fn ss => fn t => let - val ctxt = Simplifier.the_context ss |> - Config.put MetaSimplifier.simp_depth_limit 100 + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100; val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt)); val ss' = (Simplifier.context ctxt ex_lookup_ss); fun prove prop = diff -r bb28bf635202 -r 4ae674714876 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/TLA/Intensional.thy Fri Dec 17 18:38:33 2010 +0100 @@ -33,9 +33,7 @@ (** concrete syntax **) -nonterminals - lift - liftargs +nonterminal lift and liftargs syntax "" :: "id => lift" ("_") diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Dec 17 18:38:33 2010 +0100 @@ -52,7 +52,7 @@ in thms |> Conjunction.intr_balanced - |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm] + |> Raw_Simplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm] |> Thm.implies_intr asm |> Thm.generalize ([], params) 0 |> AxClass.unoverload thy diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 18:38:33 2010 +0100 @@ -39,12 +39,12 @@ branches: scheme_branch list, cases: scheme_case list} -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize} -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} +val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize} +val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify} fun meta thm = thm RS eq_reflection -val sum_prod_conv = MetaSimplifier.rewrite true +val sum_prod_conv = Raw_Simplifier.rewrite true (map meta (@{thm split_conv} :: @{thms sum.cases})) fun term_conv thy cv t = @@ -312,7 +312,7 @@ val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |> Goal.init - |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) + |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) THEN CONVERSION ind_rulify 1) |> Seq.hd |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 17 18:38:33 2010 +0100 @@ -297,7 +297,7 @@ else Conv.all_conv | _ => Conv.all_conv) -fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths +fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths val cheat_choice = @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Dec 17 18:38:33 2010 +0100 @@ -219,9 +219,9 @@ fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of) val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) - val case_th = MetaSimplifier.simplify true + val case_th = Raw_Simplifier.simplify true (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) - val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems + val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th OF (replicate nargs @{thm refl}) @@ -237,7 +237,7 @@ (PEEK nprems_of (fn n => ALLGOALS (fn i => - MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i + Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i THEN (SUBPROOF (instantiate i n) ctxt i)))) in Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 17 18:38:33 2010 +0100 @@ -969,7 +969,7 @@ val Tcons = datatype_names_of_case_name thy case_name val ths = maps (instantiated_case_rewrites thy) Tcons in - MetaSimplifier.rewrite_term thy + Raw_Simplifier.rewrite_term thy (map (fn th => th RS @{thm eq_reflection}) ths) [] t end @@ -1044,7 +1044,7 @@ fun peephole_optimisation thy intro = let val process = - MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy)) + Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy)) fun process_False intro_t = if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t fun process_True intro_t = diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Dec 17 18:38:33 2010 +0100 @@ -96,7 +96,7 @@ (Const (@{const_name If}, _)) => let val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} - val atom' = MetaSimplifier.rewrite_term thy + val atom' = Raw_Simplifier.rewrite_term thy (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom val _ = assert (not (atom = atom')) in @@ -212,7 +212,7 @@ error ("unexpected specification for constant " ^ quote constname ^ ":\n" ^ commas (map (quote o Display.string_of_thm_global thy) specs)) val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} - val intros = map (MetaSimplifier.rewrite_rule + val intros = map (Raw_Simplifier.rewrite_rule [if_beta RS @{thm eq_reflection}]) intros val _ = print_specs options thy "normalized intros" intros (*val intros = maps (split_cases thy) intros*) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Dec 17 18:38:33 2010 +0100 @@ -83,7 +83,7 @@ let val prems' = maps dest_conjunct_prem (take nargs prems) in - MetaSimplifier.rewrite_goal_tac + Simplifier.rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 end) ctxt 1 | Abs _ => raise Fail "prove_param: No valid parameter term" @@ -127,7 +127,7 @@ fun param_rewrite prem = param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem))) val SOME rew_eq = find_first param_rewrite prems' - val param_prem' = MetaSimplifier.rewrite_rule + val param_prem' = Raw_Simplifier.rewrite_rule (map (fn th => th RS @{thm eq_reflection}) [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) param_prem @@ -184,7 +184,7 @@ let val prems' = maps dest_conjunct_prem (take nargs prems) in - MetaSimplifier.rewrite_goal_tac + Simplifier.rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 end THEN REPEAT_DETERM (rtac @{thm refl} 1)) @@ -225,7 +225,7 @@ let val prems' = maps dest_conjunct_prem (take nargs prems) in - MetaSimplifier.rewrite_goal_tac + Simplifier.rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 end) ctxt 1 THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Dec 17 18:38:33 2010 +0100 @@ -486,7 +486,7 @@ val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1) - val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 + val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 val (insp, inst) = if ty_c = ty_d then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Dec 17 18:38:33 2010 +0100 @@ -589,7 +589,7 @@ type T = extra_norm U.dict val empty = [] val extend = I - fun merge xx = U.dict_merge fst xx + fun merge data = U.dict_merge fst data ) fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 17 18:38:33 2010 +0100 @@ -567,7 +567,7 @@ type T = (Proof.context -> config) U.dict val empty = [] val extend = I - fun merge xx = U.dict_merge fst xx + fun merge data = U.dict_merge fst data ) fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg)) diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Fri Dec 17 18:38:33 2010 +0100 @@ -73,8 +73,8 @@ functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = struct -val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify; -val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize; +val rulify_goals = Raw_Simplifier.rewrite_goals_rule Data.rulify; +val atomize_goals = Raw_Simplifier.rewrite_goals_rule Data.atomize; (* beta-eta contract the theorem *) fun beta_eta_contract thm = diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Fri Dec 17 18:38:33 2010 +0100 @@ -422,7 +422,7 @@ fun SUBS thl = rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl); -val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)); +val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)); fun simpl_conv ss thl ctm = rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq; @@ -669,7 +669,7 @@ val eq = Logic.strip_imp_concl imp val lhs = tych(get_lhs eq) val ss' = Simplifier.add_prems (map ASSUME ants) ss - val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs + val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs handle Utils.ERR _ => Thm.reflexive lhs val dummy = print_thms "proven:" [lhs_eq_lhs1] val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 @@ -690,7 +690,7 @@ val QeqQ1 = pbeta_reduce (tych Q) val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1)) val ss' = Simplifier.add_prems (map ASSUME ants1) ss - val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1 + val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1 handle Utils.ERR _ => Thm.reflexive Q1 val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) @@ -714,8 +714,8 @@ else let val tych = cterm_of thy val ants1 = map tych ants - val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss - val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm + val ss' = Simplifier.add_prems (map ASSUME ants1) ss + val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ss' (tych Q) handle Utils.ERR _ => Thm.reflexive (tych Q) val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 @@ -783,7 +783,7 @@ end val ctm = cprop_of th val names = OldTerm.add_term_names (term_of ctm, []) - val th1 = MetaSimplifier.rewrite_cterm(false,true,false) + val th1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm val th2 = Thm.equal_elim th1 th in diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Dec 17 18:38:33 2010 +0100 @@ -282,7 +282,7 @@ val bad_app = "Inductive predicate must be applied to parameter(s) "; -fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; +fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize []; in diff -r bb28bf635202 -r 4ae674714876 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Fri Dec 17 18:38:33 2010 +0100 @@ -807,7 +807,7 @@ add_discrete_type @{type_name nat}; fun add_arith_facts ss = - add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss; + Simplifier.add_prems (Arith_Data.get_arith_facts (Simplifier.the_context ss)) ss; val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc; diff -r bb28bf635202 -r 4ae674714876 src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/HOL/ex/Numeral.thy Fri Dec 17 18:38:33 2010 +0100 @@ -592,14 +592,14 @@ fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); fun attach_num ct = (dest_num (Thm.term_of ct), ct); fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; - val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); + val simplify = Raw_Simplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \ _"}, [Drule.list_comb (@{cterm "op + :: num \ _"}, [ck, cl]), cj]))]]; in fn phi => fn _ => fn ct => case try cdifference ct of NONE => (NONE) | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0 - then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct + then Raw_Simplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct else mk_meta_eq (let val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j)); in diff -r bb28bf635202 -r 4ae674714876 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/IsaMakefile Fri Dec 17 18:38:33 2010 +0100 @@ -227,7 +227,6 @@ item_net.ML \ library.ML \ logic.ML \ - meta_simplifier.ML \ more_thm.ML \ morphism.ML \ name.ML \ @@ -238,6 +237,7 @@ proofterm.ML \ pure_setup.ML \ pure_thy.ML \ + raw_simplifier.ML \ search.ML \ sign.ML \ simplifier.ML \ diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Dec 17 18:38:33 2010 +0100 @@ -415,9 +415,9 @@ register_config Unify.search_bound_raw #> register_config Unify.trace_simp_raw #> register_config Unify.trace_types_raw #> - register_config MetaSimplifier.simp_depth_limit_raw #> - register_config MetaSimplifier.simp_trace_depth_limit_raw #> - register_config MetaSimplifier.simp_debug_raw #> - register_config MetaSimplifier.simp_trace_raw)); + register_config Raw_Simplifier.simp_depth_limit_raw #> + register_config Raw_Simplifier.simp_trace_depth_limit_raw #> + register_config Raw_Simplifier.simp_debug_raw #> + register_config Raw_Simplifier.simp_trace_raw)); end; diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/element.ML Fri Dec 17 18:38:33 2010 +0100 @@ -224,7 +224,7 @@ val thy = ProofContext.theory_of ctxt; val cert = Thm.cterm_of thy; - val th = MetaSimplifier.norm_hhf raw_th; + val th = Raw_Simplifier.norm_hhf raw_th; val is_elim = Object_Logic.is_elim th; val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt); @@ -318,7 +318,7 @@ end; fun conclude_witness (Witness (_, th)) = - Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); + Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th)); fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in @@ -459,8 +459,8 @@ fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism {binding = I, typ = I, - term = MetaSimplifier.rewrite_term thy thms [], - fact = map (MetaSimplifier.rewrite_rule thms)}); + term = Raw_Simplifier.rewrite_term thy thms [], + fact = map (Raw_Simplifier.rewrite_rule thms)}); (* transfer to theory using closure *) diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/expression.ML Fri Dec 17 18:38:33 2010 +0100 @@ -647,18 +647,18 @@ val cert = Thm.cterm_of defs_thy; val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => - MetaSimplifier.rewrite_goals_tac [pred_def] THEN + rewrite_goals_tac [pred_def] THEN Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN Tactic.compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF [body_eq, - MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) + Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |> Conjunction.elim_balanced (length ts); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness defs_ctxt t - (MetaSimplifier.rewrite_goals_tac defs THEN + (rewrite_goals_tac defs THEN Tactic.compose_tac (false, ax, 0) 1)); in ((statement, intro, axioms), defs_thy) end; diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/generic_target.ML Fri Dec 17 18:38:33 2010 +0100 @@ -58,7 +58,7 @@ (*term and type parameters*) val crhs = Thm.cterm_of thy rhs; val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of; - val rhs_conv = MetaSimplifier.rewrite true defs crhs; + val rhs_conv = Raw_Simplifier.rewrite true defs crhs; val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' []; val T = Term.fastype_of rhs; @@ -107,7 +107,7 @@ (*export assumes/defines*) val th = Goal.norm_result raw_th; val (defs, th') = Local_Defs.export ctxt thy_ctxt th; - val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) + val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt); val nprems = Thm.nprems_of th' - Thm.nprems_of th; diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Dec 17 18:38:33 2010 +0100 @@ -111,16 +111,24 @@ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); +val type_abbrev = + Parse.type_args -- Parse.binding -- + (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')); + val _ = Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl - (Scan.repeat1 - (Parse.type_args -- Parse.binding -- - (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))) - >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs))); + (Scan.repeat1 type_abbrev >> (fn specs => fn lthy => + (legacy_feature "Old 'types' commands -- use 'type_synonym' instead"; + fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy))); val _ = - Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" - Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals)); + Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl + (type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); + +val _ = + Outer_Syntax.command "nonterminal" + "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl + (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals)); val _ = Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/local_defs.ML Fri Dec 17 18:38:33 2010 +0100 @@ -182,7 +182,7 @@ end; fun contract ctxt defs ct th = - trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)]; + trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)]; (** defived definitions **) @@ -208,8 +208,8 @@ (* meta rewrite rules *) fun meta_rewrite_conv ctxt = - MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE)) - (MetaSimplifier.context ctxt MetaSimplifier.empty_ss + Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) + (Raw_Simplifier.context ctxt empty_ss addeqcongs [Drule.equals_cong] (*protect meta-level equality*) addsimps (Rules.get (Context.Proof ctxt))); @@ -220,11 +220,11 @@ fun meta f ctxt = f o map (meta_rewrite_rule ctxt); -val unfold = meta MetaSimplifier.rewrite_rule; -val unfold_goals = meta MetaSimplifier.rewrite_goals_rule; -val unfold_tac = meta MetaSimplifier.rewrite_goals_tac; -val fold = meta MetaSimplifier.fold_rule; -val fold_tac = meta MetaSimplifier.fold_goals_tac; +val unfold = meta Raw_Simplifier.rewrite_rule; +val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule; +val unfold_tac = meta Raw_Simplifier.rewrite_goals_tac; +val fold = meta Raw_Simplifier.fold_rule; +val fold_tac = meta Raw_Simplifier.fold_goals_tac; (* derived defs -- potentially within the object-logic *) @@ -244,7 +244,7 @@ in Goal.prove ctxt' frees [] prop (K (ALLGOALS (CONVERSION (meta_rewrite_conv ctxt') THEN' - MetaSimplifier.rewrite_goal_tac [def] THEN' + rewrite_goal_tac [def] THEN' resolve_tac [Drule.reflexive_thm]))) handle ERROR msg => cat_error msg "Failed to prove definitional specification" end; diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/object_logic.ML Fri Dec 17 18:38:33 2010 +0100 @@ -178,10 +178,10 @@ (* atomize *) fun atomize_term thy = - drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; + drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) []; fun atomize ct = - MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; + Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; fun atomize_prems ct = if Logic.has_meta_prems (Thm.term_of ct) then @@ -195,11 +195,11 @@ (* rulify *) -fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) []; -fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st; +fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) []; +fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st; fun gen_rulify full thm = - MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm + Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes; val rulify = gen_rulify true; diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/obtain.ML Fri Dec 17 18:38:33 2010 +0100 @@ -193,7 +193,7 @@ val rule = (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of NONE => raise THM ("Obtain.result: tactic failed", 0, facts) - | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th))); + | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th))); val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; @@ -299,7 +299,7 @@ val goal = Var (("guess", 0), propT); fun print_result ctxt' (k, [(s, [_, th])]) = Proof_Display.print_results int ctxt' (k, [(s, [th])]); - val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #> + val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #> (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); fun after_qed [[_, res]] = Proof.end_block #> guess_context (check_result ctxt thesis res); diff -r bb28bf635202 -r 4ae674714876 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/Isar/rule_cases.ML Fri Dec 17 18:38:33 2010 +0100 @@ -189,14 +189,14 @@ fun unfold_prems n defs th = if null defs then th - else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.rewrite true defs)) th; + else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th; fun unfold_prems_concls defs th = if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th else Conv.fconv_rule (Conv.concl_conv ~1 (Conjunction.convs - (Conv.prems_conv ~1 (MetaSimplifier.rewrite true defs)))) th; + (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th; in diff -r bb28bf635202 -r 4ae674714876 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Dec 17 18:38:33 2010 +0100 @@ -147,10 +147,10 @@ "Show leading question mark of variable name"]; val tracing_preferences = - [bool_pref simp_trace_default + [bool_pref Raw_Simplifier.simp_trace_default "trace-simplifier" "Trace simplification rules.", - nat_pref simp_trace_depth_limit_default + nat_pref Raw_Simplifier.simp_trace_depth_limit_default "trace-simplifier-depth" "Trace simplifier depth limit.", bool_pref trace_rules diff -r bb28bf635202 -r 4ae674714876 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/ROOT.ML Fri Dec 17 18:38:33 2010 +0100 @@ -153,7 +153,7 @@ use "tactical.ML"; use "search.ML"; use "tactic.ML"; -use "meta_simplifier.ML"; +use "raw_simplifier.ML"; use "conjunction.ML"; use "assumption.ML"; use "display.ML"; diff -r bb28bf635202 -r 4ae674714876 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/assumption.ML Fri Dec 17 18:38:33 2010 +0100 @@ -48,7 +48,7 @@ *) fun presume_export _ = assume_export false; -val assume = MetaSimplifier.norm_hhf o Thm.assume; +val assume = Raw_Simplifier.norm_hhf o Thm.assume; @@ -110,9 +110,9 @@ (* export *) fun export is_goal inner outer = - MetaSimplifier.norm_hhf_protect #> + Raw_Simplifier.norm_hhf_protect #> fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> - MetaSimplifier.norm_hhf_protect; + Raw_Simplifier.norm_hhf_protect; fun export_term inner outer = fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); diff -r bb28bf635202 -r 4ae674714876 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/axclass.ML Fri Dec 17 18:38:33 2010 +0100 @@ -322,11 +322,11 @@ fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); -fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy); -fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy)); +fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy); +fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy)); -fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy); -fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); +fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy); +fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy)); fun lookup_inst_param consts params (c, T) = (case get_inst_tyco consts (c, T) of diff -r bb28bf635202 -r 4ae674714876 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/codegen.ML Fri Dec 17 18:38:33 2010 +0100 @@ -293,8 +293,8 @@ ); val map_unfold = UnfoldData.map; -val add_unfold = map_unfold o MetaSimplifier.add_simp; -val del_unfold = map_unfold o MetaSimplifier.del_simp; +val add_unfold = map_unfold o Simplifier.add_simp; +val del_unfold = map_unfold o Simplifier.del_simp; fun unfold_preprocessor thy = let val ss = Simplifier.global_context thy (UnfoldData.get thy) diff -r bb28bf635202 -r 4ae674714876 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/goal.ML Fri Dec 17 18:38:33 2010 +0100 @@ -99,7 +99,7 @@ val norm_result = Drule.flexflex_unique - #> MetaSimplifier.norm_hhf_protect + #> Raw_Simplifier.norm_hhf_protect #> Thm.strip_shyps #> Drule.zero_var_indexes; @@ -278,7 +278,7 @@ rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*) THEN' SUBGOAL (fn (t, i) => if Drule.is_norm_hhf t then all_tac - else MetaSimplifier.rewrite_goal_tac Drule.norm_hhf_eqs i); + else rewrite_goal_tac Drule.norm_hhf_eqs i); fun compose_hhf_tac th i st = PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; @@ -296,7 +296,7 @@ val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val tacs = Rs |> map (fn R => - Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac); + Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac); in fold_rev (curry op APPEND') tacs (K no_tac) i end); diff -r bb28bf635202 -r 4ae674714876 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Dec 17 18:32:40 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1379 +0,0 @@ -(* Title: Pure/meta_simplifier.ML - Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen - -Meta-level Simplification. -*) - -infix 4 - addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs - setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler - setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver; - -signature BASIC_META_SIMPLIFIER = -sig - val simp_debug: bool Config.T - val simp_debug_raw: Config.raw - val simp_trace: bool Config.T - val simp_trace_raw: Config.raw - val simp_trace_default: bool Unsynchronized.ref - val simp_trace_depth_limit: int Config.T - val simp_trace_depth_limit_raw: Config.raw - val simp_trace_depth_limit_default: int Unsynchronized.ref - type rrule - val eq_rrule: rrule * rrule -> bool - type simpset - type proc - type solver - val mk_solver': string -> (simpset -> int -> tactic) -> solver - val mk_solver: string -> (thm list -> int -> tactic) -> solver - val empty_ss: simpset - val merge_ss: simpset * simpset -> simpset - val dest_ss: simpset -> - {simps: (string * thm) list, - procs: (string * cterm list) list, - congs: (string * thm) list, - weak_congs: string list, - loopers: string list, - unsafe_solvers: string list, - safe_solvers: string list} - type simproc - val eq_simproc: simproc * simproc -> bool - val morph_simproc: morphism -> simproc -> simproc - val make_simproc: {name: string, lhss: cterm list, - proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc - val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc - val add_prems: thm list -> simpset -> simpset - val prems_of_ss: simpset -> thm list - val addsimps: simpset * thm list -> simpset - val delsimps: simpset * thm list -> simpset - val addeqcongs: simpset * thm list -> simpset - val deleqcongs: simpset * thm list -> simpset - val addcongs: simpset * thm list -> simpset - val delcongs: simpset * thm list -> simpset - val addsimprocs: simpset * simproc list -> simpset - val delsimprocs: simpset * simproc list -> simpset - val mksimps: simpset -> thm -> thm list - val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset - val setmkcong: simpset * (simpset -> thm -> thm) -> simpset - val setmksym: simpset * (simpset -> thm -> thm option) -> simpset - val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset - val settermless: simpset * (term * term -> bool) -> simpset - val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset - val setloop': simpset * (simpset -> int -> tactic) -> simpset - val setloop: simpset * (int -> tactic) -> simpset - val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset - val addloop: simpset * (string * (int -> tactic)) -> simpset - val delloop: simpset * string -> simpset - val setSSolver: simpset * solver -> simpset - val addSSolver: simpset * solver -> simpset - val setSolver: simpset * solver -> simpset - val addSolver: simpset * solver -> simpset - - val rewrite_rule: thm list -> thm -> thm - val rewrite_goals_rule: thm list -> thm -> thm - val rewrite_goals_tac: thm list -> tactic - val rewrite_goal_tac: thm list -> int -> tactic - val rewtac: thm -> tactic - val prune_params_tac: tactic - val fold_rule: thm list -> thm -> thm - val fold_goals_tac: thm list -> tactic - val norm_hhf: thm -> thm - val norm_hhf_protect: thm -> thm -end; - -signature META_SIMPLIFIER = -sig - include BASIC_META_SIMPLIFIER - exception SIMPLIFIER of string * thm - val internal_ss: simpset -> - {rules: rrule Net.net, - prems: thm list, - bounds: int * ((string * typ) * string) list, - depth: int * bool Unsynchronized.ref, - context: Proof.context option} * - {congs: (string * thm) list * string list, - procs: proc Net.net, - mk_rews: - {mk: simpset -> thm -> thm list, - mk_cong: simpset -> thm -> thm, - mk_sym: simpset -> thm -> thm option, - mk_eq_True: simpset -> thm -> thm option, - reorient: theory -> term list -> term -> term -> bool}, - termless: term * term -> bool, - subgoal_tac: simpset -> int -> tactic, - loop_tacs: (string * (simpset -> int -> tactic)) list, - solvers: solver list * solver list} - val add_simp: thm -> simpset -> simpset - val del_simp: thm -> simpset -> simpset - val solver: simpset -> solver -> int -> tactic - val simp_depth_limit_raw: Config.raw - val simp_depth_limit: int Config.T - val clear_ss: simpset -> simpset - val simproc_global_i: theory -> string -> term list - -> (theory -> simpset -> term -> thm option) -> simproc - val simproc_global: theory -> string -> string list - -> (theory -> simpset -> term -> thm option) -> simproc - val inherit_context: simpset -> simpset -> simpset - val the_context: simpset -> Proof.context - val context: Proof.context -> simpset -> simpset - val global_context: theory -> simpset -> simpset - val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset - val debug_bounds: bool Unsynchronized.ref - val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset - val set_solvers: solver list -> simpset -> simpset - val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv - val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term - val rewrite_thm: bool * bool * bool -> - (simpset -> thm -> thm option) -> simpset -> thm -> thm - val rewrite_goal_rule: bool * bool * bool -> - (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm - val asm_rewrite_goal_tac: bool * bool * bool -> - (simpset -> tactic) -> simpset -> int -> tactic - val rewrite: bool -> thm list -> conv - val simplify: bool -> thm list -> thm -> thm -end; - -structure MetaSimplifier: META_SIMPLIFIER = -struct - -(** datatype simpset **) - -(* rewrite rules *) - -type rrule = - {thm: thm, (*the rewrite rule*) - name: string, (*name of theorem from which rewrite rule was extracted*) - lhs: term, (*the left-hand side*) - elhs: cterm, (*the etac-contracted lhs*) - extra: bool, (*extra variables outside of elhs*) - fo: bool, (*use first-order matching*) - perm: bool}; (*the rewrite rule is permutative*) - -(* -Remarks: - - elhs is used for matching, - lhs only for preservation of bound variable names; - - fo is set iff - either elhs is first-order (no Var is applied), - in which case fo-matching is complete, - or elhs is not a pattern, - in which case there is nothing better to do; -*) - -fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = - Thm.eq_thm_prop (thm1, thm2); - - -(* simplification sets, procedures, and solvers *) - -(*A simpset contains data required during conversion: - rules: discrimination net of rewrite rules; - prems: current premises; - bounds: maximal index of bound variables already used - (for generating new names when rewriting under lambda abstractions); - depth: simp_depth and exceeded flag; - congs: association list of congruence rules and - a list of `weak' congruence constants. - A congruence is `weak' if it avoids normalization of some argument. - procs: discrimination net of simplification procedures - (functions that prove rewrite rules on the fly); - mk_rews: - mk: turn simplification thms into rewrite rules; - mk_cong: prepare congruence rules; - mk_sym: turn == around; - mk_eq_True: turn P into P == True; - termless: relation for ordered rewriting;*) - -datatype simpset = - Simpset of - {rules: rrule Net.net, - prems: thm list, - bounds: int * ((string * typ) * string) list, - depth: int * bool Unsynchronized.ref, - context: Proof.context option} * - {congs: (string * thm) list * string list, - procs: proc Net.net, - mk_rews: - {mk: simpset -> thm -> thm list, - mk_cong: simpset -> thm -> thm, - mk_sym: simpset -> thm -> thm option, - mk_eq_True: simpset -> thm -> thm option, - reorient: theory -> term list -> term -> term -> bool}, - termless: term * term -> bool, - subgoal_tac: simpset -> int -> tactic, - loop_tacs: (string * (simpset -> int -> tactic)) list, - solvers: solver list * solver list} -and proc = - Proc of - {name: string, - lhs: cterm, - proc: simpset -> cterm -> thm option, - id: stamp * thm list} -and solver = - Solver of - {name: string, - solver: simpset -> int -> tactic, - id: stamp}; - - -fun internal_ss (Simpset args) = args; - -fun make_ss1 (rules, prems, bounds, depth, context) = - {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context}; - -fun map_ss1 f {rules, prems, bounds, depth, context} = - make_ss1 (f (rules, prems, bounds, depth, context)); - -fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = - {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, - subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; - -fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = - make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); - -fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); - -fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2); -fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2); - -fun prems_of_ss (Simpset ({prems, ...}, _)) = prems; - -fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) = - s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2); -fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2); - -fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()}; -fun mk_solver name solver = mk_solver' name (solver o prems_of_ss); - -fun solver_name (Solver {name, ...}) = name; -fun solver ss (Solver {solver = tac, ...}) = tac ss; -fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); - - -(* simp depth *) - -val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100)); -val simp_depth_limit = Config.int simp_depth_limit_raw; - -val simp_trace_depth_limit_default = Unsynchronized.ref 1; -val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit" - (fn _ => Config.Int (! simp_trace_depth_limit_default)); -val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw; - -fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default - | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit; - -fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg = - if depth > simp_trace_depth_limit_of context then - if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) - else - (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false); - -val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) => - (rules, prems, bounds, - (depth + 1, - if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context)); - -fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth; - - -(* diagnostics *) - -exception SIMPLIFIER of string * thm; - -val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false)); -val simp_debug = Config.bool simp_debug_raw; - -val simp_trace_default = Unsynchronized.ref false; -val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); -val simp_trace = Config.bool simp_trace_raw; - -fun if_enabled (Simpset ({context, ...}, _)) flag f = - (case context of - SOME ctxt => if Config.get ctxt flag then f ctxt else () - | NONE => ()) - -fun if_visible (Simpset ({context, ...}, _)) f x = - (case context of - SOME ctxt => if Context_Position.is_visible ctxt then f x else () - | NONE => ()); - -local - -fun prnt ss warn a = if warn then warning a else trace_depth ss a; - -fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = - let - val names = Term.declare_term_names t Name.context; - val xs = rev (#1 (Name.variants (rev (map #2 bs)) names)); - fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T)); - in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; - -fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ - Syntax.string_of_term ctxt - (if Config.get ctxt simp_debug then t else show_bounds ss t)); - -in - -fun print_term_global ss warn a thy t = - print_term ss warn (K a) t (ProofContext.init_global thy); - -fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ())); -fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ())); - -fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t); -fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t); - -fun trace_cterm warn a ss ct = - if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct)); - -fun trace_thm a ss th = - if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th)); - -fun trace_named_thm a ss (th, name) = - if_enabled ss simp_trace (print_term ss false - (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":") - (Thm.full_prop_of th)); - -fun warn_thm a ss th = - print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th); - -fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) (); - -end; - - - -(** simpset operations **) - -(* context *) - -fun eq_bound (x: string, (y, _)) = x = y; - -fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) => - (rules, prems, (count + 1, bound :: bounds), depth, context)); - -fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) => - (rules, ths @ prems, bounds, depth, context)); - -fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) = - map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context)); - -fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt - | the_context _ = raise Fail "Simplifier: no proof context in simpset"; - -fun context ctxt = - map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt)); - -val global_context = context o ProofContext.init_global; - -fun activate_context thy ss = - let - val ctxt = the_context ss; - val ctxt' = ctxt - |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) - |> Context_Position.set_visible false; - in context ctxt' ss end; - -fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss)); - - -(* maintain simp rules *) - -(* FIXME: it seems that the conditions on extra variables are too liberal if -prems are nonempty: does solving the prems really guarantee instantiation of -all its Vars? Better: a dynamic check each time a rule is applied. -*) -fun rewrite_rule_extra_vars prems elhs erhs = - let - val elhss = elhs :: prems; - val tvars = fold Term.add_tvars elhss []; - val vars = fold Term.add_vars elhss []; - in - erhs |> Term.exists_type (Term.exists_subtype - (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse - erhs |> Term.exists_subterm - (fn Var v => not (member (op =) vars v) | _ => false) - end; - -fun rrule_extra_vars elhs thm = - rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm); - -fun mk_rrule2 {thm, name, lhs, elhs, perm} = - let - val t = term_of elhs; - val fo = Pattern.first_order t orelse not (Pattern.pattern t); - val extra = rrule_extra_vars elhs thm; - in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end; - -fun del_rrule (rrule as {thm, elhs, ...}) ss = - ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => - (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context)) - handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss); - -fun insert_rrule (rrule as {thm, name, ...}) ss = - (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name); - ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => - let - val rrule2 as {elhs, ...} = mk_rrule2 rrule; - val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules; - in (rules', prems, bounds, depth, context) end) - handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss)); - -fun vperm (Var _, Var _) = true - | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) - | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) - | vperm (t, u) = (t = u); - -fun var_perm (t, u) = - vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); - -(*simple test for looping rewrite rules and stupid orientations*) -fun default_reorient thy prems lhs rhs = - rewrite_rule_extra_vars prems lhs rhs - orelse - is_Var (head_of lhs) - orelse -(* turns t = x around, which causes a headache if x is a local variable - - usually it is very useful :-( - is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) - andalso not(exists_subterm is_Var lhs) - orelse -*) - exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) - orelse - null prems andalso Pattern.matches thy (lhs, rhs) - (*the condition "null prems" is necessary because conditional rewrites - with extra variables in the conditions may terminate although - the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) - orelse - is_Const lhs andalso not (is_Const rhs); - -fun decomp_simp thm = - let - val thy = Thm.theory_of_thm thm; - val prop = Thm.prop_of thm; - val prems = Logic.strip_imp_prems prop; - val concl = Drule.strip_imp_concl (Thm.cprop_of thm); - val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => - raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); - val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); - val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*) - val erhs = Envir.eta_contract (term_of rhs); - val perm = - var_perm (term_of elhs, erhs) andalso - not (term_of elhs aconv erhs) andalso - not (is_Var (term_of elhs)); - in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end; - -fun decomp_simp' thm = - let val (_, _, lhs, _, rhs, _) = decomp_simp thm in - if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm) - else (lhs, rhs) - end; - -fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) = - (case mk_eq_True ss thm of - NONE => [] - | SOME eq_True => - let - val (_, _, lhs, elhs, _, _) = decomp_simp eq_True; - in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end); - -(*create the rewrite rule and possibly also the eq_True variant, - in case there are extra vars on the rhs*) -fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) = - let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in - if rewrite_rule_extra_vars [] lhs rhs then - mk_eq_True ss (thm2, name) @ [rrule] - else [rrule] - end; - -fun mk_rrule ss (thm, name) = - let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in - if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] - else - (*weak test for loops*) - if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs) - then mk_eq_True ss (thm, name) - else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) - end; - -fun orient_rrule ss (thm, name) = - let - val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm; - val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss; - in - if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] - else if reorient thy prems lhs rhs then - if reorient thy prems rhs lhs - then mk_eq_True ss (thm, name) - else - (case mk_sym ss thm of - NONE => [] - | SOME thm' => - let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' - in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) - else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) - end; - -fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = - maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms; - -fun extract_safe_rrules (ss, thm) = - maps (orient_rrule ss) (extract_rews (ss, [thm])); - - -(* add/del rules explicitly *) - -fun comb_simps comb mk_rrule (ss, thms) = - let - val rews = extract_rews (ss, thms); - in fold (fold comb o mk_rrule) rews ss end; - -fun ss addsimps thms = - comb_simps insert_rrule (mk_rrule ss) (ss, thms); - -fun ss delsimps thms = - comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); - -fun add_simp thm ss = ss addsimps [thm]; -fun del_simp thm ss = ss delsimps [thm]; - - -(* congs *) - -fun cong_name (Const (a, _)) = SOME a - | cong_name (Free (a, _)) = SOME ("Free: " ^ a) - | cong_name _ = NONE; - -local - -fun is_full_cong_prems [] [] = true - | is_full_cong_prems [] _ = false - | is_full_cong_prems (p :: prems) varpairs = - (case Logic.strip_assums_concl p of - Const ("==", _) $ lhs $ rhs => - let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in - is_Var x andalso forall is_Bound xs andalso - not (has_duplicates (op =) xs) andalso xs = ys andalso - member (op =) varpairs (x, y) andalso - is_full_cong_prems prems (remove (op =) (x, y) varpairs) - end - | _ => false); - -fun is_full_cong thm = - let - val prems = prems_of thm and concl = concl_of thm; - val (lhs, rhs) = Logic.dest_equals concl; - val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; - in - f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso - is_full_cong_prems prems (xs ~~ ys) - end; - -fun add_cong (ss, thm) = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - let - val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) - handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); - (*val lhs = Envir.eta_contract lhs;*) - val a = the (cong_name (head_of (term_of lhs))) handle Option.Option => - raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); - val (xs, weak) = congs; - val _ = - if AList.defined (op =) xs a - then if_visible ss warning ("Overwriting congruence rule for " ^ quote a) - else (); - val xs' = AList.update (op =) (a, thm) xs; - val weak' = if is_full_cong thm then weak else a :: weak; - in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); - -fun del_cong (ss, thm) = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - let - val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => - raise SIMPLIFIER ("Congruence not a meta-equality", thm); - (*val lhs = Envir.eta_contract lhs;*) - val a = the (cong_name (head_of lhs)) handle Option.Option => - raise SIMPLIFIER ("Congruence must start with a constant", thm); - val (xs, _) = congs; - val xs' = filter_out (fn (x : string, _) => x = a) xs; - val weak' = xs' |> map_filter (fn (a, thm) => - if is_full_cong thm then NONE else SOME a); - in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); - -fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss; - -in - -val (op addeqcongs) = Library.foldl add_cong; -val (op deleqcongs) = Library.foldl del_cong; - -fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; -fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; - -end; - - -(* simprocs *) - -datatype simproc = - Simproc of - {name: string, - lhss: cterm list, - proc: morphism -> simpset -> cterm -> thm option, - id: stamp * thm list}; - -fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); - -fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = - Simproc - {name = name, - lhss = map (Morphism.cterm phi) lhss, - proc = Morphism.transform phi proc, - id = (s, Morphism.fact phi ths)}; - -fun make_simproc {name, lhss, proc, identifier} = - Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)}; - -fun mk_simproc name lhss proc = - make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct => - proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []}; - -(* FIXME avoid global thy and Logic.varify_global *) -fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy); - - -local - -fun add_proc (proc as Proc {name, lhs, ...}) ss = - (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs; - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, Net.insert_term eq_proc (term_of lhs, proc) procs, - mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss - handle Net.INSERT => - (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss)); - -fun del_proc (proc as Proc {name, lhs, ...}) ss = - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, - mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss - handle Net.DELETE => - (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss); - -fun prep_procs (Simproc {name, lhss, proc, id}) = - lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id}); - -in - -fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss; -fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss; - -end; - - -(* mk_rews *) - -local - -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient}, - termless, subgoal_tac, loop_tacs, solvers) => - let - val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = - f (mk, mk_cong, mk_sym, mk_eq_True, reorient); - val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', - reorient = reorient'}; - in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); - -in - -fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss; - -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => - (mk, mk_cong, mk_sym, mk_eq_True, reorient)); - -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => - (mk, mk_cong, mk_sym, mk_eq_True, reorient)); - -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => - (mk, mk_cong, mk_sym, mk_eq_True, reorient)); - -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => - (mk, mk_cong, mk_sym, mk_eq_True, reorient)); - -fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => - (mk, mk_cong, mk_sym, mk_eq_True, reorient)); - -end; - - -(* termless *) - -fun ss settermless termless = ss |> - map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => - (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); - - -(* tactics *) - -fun ss setsubgoaler subgoal_tac = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => - (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); - -fun ss setloop' tac = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => - (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); - -fun ss setloop tac = ss setloop' (K tac); - -fun ss addloop' (name, tac) = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, procs, mk_rews, termless, subgoal_tac, - (if AList.defined (op =) loop_tacs name - then if_visible ss warning ("Overwriting looper " ^ quote name) - else (); AList.update (op =) (name, tac) loop_tacs), solvers)); - -fun ss addloop (name, tac) = ss addloop' (name, K tac); - -fun ss delloop name = ss |> - map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, procs, mk_rews, termless, subgoal_tac, - (if AList.defined (op =) loop_tacs name then () - else if_visible ss warning ("No such looper in simpset: " ^ quote name); - AList.delete (op =) name loop_tacs), solvers)); - -fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (unsafe_solvers, _)) => - (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); - -fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); - -fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, ([solver], solvers))); - -fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); - -fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, - subgoal_tac, loop_tacs, (solvers, solvers))); - - -(* empty *) - -fun init_ss mk_rews termless subgoal_tac solvers = - make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE), - (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); - -fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = - init_ss mk_rews termless subgoal_tac solvers - |> inherit_context ss; - -val empty_ss = - init_ss - {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], - mk_cong = K I, - mk_sym = K (SOME o Drule.symmetric_fun), - mk_eq_True = K (K NONE), - reorient = default_reorient} - Term_Ord.termless (K (K no_tac)) ([], []); - - -(* merge *) (*NOTE: ignores some fields of 2nd simpset*) - -fun merge_ss (ss1, ss2) = - if pointer_eq (ss1, ss2) then ss1 - else - let - val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _}, - {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, - loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; - val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, - {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, - loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; - - val rules' = Net.merge eq_rrule (rules1, rules2); - val prems' = Thm.merge_thms (prems1, prems2); - val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; - val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; - val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); - val weak' = merge (op =) (weak1, weak2); - val procs' = Net.merge eq_proc (procs1, procs2); - val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); - val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); - val solvers' = merge eq_solver (solvers1, solvers2); - in - make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs', - mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) - end; - - -(* dest_ss *) - -fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = - {simps = Net.entries rules - |> map (fn {name, thm, ...} => (name, thm)), - procs = Net.entries procs - |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) - |> partition_eq (eq_snd eq_procid) - |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), - congs = #1 congs, - weak_congs = #2 congs, - loopers = map fst loop_tacs, - unsafe_solvers = map solver_name (#1 solvers), - safe_solvers = map solver_name (#2 solvers)}; - - - -(** rewriting **) - -(* - Uses conversions, see: - L C Paulson, A higher-order implementation of rewriting, - Science of Computer Programming 3 (1983), pages 119-149. -*) - -fun check_conv msg ss thm thm' = - let - val thm'' = Thm.transitive thm thm' handle THM _ => - Thm.transitive thm (Thm.transitive - (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') - in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end - handle THM _ => - let - val _ $ _ $ prop0 = Thm.prop_of thm; - in - trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; - trace_term false (fn () => "Should have proved:") ss prop0; - NONE - end; - - -(* mk_procrule *) - -fun mk_procrule ss thm = - let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in - if rewrite_rule_extra_vars prems lhs rhs - then (cond_warn_thm "Extra vars on rhs:" ss thm; []) - else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] - end; - - -(* rewritec: conversion to apply the meta simpset to a term *) - -(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already - normalized terms by carrying around the rhs of the rewrite rule just - applied. This is called the `skeleton'. It is decomposed in parallel - with the term. Once a Var is encountered, the corresponding term is - already in normal form. - skel0 is a dummy skeleton that is to enforce complete normalization.*) - -val skel0 = Bound 0; - -(*Use rhs as skeleton only if the lhs does not contain unnormalized bits. - The latter may happen iff there are weak congruence rules for constants - in the lhs.*) - -fun uncond_skel ((_, weak), (lhs, rhs)) = - if null weak then rhs (*optimization*) - else if exists_Const (member (op =) weak o #1) lhs then skel0 - else rhs; - -(*Behaves like unconditional rule if rhs does not contain vars not in the lhs. - Otherwise those vars may become instantiated with unnormalized terms - while the premises are solved.*) - -fun cond_skel (args as (_, (lhs, rhs))) = - if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args - else skel0; - -(* - Rewriting -- we try in order: - (1) beta reduction - (2) unconditional rewrite rules - (3) conditional rewrite rules - (4) simplification procedures - - IMPORTANT: rewrite rules must not introduce new Vars or TVars! -*) - -fun rewritec (prover, thyt, maxt) ss t = - let - val ctxt = the_context ss; - val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss; - val eta_thm = Thm.eta_conversion t; - val eta_t' = Thm.rhs_of eta_thm; - val eta_t = term_of eta_t'; - fun rew {thm, name, lhs, elhs, extra, fo, perm} = - let - val prop = Thm.prop_of thm; - val (rthm, elhs') = - if maxt = ~1 orelse not extra then (thm, elhs) - else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); - val insts = - if fo then Thm.first_order_match (elhs', eta_t') - else Thm.match (elhs', eta_t'); - val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); - val prop' = Thm.prop_of thm'; - val unconditional = (Logic.count_prems prop' = 0); - val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') - in - if perm andalso not (termless (rhs', lhs')) - then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name); - trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE) - else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name); - if unconditional - then - (trace_thm (fn () => "Rewriting:") ss thm'; - let - val lr = Logic.dest_equals prop; - val SOME thm'' = check_conv false ss eta_thm thm'; - in SOME (thm'', uncond_skel (congs, lr)) end) - else - (trace_thm (fn () => "Trying to rewrite:") ss thm'; - if simp_depth ss > Config.get ctxt simp_depth_limit - then - let - val s = "simp_depth_limit exceeded - giving up"; - val _ = trace false (fn () => s) ss; - val _ = if_visible ss warning s; - in NONE end - else - case prover ss thm' of - NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE) - | SOME thm2 => - (case check_conv true ss eta_thm thm2 of - NONE => NONE | - SOME thm2' => - let val concl = Logic.strip_imp_concl prop - val lr = Logic.dest_equals concl - in SOME (thm2', cond_skel (congs, lr)) end))) - end - - fun rews [] = NONE - | rews (rrule :: rrules) = - let val opt = rew rrule handle Pattern.MATCH => NONE - in case opt of NONE => rews rrules | some => some end; - - fun sort_rrules rrs = - let - fun is_simple ({thm, ...}: rrule) = - (case Thm.prop_of thm of - Const ("==", _) $ _ $ _ => true - | _ => false); - fun sort [] (re1, re2) = re1 @ re2 - | sort (rr :: rrs) (re1, re2) = - if is_simple rr - then sort rrs (rr :: re1, re2) - else sort rrs (re1, rr :: re2); - in sort rrs ([], []) end; - - fun proc_rews [] = NONE - | proc_rews (Proc {name, proc, lhs, ...} :: ps) = - if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then - (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t; - case proc ss eta_t' of - NONE => (debug false (fn () => "FAILED") ss; proc_rews ps) - | SOME raw_thm => - (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") - ss raw_thm; - (case rews (mk_procrule ss raw_thm) of - NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^ - " -- does not match") ss t; proc_rews ps) - | some => some))) - else proc_rews ps; - in - (case eta_t of - Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0) - | _ => - (case rews (sort_rrules (Net.match_term rules eta_t)) of - NONE => proc_rews (Net.match_term procs eta_t) - | some => some)) - end; - - -(* conversion to apply a congruence rule to a term *) - -fun congc prover ss maxt cong t = - let val rthm = Thm.incr_indexes (maxt + 1) cong; - val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); - val insts = Thm.match (rlhs, t) - (* Thm.match can raise Pattern.MATCH; - is handled when congc is called *) - val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); - val _ = trace_thm (fn () => "Applying congruence rule:") ss thm'; - fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE) - in - (case prover thm' of - NONE => err ("Congruence proof failed. Could not prove", thm') - | SOME thm2 => - (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of - NONE => err ("Congruence proof failed. Should not have proved", thm2) - | SOME thm2' => - if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) - then NONE else SOME thm2')) - end; - -val (cA, (cB, cC)) = - apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); - -fun transitive1 NONE NONE = NONE - | transitive1 (SOME thm1) NONE = SOME thm1 - | transitive1 NONE (SOME thm2) = SOME thm2 - | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2) - -fun transitive2 thm = transitive1 (SOME thm); -fun transitive3 thm = transitive1 thm o SOME; - -fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) = - let - fun botc skel ss t = - if is_Var skel then NONE - else - (case subc skel ss t of - some as SOME thm1 => - (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of - SOME (thm2, skel2) => - transitive2 (Thm.transitive thm1 thm2) - (botc skel2 ss (Thm.rhs_of thm2)) - | NONE => some) - | NONE => - (case rewritec (prover, thy, maxidx) ss t of - SOME (thm2, skel2) => transitive2 thm2 - (botc skel2 ss (Thm.rhs_of thm2)) - | NONE => NONE)) - - and try_botc ss t = - (case botc skel0 ss t of - SOME trec1 => trec1 | NONE => (Thm.reflexive t)) - - and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 = - (case term_of t0 of - Abs (a, T, _) => - let - val b = Name.bound (#1 bounds); - val (v, t') = Thm.dest_abs (SOME b) t0; - val b' = #1 (Term.dest_Free (Thm.term_of v)); - val _ = - if b <> b' then - warning ("Simplifier: renamed bound variable " ^ - quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ())) - else (); - val ss' = add_bound ((b', T), a) ss; - val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; - in case botc skel' ss' t' of - SOME thm => SOME (Thm.abstract_rule a v thm) - | NONE => NONE - end - | t $ _ => (case t of - Const ("==>", _) $ _ => impc t0 ss - | Abs _ => - let val thm = Thm.beta_conversion false t0 - in case subc skel0 ss (Thm.rhs_of thm) of - NONE => SOME thm - | SOME thm' => SOME (Thm.transitive thm thm') - end - | _ => - let fun appc () = - let - val (tskel, uskel) = case skel of - tskel $ uskel => (tskel, uskel) - | _ => (skel0, skel0); - val (ct, cu) = Thm.dest_comb t0 - in - (case botc tskel ss ct of - SOME thm1 => - (case botc uskel ss cu of - SOME thm2 => SOME (Thm.combination thm1 thm2) - | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) - | NONE => - (case botc uskel ss cu of - SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) - | NONE => NONE)) - end - val (h, ts) = strip_comb t - in case cong_name h of - SOME a => - (case AList.lookup (op =) (fst congs) a of - NONE => appc () - | SOME cong => - (*post processing: some partial applications h t1 ... tj, j <= length ts, - may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) - (let - val thm = congc (prover ss) ss maxidx cong t0; - val t = the_default t0 (Option.map Thm.rhs_of thm); - val (cl, cr) = Thm.dest_comb t - val dVar = Var(("", 0), dummyT) - val skel = - list_comb (h, replicate (length ts) dVar) - in case botc skel ss cl of - NONE => thm - | SOME thm' => transitive3 thm - (Thm.combination thm' (Thm.reflexive cr)) - end handle Pattern.MATCH => appc ())) - | _ => appc () - end) - | _ => NONE) - - and impc ct ss = - if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss - - and rules_of_prem ss prem = - if maxidx_of_term (term_of prem) <> ~1 - then (trace_cterm true - (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:") - ss prem; ([], NONE)) - else - let val asm = Thm.assume prem - in (extract_safe_rrules (ss, asm), SOME asm) end - - and add_rrules (rrss, asms) ss = - (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms) - - and disch r prem eq = - let - val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); - val eq' = Thm.implies_elim (Thm.instantiate - ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) - (Thm.implies_intr prem eq) - in if not r then eq' else - let - val (prem', concl) = Thm.dest_implies lhs; - val (prem'', _) = Thm.dest_implies rhs - in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) - Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) - Drule.swap_prems_eq) - end - end - - and rebuild [] _ _ _ _ eq = eq - | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq = - let - val ss' = add_rrules (rev rrss, rev asms) ss; - val concl' = - Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); - val dprem = Option.map (disch false prem) - in - (case rewritec (prover, thy, maxidx) ss' concl' of - NONE => rebuild prems concl' rrss asms ss (dprem eq) - | SOME (eq', _) => transitive2 (fold (disch false) - prems (the (transitive3 (dprem eq) eq'))) - (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)) - end - - and mut_impc0 prems concl rrss asms ss = - let - val prems' = strip_imp_prems concl; - val (rrss', asms') = split_list (map (rules_of_prem ss) prems') - in - mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') - (asms @ asms') [] [] [] [] ss ~1 ~1 - end - - and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = - transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 - (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) - (if changed > 0 then - mut_impc (rev prems') concl (rev rrss') (rev asms') - [] [] [] [] ss ~1 changed - else rebuild prems' concl rrss' asms' ss - (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl)) - - | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) - prems' rrss' asms' eqns ss changed k = - case (if k = 0 then NONE else botc skel0 (add_rrules - (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of - NONE => mut_impc prems concl rrss asms (prem :: prems') - (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed - (if k = 0 then 0 else k - 1) - | SOME eqn => - let - val prem' = Thm.rhs_of eqn; - val tprems = map term_of prems; - val i = 1 + fold Integer.max (map (fn p => - find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1; - val (rrs', asm') = rules_of_prem ss prem' - in mut_impc prems concl rrss asms (prem' :: prems') - (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) - (take i prems) - (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies - (drop i prems, concl))))) :: eqns) - ss (length prems') ~1 - end - - (*legacy code - only for backwards compatibility*) - and nonmut_impc ct ss = - let - val (prem, conc) = Thm.dest_implies ct; - val thm1 = if simprem then botc skel0 ss prem else NONE; - val prem1 = the_default prem (Option.map Thm.rhs_of thm1); - val ss1 = - if not useprem then ss - else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss - in - (case botc skel0 ss1 conc of - NONE => - (case thm1 of - NONE => NONE - | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc))) - | SOME thm2 => - let val thm2' = disch false prem1 thm2 in - (case thm1 of - NONE => SOME thm2' - | SOME thm1' => - SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) - end) - end - - in try_botc end; - - -(* Meta-rewriting: rewrites t to u and returns the theorem t==u *) - -(* - Parameters: - mode = (simplify A, - use A in simplifying B, - use prems of B (if B is again a meta-impl.) to simplify A) - when simplifying A ==> B - prover: how to solve premises in conditional rewrites and congruences -*) - -val debug_bounds = Unsynchronized.ref false; - -fun check_bounds ss ct = - if ! debug_bounds then - let - val Simpset ({bounds = (_, bounds), ...}, _) = ss; - val bs = fold_aterms (fn Free (x, _) => - if Name.is_bound x andalso not (AList.defined eq_bound bounds x) - then insert (op =) x else I - | _ => I) (term_of ct) []; - in - if null bs then () - else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) - (Thm.theory_of_cterm ct) (Thm.term_of ct) - end - else (); - -fun rewrite_cterm mode prover raw_ss raw_ct = - let - val thy = Thm.theory_of_cterm raw_ct; - val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; - val {maxidx, ...} = Thm.rep_cterm ct; - val ss = inc_simp_depth (activate_context thy raw_ss); - val depth = simp_depth ss; - val _ = - if depth mod 20 = 0 then - if_visible ss warning ("Simplification depth " ^ string_of_int depth) - else (); - val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct; - val _ = check_bounds ss ct; - in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end; - -val simple_prover = - SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss))); - -fun rewrite _ [] ct = Thm.reflexive ct - | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover - (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct; - -fun simplify full thms = Conv.fconv_rule (rewrite full thms); -val rewrite_rule = simplify true; - -(*simple term rewriting -- no proof*) -fun rewrite_term thy rules procs = - Pattern.rewrite_term thy (map decomp_simp' rules) procs; - -fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss); - -(*Rewrite the subgoals of a proof state (represented by a theorem)*) -fun rewrite_goals_rule thms th = - Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover - (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th; - -(*Rewrite the subgoal of a proof state (represented by a theorem)*) -fun rewrite_goal_rule mode prover ss i thm = - if 0 < i andalso i <= Thm.nprems_of thm - then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm - else raise THM ("rewrite_goal_rule", i, [thm]); - - -(** meta-rewriting tactics **) - -(*Rewrite all subgoals*) -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); -fun rewtac def = rewrite_goals_tac [def]; - -(*Rewrite one subgoal*) -fun asm_rewrite_goal_tac mode prover_tac ss i thm = - if 0 < i andalso i <= Thm.nprems_of thm then - Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) - else Seq.empty; - -fun rewrite_goal_tac rews = - let val ss = empty_ss addsimps rews in - fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac) - (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.*) -val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; - - -(* for folding definitions, handling critical pairs *) - -(*The depth of nesting in a term*) -fun term_depth (Abs (_, _, t)) = 1 + term_depth t - | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t) - | term_depth _ = 0; - -val lhs_of_thm = #1 o Logic.dest_equals o prop_of; - -(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) - Returns longest lhs first to avoid folding its subexpressions.*) -fun sort_lhs_depths defs = - let val keylist = AList.make (term_depth o lhs_of_thm) defs - val keys = sort_distinct (rev_order o int_ord) (map #2 keylist) - in map (AList.find (op =) keylist) keys end; - -val rev_defs = sort_lhs_depths o map Thm.symmetric; - -fun fold_rule defs = fold rewrite_rule (rev_defs defs); -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); - - -(* HHF normal form: !! before ==>, outermost !! generalized *) - -local - -fun gen_norm_hhf ss th = - (if Drule.is_norm_hhf (Thm.prop_of th) then th - else Conv.fconv_rule - (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th) - |> Thm.adjust_maxidx_thm ~1 - |> Drule.gen_all; - -val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs; - -in - -val norm_hhf = gen_norm_hhf hhf_ss; -val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]); - -end; - -end; - -structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier; -open Basic_Meta_Simplifier; diff -r bb28bf635202 -r 4ae674714876 src/Pure/raw_simplifier.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/raw_simplifier.ML Fri Dec 17 18:38:33 2010 +0100 @@ -0,0 +1,1379 @@ +(* Title: Pure/raw_simplifier.ML + Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen + +Higher-order Simplification. +*) + +infix 4 + addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs + setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler + setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver; + +signature BASIC_RAW_SIMPLIFIER = +sig + val simp_depth_limit: int Config.T + val simp_trace_depth_limit: int Config.T + val simp_debug: bool Config.T + val simp_trace: bool Config.T + type rrule + val eq_rrule: rrule * rrule -> bool + type simpset + type proc + type solver + val mk_solver': string -> (simpset -> int -> tactic) -> solver + val mk_solver: string -> (thm list -> int -> tactic) -> solver + val empty_ss: simpset + val merge_ss: simpset * simpset -> simpset + val dest_ss: simpset -> + {simps: (string * thm) list, + procs: (string * cterm list) list, + congs: (string * thm) list, + weak_congs: string list, + loopers: string list, + unsafe_solvers: string list, + safe_solvers: string list} + type simproc + val eq_simproc: simproc * simproc -> bool + val morph_simproc: morphism -> simproc -> simproc + val make_simproc: {name: string, lhss: cterm list, + proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc + val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc + val prems_of_ss: simpset -> thm list + val addsimps: simpset * thm list -> simpset + val delsimps: simpset * thm list -> simpset + val addeqcongs: simpset * thm list -> simpset + val deleqcongs: simpset * thm list -> simpset + val addcongs: simpset * thm list -> simpset + val delcongs: simpset * thm list -> simpset + val addsimprocs: simpset * simproc list -> simpset + val delsimprocs: simpset * simproc list -> simpset + val mksimps: simpset -> thm -> thm list + val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset + val setmkcong: simpset * (simpset -> thm -> thm) -> simpset + val setmksym: simpset * (simpset -> thm -> thm option) -> simpset + val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset + val settermless: simpset * (term * term -> bool) -> simpset + val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset + val setloop': simpset * (simpset -> int -> tactic) -> simpset + val setloop: simpset * (int -> tactic) -> simpset + val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset + val addloop: simpset * (string * (int -> tactic)) -> simpset + val delloop: simpset * string -> simpset + val setSSolver: simpset * solver -> simpset + val addSSolver: simpset * solver -> simpset + val setSolver: simpset * solver -> simpset + val addSolver: simpset * solver -> simpset + + val rewrite_rule: thm list -> thm -> thm + val rewrite_goals_rule: thm list -> thm -> thm + val rewrite_goals_tac: thm list -> tactic + val rewrite_goal_tac: thm list -> int -> tactic + val rewtac: thm -> tactic + val prune_params_tac: tactic + val fold_rule: thm list -> thm -> thm + val fold_goals_tac: thm list -> tactic + val norm_hhf: thm -> thm + val norm_hhf_protect: thm -> thm +end; + +signature RAW_SIMPLIFIER = +sig + include BASIC_RAW_SIMPLIFIER + exception SIMPLIFIER of string * thm + val internal_ss: simpset -> + {rules: rrule Net.net, + prems: thm list, + bounds: int * ((string * typ) * string) list, + depth: int * bool Unsynchronized.ref, + context: Proof.context option} * + {congs: (string * thm) list * string list, + procs: proc Net.net, + mk_rews: + {mk: simpset -> thm -> thm list, + mk_cong: simpset -> thm -> thm, + mk_sym: simpset -> thm -> thm option, + mk_eq_True: simpset -> thm -> thm option, + reorient: theory -> term list -> term -> term -> bool}, + termless: term * term -> bool, + subgoal_tac: simpset -> int -> tactic, + loop_tacs: (string * (simpset -> int -> tactic)) list, + solvers: solver list * solver list} + val add_simp: thm -> simpset -> simpset + val del_simp: thm -> simpset -> simpset + val solver: simpset -> solver -> int -> tactic + val simp_depth_limit_raw: Config.raw + val clear_ss: simpset -> simpset + val simproc_global_i: theory -> string -> term list + -> (theory -> simpset -> term -> thm option) -> simproc + val simproc_global: theory -> string -> string list + -> (theory -> simpset -> term -> thm option) -> simproc + val simp_trace_depth_limit_raw: Config.raw + val simp_trace_depth_limit_default: int Unsynchronized.ref + val simp_trace_default: bool Unsynchronized.ref + val simp_trace_raw: Config.raw + val simp_debug_raw: Config.raw + val add_prems: thm list -> simpset -> simpset + val inherit_context: simpset -> simpset -> simpset + val the_context: simpset -> Proof.context + val context: Proof.context -> simpset -> simpset + val global_context: theory -> simpset -> simpset + val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset + val debug_bounds: bool Unsynchronized.ref + val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset + val set_solvers: solver list -> simpset -> simpset + val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv + val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term + val rewrite_thm: bool * bool * bool -> + (simpset -> thm -> thm option) -> simpset -> thm -> thm + val rewrite_goal_rule: bool * bool * bool -> + (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm + val asm_rewrite_goal_tac: bool * bool * bool -> + (simpset -> tactic) -> simpset -> int -> tactic + val rewrite: bool -> thm list -> conv + val simplify: bool -> thm list -> thm -> thm +end; + +structure Raw_Simplifier: RAW_SIMPLIFIER = +struct + +(** datatype simpset **) + +(* rewrite rules *) + +type rrule = + {thm: thm, (*the rewrite rule*) + name: string, (*name of theorem from which rewrite rule was extracted*) + lhs: term, (*the left-hand side*) + elhs: cterm, (*the etac-contracted lhs*) + extra: bool, (*extra variables outside of elhs*) + fo: bool, (*use first-order matching*) + perm: bool}; (*the rewrite rule is permutative*) + +(* +Remarks: + - elhs is used for matching, + lhs only for preservation of bound variable names; + - fo is set iff + either elhs is first-order (no Var is applied), + in which case fo-matching is complete, + or elhs is not a pattern, + in which case there is nothing better to do; +*) + +fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = + Thm.eq_thm_prop (thm1, thm2); + + +(* simplification sets, procedures, and solvers *) + +(*A simpset contains data required during conversion: + rules: discrimination net of rewrite rules; + prems: current premises; + bounds: maximal index of bound variables already used + (for generating new names when rewriting under lambda abstractions); + depth: simp_depth and exceeded flag; + congs: association list of congruence rules and + a list of `weak' congruence constants. + A congruence is `weak' if it avoids normalization of some argument. + procs: discrimination net of simplification procedures + (functions that prove rewrite rules on the fly); + mk_rews: + mk: turn simplification thms into rewrite rules; + mk_cong: prepare congruence rules; + mk_sym: turn == around; + mk_eq_True: turn P into P == True; + termless: relation for ordered rewriting;*) + +datatype simpset = + Simpset of + {rules: rrule Net.net, + prems: thm list, + bounds: int * ((string * typ) * string) list, + depth: int * bool Unsynchronized.ref, + context: Proof.context option} * + {congs: (string * thm) list * string list, + procs: proc Net.net, + mk_rews: + {mk: simpset -> thm -> thm list, + mk_cong: simpset -> thm -> thm, + mk_sym: simpset -> thm -> thm option, + mk_eq_True: simpset -> thm -> thm option, + reorient: theory -> term list -> term -> term -> bool}, + termless: term * term -> bool, + subgoal_tac: simpset -> int -> tactic, + loop_tacs: (string * (simpset -> int -> tactic)) list, + solvers: solver list * solver list} +and proc = + Proc of + {name: string, + lhs: cterm, + proc: simpset -> cterm -> thm option, + id: stamp * thm list} +and solver = + Solver of + {name: string, + solver: simpset -> int -> tactic, + id: stamp}; + + +fun internal_ss (Simpset args) = args; + +fun make_ss1 (rules, prems, bounds, depth, context) = + {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context}; + +fun map_ss1 f {rules, prems, bounds, depth, context} = + make_ss1 (f (rules, prems, bounds, depth, context)); + +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = + {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, + subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; + +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = + make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); + +fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); + +fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2); +fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2); + +fun prems_of_ss (Simpset ({prems, ...}, _)) = prems; + +fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) = + s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2); +fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2); + +fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()}; +fun mk_solver name solver = mk_solver' name (solver o prems_of_ss); + +fun solver_name (Solver {name, ...}) = name; +fun solver ss (Solver {solver = tac, ...}) = tac ss; +fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); + + +(* simp depth *) + +val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100)); +val simp_depth_limit = Config.int simp_depth_limit_raw; + +val simp_trace_depth_limit_default = Unsynchronized.ref 1; +val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit" + (fn _ => Config.Int (! simp_trace_depth_limit_default)); +val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw; + +fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default + | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit; + +fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg = + if depth > simp_trace_depth_limit_of context then + if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) + else + (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false); + +val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) => + (rules, prems, bounds, + (depth + 1, + if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context)); + +fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth; + + +(* diagnostics *) + +exception SIMPLIFIER of string * thm; + +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false)); +val simp_debug = Config.bool simp_debug_raw; + +val simp_trace_default = Unsynchronized.ref false; +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); +val simp_trace = Config.bool simp_trace_raw; + +fun if_enabled (Simpset ({context, ...}, _)) flag f = + (case context of + SOME ctxt => if Config.get ctxt flag then f ctxt else () + | NONE => ()) + +fun if_visible (Simpset ({context, ...}, _)) f x = + (case context of + SOME ctxt => if Context_Position.is_visible ctxt then f x else () + | NONE => ()); + +local + +fun prnt ss warn a = if warn then warning a else trace_depth ss a; + +fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = + let + val names = Term.declare_term_names t Name.context; + val xs = rev (#1 (Name.variants (rev (map #2 bs)) names)); + fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T)); + in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; + +fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ + Syntax.string_of_term ctxt + (if Config.get ctxt simp_debug then t else show_bounds ss t)); + +in + +fun print_term_global ss warn a thy t = + print_term ss warn (K a) t (ProofContext.init_global thy); + +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ())); +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ())); + +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t); +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t); + +fun trace_cterm warn a ss ct = + if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct)); + +fun trace_thm a ss th = + if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th)); + +fun trace_named_thm a ss (th, name) = + if_enabled ss simp_trace (print_term ss false + (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":") + (Thm.full_prop_of th)); + +fun warn_thm a ss th = + print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th); + +fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) (); + +end; + + + +(** simpset operations **) + +(* context *) + +fun eq_bound (x: string, (y, _)) = x = y; + +fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) => + (rules, prems, (count + 1, bound :: bounds), depth, context)); + +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) => + (rules, ths @ prems, bounds, depth, context)); + +fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) = + map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context)); + +fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt + | the_context _ = raise Fail "Simplifier: no proof context in simpset"; + +fun context ctxt = + map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt)); + +val global_context = context o ProofContext.init_global; + +fun activate_context thy ss = + let + val ctxt = the_context ss; + val ctxt' = ctxt + |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) + |> Context_Position.set_visible false; + in context ctxt' ss end; + +fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss)); + + +(* maintain simp rules *) + +(* FIXME: it seems that the conditions on extra variables are too liberal if +prems are nonempty: does solving the prems really guarantee instantiation of +all its Vars? Better: a dynamic check each time a rule is applied. +*) +fun rewrite_rule_extra_vars prems elhs erhs = + let + val elhss = elhs :: prems; + val tvars = fold Term.add_tvars elhss []; + val vars = fold Term.add_vars elhss []; + in + erhs |> Term.exists_type (Term.exists_subtype + (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse + erhs |> Term.exists_subterm + (fn Var v => not (member (op =) vars v) | _ => false) + end; + +fun rrule_extra_vars elhs thm = + rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm); + +fun mk_rrule2 {thm, name, lhs, elhs, perm} = + let + val t = term_of elhs; + val fo = Pattern.first_order t orelse not (Pattern.pattern t); + val extra = rrule_extra_vars elhs thm; + in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end; + +fun del_rrule (rrule as {thm, elhs, ...}) ss = + ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => + (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context)) + handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss); + +fun insert_rrule (rrule as {thm, name, ...}) ss = + (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name); + ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => + let + val rrule2 as {elhs, ...} = mk_rrule2 rrule; + val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules; + in (rules', prems, bounds, depth, context) end) + handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss)); + +fun vperm (Var _, Var _) = true + | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) + | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) + | vperm (t, u) = (t = u); + +fun var_perm (t, u) = + vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); + +(*simple test for looping rewrite rules and stupid orientations*) +fun default_reorient thy prems lhs rhs = + rewrite_rule_extra_vars prems lhs rhs + orelse + is_Var (head_of lhs) + orelse +(* turns t = x around, which causes a headache if x is a local variable - + usually it is very useful :-( + is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) + andalso not(exists_subterm is_Var lhs) + orelse +*) + exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) + orelse + null prems andalso Pattern.matches thy (lhs, rhs) + (*the condition "null prems" is necessary because conditional rewrites + with extra variables in the conditions may terminate although + the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) + orelse + is_Const lhs andalso not (is_Const rhs); + +fun decomp_simp thm = + let + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; + val prems = Logic.strip_imp_prems prop; + val concl = Drule.strip_imp_concl (Thm.cprop_of thm); + val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => + raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); + val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); + val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*) + val erhs = Envir.eta_contract (term_of rhs); + val perm = + var_perm (term_of elhs, erhs) andalso + not (term_of elhs aconv erhs) andalso + not (is_Var (term_of elhs)); + in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end; + +fun decomp_simp' thm = + let val (_, _, lhs, _, rhs, _) = decomp_simp thm in + if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm) + else (lhs, rhs) + end; + +fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) = + (case mk_eq_True ss thm of + NONE => [] + | SOME eq_True => + let + val (_, _, lhs, elhs, _, _) = decomp_simp eq_True; + in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end); + +(*create the rewrite rule and possibly also the eq_True variant, + in case there are extra vars on the rhs*) +fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) = + let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in + if rewrite_rule_extra_vars [] lhs rhs then + mk_eq_True ss (thm2, name) @ [rrule] + else [rrule] + end; + +fun mk_rrule ss (thm, name) = + let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in + if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] + else + (*weak test for loops*) + if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs) + then mk_eq_True ss (thm, name) + else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) + end; + +fun orient_rrule ss (thm, name) = + let + val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm; + val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss; + in + if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] + else if reorient thy prems lhs rhs then + if reorient thy prems rhs lhs + then mk_eq_True ss (thm, name) + else + (case mk_sym ss thm of + NONE => [] + | SOME thm' => + let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' + in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) + else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) + end; + +fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = + maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms; + +fun extract_safe_rrules (ss, thm) = + maps (orient_rrule ss) (extract_rews (ss, [thm])); + + +(* add/del rules explicitly *) + +fun comb_simps comb mk_rrule (ss, thms) = + let + val rews = extract_rews (ss, thms); + in fold (fold comb o mk_rrule) rews ss end; + +fun ss addsimps thms = + comb_simps insert_rrule (mk_rrule ss) (ss, thms); + +fun ss delsimps thms = + comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); + +fun add_simp thm ss = ss addsimps [thm]; +fun del_simp thm ss = ss delsimps [thm]; + + +(* congs *) + +fun cong_name (Const (a, _)) = SOME a + | cong_name (Free (a, _)) = SOME ("Free: " ^ a) + | cong_name _ = NONE; + +local + +fun is_full_cong_prems [] [] = true + | is_full_cong_prems [] _ = false + | is_full_cong_prems (p :: prems) varpairs = + (case Logic.strip_assums_concl p of + Const ("==", _) $ lhs $ rhs => + let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in + is_Var x andalso forall is_Bound xs andalso + not (has_duplicates (op =) xs) andalso xs = ys andalso + member (op =) varpairs (x, y) andalso + is_full_cong_prems prems (remove (op =) (x, y) varpairs) + end + | _ => false); + +fun is_full_cong thm = + let + val prems = prems_of thm and concl = concl_of thm; + val (lhs, rhs) = Logic.dest_equals concl; + val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; + in + f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso + is_full_cong_prems prems (xs ~~ ys) + end; + +fun add_cong (ss, thm) = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + let + val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) + handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); + (*val lhs = Envir.eta_contract lhs;*) + val a = the (cong_name (head_of (term_of lhs))) handle Option.Option => + raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); + val (xs, weak) = congs; + val _ = + if AList.defined (op =) xs a + then if_visible ss warning ("Overwriting congruence rule for " ^ quote a) + else (); + val xs' = AList.update (op =) (a, thm) xs; + val weak' = if is_full_cong thm then weak else a :: weak; + in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); + +fun del_cong (ss, thm) = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + let + val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => + raise SIMPLIFIER ("Congruence not a meta-equality", thm); + (*val lhs = Envir.eta_contract lhs;*) + val a = the (cong_name (head_of lhs)) handle Option.Option => + raise SIMPLIFIER ("Congruence must start with a constant", thm); + val (xs, _) = congs; + val xs' = filter_out (fn (x : string, _) => x = a) xs; + val weak' = xs' |> map_filter (fn (a, thm) => + if is_full_cong thm then NONE else SOME a); + in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); + +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss; + +in + +val (op addeqcongs) = Library.foldl add_cong; +val (op deleqcongs) = Library.foldl del_cong; + +fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; +fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; + +end; + + +(* simprocs *) + +datatype simproc = + Simproc of + {name: string, + lhss: cterm list, + proc: morphism -> simpset -> cterm -> thm option, + id: stamp * thm list}; + +fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); + +fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = + Simproc + {name = name, + lhss = map (Morphism.cterm phi) lhss, + proc = Morphism.transform phi proc, + id = (s, Morphism.fact phi ths)}; + +fun make_simproc {name, lhss, proc, identifier} = + Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)}; + +fun mk_simproc name lhss proc = + make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct => + proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []}; + +(* FIXME avoid global thy and Logic.varify_global *) +fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); +fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy); + + +local + +fun add_proc (proc as Proc {name, lhs, ...}) ss = + (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs; + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + (congs, Net.insert_term eq_proc (term_of lhs, proc) procs, + mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss + handle Net.INSERT => + (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss)); + +fun del_proc (proc as Proc {name, lhs, ...}) ss = + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, + mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss + handle Net.DELETE => + (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss); + +fun prep_procs (Simproc {name, lhss, proc, id}) = + lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id}); + +in + +fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss; +fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss; + +end; + + +(* mk_rews *) + +local + +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient}, + termless, subgoal_tac, loop_tacs, solvers) => + let + val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = + f (mk, mk_cong, mk_sym, mk_eq_True, reorient); + val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', + reorient = reorient'}; + in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); + +in + +fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss; + +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +end; + + +(* termless *) + +fun ss settermless termless = ss |> + map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => + (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); + + +(* tactics *) + +fun ss setsubgoaler subgoal_tac = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => + (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); + +fun ss setloop' tac = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => + (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); + +fun ss setloop tac = ss setloop' (K tac); + +fun ss addloop' (name, tac) = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + (congs, procs, mk_rews, termless, subgoal_tac, + (if AList.defined (op =) loop_tacs name + then if_visible ss warning ("Overwriting looper " ^ quote name) + else (); AList.update (op =) (name, tac) loop_tacs), solvers)); + +fun ss addloop (name, tac) = ss addloop' (name, K tac); + +fun ss delloop name = ss |> + map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => + (congs, procs, mk_rews, termless, subgoal_tac, + (if AList.defined (op =) loop_tacs name then () + else if_visible ss warning ("No such looper in simpset: " ^ quote name); + AList.delete (op =) name loop_tacs), solvers)); + +fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (unsafe_solvers, _)) => + (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); + +fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); + +fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, ([solver], solvers))); + +fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); + +fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, + subgoal_tac, loop_tacs, (solvers, solvers))); + + +(* empty *) + +fun init_ss mk_rews termless subgoal_tac solvers = + make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE), + (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); + +fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = + init_ss mk_rews termless subgoal_tac solvers + |> inherit_context ss; + +val empty_ss = + init_ss + {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], + mk_cong = K I, + mk_sym = K (SOME o Drule.symmetric_fun), + mk_eq_True = K (K NONE), + reorient = default_reorient} + Term_Ord.termless (K (K no_tac)) ([], []); + + +(* merge *) (*NOTE: ignores some fields of 2nd simpset*) + +fun merge_ss (ss1, ss2) = + if pointer_eq (ss1, ss2) then ss1 + else + let + val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _}, + {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, + loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; + val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, + {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, + loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; + + val rules' = Net.merge eq_rrule (rules1, rules2); + val prems' = Thm.merge_thms (prems1, prems2); + val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; + val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; + val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); + val weak' = merge (op =) (weak1, weak2); + val procs' = Net.merge eq_proc (procs1, procs2); + val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); + val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); + val solvers' = merge eq_solver (solvers1, solvers2); + in + make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs', + mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) + end; + + +(* dest_ss *) + +fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = + {simps = Net.entries rules + |> map (fn {name, thm, ...} => (name, thm)), + procs = Net.entries procs + |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) + |> partition_eq (eq_snd eq_procid) + |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), + congs = #1 congs, + weak_congs = #2 congs, + loopers = map fst loop_tacs, + unsafe_solvers = map solver_name (#1 solvers), + safe_solvers = map solver_name (#2 solvers)}; + + + +(** rewriting **) + +(* + Uses conversions, see: + L C Paulson, A higher-order implementation of rewriting, + Science of Computer Programming 3 (1983), pages 119-149. +*) + +fun check_conv msg ss thm thm' = + let + val thm'' = Thm.transitive thm thm' handle THM _ => + Thm.transitive thm (Thm.transitive + (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') + in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end + handle THM _ => + let + val _ $ _ $ prop0 = Thm.prop_of thm; + in + trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; + trace_term false (fn () => "Should have proved:") ss prop0; + NONE + end; + + +(* mk_procrule *) + +fun mk_procrule ss thm = + let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in + if rewrite_rule_extra_vars prems lhs rhs + then (cond_warn_thm "Extra vars on rhs:" ss thm; []) + else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] + end; + + +(* rewritec: conversion to apply the meta simpset to a term *) + +(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already + normalized terms by carrying around the rhs of the rewrite rule just + applied. This is called the `skeleton'. It is decomposed in parallel + with the term. Once a Var is encountered, the corresponding term is + already in normal form. + skel0 is a dummy skeleton that is to enforce complete normalization.*) + +val skel0 = Bound 0; + +(*Use rhs as skeleton only if the lhs does not contain unnormalized bits. + The latter may happen iff there are weak congruence rules for constants + in the lhs.*) + +fun uncond_skel ((_, weak), (lhs, rhs)) = + if null weak then rhs (*optimization*) + else if exists_Const (member (op =) weak o #1) lhs then skel0 + else rhs; + +(*Behaves like unconditional rule if rhs does not contain vars not in the lhs. + Otherwise those vars may become instantiated with unnormalized terms + while the premises are solved.*) + +fun cond_skel (args as (_, (lhs, rhs))) = + if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args + else skel0; + +(* + Rewriting -- we try in order: + (1) beta reduction + (2) unconditional rewrite rules + (3) conditional rewrite rules + (4) simplification procedures + + IMPORTANT: rewrite rules must not introduce new Vars or TVars! +*) + +fun rewritec (prover, thyt, maxt) ss t = + let + val ctxt = the_context ss; + val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss; + val eta_thm = Thm.eta_conversion t; + val eta_t' = Thm.rhs_of eta_thm; + val eta_t = term_of eta_t'; + fun rew {thm, name, lhs, elhs, extra, fo, perm} = + let + val prop = Thm.prop_of thm; + val (rthm, elhs') = + if maxt = ~1 orelse not extra then (thm, elhs) + else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); + val insts = + if fo then Thm.first_order_match (elhs', eta_t') + else Thm.match (elhs', eta_t'); + val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); + val prop' = Thm.prop_of thm'; + val unconditional = (Logic.count_prems prop' = 0); + val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') + in + if perm andalso not (termless (rhs', lhs')) + then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name); + trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE) + else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name); + if unconditional + then + (trace_thm (fn () => "Rewriting:") ss thm'; + let + val lr = Logic.dest_equals prop; + val SOME thm'' = check_conv false ss eta_thm thm'; + in SOME (thm'', uncond_skel (congs, lr)) end) + else + (trace_thm (fn () => "Trying to rewrite:") ss thm'; + if simp_depth ss > Config.get ctxt simp_depth_limit + then + let + val s = "simp_depth_limit exceeded - giving up"; + val _ = trace false (fn () => s) ss; + val _ = if_visible ss warning s; + in NONE end + else + case prover ss thm' of + NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE) + | SOME thm2 => + (case check_conv true ss eta_thm thm2 of + NONE => NONE | + SOME thm2' => + let val concl = Logic.strip_imp_concl prop + val lr = Logic.dest_equals concl + in SOME (thm2', cond_skel (congs, lr)) end))) + end + + fun rews [] = NONE + | rews (rrule :: rrules) = + let val opt = rew rrule handle Pattern.MATCH => NONE + in case opt of NONE => rews rrules | some => some end; + + fun sort_rrules rrs = + let + fun is_simple ({thm, ...}: rrule) = + (case Thm.prop_of thm of + Const ("==", _) $ _ $ _ => true + | _ => false); + fun sort [] (re1, re2) = re1 @ re2 + | sort (rr :: rrs) (re1, re2) = + if is_simple rr + then sort rrs (rr :: re1, re2) + else sort rrs (re1, rr :: re2); + in sort rrs ([], []) end; + + fun proc_rews [] = NONE + | proc_rews (Proc {name, proc, lhs, ...} :: ps) = + if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then + (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t; + case proc ss eta_t' of + NONE => (debug false (fn () => "FAILED") ss; proc_rews ps) + | SOME raw_thm => + (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") + ss raw_thm; + (case rews (mk_procrule ss raw_thm) of + NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^ + " -- does not match") ss t; proc_rews ps) + | some => some))) + else proc_rews ps; + in + (case eta_t of + Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0) + | _ => + (case rews (sort_rrules (Net.match_term rules eta_t)) of + NONE => proc_rews (Net.match_term procs eta_t) + | some => some)) + end; + + +(* conversion to apply a congruence rule to a term *) + +fun congc prover ss maxt cong t = + let val rthm = Thm.incr_indexes (maxt + 1) cong; + val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); + val insts = Thm.match (rlhs, t) + (* Thm.match can raise Pattern.MATCH; + is handled when congc is called *) + val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); + val _ = trace_thm (fn () => "Applying congruence rule:") ss thm'; + fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE) + in + (case prover thm' of + NONE => err ("Congruence proof failed. Could not prove", thm') + | SOME thm2 => + (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of + NONE => err ("Congruence proof failed. Should not have proved", thm2) + | SOME thm2' => + if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) + then NONE else SOME thm2')) + end; + +val (cA, (cB, cC)) = + apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); + +fun transitive1 NONE NONE = NONE + | transitive1 (SOME thm1) NONE = SOME thm1 + | transitive1 NONE (SOME thm2) = SOME thm2 + | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2) + +fun transitive2 thm = transitive1 (SOME thm); +fun transitive3 thm = transitive1 thm o SOME; + +fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) = + let + fun botc skel ss t = + if is_Var skel then NONE + else + (case subc skel ss t of + some as SOME thm1 => + (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of + SOME (thm2, skel2) => + transitive2 (Thm.transitive thm1 thm2) + (botc skel2 ss (Thm.rhs_of thm2)) + | NONE => some) + | NONE => + (case rewritec (prover, thy, maxidx) ss t of + SOME (thm2, skel2) => transitive2 thm2 + (botc skel2 ss (Thm.rhs_of thm2)) + | NONE => NONE)) + + and try_botc ss t = + (case botc skel0 ss t of + SOME trec1 => trec1 | NONE => (Thm.reflexive t)) + + and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 = + (case term_of t0 of + Abs (a, T, _) => + let + val b = Name.bound (#1 bounds); + val (v, t') = Thm.dest_abs (SOME b) t0; + val b' = #1 (Term.dest_Free (Thm.term_of v)); + val _ = + if b <> b' then + warning ("Simplifier: renamed bound variable " ^ + quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ())) + else (); + val ss' = add_bound ((b', T), a) ss; + val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; + in case botc skel' ss' t' of + SOME thm => SOME (Thm.abstract_rule a v thm) + | NONE => NONE + end + | t $ _ => (case t of + Const ("==>", _) $ _ => impc t0 ss + | Abs _ => + let val thm = Thm.beta_conversion false t0 + in case subc skel0 ss (Thm.rhs_of thm) of + NONE => SOME thm + | SOME thm' => SOME (Thm.transitive thm thm') + end + | _ => + let fun appc () = + let + val (tskel, uskel) = case skel of + tskel $ uskel => (tskel, uskel) + | _ => (skel0, skel0); + val (ct, cu) = Thm.dest_comb t0 + in + (case botc tskel ss ct of + SOME thm1 => + (case botc uskel ss cu of + SOME thm2 => SOME (Thm.combination thm1 thm2) + | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) + | NONE => + (case botc uskel ss cu of + SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) + | NONE => NONE)) + end + val (h, ts) = strip_comb t + in case cong_name h of + SOME a => + (case AList.lookup (op =) (fst congs) a of + NONE => appc () + | SOME cong => + (*post processing: some partial applications h t1 ... tj, j <= length ts, + may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) + (let + val thm = congc (prover ss) ss maxidx cong t0; + val t = the_default t0 (Option.map Thm.rhs_of thm); + val (cl, cr) = Thm.dest_comb t + val dVar = Var(("", 0), dummyT) + val skel = + list_comb (h, replicate (length ts) dVar) + in case botc skel ss cl of + NONE => thm + | SOME thm' => transitive3 thm + (Thm.combination thm' (Thm.reflexive cr)) + end handle Pattern.MATCH => appc ())) + | _ => appc () + end) + | _ => NONE) + + and impc ct ss = + if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss + + and rules_of_prem ss prem = + if maxidx_of_term (term_of prem) <> ~1 + then (trace_cterm true + (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:") + ss prem; ([], NONE)) + else + let val asm = Thm.assume prem + in (extract_safe_rrules (ss, asm), SOME asm) end + + and add_rrules (rrss, asms) ss = + (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms) + + and disch r prem eq = + let + val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); + val eq' = Thm.implies_elim (Thm.instantiate + ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) + (Thm.implies_intr prem eq) + in if not r then eq' else + let + val (prem', concl) = Thm.dest_implies lhs; + val (prem'', _) = Thm.dest_implies rhs + in Thm.transitive (Thm.transitive + (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) + Drule.swap_prems_eq) eq') + (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) + Drule.swap_prems_eq) + end + end + + and rebuild [] _ _ _ _ eq = eq + | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq = + let + val ss' = add_rrules (rev rrss, rev asms) ss; + val concl' = + Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); + val dprem = Option.map (disch false prem) + in + (case rewritec (prover, thy, maxidx) ss' concl' of + NONE => rebuild prems concl' rrss asms ss (dprem eq) + | SOME (eq', _) => transitive2 (fold (disch false) + prems (the (transitive3 (dprem eq) eq'))) + (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)) + end + + and mut_impc0 prems concl rrss asms ss = + let + val prems' = strip_imp_prems concl; + val (rrss', asms') = split_list (map (rules_of_prem ss) prems') + in + mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') + (asms @ asms') [] [] [] [] ss ~1 ~1 + end + + and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = + transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 + (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) + (if changed > 0 then + mut_impc (rev prems') concl (rev rrss') (rev asms') + [] [] [] [] ss ~1 changed + else rebuild prems' concl rrss' asms' ss + (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl)) + + | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) + prems' rrss' asms' eqns ss changed k = + case (if k = 0 then NONE else botc skel0 (add_rrules + (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of + NONE => mut_impc prems concl rrss asms (prem :: prems') + (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed + (if k = 0 then 0 else k - 1) + | SOME eqn => + let + val prem' = Thm.rhs_of eqn; + val tprems = map term_of prems; + val i = 1 + fold Integer.max (map (fn p => + find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1; + val (rrs', asm') = rules_of_prem ss prem' + in mut_impc prems concl rrss asms (prem' :: prems') + (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) + (take i prems) + (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies + (drop i prems, concl))))) :: eqns) + ss (length prems') ~1 + end + + (*legacy code - only for backwards compatibility*) + and nonmut_impc ct ss = + let + val (prem, conc) = Thm.dest_implies ct; + val thm1 = if simprem then botc skel0 ss prem else NONE; + val prem1 = the_default prem (Option.map Thm.rhs_of thm1); + val ss1 = + if not useprem then ss + else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss + in + (case botc skel0 ss1 conc of + NONE => + (case thm1 of + NONE => NONE + | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc))) + | SOME thm2 => + let val thm2' = disch false prem1 thm2 in + (case thm1 of + NONE => SOME thm2' + | SOME thm1' => + SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) + end) + end + + in try_botc end; + + +(* Meta-rewriting: rewrites t to u and returns the theorem t==u *) + +(* + Parameters: + mode = (simplify A, + use A in simplifying B, + use prems of B (if B is again a meta-impl.) to simplify A) + when simplifying A ==> B + prover: how to solve premises in conditional rewrites and congruences +*) + +val debug_bounds = Unsynchronized.ref false; + +fun check_bounds ss ct = + if ! debug_bounds then + let + val Simpset ({bounds = (_, bounds), ...}, _) = ss; + val bs = fold_aterms (fn Free (x, _) => + if Name.is_bound x andalso not (AList.defined eq_bound bounds x) + then insert (op =) x else I + | _ => I) (term_of ct) []; + in + if null bs then () + else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) + (Thm.theory_of_cterm ct) (Thm.term_of ct) + end + else (); + +fun rewrite_cterm mode prover raw_ss raw_ct = + let + val thy = Thm.theory_of_cterm raw_ct; + val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; + val {maxidx, ...} = Thm.rep_cterm ct; + val ss = inc_simp_depth (activate_context thy raw_ss); + val depth = simp_depth ss; + val _ = + if depth mod 20 = 0 then + if_visible ss warning ("Simplification depth " ^ string_of_int depth) + else (); + val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct; + val _ = check_bounds ss ct; + in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end; + +val simple_prover = + SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss))); + +fun rewrite _ [] ct = Thm.reflexive ct + | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover + (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct; + +fun simplify full thms = Conv.fconv_rule (rewrite full thms); +val rewrite_rule = simplify true; + +(*simple term rewriting -- no proof*) +fun rewrite_term thy rules procs = + Pattern.rewrite_term thy (map decomp_simp' rules) procs; + +fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss); + +(*Rewrite the subgoals of a proof state (represented by a theorem)*) +fun rewrite_goals_rule thms th = + Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover + (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th; + +(*Rewrite the subgoal of a proof state (represented by a theorem)*) +fun rewrite_goal_rule mode prover ss i thm = + if 0 < i andalso i <= Thm.nprems_of thm + then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm + else raise THM ("rewrite_goal_rule", i, [thm]); + + +(** meta-rewriting tactics **) + +(*Rewrite all subgoals*) +fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); +fun rewtac def = rewrite_goals_tac [def]; + +(*Rewrite one subgoal*) +fun asm_rewrite_goal_tac mode prover_tac ss i thm = + if 0 < i andalso i <= Thm.nprems_of thm then + Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) + else Seq.empty; + +fun rewrite_goal_tac rews = + let val ss = empty_ss addsimps rews in + fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac) + (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.*) +val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; + + +(* for folding definitions, handling critical pairs *) + +(*The depth of nesting in a term*) +fun term_depth (Abs (_, _, t)) = 1 + term_depth t + | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t) + | term_depth _ = 0; + +val lhs_of_thm = #1 o Logic.dest_equals o prop_of; + +(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) + Returns longest lhs first to avoid folding its subexpressions.*) +fun sort_lhs_depths defs = + let val keylist = AList.make (term_depth o lhs_of_thm) defs + val keys = sort_distinct (rev_order o int_ord) (map #2 keylist) + in map (AList.find (op =) keylist) keys end; + +val rev_defs = sort_lhs_depths o map Thm.symmetric; + +fun fold_rule defs = fold rewrite_rule (rev_defs defs); +fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); + + +(* HHF normal form: !! before ==>, outermost !! generalized *) + +local + +fun gen_norm_hhf ss th = + (if Drule.is_norm_hhf (Thm.prop_of th) then th + else Conv.fconv_rule + (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th) + |> Thm.adjust_maxidx_thm ~1 + |> Drule.gen_all; + +val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs; + +in + +val norm_hhf = gen_norm_hhf hhf_ss; +val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]); + +end; + +end; + +structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier; +open Basic_Meta_Simplifier; diff -r bb28bf635202 -r 4ae674714876 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Pure/simplifier.ML Fri Dec 17 18:38:33 2010 +0100 @@ -7,7 +7,7 @@ signature BASIC_SIMPLIFIER = sig - include BASIC_META_SIMPLIFIER + include BASIC_RAW_SIMPLIFIER val change_simpset: (simpset -> simpset) -> unit val global_simpset_of: theory -> simpset val Addsimprocs: simproc list -> unit @@ -33,6 +33,9 @@ val pretty_ss: Proof.context -> simpset -> Pretty.T val clear_ss: simpset -> simpset val debug_bounds: bool Unsynchronized.ref + val add_simp: thm -> simpset -> simpset + val del_simp: thm -> simpset -> simpset + val add_prems: thm list -> simpset -> simpset val inherit_context: simpset -> simpset -> simpset val the_context: simpset -> Proof.context val context: Proof.context -> simpset -> simpset @@ -72,7 +75,7 @@ structure Simplifier: SIMPLIFIER = struct -open MetaSimplifier; +open Raw_Simplifier; (** pretty printing **) @@ -104,7 +107,7 @@ ( type T = simpset; val empty = empty_ss; - fun extend ss = MetaSimplifier.inherit_context empty_ss ss; + fun extend ss = Raw_Simplifier.inherit_context empty_ss ss; val merge = merge_ss; ); @@ -127,7 +130,7 @@ fun map_simpset f = Context.theory_map (map_ss f); fun change_simpset f = Context.>> (Context.map_theory (map_simpset f)); fun global_simpset_of thy = - MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy)); + Raw_Simplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy)); fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args); fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); @@ -135,7 +138,7 @@ (* local simpset *) -fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt)); +fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt)); val _ = ML_Antiquote.value "simpset" (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"); @@ -215,16 +218,16 @@ fun solve_all_tac solvers ss = let - val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss; - val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); + val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss ss; + val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); in DEPTH_SOLVE (solve_tac 1) end; (*NOTE: may instantiate unknowns that appear also in other subgoals*) fun generic_simp_tac safe mode ss = let - val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss; + val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = Raw_Simplifier.internal_ss ss; val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); - val solve_tac = FIRST' (map (MetaSimplifier.solver ss) + val solve_tac = FIRST' (map (Raw_Simplifier.solver ss) (rev (if safe then solvers else unsafe_solvers))); fun simp_loop_tac i = @@ -236,15 +239,15 @@ fun simp rew mode ss thm = let - val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss; + val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss ss; val tacf = solve_all_tac (rev unsafe_solvers); fun prover s th = Option.map #1 (Seq.pull (tacf s th)); in rew mode prover ss thm end; in -val simp_thm = simp MetaSimplifier.rewrite_thm; -val simp_cterm = simp MetaSimplifier.rewrite_cterm; +val simp_thm = simp Raw_Simplifier.rewrite_thm; +val simp_cterm = simp Raw_Simplifier.rewrite_cterm; end; @@ -323,7 +326,7 @@ val simplified = conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context => - f ((if null ths then I else MetaSimplifier.clear_ss) + f ((if null ths then I else Raw_Simplifier.clear_ss) (simpset_of (Context.proof_of context)) addsimps ths))); end; @@ -354,14 +357,14 @@ Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add), Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del), Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon - >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] + >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)] @ cong_modifiers; val simp_modifiers' = [Args.add -- Args.colon >> K (I, simp_add), Args.del -- Args.colon >> K (I, simp_del), Args.$$$ onlyN -- Args.colon - >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] + >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)] @ cong_modifiers; val simp_options = diff -r bb28bf635202 -r 4ae674714876 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Sequents/Sequents.thy Fri Dec 17 18:38:33 2010 +0100 @@ -28,9 +28,7 @@ (* concrete syntax *) -nonterminals - seq seqobj seqcont - +nonterminal seq and seqobj and seqcont syntax "_SeqEmp" :: seq ("") diff -r bb28bf635202 -r 4ae674714876 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Tools/Code/code_preproc.ML Fri Dec 17 18:38:33 2010 +0100 @@ -83,10 +83,10 @@ val map_pre = map_pre_post o apfst; val map_post = map_pre_post o apsnd; -val add_unfold = map_pre o MetaSimplifier.add_simp; -val del_unfold = map_pre o MetaSimplifier.del_simp; -val add_post = map_post o MetaSimplifier.add_simp; -val del_post = map_post o MetaSimplifier.del_simp; +val add_unfold = map_pre o Simplifier.add_simp; +val del_unfold = map_pre o Simplifier.del_simp; +val add_post = map_post o Simplifier.add_simp; +val del_post = map_post o Simplifier.del_simp; fun add_unfold_post raw_thm thy = let @@ -94,7 +94,7 @@ val thm_sym = Thm.symmetric thm; in thy |> map_pre_post (fn (pre, post) => - (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym)) + (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym)) end; fun add_functrans (name, f) = (map_data o apsnd) diff -r bb28bf635202 -r 4ae674714876 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Tools/Code/code_simp.ML Fri Dec 17 18:38:33 2010 +0100 @@ -24,7 +24,7 @@ ( type T = simpset; val empty = empty_ss; - fun extend ss = MetaSimplifier.inherit_context empty_ss ss; + fun extend ss = Simplifier.inherit_context empty_ss ss; val merge = merge_ss; ); diff -r bb28bf635202 -r 4ae674714876 src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Tools/atomize_elim.ML Fri Dec 17 18:38:33 2010 +0100 @@ -60,7 +60,7 @@ *) fun atomize_elim_conv ctxt ct = (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt - then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt) + then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt) then_conv (fn ct' => if can Object_Logic.dest_judgment ct' then all_conv ct' else raise CTERM ("atomize_elim", [ct', ct]))) diff -r bb28bf635202 -r 4ae674714876 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Tools/coherent.ML Fri Dec 17 18:38:33 2010 +0100 @@ -45,7 +45,7 @@ if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct))) (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv - MetaSimplifier.rewrite true (map Thm.symmetric + Raw_Simplifier.rewrite true (map Thm.symmetric [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); diff -r bb28bf635202 -r 4ae674714876 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Dec 17 18:32:40 2010 +0100 +++ b/src/Tools/induct.ML Fri Dec 17 18:38:33 2010 +0100 @@ -420,10 +420,10 @@ fun mark_constraints n ctxt = Conv.fconv_rule (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n - (MetaSimplifier.rewrite false [equal_def']))) ctxt)); + (Raw_Simplifier.rewrite false [equal_def']))) ctxt)); val unmark_constraints = Conv.fconv_rule - (MetaSimplifier.rewrite true [Induct_Args.equal_def]); + (Raw_Simplifier.rewrite true [Induct_Args.equal_def]); (* simplify *) @@ -514,10 +514,10 @@ (* atomize *) fun atomize_term thy = - MetaSimplifier.rewrite_term thy Induct_Args.atomize [] + Raw_Simplifier.rewrite_term thy Induct_Args.atomize [] #> Object_Logic.drop_judgment thy; -val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize; +val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize; val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize; @@ -528,8 +528,8 @@ (* rulify *) fun rulify_term thy = - MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> - MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback []; + Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> + Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback []; fun rulified_term thm = let @@ -668,7 +668,7 @@ end); fun miniscope_tac p = CONVERSION o - Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); + Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); in diff -r bb28bf635202 -r 4ae674714876 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/ZF/ZF.thy Fri Dec 17 18:38:33 2010 +0100 @@ -102,7 +102,7 @@ where "A -> B == Pi(A, %_. B)" -nonterminals "is" patterns +nonterminal "is" and patterns syntax "" :: "i => is" ("_") diff -r bb28bf635202 -r 4ae674714876 src/ZF/func.thy --- a/src/ZF/func.thy Fri Dec 17 18:32:40 2010 +0100 +++ b/src/ZF/func.thy Fri Dec 17 18:38:33 2010 +0100 @@ -445,8 +445,7 @@ update :: "[i,i,i] => i" where "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)" -nonterminals - updbinds updbind +nonterminal updbinds and updbind syntax