merged
authorwenzelm
Fri Dec 17 18:33:35 2010 +0100 (2010-12-17)
changeset 412511e6d86821718
parent 41247 c5cb19ecbd41
parent 41250 41f86829e22f
child 41252 4ae674714876
merged
src/HOL/HOL.thy
src/Pure/meta_simplifier.ML
src/Tools/Code/code_simp.ML
     1.1 --- a/NEWS	Fri Dec 17 18:24:44 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 17 18:33:35 2010 +0100
     1.3 @@ -83,6 +83,13 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Command 'type_synonym' (with single argument) replaces somewhat
     1.8 +outdated 'types', which is still available as legacy feature for some
     1.9 +time.
    1.10 +
    1.11 +* Command 'nonterminal' (with 'and' separated list of arguments)
    1.12 +replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.
    1.13 +
    1.14  * Command 'notepad' replaces former 'example_proof' for
    1.15  experimentation in Isar without any result.  INCOMPATIBILITY.
    1.16  
    1.17 @@ -599,6 +606,9 @@
    1.18  
    1.19  *** ML ***
    1.20  
    1.21 +* Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the
    1.22 +main functionality is provided by structure Simplifier.
    1.23 +
    1.24  * Syntax.pretty_priority (default 0) configures the required priority
    1.25  of pretty-printed output and thus affects insertion of parentheses.
    1.26  
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Dec 17 18:24:44 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Dec 17 18:33:35 2010 +0100
     2.3 @@ -723,7 +723,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
     2.9      @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
    2.10      @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
    2.11      @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
    2.12 @@ -731,7 +731,7 @@
    2.13    \end{matharray}
    2.14  
    2.15    \begin{rail}
    2.16 -    'nonterminals' (name +)
    2.17 +    'nonterminal' (name + 'and')
    2.18      ;
    2.19      ('syntax' | 'no_syntax') mode? (constdecl +)
    2.20      ;
    2.21 @@ -746,7 +746,7 @@
    2.22  
    2.23    \begin{description}
    2.24    
    2.25 -  \item @{command "nonterminals"}~@{text c} declares a type
    2.26 +  \item @{command "nonterminal"}~@{text c} declares a type
    2.27    constructor @{text c} (without arguments) to act as purely syntactic
    2.28    type: a nonterminal symbol of the inner syntax.
    2.29  
     3.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 18:24:44 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 18:33:35 2010 +0100
     3.3 @@ -973,13 +973,13 @@
     3.4  
     3.5  text {*
     3.6    \begin{matharray}{rcll}
     3.7 -    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.8 +    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.9      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    3.10      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    3.11    \end{matharray}
    3.12  
    3.13    \begin{rail}
    3.14 -    'types' (typespec '=' type mixfix? +)
    3.15 +    'type_synonym' (typespec '=' type mixfix?)
    3.16      ;
    3.17      'typedecl' typespec mixfix?
    3.18      ;
    3.19 @@ -989,12 +989,12 @@
    3.20  
    3.21    \begin{description}
    3.22  
    3.23 -  \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
    3.24 -  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
    3.25 -  @{text "\<tau>"}.  Unlike actual type definitions, as are available in
    3.26 -  Isabelle/HOL for example, type synonyms are merely syntactic
    3.27 -  abbreviations without any logical significance.  Internally, type
    3.28 -  synonyms are fully expanded.
    3.29 +  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
    3.30 +  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
    3.31 +  existing type @{text "\<tau>"}.  Unlike actual type definitions, as are
    3.32 +  available in Isabelle/HOL for example, type synonyms are merely
    3.33 +  syntactic abbreviations without any logical significance.
    3.34 +  Internally, type synonyms are fully expanded.
    3.35    
    3.36    \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
    3.37    type constructor @{text t}.  If the object-logic defines a base sort
     4.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Dec 17 18:24:44 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Dec 17 18:33:35 2010 +0100
     4.3 @@ -742,7 +742,7 @@
     4.4  %
     4.5  \begin{isamarkuptext}%
     4.6  \begin{matharray}{rcl}
     4.7 -    \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}}} \\
     4.8 +    \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}}} \\
     4.9      \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}}} \\
    4.10      \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}}} \\
    4.11      \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}}} \\
    4.12 @@ -750,7 +750,7 @@
    4.13    \end{matharray}
    4.14  
    4.15    \begin{rail}
    4.16 -    'nonterminals' (name +)
    4.17 +    'nonterminal' (name + 'and')
    4.18      ;
    4.19      ('syntax' | 'no_syntax') mode? (constdecl +)
    4.20      ;
    4.21 @@ -765,7 +765,7 @@
    4.22  
    4.23    \begin{description}
    4.24    
    4.25 -  \item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type
    4.26 +  \item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type
    4.27    constructor \isa{c} (without arguments) to act as purely syntactic
    4.28    type: a nonterminal symbol of the inner syntax.
    4.29  
     5.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 18:24:44 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 18:33:35 2010 +0100
     5.3 @@ -1010,13 +1010,13 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{matharray}{rcll}
     5.7 -    \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}}} \\
     5.8 +    \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}}} \\
     5.9      \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}}} \\
    5.10      \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!) \\
    5.11    \end{matharray}
    5.12  
    5.13    \begin{rail}
    5.14 -    'types' (typespec '=' type mixfix? +)
    5.15 +    'type_synonym' (typespec '=' type mixfix?)
    5.16      ;
    5.17      'typedecl' typespec mixfix?
    5.18      ;
    5.19 @@ -1026,12 +1026,12 @@
    5.20  
    5.21    \begin{description}
    5.22  
    5.23 -  \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
    5.24 -  \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
    5.25 -  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are available in
    5.26 -  Isabelle/HOL for example, type synonyms are merely syntactic
    5.27 -  abbreviations without any logical significance.  Internally, type
    5.28 -  synonyms are fully expanded.
    5.29 +  \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}}}
    5.30 +  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
    5.31 +  existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are
    5.32 +  available in Isabelle/HOL for example, type synonyms are merely
    5.33 +  syntactic abbreviations without any logical significance.
    5.34 +  Internally, type synonyms are fully expanded.
    5.35    
    5.36    \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
    5.37    type constructor \isa{t}.  If the object-logic defines a base sort
     6.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Dec 17 18:24:44 2010 +0100
     6.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Dec 17 18:33:35 2010 +0100
     6.3 @@ -673,7 +673,7 @@
     6.4  %
     6.5  \isatagproof
     6.6  \isacommand{using}\isamarkupfalse%
     6.7 -\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}trace{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
     6.8 +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
     6.9  \isacommand{apply}\isamarkupfalse%
    6.10  \ simp%
    6.11  \endisatagproof
     7.1 --- a/etc/isar-keywords-ZF.el	Fri Dec 17 18:24:44 2010 +0100
     7.2 +++ b/etc/isar-keywords-ZF.el	Fri Dec 17 18:33:35 2010 +0100
     7.3 @@ -103,7 +103,7 @@
     7.4      "no_syntax"
     7.5      "no_translations"
     7.6      "no_type_notation"
     7.7 -    "nonterminals"
     7.8 +    "nonterminal"
     7.9      "notation"
    7.10      "note"
    7.11      "notepad"
    7.12 @@ -189,6 +189,7 @@
    7.13      "txt_raw"
    7.14      "typ"
    7.15      "type_notation"
    7.16 +    "type_synonym"
    7.17      "typed_print_translation"
    7.18      "typedecl"
    7.19      "types"
    7.20 @@ -381,7 +382,7 @@
    7.21      "no_syntax"
    7.22      "no_translations"
    7.23      "no_type_notation"
    7.24 -    "nonterminals"
    7.25 +    "nonterminal"
    7.26      "notation"
    7.27      "notepad"
    7.28      "oracle"
    7.29 @@ -403,6 +404,7 @@
    7.30      "theorems"
    7.31      "translations"
    7.32      "type_notation"
    7.33 +    "type_synonym"
    7.34      "typed_print_translation"
    7.35      "typedecl"
    7.36      "types"
     8.1 --- a/etc/isar-keywords.el	Fri Dec 17 18:24:44 2010 +0100
     8.2 +++ b/etc/isar-keywords.el	Fri Dec 17 18:33:35 2010 +0100
     8.3 @@ -140,7 +140,7 @@
     8.4      "nominal_inductive"
     8.5      "nominal_inductive2"
     8.6      "nominal_primrec"
     8.7 -    "nonterminals"
     8.8 +    "nonterminal"
     8.9      "notation"
    8.10      "note"
    8.11      "notepad"
    8.12 @@ -250,6 +250,7 @@
    8.13      "typ"
    8.14      "type_lifting"
    8.15      "type_notation"
    8.16 +    "type_synonym"
    8.17      "typed_print_translation"
    8.18      "typedecl"
    8.19      "typedef"
    8.20 @@ -487,7 +488,7 @@
    8.21      "no_translations"
    8.22      "no_type_notation"
    8.23      "nominal_datatype"
    8.24 -    "nonterminals"
    8.25 +    "nonterminal"
    8.26      "notation"
    8.27      "notepad"
    8.28      "oracle"
    8.29 @@ -516,6 +517,7 @@
    8.30      "theorems"
    8.31      "translations"
    8.32      "type_notation"
    8.33 +    "type_synonym"
    8.34      "typed_print_translation"
    8.35      "typedecl"
    8.36      "types"
     9.1 --- a/src/Cube/Cube.thy	Fri Dec 17 18:24:44 2010 +0100
     9.2 +++ b/src/Cube/Cube.thy	Fri Dec 17 18:33:35 2010 +0100
     9.3 @@ -14,8 +14,7 @@
     9.4  typedecl "context"
     9.5  typedecl typing
     9.6  
     9.7 -nonterminals
     9.8 -  context' typing'
     9.9 +nonterminal context' and typing'
    9.10  
    9.11  consts
    9.12    Abs :: "[term, term => term] => term"
    10.1 --- a/src/FOL/IFOL.thy	Fri Dec 17 18:24:44 2010 +0100
    10.2 +++ b/src/FOL/IFOL.thy	Fri Dec 17 18:33:35 2010 +0100
    10.3 @@ -754,7 +754,7 @@
    10.4  
    10.5  subsection {* ``Let'' declarations *}
    10.6  
    10.7 -nonterminals letbinds letbind
    10.8 +nonterminal letbinds and letbind
    10.9  
   10.10  definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
   10.11      "Let(s, f) == f(s)"
    11.1 --- a/src/HOL/Decision_Procs/langford_data.ML	Fri Dec 17 18:24:44 2010 +0100
    11.2 +++ b/src/HOL/Decision_Procs/langford_data.ML	Fri Dec 17 18:33:35 2010 +0100
    11.3 @@ -36,11 +36,9 @@
    11.4      Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    11.5        (del_data key #> apsnd (cons (key, entry))));
    11.6  
    11.7 -val add_simp = Thm.declaration_attribute (fn th => fn context => 
    11.8 -  context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) 
    11.9 +val add_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.add_simp);
   11.10  
   11.11 -val del_simp = Thm.declaration_attribute (fn th => fn context => 
   11.12 -  context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) 
   11.13 +val del_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.del_simp);
   11.14  
   11.15  fun match ctxt tm =
   11.16    let
    12.1 --- a/src/HOL/Fun.thy	Fri Dec 17 18:24:44 2010 +0100
    12.2 +++ b/src/HOL/Fun.thy	Fri Dec 17 18:33:35 2010 +0100
    12.3 @@ -558,8 +558,8 @@
    12.4    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
    12.5    "fun_upd f a b == % x. if x=a then b else f x"
    12.6  
    12.7 -nonterminals
    12.8 -  updbinds updbind
    12.9 +nonterminal updbinds and updbind
   12.10 +
   12.11  syntax
   12.12    "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
   12.13    ""         :: "updbind => updbinds"             ("_")
    13.1 --- a/src/HOL/HOL.thy	Fri Dec 17 18:24:44 2010 +0100
    13.2 +++ b/src/HOL/HOL.thy	Fri Dec 17 18:33:35 2010 +0100
    13.3 @@ -103,9 +103,8 @@
    13.4  notation (xsymbols)
    13.5    iff  (infixr "\<longleftrightarrow>" 25)
    13.6  
    13.7 -nonterminals
    13.8 -  letbinds  letbind
    13.9 -  case_syn  cases_syn
   13.10 +nonterminal letbinds and letbind
   13.11 +nonterminal case_syn and cases_syn
   13.12  
   13.13  syntax
   13.14    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    14.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Dec 17 18:24:44 2010 +0100
    14.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Dec 17 18:33:35 2010 +0100
    14.3 @@ -170,7 +170,7 @@
    14.4      val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef
    14.5      val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef
    14.6      val type_definition_thm =
    14.7 -      MetaSimplifier.rewrite_rule
    14.8 +      Raw_Simplifier.rewrite_rule
    14.9          (the_list (#set_def (#2 info)))
   14.10          (#type_definition (#2 info))
   14.11      val typedef_thms =
    15.1 --- a/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 18:24:44 2010 +0100
    15.2 +++ b/src/HOL/HOLCF/ex/Letrec.thy	Fri Dec 17 18:33:35 2010 +0100
    15.3 @@ -14,8 +14,7 @@
    15.4    CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
    15.5    "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
    15.6  
    15.7 -nonterminals
    15.8 -  recbinds recbindt recbind
    15.9 +nonterminal recbinds and recbindt and recbind
   15.10  
   15.11  syntax
   15.12    "_recbind"  :: "['a, 'a] \<Rightarrow> recbind"               ("(2_ =/ _)" 10)
    16.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 17 18:24:44 2010 +0100
    16.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 17 18:33:35 2010 +0100
    16.3 @@ -100,8 +100,7 @@
    16.4  
    16.5  subsection {* Case syntax *}
    16.6  
    16.7 -nonterminals
    16.8 -  Case_syn  Cases_syn
    16.9 +nonterminal Case_syn and Cases_syn
   16.10  
   16.11  syntax
   16.12    "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
    17.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 18:24:44 2010 +0100
    17.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Dec 17 18:33:35 2010 +0100
    17.3 @@ -56,8 +56,7 @@
    17.4    "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
    17.5    "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
    17.6   
    17.7 -nonterminals
    17.8 -  prgs
    17.9 +nonterminal prgs
   17.10  
   17.11  syntax
   17.12    "_PAR" :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" [57] 56)
    18.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 18:24:44 2010 +0100
    18.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Dec 17 18:33:35 2010 +0100
    18.3 @@ -27,8 +27,7 @@
    18.4    "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
    18.5    "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
    18.6  
    18.7 -nonterminals
    18.8 -  prgs
    18.9 +nonterminal prgs
   18.10  
   18.11  syntax
   18.12    "_PAR"        :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" 60)
    19.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 18:24:44 2010 +0100
    19.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 18:33:35 2010 +0100
    19.3 @@ -37,8 +37,7 @@
    19.4  notation (latex output)
    19.5    bind_do (infixr "\<bind>" 54)
    19.6  
    19.7 -nonterminals
    19.8 -  do_binds do_bind
    19.9 +nonterminal do_binds and do_bind
   19.10  
   19.11  syntax
   19.12    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    20.1 --- a/src/HOL/Library/State_Monad.thy	Fri Dec 17 18:24:44 2010 +0100
    20.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Dec 17 18:33:35 2010 +0100
    20.3 @@ -114,8 +114,7 @@
    20.4  
    20.5  subsection {* Do-syntax *}
    20.6  
    20.7 -nonterminals
    20.8 -  sdo_binds sdo_bind
    20.9 +nonterminal sdo_binds and sdo_bind
   20.10  
   20.11  syntax
   20.12    "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
    21.1 --- a/src/HOL/List.thy	Fri Dec 17 18:24:44 2010 +0100
    21.2 +++ b/src/HOL/List.thy	Fri Dec 17 18:33:35 2010 +0100
    21.3 @@ -123,7 +123,7 @@
    21.4      "list_update [] i v = []"
    21.5    | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
    21.6  
    21.7 -nonterminals lupdbinds lupdbind
    21.8 +nonterminal lupdbinds and lupdbind
    21.9  
   21.10  syntax
   21.11    "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   21.12 @@ -346,7 +346,7 @@
   21.13  @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   21.14  *)
   21.15  
   21.16 -nonterminals lc_qual lc_quals
   21.17 +nonterminal lc_qual and lc_quals
   21.18  
   21.19  syntax
   21.20  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    22.1 --- a/src/HOL/Map.thy	Fri Dec 17 18:24:44 2010 +0100
    22.2 +++ b/src/HOL/Map.thy	Fri Dec 17 18:33:35 2010 +0100
    22.3 @@ -50,8 +50,7 @@
    22.4    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
    22.5    "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
    22.6  
    22.7 -nonterminals
    22.8 -  maplets maplet
    22.9 +nonterminal maplets and maplet
   22.10  
   22.11  syntax
   22.12    "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    23.1 --- a/src/HOL/NSA/transfer.ML	Fri Dec 17 18:24:44 2010 +0100
    23.2 +++ b/src/HOL/NSA/transfer.ML	Fri Dec 17 18:33:35 2010 +0100
    23.3 @@ -58,7 +58,7 @@
    23.4      val meta = Local_Defs.meta_rewrite_rule ctxt;
    23.5      val ths' = map meta ths;
    23.6      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    23.7 -    val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
    23.8 +    val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
    23.9      val u = unstar_term consts t'
   23.10      val tac =
   23.11        rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
    24.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Dec 17 18:24:44 2010 +0100
    24.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Dec 17 18:33:35 2010 +0100
    24.3 @@ -19,10 +19,10 @@
    24.4  val inductive_atomize = @{thms induct_atomize};
    24.5  val inductive_rulify = @{thms induct_rulify};
    24.6  
    24.7 -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
    24.8 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
    24.9  
   24.10  val atomize_conv =
   24.11 -  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
   24.12 +  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
   24.13      (HOL_basic_ss addsimps inductive_atomize);
   24.14  val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
   24.15  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
    25.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Dec 17 18:24:44 2010 +0100
    25.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Dec 17 18:33:35 2010 +0100
    25.3 @@ -20,10 +20,10 @@
    25.4  val inductive_atomize = @{thms induct_atomize};
    25.5  val inductive_rulify = @{thms induct_rulify};
    25.6  
    25.7 -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
    25.8 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
    25.9  
   25.10  val atomize_conv =
   25.11 -  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
   25.12 +  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
   25.13      (HOL_basic_ss addsimps inductive_atomize);
   25.14  val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
   25.15  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
    26.1 --- a/src/HOL/Product_Type.thy	Fri Dec 17 18:24:44 2010 +0100
    26.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 17 18:33:35 2010 +0100
    26.3 @@ -173,8 +173,7 @@
    26.4    abstractions.
    26.5  *}
    26.6  
    26.7 -nonterminals
    26.8 -  tuple_args patterns
    26.9 +nonterminal tuple_args and patterns
   26.10  
   26.11  syntax
   26.12    "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
    27.1 --- a/src/HOL/Record.thy	Fri Dec 17 18:24:44 2010 +0100
    27.2 +++ b/src/HOL/Record.thy	Fri Dec 17 18:33:35 2010 +0100
    27.3 @@ -419,8 +419,15 @@
    27.4  
    27.5  subsection {* Concrete record syntax *}
    27.6  
    27.7 -nonterminals
    27.8 -  ident field_type field_types field fields field_update field_updates
    27.9 +nonterminal
   27.10 +  ident and
   27.11 +  field_type and
   27.12 +  field_types and
   27.13 +  field and
   27.14 +  fields and
   27.15 +  field_update and
   27.16 +  field_updates
   27.17 +
   27.18  syntax
   27.19    "_constify"           :: "id => ident"                        ("_")
   27.20    "_constify"           :: "longid => ident"                    ("_")
    28.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Dec 17 18:24:44 2010 +0100
    28.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Dec 17 18:33:35 2010 +0100
    28.3 @@ -141,8 +141,7 @@
    28.4                      (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
    28.5            val ctxt = Simplifier.the_context ss;
    28.6            val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
    28.7 -          val ss' = Simplifier.context 
    28.8 -                     (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss;
    28.9 +          val ss' = Simplifier.context (Config.put simp_depth_limit 100 ctxt) basic_ss;
   28.10            val thm = Simplifier.rewrite ss' ct;
   28.11          in if (op aconv) (Logic.dest_equals (prop_of thm))
   28.12             then NONE
   28.13 @@ -232,8 +231,7 @@
   28.14                        end
   28.15                 | mk_updterm _ t = init_seed t;
   28.16  
   28.17 -             val ctxt = Simplifier.the_context ss |>
   28.18 -                        Config.put MetaSimplifier.simp_depth_limit 100;
   28.19 +             val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
   28.20               val ss1 = Simplifier.context ctxt ss';
   28.21               val ss2 = Simplifier.context ctxt 
   28.22                           (#1 (StateFunData.get (Context.Proof ctxt)));
   28.23 @@ -266,8 +264,7 @@
   28.24    Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
   28.25      (fn thy => fn ss => fn t =>
   28.26         let
   28.27 -         val ctxt = Simplifier.the_context ss |>
   28.28 -                    Config.put MetaSimplifier.simp_depth_limit 100
   28.29 +         val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
   28.30           val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
   28.31           val ss' = (Simplifier.context ctxt ex_lookup_ss);
   28.32           fun prove prop =
    29.1 --- a/src/HOL/TLA/Intensional.thy	Fri Dec 17 18:24:44 2010 +0100
    29.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Dec 17 18:33:35 2010 +0100
    29.3 @@ -33,9 +33,7 @@
    29.4  
    29.5  (** concrete syntax **)
    29.6  
    29.7 -nonterminals
    29.8 -  lift
    29.9 -  liftargs
   29.10 +nonterminal lift and liftargs
   29.11  
   29.12  syntax
   29.13    ""            :: "id => lift"                          ("_")
    30.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 17 18:24:44 2010 +0100
    30.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 17 18:33:35 2010 +0100
    30.3 @@ -52,7 +52,7 @@
    30.4    in
    30.5      thms
    30.6      |> Conjunction.intr_balanced
    30.7 -    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
    30.8 +    |> Raw_Simplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
    30.9      |> Thm.implies_intr asm
   30.10      |> Thm.generalize ([], params) 0
   30.11      |> AxClass.unoverload thy
    31.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 18:24:44 2010 +0100
    31.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 18:33:35 2010 +0100
    31.3 @@ -39,12 +39,12 @@
    31.4    branches: scheme_branch list,
    31.5    cases: scheme_case list}
    31.6  
    31.7 -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
    31.8 -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
    31.9 +val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
   31.10 +val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
   31.11  
   31.12  fun meta thm = thm RS eq_reflection
   31.13  
   31.14 -val sum_prod_conv = MetaSimplifier.rewrite true
   31.15 +val sum_prod_conv = Raw_Simplifier.rewrite true
   31.16    (map meta (@{thm split_conv} :: @{thms sum.cases}))
   31.17  
   31.18  fun term_conv thy cv t =
   31.19 @@ -312,7 +312,7 @@
   31.20  
   31.21          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   31.22            |> Goal.init
   31.23 -          |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   31.24 +          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   31.25                THEN CONVERSION ind_rulify 1)
   31.26            |> Seq.hd
   31.27            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
    32.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 17 18:24:44 2010 +0100
    32.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 17 18:33:35 2010 +0100
    32.3 @@ -297,7 +297,7 @@
    32.4          else Conv.all_conv
    32.5        | _ => Conv.all_conv)
    32.6  
    32.7 -fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
    32.8 +fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths
    32.9  
   32.10  val cheat_choice =
   32.11    @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
    33.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 18:24:44 2010 +0100
    33.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 18:33:35 2010 +0100
    33.3 @@ -219,9 +219,9 @@
    33.4          fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
    33.5            |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
    33.6          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
    33.7 -        val case_th = MetaSimplifier.simplify true
    33.8 +        val case_th = Raw_Simplifier.simplify true
    33.9            (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
   33.10 -        val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
   33.11 +        val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems
   33.12          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
   33.13          val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
   33.14            OF (replicate nargs @{thm refl})
   33.15 @@ -237,7 +237,7 @@
   33.16        (PEEK nprems_of
   33.17          (fn n =>
   33.18            ALLGOALS (fn i =>
   33.19 -            MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
   33.20 +            Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
   33.21              THEN (SUBPROOF (instantiate i n) ctxt i))))
   33.22    in
   33.23      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
    34.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 18:24:44 2010 +0100
    34.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 18:33:35 2010 +0100
    34.3 @@ -969,7 +969,7 @@
    34.4      val Tcons = datatype_names_of_case_name thy case_name
    34.5      val ths = maps (instantiated_case_rewrites thy) Tcons
    34.6    in
    34.7 -    MetaSimplifier.rewrite_term thy
    34.8 +    Raw_Simplifier.rewrite_term thy
    34.9        (map (fn th => th RS @{thm eq_reflection}) ths) [] t
   34.10    end
   34.11  
   34.12 @@ -1044,7 +1044,7 @@
   34.13  fun peephole_optimisation thy intro =
   34.14    let
   34.15      val process =
   34.16 -      MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
   34.17 +      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
   34.18      fun process_False intro_t =
   34.19        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
   34.20      fun process_True intro_t =
    35.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 18:24:44 2010 +0100
    35.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 18:33:35 2010 +0100
    35.3 @@ -96,7 +96,7 @@
    35.4        (Const (@{const_name If}, _)) =>
    35.5          let
    35.6            val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
    35.7 -          val atom' = MetaSimplifier.rewrite_term thy
    35.8 +          val atom' = Raw_Simplifier.rewrite_term thy
    35.9              (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
   35.10            val _ = assert (not (atom = atom'))
   35.11          in
   35.12 @@ -212,7 +212,7 @@
   35.13            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   35.14              ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   35.15        val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
   35.16 -      val intros = map (MetaSimplifier.rewrite_rule
   35.17 +      val intros = map (Raw_Simplifier.rewrite_rule
   35.18            [if_beta RS @{thm eq_reflection}]) intros
   35.19        val _ = print_specs options thy "normalized intros" intros
   35.20        (*val intros = maps (split_cases thy) intros*)
    36.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 18:24:44 2010 +0100
    36.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 18:33:35 2010 +0100
    36.3 @@ -83,7 +83,7 @@
    36.4          let
    36.5            val prems' = maps dest_conjunct_prem (take nargs prems)
    36.6          in
    36.7 -          MetaSimplifier.rewrite_goal_tac
    36.8 +          Simplifier.rewrite_goal_tac
    36.9              (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   36.10          end) ctxt 1
   36.11      | Abs _ => raise Fail "prove_param: No valid parameter term"
   36.12 @@ -127,7 +127,7 @@
   36.13            fun param_rewrite prem =
   36.14              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
   36.15            val SOME rew_eq = find_first param_rewrite prems'
   36.16 -          val param_prem' = MetaSimplifier.rewrite_rule
   36.17 +          val param_prem' = Raw_Simplifier.rewrite_rule
   36.18              (map (fn th => th RS @{thm eq_reflection})
   36.19                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   36.20              param_prem
   36.21 @@ -184,7 +184,7 @@
   36.22                  let
   36.23                    val prems' = maps dest_conjunct_prem (take nargs prems)
   36.24                  in
   36.25 -                  MetaSimplifier.rewrite_goal_tac
   36.26 +                  Simplifier.rewrite_goal_tac
   36.27                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   36.28                  end
   36.29               THEN REPEAT_DETERM (rtac @{thm refl} 1))
   36.30 @@ -225,7 +225,7 @@
   36.31                let
   36.32                  val prems' = maps dest_conjunct_prem (take nargs prems)
   36.33                in
   36.34 -                MetaSimplifier.rewrite_goal_tac
   36.35 +                Simplifier.rewrite_goal_tac
   36.36                    (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   36.37                end) ctxt 1
   36.38        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
    37.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Dec 17 18:24:44 2010 +0100
    37.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Dec 17 18:33:35 2010 +0100
    37.3 @@ -486,7 +486,7 @@
    37.4          val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
    37.5          val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
    37.6          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
    37.7 -        val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    37.8 +        val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    37.9          val (insp, inst) =
   37.10            if ty_c = ty_d
   37.11            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
    38.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 18:24:44 2010 +0100
    38.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 18:33:35 2010 +0100
    38.3 @@ -589,7 +589,7 @@
    38.4    type T = extra_norm U.dict
    38.5    val empty = []
    38.6    val extend = I
    38.7 -  fun merge xx = U.dict_merge fst xx
    38.8 +  fun merge data = U.dict_merge fst data
    38.9  )
   38.10  
   38.11  fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
    39.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 18:24:44 2010 +0100
    39.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 18:33:35 2010 +0100
    39.3 @@ -567,7 +567,7 @@
    39.4    type T = (Proof.context -> config) U.dict
    39.5    val empty = []
    39.6    val extend = I
    39.7 -  fun merge xx = U.dict_merge fst xx
    39.8 +  fun merge data = U.dict_merge fst data
    39.9  )
   39.10  
   39.11  fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
    40.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Fri Dec 17 18:24:44 2010 +0100
    40.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Dec 17 18:33:35 2010 +0100
    40.3 @@ -73,8 +73,8 @@
    40.4  functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    40.5  struct
    40.6  
    40.7 -val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
    40.8 -val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
    40.9 +val rulify_goals = Raw_Simplifier.rewrite_goals_rule Data.rulify;
   40.10 +val atomize_goals = Raw_Simplifier.rewrite_goals_rule Data.atomize;
   40.11  
   40.12  (* beta-eta contract the theorem *)
   40.13  fun beta_eta_contract thm =
    41.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 18:24:44 2010 +0100
    41.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 18:33:35 2010 +0100
    41.3 @@ -422,7 +422,7 @@
    41.4  fun SUBS thl =
    41.5    rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
    41.6  
    41.7 -val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));
    41.8 +val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
    41.9  
   41.10  fun simpl_conv ss thl ctm =
   41.11   rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
   41.12 @@ -669,7 +669,7 @@
   41.13                       val eq = Logic.strip_imp_concl imp
   41.14                       val lhs = tych(get_lhs eq)
   41.15                       val ss' = Simplifier.add_prems (map ASSUME ants) ss
   41.16 -                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   41.17 +                     val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   41.18                         handle Utils.ERR _ => Thm.reflexive lhs
   41.19                       val dummy = print_thms "proven:" [lhs_eq_lhs1]
   41.20                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   41.21 @@ -690,7 +690,7 @@
   41.22                    val QeqQ1 = pbeta_reduce (tych Q)
   41.23                    val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
   41.24                    val ss' = Simplifier.add_prems (map ASSUME ants1) ss
   41.25 -                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   41.26 +                  val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   41.27                                  handle Utils.ERR _ => Thm.reflexive Q1
   41.28                    val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
   41.29                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   41.30 @@ -714,8 +714,8 @@
   41.31                   else
   41.32                   let val tych = cterm_of thy
   41.33                       val ants1 = map tych ants
   41.34 -                     val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
   41.35 -                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   41.36 +                     val ss' = Simplifier.add_prems (map ASSUME ants1) ss
   41.37 +                     val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
   41.38                          (false,true,false) (prover used') ss' (tych Q)
   41.39                        handle Utils.ERR _ => Thm.reflexive (tych Q)
   41.40                       val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   41.41 @@ -783,7 +783,7 @@
   41.42      end
   41.43      val ctm = cprop_of th
   41.44      val names = OldTerm.add_term_names (term_of ctm, [])
   41.45 -    val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   41.46 +    val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
   41.47        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   41.48      val th2 = Thm.equal_elim th1 th
   41.49   in
    42.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 17 18:24:44 2010 +0100
    42.2 +++ b/src/HOL/Tools/inductive.ML	Fri Dec 17 18:33:35 2010 +0100
    42.3 @@ -282,7 +282,7 @@
    42.4  
    42.5  val bad_app = "Inductive predicate must be applied to parameter(s) ";
    42.6  
    42.7 -fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
    42.8 +fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
    42.9  
   42.10  in
   42.11  
    43.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Dec 17 18:24:44 2010 +0100
    43.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Dec 17 18:33:35 2010 +0100
    43.3 @@ -807,7 +807,7 @@
    43.4    add_discrete_type @{type_name nat};
    43.5  
    43.6  fun add_arith_facts ss =
    43.7 -  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
    43.8 +  Simplifier.add_prems (Arith_Data.get_arith_facts (Simplifier.the_context ss)) ss;
    43.9  
   43.10  val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
   43.11  
    44.1 --- a/src/HOL/ex/Numeral.thy	Fri Dec 17 18:24:44 2010 +0100
    44.2 +++ b/src/HOL/ex/Numeral.thy	Fri Dec 17 18:33:35 2010 +0100
    44.3 @@ -592,14 +592,14 @@
    44.4      fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
    44.5      fun attach_num ct = (dest_num (Thm.term_of ct), ct);
    44.6      fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
    44.7 -    val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
    44.8 +    val simplify = Raw_Simplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
    44.9      fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq}
   44.10        OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
   44.11          [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
   44.12    in fn phi => fn _ => fn ct => case try cdifference ct
   44.13     of NONE => (NONE)
   44.14      | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
   44.15 -        then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
   44.16 +        then Raw_Simplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
   44.17          else mk_meta_eq (let
   44.18            val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));
   44.19          in
    45.1 --- a/src/Pure/IsaMakefile	Fri Dec 17 18:24:44 2010 +0100
    45.2 +++ b/src/Pure/IsaMakefile	Fri Dec 17 18:33:35 2010 +0100
    45.3 @@ -227,7 +227,6 @@
    45.4    item_net.ML						\
    45.5    library.ML						\
    45.6    logic.ML						\
    45.7 -  meta_simplifier.ML					\
    45.8    more_thm.ML						\
    45.9    morphism.ML						\
   45.10    name.ML						\
   45.11 @@ -238,6 +237,7 @@
   45.12    proofterm.ML						\
   45.13    pure_setup.ML						\
   45.14    pure_thy.ML						\
   45.15 +  raw_simplifier.ML					\
   45.16    search.ML						\
   45.17    sign.ML						\
   45.18    simplifier.ML						\
    46.1 --- a/src/Pure/Isar/attrib.ML	Fri Dec 17 18:24:44 2010 +0100
    46.2 +++ b/src/Pure/Isar/attrib.ML	Fri Dec 17 18:33:35 2010 +0100
    46.3 @@ -415,9 +415,9 @@
    46.4    register_config Unify.search_bound_raw #>
    46.5    register_config Unify.trace_simp_raw #>
    46.6    register_config Unify.trace_types_raw #>
    46.7 -  register_config MetaSimplifier.simp_depth_limit_raw #>
    46.8 -  register_config MetaSimplifier.simp_trace_depth_limit_raw #>
    46.9 -  register_config MetaSimplifier.simp_debug_raw #>
   46.10 -  register_config MetaSimplifier.simp_trace_raw));
   46.11 +  register_config Raw_Simplifier.simp_depth_limit_raw #>
   46.12 +  register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
   46.13 +  register_config Raw_Simplifier.simp_debug_raw #>
   46.14 +  register_config Raw_Simplifier.simp_trace_raw));
   46.15  
   46.16  end;
    47.1 --- a/src/Pure/Isar/element.ML	Fri Dec 17 18:24:44 2010 +0100
    47.2 +++ b/src/Pure/Isar/element.ML	Fri Dec 17 18:33:35 2010 +0100
    47.3 @@ -224,7 +224,7 @@
    47.4      val thy = ProofContext.theory_of ctxt;
    47.5      val cert = Thm.cterm_of thy;
    47.6  
    47.7 -    val th = MetaSimplifier.norm_hhf raw_th;
    47.8 +    val th = Raw_Simplifier.norm_hhf raw_th;
    47.9      val is_elim = Object_Logic.is_elim th;
   47.10  
   47.11      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
   47.12 @@ -318,7 +318,7 @@
   47.13    end;
   47.14  
   47.15  fun conclude_witness (Witness (_, th)) =
   47.16 -  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
   47.17 +  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
   47.18  
   47.19  fun pretty_witness ctxt witn =
   47.20    let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
   47.21 @@ -459,8 +459,8 @@
   47.22  fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
   47.23   {binding = I,
   47.24    typ = I,
   47.25 -  term = MetaSimplifier.rewrite_term thy thms [],
   47.26 -  fact = map (MetaSimplifier.rewrite_rule thms)});
   47.27 +  term = Raw_Simplifier.rewrite_term thy thms [],
   47.28 +  fact = map (Raw_Simplifier.rewrite_rule thms)});
   47.29  
   47.30  
   47.31  (* transfer to theory using closure *)
    48.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 17 18:24:44 2010 +0100
    48.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 17 18:33:35 2010 +0100
    48.3 @@ -647,18 +647,18 @@
    48.4      val cert = Thm.cterm_of defs_thy;
    48.5  
    48.6      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    48.7 -      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
    48.8 +      rewrite_goals_tac [pred_def] THEN
    48.9        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   48.10        Tactic.compose_tac (false,
   48.11          Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   48.12  
   48.13      val conjuncts =
   48.14        (Drule.equal_elim_rule2 OF [body_eq,
   48.15 -        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   48.16 +        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   48.17        |> Conjunction.elim_balanced (length ts);
   48.18      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   48.19        Element.prove_witness defs_ctxt t
   48.20 -       (MetaSimplifier.rewrite_goals_tac defs THEN
   48.21 +       (rewrite_goals_tac defs THEN
   48.22          Tactic.compose_tac (false, ax, 0) 1));
   48.23    in ((statement, intro, axioms), defs_thy) end;
   48.24  
    49.1 --- a/src/Pure/Isar/generic_target.ML	Fri Dec 17 18:24:44 2010 +0100
    49.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Dec 17 18:33:35 2010 +0100
    49.3 @@ -58,7 +58,7 @@
    49.4      (*term and type parameters*)
    49.5      val crhs = Thm.cterm_of thy rhs;
    49.6      val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
    49.7 -    val rhs_conv = MetaSimplifier.rewrite true defs crhs;
    49.8 +    val rhs_conv = Raw_Simplifier.rewrite true defs crhs;
    49.9  
   49.10      val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
   49.11      val T = Term.fastype_of rhs;
   49.12 @@ -107,7 +107,7 @@
   49.13      (*export assumes/defines*)
   49.14      val th = Goal.norm_result raw_th;
   49.15      val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
   49.16 -    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume)
   49.17 +    val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
   49.18        (Assumption.all_assms_of ctxt);
   49.19      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
   49.20  
    50.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 17 18:24:44 2010 +0100
    50.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 17 18:33:35 2010 +0100
    50.3 @@ -111,16 +111,24 @@
    50.4      (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
    50.5        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
    50.6  
    50.7 +val type_abbrev =
    50.8 +  Parse.type_args -- Parse.binding --
    50.9 +    (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'));
   50.10 +
   50.11  val _ =
   50.12    Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
   50.13 -    (Scan.repeat1
   50.14 -      (Parse.type_args -- Parse.binding --
   50.15 -        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
   50.16 -      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
   50.17 +    (Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
   50.18 +     (legacy_feature "Old 'types' commands -- use 'type_synonym' instead";
   50.19 +      fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
   50.20  
   50.21  val _ =
   50.22 -  Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   50.23 -    Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
   50.24 +  Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
   50.25 +    (type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   50.26 +
   50.27 +val _ =
   50.28 +  Outer_Syntax.command "nonterminal"
   50.29 +    "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
   50.30 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
   50.31  
   50.32  val _ =
   50.33    Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
    51.1 --- a/src/Pure/Isar/local_defs.ML	Fri Dec 17 18:24:44 2010 +0100
    51.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Dec 17 18:33:35 2010 +0100
    51.3 @@ -182,7 +182,7 @@
    51.4  end;
    51.5  
    51.6  fun contract ctxt defs ct th =
    51.7 -  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
    51.8 +  trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)];
    51.9  
   51.10  
   51.11  (** defived definitions **)
   51.12 @@ -208,8 +208,8 @@
   51.13  (* meta rewrite rules *)
   51.14  
   51.15  fun meta_rewrite_conv ctxt =
   51.16 -  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
   51.17 -    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
   51.18 +  Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
   51.19 +    (Raw_Simplifier.context ctxt empty_ss
   51.20        addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
   51.21        addsimps (Rules.get (Context.Proof ctxt)));
   51.22  
   51.23 @@ -220,11 +220,11 @@
   51.24  
   51.25  fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
   51.26  
   51.27 -val unfold       = meta MetaSimplifier.rewrite_rule;
   51.28 -val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
   51.29 -val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
   51.30 -val fold         = meta MetaSimplifier.fold_rule;
   51.31 -val fold_tac     = meta MetaSimplifier.fold_goals_tac;
   51.32 +val unfold       = meta Raw_Simplifier.rewrite_rule;
   51.33 +val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
   51.34 +val unfold_tac   = meta Raw_Simplifier.rewrite_goals_tac;
   51.35 +val fold         = meta Raw_Simplifier.fold_rule;
   51.36 +val fold_tac     = meta Raw_Simplifier.fold_goals_tac;
   51.37  
   51.38  
   51.39  (* derived defs -- potentially within the object-logic *)
   51.40 @@ -244,7 +244,7 @@
   51.41        in
   51.42          Goal.prove ctxt' frees [] prop (K (ALLGOALS
   51.43            (CONVERSION (meta_rewrite_conv ctxt') THEN'
   51.44 -            MetaSimplifier.rewrite_goal_tac [def] THEN'
   51.45 +            rewrite_goal_tac [def] THEN'
   51.46              resolve_tac [Drule.reflexive_thm])))
   51.47          handle ERROR msg => cat_error msg "Failed to prove definitional specification"
   51.48        end;
    52.1 --- a/src/Pure/Isar/object_logic.ML	Fri Dec 17 18:24:44 2010 +0100
    52.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Dec 17 18:33:35 2010 +0100
    52.3 @@ -178,10 +178,10 @@
    52.4  (* atomize *)
    52.5  
    52.6  fun atomize_term thy =
    52.7 -  drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
    52.8 +  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
    52.9  
   52.10  fun atomize ct =
   52.11 -  MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   52.12 +  Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   52.13  
   52.14  fun atomize_prems ct =
   52.15    if Logic.has_meta_prems (Thm.term_of ct) then
   52.16 @@ -195,11 +195,11 @@
   52.17  
   52.18  (* rulify *)
   52.19  
   52.20 -fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
   52.21 -fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   52.22 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
   52.23 +fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   52.24  
   52.25  fun gen_rulify full thm =
   52.26 -  MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   52.27 +  Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   52.28    |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
   52.29  
   52.30  val rulify = gen_rulify true;
    53.1 --- a/src/Pure/Isar/obtain.ML	Fri Dec 17 18:24:44 2010 +0100
    53.2 +++ b/src/Pure/Isar/obtain.ML	Fri Dec 17 18:33:35 2010 +0100
    53.3 @@ -193,7 +193,7 @@
    53.4      val rule =
    53.5        (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
    53.6          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
    53.7 -      | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
    53.8 +      | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
    53.9  
   53.10      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
   53.11      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
   53.12 @@ -299,7 +299,7 @@
   53.13      val goal = Var (("guess", 0), propT);
   53.14      fun print_result ctxt' (k, [(s, [_, th])]) =
   53.15        Proof_Display.print_results int ctxt' (k, [(s, [th])]);
   53.16 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
   53.17 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
   53.18          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   53.19      fun after_qed [[_, res]] =
   53.20        Proof.end_block #> guess_context (check_result ctxt thesis res);
    54.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Dec 17 18:24:44 2010 +0100
    54.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Dec 17 18:33:35 2010 +0100
    54.3 @@ -189,14 +189,14 @@
    54.4  
    54.5  fun unfold_prems n defs th =
    54.6    if null defs then th
    54.7 -  else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.rewrite true defs)) th;
    54.8 +  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
    54.9  
   54.10  fun unfold_prems_concls defs th =
   54.11    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   54.12    else
   54.13      Conv.fconv_rule
   54.14        (Conv.concl_conv ~1 (Conjunction.convs
   54.15 -        (Conv.prems_conv ~1 (MetaSimplifier.rewrite true defs)))) th;
   54.16 +        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
   54.17  
   54.18  in
   54.19  
    55.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Dec 17 18:24:44 2010 +0100
    55.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Dec 17 18:33:35 2010 +0100
    55.3 @@ -147,10 +147,10 @@
    55.4      "Show leading question mark of variable name"];
    55.5  
    55.6  val tracing_preferences =
    55.7 - [bool_pref simp_trace_default
    55.8 + [bool_pref Raw_Simplifier.simp_trace_default
    55.9      "trace-simplifier"
   55.10      "Trace simplification rules.",
   55.11 -  nat_pref simp_trace_depth_limit_default
   55.12 +  nat_pref Raw_Simplifier.simp_trace_depth_limit_default
   55.13      "trace-simplifier-depth"
   55.14      "Trace simplifier depth limit.",
   55.15    bool_pref trace_rules
    56.1 --- a/src/Pure/ROOT.ML	Fri Dec 17 18:24:44 2010 +0100
    56.2 +++ b/src/Pure/ROOT.ML	Fri Dec 17 18:33:35 2010 +0100
    56.3 @@ -153,7 +153,7 @@
    56.4  use "tactical.ML";
    56.5  use "search.ML";
    56.6  use "tactic.ML";
    56.7 -use "meta_simplifier.ML";
    56.8 +use "raw_simplifier.ML";
    56.9  use "conjunction.ML";
   56.10  use "assumption.ML";
   56.11  use "display.ML";
    57.1 --- a/src/Pure/assumption.ML	Fri Dec 17 18:24:44 2010 +0100
    57.2 +++ b/src/Pure/assumption.ML	Fri Dec 17 18:33:35 2010 +0100
    57.3 @@ -48,7 +48,7 @@
    57.4  *)
    57.5  fun presume_export _ = assume_export false;
    57.6  
    57.7 -val assume = MetaSimplifier.norm_hhf o Thm.assume;
    57.8 +val assume = Raw_Simplifier.norm_hhf o Thm.assume;
    57.9  
   57.10  
   57.11  
   57.12 @@ -110,9 +110,9 @@
   57.13  (* export *)
   57.14  
   57.15  fun export is_goal inner outer =
   57.16 -  MetaSimplifier.norm_hhf_protect #>
   57.17 +  Raw_Simplifier.norm_hhf_protect #>
   57.18    fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
   57.19 -  MetaSimplifier.norm_hhf_protect;
   57.20 +  Raw_Simplifier.norm_hhf_protect;
   57.21  
   57.22  fun export_term inner outer =
   57.23    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
    58.1 --- a/src/Pure/axclass.ML	Fri Dec 17 18:24:44 2010 +0100
    58.2 +++ b/src/Pure/axclass.ML	Fri Dec 17 18:33:35 2010 +0100
    58.3 @@ -322,11 +322,11 @@
    58.4  
    58.5  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    58.6  
    58.7 -fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    58.8 -fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    58.9 +fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
   58.10 +fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
   58.11  
   58.12 -fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   58.13 -fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   58.14 +fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
   58.15 +fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   58.16  
   58.17  fun lookup_inst_param consts params (c, T) =
   58.18    (case get_inst_tyco consts (c, T) of
    59.1 --- a/src/Pure/codegen.ML	Fri Dec 17 18:24:44 2010 +0100
    59.2 +++ b/src/Pure/codegen.ML	Fri Dec 17 18:33:35 2010 +0100
    59.3 @@ -293,8 +293,8 @@
    59.4  );
    59.5  
    59.6  val map_unfold = UnfoldData.map;
    59.7 -val add_unfold = map_unfold o MetaSimplifier.add_simp;
    59.8 -val del_unfold = map_unfold o MetaSimplifier.del_simp;
    59.9 +val add_unfold = map_unfold o Simplifier.add_simp;
   59.10 +val del_unfold = map_unfold o Simplifier.del_simp;
   59.11  
   59.12  fun unfold_preprocessor thy =
   59.13    let val ss = Simplifier.global_context thy (UnfoldData.get thy)
    60.1 --- a/src/Pure/goal.ML	Fri Dec 17 18:24:44 2010 +0100
    60.2 +++ b/src/Pure/goal.ML	Fri Dec 17 18:33:35 2010 +0100
    60.3 @@ -99,7 +99,7 @@
    60.4  
    60.5  val norm_result =
    60.6    Drule.flexflex_unique
    60.7 -  #> MetaSimplifier.norm_hhf_protect
    60.8 +  #> Raw_Simplifier.norm_hhf_protect
    60.9    #> Thm.strip_shyps
   60.10    #> Drule.zero_var_indexes;
   60.11  
   60.12 @@ -278,7 +278,7 @@
   60.13    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   60.14    THEN' SUBGOAL (fn (t, i) =>
   60.15      if Drule.is_norm_hhf t then all_tac
   60.16 -    else MetaSimplifier.rewrite_goal_tac Drule.norm_hhf_eqs i);
   60.17 +    else rewrite_goal_tac Drule.norm_hhf_eqs i);
   60.18  
   60.19  fun compose_hhf_tac th i st =
   60.20    PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
   60.21 @@ -296,7 +296,7 @@
   60.22      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
   60.23      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
   60.24      val tacs = Rs |> map (fn R =>
   60.25 -      Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   60.26 +      Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   60.27    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   60.28  
   60.29  
    61.1 --- a/src/Pure/meta_simplifier.ML	Fri Dec 17 18:24:44 2010 +0100
    61.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    61.3 @@ -1,1379 +0,0 @@
    61.4 -(*  Title:      Pure/meta_simplifier.ML
    61.5 -    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
    61.6 -
    61.7 -Meta-level Simplification.
    61.8 -*)
    61.9 -
   61.10 -infix 4
   61.11 -  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
   61.12 -  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   61.13 -  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
   61.14 -
   61.15 -signature BASIC_META_SIMPLIFIER =
   61.16 -sig
   61.17 -  val simp_debug: bool Config.T
   61.18 -  val simp_debug_raw: Config.raw
   61.19 -  val simp_trace: bool Config.T
   61.20 -  val simp_trace_raw: Config.raw
   61.21 -  val simp_trace_default: bool Unsynchronized.ref
   61.22 -  val simp_trace_depth_limit: int Config.T
   61.23 -  val simp_trace_depth_limit_raw: Config.raw
   61.24 -  val simp_trace_depth_limit_default: int Unsynchronized.ref
   61.25 -  type rrule
   61.26 -  val eq_rrule: rrule * rrule -> bool
   61.27 -  type simpset
   61.28 -  type proc
   61.29 -  type solver
   61.30 -  val mk_solver': string -> (simpset -> int -> tactic) -> solver
   61.31 -  val mk_solver: string -> (thm list -> int -> tactic) -> solver
   61.32 -  val empty_ss: simpset
   61.33 -  val merge_ss: simpset * simpset -> simpset
   61.34 -  val dest_ss: simpset ->
   61.35 -   {simps: (string * thm) list,
   61.36 -    procs: (string * cterm list) list,
   61.37 -    congs: (string * thm) list,
   61.38 -    weak_congs: string list,
   61.39 -    loopers: string list,
   61.40 -    unsafe_solvers: string list,
   61.41 -    safe_solvers: string list}
   61.42 -  type simproc
   61.43 -  val eq_simproc: simproc * simproc -> bool
   61.44 -  val morph_simproc: morphism -> simproc -> simproc
   61.45 -  val make_simproc: {name: string, lhss: cterm list,
   61.46 -    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   61.47 -  val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
   61.48 -  val add_prems: thm list -> simpset -> simpset
   61.49 -  val prems_of_ss: simpset -> thm list
   61.50 -  val addsimps: simpset * thm list -> simpset
   61.51 -  val delsimps: simpset * thm list -> simpset
   61.52 -  val addeqcongs: simpset * thm list -> simpset
   61.53 -  val deleqcongs: simpset * thm list -> simpset
   61.54 -  val addcongs: simpset * thm list -> simpset
   61.55 -  val delcongs: simpset * thm list -> simpset
   61.56 -  val addsimprocs: simpset * simproc list -> simpset
   61.57 -  val delsimprocs: simpset * simproc list -> simpset
   61.58 -  val mksimps: simpset -> thm -> thm list
   61.59 -  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
   61.60 -  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
   61.61 -  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
   61.62 -  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   61.63 -  val settermless: simpset * (term * term -> bool) -> simpset
   61.64 -  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   61.65 -  val setloop': simpset * (simpset -> int -> tactic) -> simpset
   61.66 -  val setloop: simpset * (int -> tactic) -> simpset
   61.67 -  val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
   61.68 -  val addloop: simpset * (string * (int -> tactic)) -> simpset
   61.69 -  val delloop: simpset * string -> simpset
   61.70 -  val setSSolver: simpset * solver -> simpset
   61.71 -  val addSSolver: simpset * solver -> simpset
   61.72 -  val setSolver: simpset * solver -> simpset
   61.73 -  val addSolver: simpset * solver -> simpset
   61.74 -
   61.75 -  val rewrite_rule: thm list -> thm -> thm
   61.76 -  val rewrite_goals_rule: thm list -> thm -> thm
   61.77 -  val rewrite_goals_tac: thm list -> tactic
   61.78 -  val rewrite_goal_tac: thm list -> int -> tactic
   61.79 -  val rewtac: thm -> tactic
   61.80 -  val prune_params_tac: tactic
   61.81 -  val fold_rule: thm list -> thm -> thm
   61.82 -  val fold_goals_tac: thm list -> tactic
   61.83 -  val norm_hhf: thm -> thm
   61.84 -  val norm_hhf_protect: thm -> thm
   61.85 -end;
   61.86 -
   61.87 -signature META_SIMPLIFIER =
   61.88 -sig
   61.89 -  include BASIC_META_SIMPLIFIER
   61.90 -  exception SIMPLIFIER of string * thm
   61.91 -  val internal_ss: simpset ->
   61.92 -   {rules: rrule Net.net,
   61.93 -    prems: thm list,
   61.94 -    bounds: int * ((string * typ) * string) list,
   61.95 -    depth: int * bool Unsynchronized.ref,
   61.96 -    context: Proof.context option} *
   61.97 -   {congs: (string * thm) list * string list,
   61.98 -    procs: proc Net.net,
   61.99 -    mk_rews:
  61.100 -     {mk: simpset -> thm -> thm list,
  61.101 -      mk_cong: simpset -> thm -> thm,
  61.102 -      mk_sym: simpset -> thm -> thm option,
  61.103 -      mk_eq_True: simpset -> thm -> thm option,
  61.104 -      reorient: theory -> term list -> term -> term -> bool},
  61.105 -    termless: term * term -> bool,
  61.106 -    subgoal_tac: simpset -> int -> tactic,
  61.107 -    loop_tacs: (string * (simpset -> int -> tactic)) list,
  61.108 -    solvers: solver list * solver list}
  61.109 -  val add_simp: thm -> simpset -> simpset
  61.110 -  val del_simp: thm -> simpset -> simpset
  61.111 -  val solver: simpset -> solver -> int -> tactic
  61.112 -  val simp_depth_limit_raw: Config.raw
  61.113 -  val simp_depth_limit: int Config.T
  61.114 -  val clear_ss: simpset -> simpset
  61.115 -  val simproc_global_i: theory -> string -> term list
  61.116 -    -> (theory -> simpset -> term -> thm option) -> simproc
  61.117 -  val simproc_global: theory -> string -> string list
  61.118 -    -> (theory -> simpset -> term -> thm option) -> simproc
  61.119 -  val inherit_context: simpset -> simpset -> simpset
  61.120 -  val the_context: simpset -> Proof.context
  61.121 -  val context: Proof.context -> simpset -> simpset
  61.122 -  val global_context: theory  -> simpset -> simpset
  61.123 -  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
  61.124 -  val debug_bounds: bool Unsynchronized.ref
  61.125 -  val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
  61.126 -  val set_solvers: solver list -> simpset -> simpset
  61.127 -  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
  61.128 -  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
  61.129 -  val rewrite_thm: bool * bool * bool ->
  61.130 -    (simpset -> thm -> thm option) -> simpset -> thm -> thm
  61.131 -  val rewrite_goal_rule: bool * bool * bool ->
  61.132 -    (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
  61.133 -  val asm_rewrite_goal_tac: bool * bool * bool ->
  61.134 -    (simpset -> tactic) -> simpset -> int -> tactic
  61.135 -  val rewrite: bool -> thm list -> conv
  61.136 -  val simplify: bool -> thm list -> thm -> thm
  61.137 -end;
  61.138 -
  61.139 -structure MetaSimplifier: META_SIMPLIFIER =
  61.140 -struct
  61.141 -
  61.142 -(** datatype simpset **)
  61.143 -
  61.144 -(* rewrite rules *)
  61.145 -
  61.146 -type rrule =
  61.147 - {thm: thm,         (*the rewrite rule*)
  61.148 -  name: string,     (*name of theorem from which rewrite rule was extracted*)
  61.149 -  lhs: term,        (*the left-hand side*)
  61.150 -  elhs: cterm,      (*the etac-contracted lhs*)
  61.151 -  extra: bool,      (*extra variables outside of elhs*)
  61.152 -  fo: bool,         (*use first-order matching*)
  61.153 -  perm: bool};      (*the rewrite rule is permutative*)
  61.154 -
  61.155 -(*
  61.156 -Remarks:
  61.157 -  - elhs is used for matching,
  61.158 -    lhs only for preservation of bound variable names;
  61.159 -  - fo is set iff
  61.160 -    either elhs is first-order (no Var is applied),
  61.161 -      in which case fo-matching is complete,
  61.162 -    or elhs is not a pattern,
  61.163 -      in which case there is nothing better to do;
  61.164 -*)
  61.165 -
  61.166 -fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
  61.167 -  Thm.eq_thm_prop (thm1, thm2);
  61.168 -
  61.169 -
  61.170 -(* simplification sets, procedures, and solvers *)
  61.171 -
  61.172 -(*A simpset contains data required during conversion:
  61.173 -    rules: discrimination net of rewrite rules;
  61.174 -    prems: current premises;
  61.175 -    bounds: maximal index of bound variables already used
  61.176 -      (for generating new names when rewriting under lambda abstractions);
  61.177 -    depth: simp_depth and exceeded flag;
  61.178 -    congs: association list of congruence rules and
  61.179 -           a list of `weak' congruence constants.
  61.180 -           A congruence is `weak' if it avoids normalization of some argument.
  61.181 -    procs: discrimination net of simplification procedures
  61.182 -      (functions that prove rewrite rules on the fly);
  61.183 -    mk_rews:
  61.184 -      mk: turn simplification thms into rewrite rules;
  61.185 -      mk_cong: prepare congruence rules;
  61.186 -      mk_sym: turn == around;
  61.187 -      mk_eq_True: turn P into P == True;
  61.188 -    termless: relation for ordered rewriting;*)
  61.189 -
  61.190 -datatype simpset =
  61.191 -  Simpset of
  61.192 -   {rules: rrule Net.net,
  61.193 -    prems: thm list,
  61.194 -    bounds: int * ((string * typ) * string) list,
  61.195 -    depth: int * bool Unsynchronized.ref,
  61.196 -    context: Proof.context option} *
  61.197 -   {congs: (string * thm) list * string list,
  61.198 -    procs: proc Net.net,
  61.199 -    mk_rews:
  61.200 -     {mk: simpset -> thm -> thm list,
  61.201 -      mk_cong: simpset -> thm -> thm,
  61.202 -      mk_sym: simpset -> thm -> thm option,
  61.203 -      mk_eq_True: simpset -> thm -> thm option,
  61.204 -      reorient: theory -> term list -> term -> term -> bool},
  61.205 -    termless: term * term -> bool,
  61.206 -    subgoal_tac: simpset -> int -> tactic,
  61.207 -    loop_tacs: (string * (simpset -> int -> tactic)) list,
  61.208 -    solvers: solver list * solver list}
  61.209 -and proc =
  61.210 -  Proc of
  61.211 -   {name: string,
  61.212 -    lhs: cterm,
  61.213 -    proc: simpset -> cterm -> thm option,
  61.214 -    id: stamp * thm list}
  61.215 -and solver =
  61.216 -  Solver of
  61.217 -   {name: string,
  61.218 -    solver: simpset -> int -> tactic,
  61.219 -    id: stamp};
  61.220 -
  61.221 -
  61.222 -fun internal_ss (Simpset args) = args;
  61.223 -
  61.224 -fun make_ss1 (rules, prems, bounds, depth, context) =
  61.225 -  {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
  61.226 -
  61.227 -fun map_ss1 f {rules, prems, bounds, depth, context} =
  61.228 -  make_ss1 (f (rules, prems, bounds, depth, context));
  61.229 -
  61.230 -fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
  61.231 -  {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
  61.232 -    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
  61.233 -
  61.234 -fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
  61.235 -  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  61.236 -
  61.237 -fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
  61.238 -
  61.239 -fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
  61.240 -fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
  61.241 -
  61.242 -fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
  61.243 -
  61.244 -fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
  61.245 -  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
  61.246 -fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
  61.247 -
  61.248 -fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
  61.249 -fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
  61.250 -
  61.251 -fun solver_name (Solver {name, ...}) = name;
  61.252 -fun solver ss (Solver {solver = tac, ...}) = tac ss;
  61.253 -fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
  61.254 -
  61.255 -
  61.256 -(* simp depth *)
  61.257 -
  61.258 -val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
  61.259 -val simp_depth_limit = Config.int simp_depth_limit_raw;
  61.260 -
  61.261 -val simp_trace_depth_limit_default = Unsynchronized.ref 1;
  61.262 -val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
  61.263 -  (fn _ => Config.Int (! simp_trace_depth_limit_default));
  61.264 -val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
  61.265 -
  61.266 -fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
  61.267 -  | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
  61.268 -
  61.269 -fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
  61.270 -  if depth > simp_trace_depth_limit_of context then
  61.271 -    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
  61.272 -  else
  61.273 -    (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
  61.274 -
  61.275 -val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
  61.276 -  (rules, prems, bounds,
  61.277 -    (depth + 1,
  61.278 -      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
  61.279 -
  61.280 -fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
  61.281 -
  61.282 -
  61.283 -(* diagnostics *)
  61.284 -
  61.285 -exception SIMPLIFIER of string * thm;
  61.286 -
  61.287 -val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
  61.288 -val simp_debug = Config.bool simp_debug_raw;
  61.289 -
  61.290 -val simp_trace_default = Unsynchronized.ref false;
  61.291 -val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
  61.292 -val simp_trace = Config.bool simp_trace_raw;
  61.293 -
  61.294 -fun if_enabled (Simpset ({context, ...}, _)) flag f =
  61.295 -  (case context of
  61.296 -    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
  61.297 -  | NONE => ())
  61.298 -
  61.299 -fun if_visible (Simpset ({context, ...}, _)) f x =
  61.300 -  (case context of
  61.301 -    SOME ctxt => if Context_Position.is_visible ctxt then f x else ()
  61.302 -  | NONE => ());
  61.303 -
  61.304 -local
  61.305 -
  61.306 -fun prnt ss warn a = if warn then warning a else trace_depth ss a;
  61.307 -
  61.308 -fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
  61.309 -  let
  61.310 -    val names = Term.declare_term_names t Name.context;
  61.311 -    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
  61.312 -    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
  61.313 -  in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
  61.314 -
  61.315 -fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
  61.316 -  Syntax.string_of_term ctxt
  61.317 -    (if Config.get ctxt simp_debug then t else show_bounds ss t));
  61.318 -
  61.319 -in
  61.320 -
  61.321 -fun print_term_global ss warn a thy t =
  61.322 -  print_term ss warn (K a) t (ProofContext.init_global thy);
  61.323 -
  61.324 -fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
  61.325 -fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
  61.326 -
  61.327 -fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
  61.328 -fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
  61.329 -
  61.330 -fun trace_cterm warn a ss ct =
  61.331 -  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
  61.332 -
  61.333 -fun trace_thm a ss th =
  61.334 -  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
  61.335 -
  61.336 -fun trace_named_thm a ss (th, name) =
  61.337 -  if_enabled ss simp_trace (print_term ss false
  61.338 -    (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
  61.339 -    (Thm.full_prop_of th));
  61.340 -
  61.341 -fun warn_thm a ss th =
  61.342 -  print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
  61.343 -
  61.344 -fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
  61.345 -
  61.346 -end;
  61.347 -
  61.348 -
  61.349 -
  61.350 -(** simpset operations **)
  61.351 -
  61.352 -(* context *)
  61.353 -
  61.354 -fun eq_bound (x: string, (y, _)) = x = y;
  61.355 -
  61.356 -fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
  61.357 -  (rules, prems, (count + 1, bound :: bounds), depth, context));
  61.358 -
  61.359 -fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  61.360 -  (rules, ths @ prems, bounds, depth, context));
  61.361 -
  61.362 -fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
  61.363 -  map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
  61.364 -
  61.365 -fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
  61.366 -  | the_context _ = raise Fail "Simplifier: no proof context in simpset";
  61.367 -
  61.368 -fun context ctxt =
  61.369 -  map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
  61.370 -
  61.371 -val global_context = context o ProofContext.init_global;
  61.372 -
  61.373 -fun activate_context thy ss =
  61.374 -  let
  61.375 -    val ctxt = the_context ss;
  61.376 -    val ctxt' = ctxt
  61.377 -      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
  61.378 -      |> Context_Position.set_visible false;
  61.379 -  in context ctxt' ss end;
  61.380 -
  61.381 -fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
  61.382 -
  61.383 -
  61.384 -(* maintain simp rules *)
  61.385 -
  61.386 -(* FIXME: it seems that the conditions on extra variables are too liberal if
  61.387 -prems are nonempty: does solving the prems really guarantee instantiation of
  61.388 -all its Vars? Better: a dynamic check each time a rule is applied.
  61.389 -*)
  61.390 -fun rewrite_rule_extra_vars prems elhs erhs =
  61.391 -  let
  61.392 -    val elhss = elhs :: prems;
  61.393 -    val tvars = fold Term.add_tvars elhss [];
  61.394 -    val vars = fold Term.add_vars elhss [];
  61.395 -  in
  61.396 -    erhs |> Term.exists_type (Term.exists_subtype
  61.397 -      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
  61.398 -    erhs |> Term.exists_subterm
  61.399 -      (fn Var v => not (member (op =) vars v) | _ => false)
  61.400 -  end;
  61.401 -
  61.402 -fun rrule_extra_vars elhs thm =
  61.403 -  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
  61.404 -
  61.405 -fun mk_rrule2 {thm, name, lhs, elhs, perm} =
  61.406 -  let
  61.407 -    val t = term_of elhs;
  61.408 -    val fo = Pattern.first_order t orelse not (Pattern.pattern t);
  61.409 -    val extra = rrule_extra_vars elhs thm;
  61.410 -  in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
  61.411 -
  61.412 -fun del_rrule (rrule as {thm, elhs, ...}) ss =
  61.413 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  61.414 -    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
  61.415 -  handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
  61.416 -
  61.417 -fun insert_rrule (rrule as {thm, name, ...}) ss =
  61.418 - (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
  61.419 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  61.420 -    let
  61.421 -      val rrule2 as {elhs, ...} = mk_rrule2 rrule;
  61.422 -      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
  61.423 -    in (rules', prems, bounds, depth, context) end)
  61.424 -  handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
  61.425 -
  61.426 -fun vperm (Var _, Var _) = true
  61.427 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  61.428 -  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  61.429 -  | vperm (t, u) = (t = u);
  61.430 -
  61.431 -fun var_perm (t, u) =
  61.432 -  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
  61.433 -
  61.434 -(*simple test for looping rewrite rules and stupid orientations*)
  61.435 -fun default_reorient thy prems lhs rhs =
  61.436 -  rewrite_rule_extra_vars prems lhs rhs
  61.437 -    orelse
  61.438 -  is_Var (head_of lhs)
  61.439 -    orelse
  61.440 -(* turns t = x around, which causes a headache if x is a local variable -
  61.441 -   usually it is very useful :-(
  61.442 -  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
  61.443 -  andalso not(exists_subterm is_Var lhs)
  61.444 -    orelse
  61.445 -*)
  61.446 -  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
  61.447 -    orelse
  61.448 -  null prems andalso Pattern.matches thy (lhs, rhs)
  61.449 -    (*the condition "null prems" is necessary because conditional rewrites
  61.450 -      with extra variables in the conditions may terminate although
  61.451 -      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
  61.452 -    orelse
  61.453 -  is_Const lhs andalso not (is_Const rhs);
  61.454 -
  61.455 -fun decomp_simp thm =
  61.456 -  let
  61.457 -    val thy = Thm.theory_of_thm thm;
  61.458 -    val prop = Thm.prop_of thm;
  61.459 -    val prems = Logic.strip_imp_prems prop;
  61.460 -    val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
  61.461 -    val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
  61.462 -      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
  61.463 -    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
  61.464 -    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
  61.465 -    val erhs = Envir.eta_contract (term_of rhs);
  61.466 -    val perm =
  61.467 -      var_perm (term_of elhs, erhs) andalso
  61.468 -      not (term_of elhs aconv erhs) andalso
  61.469 -      not (is_Var (term_of elhs));
  61.470 -  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
  61.471 -
  61.472 -fun decomp_simp' thm =
  61.473 -  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
  61.474 -    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
  61.475 -    else (lhs, rhs)
  61.476 -  end;
  61.477 -
  61.478 -fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
  61.479 -  (case mk_eq_True ss thm of
  61.480 -    NONE => []
  61.481 -  | SOME eq_True =>
  61.482 -      let
  61.483 -        val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
  61.484 -      in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
  61.485 -
  61.486 -(*create the rewrite rule and possibly also the eq_True variant,
  61.487 -  in case there are extra vars on the rhs*)
  61.488 -fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
  61.489 -  let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
  61.490 -    if rewrite_rule_extra_vars [] lhs rhs then
  61.491 -      mk_eq_True ss (thm2, name) @ [rrule]
  61.492 -    else [rrule]
  61.493 -  end;
  61.494 -
  61.495 -fun mk_rrule ss (thm, name) =
  61.496 -  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  61.497 -    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  61.498 -    else
  61.499 -      (*weak test for loops*)
  61.500 -      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
  61.501 -      then mk_eq_True ss (thm, name)
  61.502 -      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  61.503 -  end;
  61.504 -
  61.505 -fun orient_rrule ss (thm, name) =
  61.506 -  let
  61.507 -    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
  61.508 -    val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
  61.509 -  in
  61.510 -    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  61.511 -    else if reorient thy prems lhs rhs then
  61.512 -      if reorient thy prems rhs lhs
  61.513 -      then mk_eq_True ss (thm, name)
  61.514 -      else
  61.515 -        (case mk_sym ss thm of
  61.516 -          NONE => []
  61.517 -        | SOME thm' =>
  61.518 -            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
  61.519 -            in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
  61.520 -    else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  61.521 -  end;
  61.522 -
  61.523 -fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
  61.524 -  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
  61.525 -
  61.526 -fun extract_safe_rrules (ss, thm) =
  61.527 -  maps (orient_rrule ss) (extract_rews (ss, [thm]));
  61.528 -
  61.529 -
  61.530 -(* add/del rules explicitly *)
  61.531 -
  61.532 -fun comb_simps comb mk_rrule (ss, thms) =
  61.533 -  let
  61.534 -    val rews = extract_rews (ss, thms);
  61.535 -  in fold (fold comb o mk_rrule) rews ss end;
  61.536 -
  61.537 -fun ss addsimps thms =
  61.538 -  comb_simps insert_rrule (mk_rrule ss) (ss, thms);
  61.539 -
  61.540 -fun ss delsimps thms =
  61.541 -  comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
  61.542 -
  61.543 -fun add_simp thm ss = ss addsimps [thm];
  61.544 -fun del_simp thm ss = ss delsimps [thm];
  61.545 -
  61.546 -
  61.547 -(* congs *)
  61.548 -
  61.549 -fun cong_name (Const (a, _)) = SOME a
  61.550 -  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
  61.551 -  | cong_name _ = NONE;
  61.552 -
  61.553 -local
  61.554 -
  61.555 -fun is_full_cong_prems [] [] = true
  61.556 -  | is_full_cong_prems [] _ = false
  61.557 -  | is_full_cong_prems (p :: prems) varpairs =
  61.558 -      (case Logic.strip_assums_concl p of
  61.559 -        Const ("==", _) $ lhs $ rhs =>
  61.560 -          let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
  61.561 -            is_Var x andalso forall is_Bound xs andalso
  61.562 -            not (has_duplicates (op =) xs) andalso xs = ys andalso
  61.563 -            member (op =) varpairs (x, y) andalso
  61.564 -            is_full_cong_prems prems (remove (op =) (x, y) varpairs)
  61.565 -          end
  61.566 -      | _ => false);
  61.567 -
  61.568 -fun is_full_cong thm =
  61.569 -  let
  61.570 -    val prems = prems_of thm and concl = concl_of thm;
  61.571 -    val (lhs, rhs) = Logic.dest_equals concl;
  61.572 -    val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
  61.573 -  in
  61.574 -    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
  61.575 -    is_full_cong_prems prems (xs ~~ ys)
  61.576 -  end;
  61.577 -
  61.578 -fun add_cong (ss, thm) = ss |>
  61.579 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.580 -    let
  61.581 -      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
  61.582 -        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  61.583 -    (*val lhs = Envir.eta_contract lhs;*)
  61.584 -      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
  61.585 -        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
  61.586 -      val (xs, weak) = congs;
  61.587 -      val _ =
  61.588 -        if AList.defined (op =) xs a
  61.589 -        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
  61.590 -        else ();
  61.591 -      val xs' = AList.update (op =) (a, thm) xs;
  61.592 -      val weak' = if is_full_cong thm then weak else a :: weak;
  61.593 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  61.594 -
  61.595 -fun del_cong (ss, thm) = ss |>
  61.596 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.597 -    let
  61.598 -      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
  61.599 -        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  61.600 -    (*val lhs = Envir.eta_contract lhs;*)
  61.601 -      val a = the (cong_name (head_of lhs)) handle Option.Option =>
  61.602 -        raise SIMPLIFIER ("Congruence must start with a constant", thm);
  61.603 -      val (xs, _) = congs;
  61.604 -      val xs' = filter_out (fn (x : string, _) => x = a) xs;
  61.605 -      val weak' = xs' |> map_filter (fn (a, thm) =>
  61.606 -        if is_full_cong thm then NONE else SOME a);
  61.607 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  61.608 -
  61.609 -fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
  61.610 -
  61.611 -in
  61.612 -
  61.613 -val (op addeqcongs) = Library.foldl add_cong;
  61.614 -val (op deleqcongs) = Library.foldl del_cong;
  61.615 -
  61.616 -fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
  61.617 -fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
  61.618 -
  61.619 -end;
  61.620 -
  61.621 -
  61.622 -(* simprocs *)
  61.623 -
  61.624 -datatype simproc =
  61.625 -  Simproc of
  61.626 -    {name: string,
  61.627 -     lhss: cterm list,
  61.628 -     proc: morphism -> simpset -> cterm -> thm option,
  61.629 -     id: stamp * thm list};
  61.630 -
  61.631 -fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
  61.632 -
  61.633 -fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
  61.634 -  Simproc
  61.635 -   {name = name,
  61.636 -    lhss = map (Morphism.cterm phi) lhss,
  61.637 -    proc = Morphism.transform phi proc,
  61.638 -    id = (s, Morphism.fact phi ths)};
  61.639 -
  61.640 -fun make_simproc {name, lhss, proc, identifier} =
  61.641 -  Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
  61.642 -
  61.643 -fun mk_simproc name lhss proc =
  61.644 -  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
  61.645 -    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
  61.646 -
  61.647 -(* FIXME avoid global thy and Logic.varify_global *)
  61.648 -fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
  61.649 -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
  61.650 -
  61.651 -
  61.652 -local
  61.653 -
  61.654 -fun add_proc (proc as Proc {name, lhs, ...}) ss =
  61.655 - (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
  61.656 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.657 -    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
  61.658 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  61.659 -  handle Net.INSERT =>
  61.660 -    (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
  61.661 -
  61.662 -fun del_proc (proc as Proc {name, lhs, ...}) ss =
  61.663 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.664 -    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
  61.665 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  61.666 -  handle Net.DELETE =>
  61.667 -    (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
  61.668 -
  61.669 -fun prep_procs (Simproc {name, lhss, proc, id}) =
  61.670 -  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
  61.671 -
  61.672 -in
  61.673 -
  61.674 -fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
  61.675 -fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
  61.676 -
  61.677 -end;
  61.678 -
  61.679 -
  61.680 -(* mk_rews *)
  61.681 -
  61.682 -local
  61.683 -
  61.684 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
  61.685 -      termless, subgoal_tac, loop_tacs, solvers) =>
  61.686 -  let
  61.687 -    val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
  61.688 -      f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
  61.689 -    val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
  61.690 -      reorient = reorient'};
  61.691 -  in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
  61.692 -
  61.693 -in
  61.694 -
  61.695 -fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
  61.696 -
  61.697 -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
  61.698 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  61.699 -
  61.700 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
  61.701 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  61.702 -
  61.703 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
  61.704 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  61.705 -
  61.706 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
  61.707 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  61.708 -
  61.709 -fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
  61.710 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  61.711 -
  61.712 -end;
  61.713 -
  61.714 -
  61.715 -(* termless *)
  61.716 -
  61.717 -fun ss settermless termless = ss |>
  61.718 -  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
  61.719 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  61.720 -
  61.721 -
  61.722 -(* tactics *)
  61.723 -
  61.724 -fun ss setsubgoaler subgoal_tac = ss |>
  61.725 -  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
  61.726 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  61.727 -
  61.728 -fun ss setloop' tac = ss |>
  61.729 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
  61.730 -   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
  61.731 -
  61.732 -fun ss setloop tac = ss setloop' (K tac);
  61.733 -
  61.734 -fun ss addloop' (name, tac) = ss |>
  61.735 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.736 -    (congs, procs, mk_rews, termless, subgoal_tac,
  61.737 -     (if AList.defined (op =) loop_tacs name
  61.738 -      then if_visible ss warning ("Overwriting looper " ^ quote name)
  61.739 -      else (); AList.update (op =) (name, tac) loop_tacs), solvers));
  61.740 -
  61.741 -fun ss addloop (name, tac) = ss addloop' (name, K tac);
  61.742 -
  61.743 -fun ss delloop name = ss |>
  61.744 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  61.745 -    (congs, procs, mk_rews, termless, subgoal_tac,
  61.746 -     (if AList.defined (op =) loop_tacs name then ()
  61.747 -      else if_visible ss warning ("No such looper in simpset: " ^ quote name);
  61.748 -      AList.delete (op =) name loop_tacs), solvers));
  61.749 -
  61.750 -fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  61.751 -  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
  61.752 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
  61.753 -
  61.754 -fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  61.755 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  61.756 -    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
  61.757 -
  61.758 -fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  61.759 -  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
  61.760 -    subgoal_tac, loop_tacs, ([solver], solvers)));
  61.761 -
  61.762 -fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  61.763 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  61.764 -    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
  61.765 -
  61.766 -fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
  61.767 -  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
  61.768 -  subgoal_tac, loop_tacs, (solvers, solvers)));
  61.769 -
  61.770 -
  61.771 -(* empty *)
  61.772 -
  61.773 -fun init_ss mk_rews termless subgoal_tac solvers =
  61.774 -  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
  61.775 -    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
  61.776 -
  61.777 -fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
  61.778 -  init_ss mk_rews termless subgoal_tac solvers
  61.779 -  |> inherit_context ss;
  61.780 -
  61.781 -val empty_ss =
  61.782 -  init_ss
  61.783 -    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
  61.784 -      mk_cong = K I,
  61.785 -      mk_sym = K (SOME o Drule.symmetric_fun),
  61.786 -      mk_eq_True = K (K NONE),
  61.787 -      reorient = default_reorient}
  61.788 -    Term_Ord.termless (K (K no_tac)) ([], []);
  61.789 -
  61.790 -
  61.791 -(* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
  61.792 -
  61.793 -fun merge_ss (ss1, ss2) =
  61.794 -  if pointer_eq (ss1, ss2) then ss1
  61.795 -  else
  61.796 -    let
  61.797 -      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
  61.798 -       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
  61.799 -        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
  61.800 -      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
  61.801 -       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
  61.802 -        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
  61.803 -
  61.804 -      val rules' = Net.merge eq_rrule (rules1, rules2);
  61.805 -      val prems' = Thm.merge_thms (prems1, prems2);
  61.806 -      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
  61.807 -      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
  61.808 -      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
  61.809 -      val weak' = merge (op =) (weak1, weak2);
  61.810 -      val procs' = Net.merge eq_proc (procs1, procs2);
  61.811 -      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
  61.812 -      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
  61.813 -      val solvers' = merge eq_solver (solvers1, solvers2);
  61.814 -    in
  61.815 -      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
  61.816 -        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
  61.817 -    end;
  61.818 -
  61.819 -
  61.820 -(* dest_ss *)
  61.821 -
  61.822 -fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
  61.823 - {simps = Net.entries rules
  61.824 -    |> map (fn {name, thm, ...} => (name, thm)),
  61.825 -  procs = Net.entries procs
  61.826 -    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
  61.827 -    |> partition_eq (eq_snd eq_procid)
  61.828 -    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
  61.829 -  congs = #1 congs,
  61.830 -  weak_congs = #2 congs,
  61.831 -  loopers = map fst loop_tacs,
  61.832 -  unsafe_solvers = map solver_name (#1 solvers),
  61.833 -  safe_solvers = map solver_name (#2 solvers)};
  61.834 -
  61.835 -
  61.836 -
  61.837 -(** rewriting **)
  61.838 -
  61.839 -(*
  61.840 -  Uses conversions, see:
  61.841 -    L C Paulson, A higher-order implementation of rewriting,
  61.842 -    Science of Computer Programming 3 (1983), pages 119-149.
  61.843 -*)
  61.844 -
  61.845 -fun check_conv msg ss thm thm' =
  61.846 -  let
  61.847 -    val thm'' = Thm.transitive thm thm' handle THM _ =>
  61.848 -     Thm.transitive thm (Thm.transitive
  61.849 -       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
  61.850 -  in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
  61.851 -  handle THM _ =>
  61.852 -    let
  61.853 -      val _ $ _ $ prop0 = Thm.prop_of thm;
  61.854 -    in
  61.855 -      trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
  61.856 -      trace_term false (fn () => "Should have proved:") ss prop0;
  61.857 -      NONE
  61.858 -    end;
  61.859 -
  61.860 -
  61.861 -(* mk_procrule *)
  61.862 -
  61.863 -fun mk_procrule ss thm =
  61.864 -  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
  61.865 -    if rewrite_rule_extra_vars prems lhs rhs
  61.866 -    then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
  61.867 -    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
  61.868 -  end;
  61.869 -
  61.870 -
  61.871 -(* rewritec: conversion to apply the meta simpset to a term *)
  61.872 -
  61.873 -(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  61.874 -  normalized terms by carrying around the rhs of the rewrite rule just
  61.875 -  applied. This is called the `skeleton'. It is decomposed in parallel
  61.876 -  with the term. Once a Var is encountered, the corresponding term is
  61.877 -  already in normal form.
  61.878 -  skel0 is a dummy skeleton that is to enforce complete normalization.*)
  61.879 -
  61.880 -val skel0 = Bound 0;
  61.881 -
  61.882 -(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  61.883 -  The latter may happen iff there are weak congruence rules for constants
  61.884 -  in the lhs.*)
  61.885 -
  61.886 -fun uncond_skel ((_, weak), (lhs, rhs)) =
  61.887 -  if null weak then rhs  (*optimization*)
  61.888 -  else if exists_Const (member (op =) weak o #1) lhs then skel0
  61.889 -  else rhs;
  61.890 -
  61.891 -(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  61.892 -  Otherwise those vars may become instantiated with unnormalized terms
  61.893 -  while the premises are solved.*)
  61.894 -
  61.895 -fun cond_skel (args as (_, (lhs, rhs))) =
  61.896 -  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
  61.897 -  else skel0;
  61.898 -
  61.899 -(*
  61.900 -  Rewriting -- we try in order:
  61.901 -    (1) beta reduction
  61.902 -    (2) unconditional rewrite rules
  61.903 -    (3) conditional rewrite rules
  61.904 -    (4) simplification procedures
  61.905 -
  61.906 -  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  61.907 -*)
  61.908 -
  61.909 -fun rewritec (prover, thyt, maxt) ss t =
  61.910 -  let
  61.911 -    val ctxt = the_context ss;
  61.912 -    val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  61.913 -    val eta_thm = Thm.eta_conversion t;
  61.914 -    val eta_t' = Thm.rhs_of eta_thm;
  61.915 -    val eta_t = term_of eta_t';
  61.916 -    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
  61.917 -      let
  61.918 -        val prop = Thm.prop_of thm;
  61.919 -        val (rthm, elhs') =
  61.920 -          if maxt = ~1 orelse not extra then (thm, elhs)
  61.921 -          else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
  61.922 -        val insts =
  61.923 -          if fo then Thm.first_order_match (elhs', eta_t')
  61.924 -          else Thm.match (elhs', eta_t');
  61.925 -        val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
  61.926 -        val prop' = Thm.prop_of thm';
  61.927 -        val unconditional = (Logic.count_prems prop' = 0);
  61.928 -        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
  61.929 -      in
  61.930 -        if perm andalso not (termless (rhs', lhs'))
  61.931 -        then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
  61.932 -              trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
  61.933 -        else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
  61.934 -           if unconditional
  61.935 -           then
  61.936 -             (trace_thm (fn () => "Rewriting:") ss thm';
  61.937 -              let
  61.938 -                val lr = Logic.dest_equals prop;
  61.939 -                val SOME thm'' = check_conv false ss eta_thm thm';
  61.940 -              in SOME (thm'', uncond_skel (congs, lr)) end)
  61.941 -           else
  61.942 -             (trace_thm (fn () => "Trying to rewrite:") ss thm';
  61.943 -              if simp_depth ss > Config.get ctxt simp_depth_limit
  61.944 -              then
  61.945 -                let
  61.946 -                  val s = "simp_depth_limit exceeded - giving up";
  61.947 -                  val _ = trace false (fn () => s) ss;
  61.948 -                  val _ = if_visible ss warning s;
  61.949 -                in NONE end
  61.950 -              else
  61.951 -              case prover ss thm' of
  61.952 -                NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
  61.953 -              | SOME thm2 =>
  61.954 -                  (case check_conv true ss eta_thm thm2 of
  61.955 -                     NONE => NONE |
  61.956 -                     SOME thm2' =>
  61.957 -                       let val concl = Logic.strip_imp_concl prop
  61.958 -                           val lr = Logic.dest_equals concl
  61.959 -                       in SOME (thm2', cond_skel (congs, lr)) end)))
  61.960 -      end
  61.961 -
  61.962 -    fun rews [] = NONE
  61.963 -      | rews (rrule :: rrules) =
  61.964 -          let val opt = rew rrule handle Pattern.MATCH => NONE
  61.965 -          in case opt of NONE => rews rrules | some => some end;
  61.966 -
  61.967 -    fun sort_rrules rrs =
  61.968 -      let
  61.969 -        fun is_simple ({thm, ...}: rrule) =
  61.970 -          (case Thm.prop_of thm of
  61.971 -            Const ("==", _) $ _ $ _ => true
  61.972 -          | _ => false);
  61.973 -        fun sort [] (re1, re2) = re1 @ re2
  61.974 -          | sort (rr :: rrs) (re1, re2) =
  61.975 -              if is_simple rr
  61.976 -              then sort rrs (rr :: re1, re2)
  61.977 -              else sort rrs (re1, rr :: re2);
  61.978 -      in sort rrs ([], []) end;
  61.979 -
  61.980 -    fun proc_rews [] = NONE
  61.981 -      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  61.982 -          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
  61.983 -            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
  61.984 -             case proc ss eta_t' of
  61.985 -               NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
  61.986 -             | SOME raw_thm =>
  61.987 -                 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
  61.988 -                   ss raw_thm;
  61.989 -                  (case rews (mk_procrule ss raw_thm) of
  61.990 -                    NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
  61.991 -                      " -- does not match") ss t; proc_rews ps)
  61.992 -                  | some => some)))
  61.993 -          else proc_rews ps;
  61.994 -  in
  61.995 -    (case eta_t of
  61.996 -      Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
  61.997 -    | _ =>
  61.998 -      (case rews (sort_rrules (Net.match_term rules eta_t)) of
  61.999 -        NONE => proc_rews (Net.match_term procs eta_t)
 61.1000 -      | some => some))
 61.1001 -  end;
 61.1002 -
 61.1003 -
 61.1004 -(* conversion to apply a congruence rule to a term *)
 61.1005 -
 61.1006 -fun congc prover ss maxt cong t =
 61.1007 -  let val rthm = Thm.incr_indexes (maxt + 1) cong;
 61.1008 -      val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
 61.1009 -      val insts = Thm.match (rlhs, t)
 61.1010 -      (* Thm.match can raise Pattern.MATCH;
 61.1011 -         is handled when congc is called *)
 61.1012 -      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
 61.1013 -      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
 61.1014 -      fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
 61.1015 -  in
 61.1016 -    (case prover thm' of
 61.1017 -      NONE => err ("Congruence proof failed.  Could not prove", thm')
 61.1018 -    | SOME thm2 =>
 61.1019 -        (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
 61.1020 -          NONE => err ("Congruence proof failed.  Should not have proved", thm2)
 61.1021 -        | SOME thm2' =>
 61.1022 -            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
 61.1023 -            then NONE else SOME thm2'))
 61.1024 -  end;
 61.1025 -
 61.1026 -val (cA, (cB, cC)) =
 61.1027 -  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
 61.1028 -
 61.1029 -fun transitive1 NONE NONE = NONE
 61.1030 -  | transitive1 (SOME thm1) NONE = SOME thm1
 61.1031 -  | transitive1 NONE (SOME thm2) = SOME thm2
 61.1032 -  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
 61.1033 -
 61.1034 -fun transitive2 thm = transitive1 (SOME thm);
 61.1035 -fun transitive3 thm = transitive1 thm o SOME;
 61.1036 -
 61.1037 -fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
 61.1038 -  let
 61.1039 -    fun botc skel ss t =
 61.1040 -          if is_Var skel then NONE
 61.1041 -          else
 61.1042 -          (case subc skel ss t of
 61.1043 -             some as SOME thm1 =>
 61.1044 -               (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
 61.1045 -                  SOME (thm2, skel2) =>
 61.1046 -                    transitive2 (Thm.transitive thm1 thm2)
 61.1047 -                      (botc skel2 ss (Thm.rhs_of thm2))
 61.1048 -                | NONE => some)
 61.1049 -           | NONE =>
 61.1050 -               (case rewritec (prover, thy, maxidx) ss t of
 61.1051 -                  SOME (thm2, skel2) => transitive2 thm2
 61.1052 -                    (botc skel2 ss (Thm.rhs_of thm2))
 61.1053 -                | NONE => NONE))
 61.1054 -
 61.1055 -    and try_botc ss t =
 61.1056 -          (case botc skel0 ss t of
 61.1057 -             SOME trec1 => trec1 | NONE => (Thm.reflexive t))
 61.1058 -
 61.1059 -    and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
 61.1060 -       (case term_of t0 of
 61.1061 -           Abs (a, T, _) =>
 61.1062 -             let
 61.1063 -                 val b = Name.bound (#1 bounds);
 61.1064 -                 val (v, t') = Thm.dest_abs (SOME b) t0;
 61.1065 -                 val b' = #1 (Term.dest_Free (Thm.term_of v));
 61.1066 -                 val _ =
 61.1067 -                   if b <> b' then
 61.1068 -                     warning ("Simplifier: renamed bound variable " ^
 61.1069 -                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
 61.1070 -                   else ();
 61.1071 -                 val ss' = add_bound ((b', T), a) ss;
 61.1072 -                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
 61.1073 -             in case botc skel' ss' t' of
 61.1074 -                  SOME thm => SOME (Thm.abstract_rule a v thm)
 61.1075 -                | NONE => NONE
 61.1076 -             end
 61.1077 -         | t $ _ => (case t of
 61.1078 -             Const ("==>", _) $ _  => impc t0 ss
 61.1079 -           | Abs _ =>
 61.1080 -               let val thm = Thm.beta_conversion false t0
 61.1081 -               in case subc skel0 ss (Thm.rhs_of thm) of
 61.1082 -                    NONE => SOME thm
 61.1083 -                  | SOME thm' => SOME (Thm.transitive thm thm')
 61.1084 -               end
 61.1085 -           | _  =>
 61.1086 -               let fun appc () =
 61.1087 -                     let
 61.1088 -                       val (tskel, uskel) = case skel of
 61.1089 -                           tskel $ uskel => (tskel, uskel)
 61.1090 -                         | _ => (skel0, skel0);
 61.1091 -                       val (ct, cu) = Thm.dest_comb t0
 61.1092 -                     in
 61.1093 -                     (case botc tskel ss ct of
 61.1094 -                        SOME thm1 =>
 61.1095 -                          (case botc uskel ss cu of
 61.1096 -                             SOME thm2 => SOME (Thm.combination thm1 thm2)
 61.1097 -                           | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
 61.1098 -                      | NONE =>
 61.1099 -                          (case botc uskel ss cu of
 61.1100 -                             SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
 61.1101 -                           | NONE => NONE))
 61.1102 -                     end
 61.1103 -                   val (h, ts) = strip_comb t
 61.1104 -               in case cong_name h of
 61.1105 -                    SOME a =>
 61.1106 -                      (case AList.lookup (op =) (fst congs) a of
 61.1107 -                         NONE => appc ()
 61.1108 -                       | SOME cong =>
 61.1109 -  (*post processing: some partial applications h t1 ... tj, j <= length ts,
 61.1110 -    may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
 61.1111 -                          (let
 61.1112 -                             val thm = congc (prover ss) ss maxidx cong t0;
 61.1113 -                             val t = the_default t0 (Option.map Thm.rhs_of thm);
 61.1114 -                             val (cl, cr) = Thm.dest_comb t
 61.1115 -                             val dVar = Var(("", 0), dummyT)
 61.1116 -                             val skel =
 61.1117 -                               list_comb (h, replicate (length ts) dVar)
 61.1118 -                           in case botc skel ss cl of
 61.1119 -                                NONE => thm
 61.1120 -                              | SOME thm' => transitive3 thm
 61.1121 -                                  (Thm.combination thm' (Thm.reflexive cr))
 61.1122 -                           end handle Pattern.MATCH => appc ()))
 61.1123 -                  | _ => appc ()
 61.1124 -               end)
 61.1125 -         | _ => NONE)
 61.1126 -
 61.1127 -    and impc ct ss =
 61.1128 -      if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
 61.1129 -
 61.1130 -    and rules_of_prem ss prem =
 61.1131 -      if maxidx_of_term (term_of prem) <> ~1
 61.1132 -      then (trace_cterm true
 61.1133 -        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
 61.1134 -          ss prem; ([], NONE))
 61.1135 -      else
 61.1136 -        let val asm = Thm.assume prem
 61.1137 -        in (extract_safe_rrules (ss, asm), SOME asm) end
 61.1138 -
 61.1139 -    and add_rrules (rrss, asms) ss =
 61.1140 -      (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
 61.1141 -
 61.1142 -    and disch r prem eq =
 61.1143 -      let
 61.1144 -        val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
 61.1145 -        val eq' = Thm.implies_elim (Thm.instantiate
 61.1146 -          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
 61.1147 -          (Thm.implies_intr prem eq)
 61.1148 -      in if not r then eq' else
 61.1149 -        let
 61.1150 -          val (prem', concl) = Thm.dest_implies lhs;
 61.1151 -          val (prem'', _) = Thm.dest_implies rhs
 61.1152 -        in Thm.transitive (Thm.transitive
 61.1153 -          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
 61.1154 -             Drule.swap_prems_eq) eq')
 61.1155 -          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
 61.1156 -             Drule.swap_prems_eq)
 61.1157 -        end
 61.1158 -      end
 61.1159 -
 61.1160 -    and rebuild [] _ _ _ _ eq = eq
 61.1161 -      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
 61.1162 -          let
 61.1163 -            val ss' = add_rrules (rev rrss, rev asms) ss;
 61.1164 -            val concl' =
 61.1165 -              Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
 61.1166 -            val dprem = Option.map (disch false prem)
 61.1167 -          in
 61.1168 -            (case rewritec (prover, thy, maxidx) ss' concl' of
 61.1169 -              NONE => rebuild prems concl' rrss asms ss (dprem eq)
 61.1170 -            | SOME (eq', _) => transitive2 (fold (disch false)
 61.1171 -                  prems (the (transitive3 (dprem eq) eq')))
 61.1172 -                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
 61.1173 -          end
 61.1174 -
 61.1175 -    and mut_impc0 prems concl rrss asms ss =
 61.1176 -      let
 61.1177 -        val prems' = strip_imp_prems concl;
 61.1178 -        val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
 61.1179 -      in
 61.1180 -        mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
 61.1181 -          (asms @ asms') [] [] [] [] ss ~1 ~1
 61.1182 -      end
 61.1183 -
 61.1184 -    and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
 61.1185 -        transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
 61.1186 -            (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
 61.1187 -          (if changed > 0 then
 61.1188 -             mut_impc (rev prems') concl (rev rrss') (rev asms')
 61.1189 -               [] [] [] [] ss ~1 changed
 61.1190 -           else rebuild prems' concl rrss' asms' ss
 61.1191 -             (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
 61.1192 -
 61.1193 -      | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
 61.1194 -          prems' rrss' asms' eqns ss changed k =
 61.1195 -        case (if k = 0 then NONE else botc skel0 (add_rrules
 61.1196 -          (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
 61.1197 -            NONE => mut_impc prems concl rrss asms (prem :: prems')
 61.1198 -              (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
 61.1199 -              (if k = 0 then 0 else k - 1)
 61.1200 -          | SOME eqn =>
 61.1201 -            let
 61.1202 -              val prem' = Thm.rhs_of eqn;
 61.1203 -              val tprems = map term_of prems;
 61.1204 -              val i = 1 + fold Integer.max (map (fn p =>
 61.1205 -                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
 61.1206 -              val (rrs', asm') = rules_of_prem ss prem'
 61.1207 -            in mut_impc prems concl rrss asms (prem' :: prems')
 61.1208 -              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
 61.1209 -                (take i prems)
 61.1210 -                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
 61.1211 -                  (drop i prems, concl))))) :: eqns)
 61.1212 -                  ss (length prems') ~1
 61.1213 -            end
 61.1214 -
 61.1215 -     (*legacy code - only for backwards compatibility*)
 61.1216 -    and nonmut_impc ct ss =
 61.1217 -      let
 61.1218 -        val (prem, conc) = Thm.dest_implies ct;
 61.1219 -        val thm1 = if simprem then botc skel0 ss prem else NONE;
 61.1220 -        val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
 61.1221 -        val ss1 =
 61.1222 -          if not useprem then ss
 61.1223 -          else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
 61.1224 -      in
 61.1225 -        (case botc skel0 ss1 conc of
 61.1226 -          NONE =>
 61.1227 -            (case thm1 of
 61.1228 -              NONE => NONE
 61.1229 -            | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
 61.1230 -        | SOME thm2 =>
 61.1231 -            let val thm2' = disch false prem1 thm2 in
 61.1232 -              (case thm1 of
 61.1233 -                NONE => SOME thm2'
 61.1234 -              | SOME thm1' =>
 61.1235 -                 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
 61.1236 -            end)
 61.1237 -      end
 61.1238 -
 61.1239 - in try_botc end;
 61.1240 -
 61.1241 -
 61.1242 -(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
 61.1243 -
 61.1244 -(*
 61.1245 -  Parameters:
 61.1246 -    mode = (simplify A,
 61.1247 -            use A in simplifying B,
 61.1248 -            use prems of B (if B is again a meta-impl.) to simplify A)
 61.1249 -           when simplifying A ==> B
 61.1250 -    prover: how to solve premises in conditional rewrites and congruences
 61.1251 -*)
 61.1252 -
 61.1253 -val debug_bounds = Unsynchronized.ref false;
 61.1254 -
 61.1255 -fun check_bounds ss ct =
 61.1256 -  if ! debug_bounds then
 61.1257 -    let
 61.1258 -      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
 61.1259 -      val bs = fold_aterms (fn Free (x, _) =>
 61.1260 -          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
 61.1261 -          then insert (op =) x else I
 61.1262 -        | _ => I) (term_of ct) [];
 61.1263 -    in
 61.1264 -      if null bs then ()
 61.1265 -      else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
 61.1266 -        (Thm.theory_of_cterm ct) (Thm.term_of ct)
 61.1267 -    end
 61.1268 -  else ();
 61.1269 -
 61.1270 -fun rewrite_cterm mode prover raw_ss raw_ct =
 61.1271 -  let
 61.1272 -    val thy = Thm.theory_of_cterm raw_ct;
 61.1273 -    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
 61.1274 -    val {maxidx, ...} = Thm.rep_cterm ct;
 61.1275 -    val ss = inc_simp_depth (activate_context thy raw_ss);
 61.1276 -    val depth = simp_depth ss;
 61.1277 -    val _ =
 61.1278 -      if depth mod 20 = 0 then
 61.1279 -        if_visible ss warning ("Simplification depth " ^ string_of_int depth)
 61.1280 -      else ();
 61.1281 -    val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
 61.1282 -    val _ = check_bounds ss ct;
 61.1283 -  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
 61.1284 -
 61.1285 -val simple_prover =
 61.1286 -  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
 61.1287 -
 61.1288 -fun rewrite _ [] ct = Thm.reflexive ct
 61.1289 -  | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
 61.1290 -      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 61.1291 -
 61.1292 -fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 61.1293 -val rewrite_rule = simplify true;
 61.1294 -
 61.1295 -(*simple term rewriting -- no proof*)
 61.1296 -fun rewrite_term thy rules procs =
 61.1297 -  Pattern.rewrite_term thy (map decomp_simp' rules) procs;
 61.1298 -
 61.1299 -fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
 61.1300 -
 61.1301 -(*Rewrite the subgoals of a proof state (represented by a theorem)*)
 61.1302 -fun rewrite_goals_rule thms th =
 61.1303 -  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
 61.1304 -    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 61.1305 -
 61.1306 -(*Rewrite the subgoal of a proof state (represented by a theorem)*)
 61.1307 -fun rewrite_goal_rule mode prover ss i thm =
 61.1308 -  if 0 < i andalso i <= Thm.nprems_of thm
 61.1309 -  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
 61.1310 -  else raise THM ("rewrite_goal_rule", i, [thm]);
 61.1311 -
 61.1312 -
 61.1313 -(** meta-rewriting tactics **)
 61.1314 -
 61.1315 -(*Rewrite all subgoals*)
 61.1316 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 61.1317 -fun rewtac def = rewrite_goals_tac [def];
 61.1318 -
 61.1319 -(*Rewrite one subgoal*)
 61.1320 -fun asm_rewrite_goal_tac mode prover_tac ss i thm =
 61.1321 -  if 0 < i andalso i <= Thm.nprems_of thm then
 61.1322 -    Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
 61.1323 -  else Seq.empty;
 61.1324 -
 61.1325 -fun rewrite_goal_tac rews =
 61.1326 -  let val ss = empty_ss addsimps rews in
 61.1327 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
 61.1328 -      (global_context (Thm.theory_of_thm st) ss) i st
 61.1329 -  end;
 61.1330 -
 61.1331 -(*Prunes all redundant parameters from the proof state by rewriting.
 61.1332 -  DOES NOT rewrite main goal, where quantification over an unused bound
 61.1333 -    variable is sometimes done to avoid the need for cut_facts_tac.*)
 61.1334 -val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
 61.1335 -
 61.1336 -
 61.1337 -(* for folding definitions, handling critical pairs *)
 61.1338 -
 61.1339 -(*The depth of nesting in a term*)
 61.1340 -fun term_depth (Abs (_, _, t)) = 1 + term_depth t
 61.1341 -  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
 61.1342 -  | term_depth _ = 0;
 61.1343 -
 61.1344 -val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
 61.1345 -
 61.1346 -(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
 61.1347 -  Returns longest lhs first to avoid folding its subexpressions.*)
 61.1348 -fun sort_lhs_depths defs =
 61.1349 -  let val keylist = AList.make (term_depth o lhs_of_thm) defs
 61.1350 -      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
 61.1351 -  in map (AList.find (op =) keylist) keys end;
 61.1352 -
 61.1353 -val rev_defs = sort_lhs_depths o map Thm.symmetric;
 61.1354 -
 61.1355 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
 61.1356 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 61.1357 -
 61.1358 -
 61.1359 -(* HHF normal form: !! before ==>, outermost !! generalized *)
 61.1360 -
 61.1361 -local
 61.1362 -
 61.1363 -fun gen_norm_hhf ss th =
 61.1364 -  (if Drule.is_norm_hhf (Thm.prop_of th) then th
 61.1365 -   else Conv.fconv_rule
 61.1366 -    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
 61.1367 -  |> Thm.adjust_maxidx_thm ~1
 61.1368 -  |> Drule.gen_all;
 61.1369 -
 61.1370 -val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 61.1371 -
 61.1372 -in
 61.1373 -
 61.1374 -val norm_hhf = gen_norm_hhf hhf_ss;
 61.1375 -val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
 61.1376 -
 61.1377 -end;
 61.1378 -
 61.1379 -end;
 61.1380 -
 61.1381 -structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
 61.1382 -open Basic_Meta_Simplifier;
    62.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    62.2 +++ b/src/Pure/raw_simplifier.ML	Fri Dec 17 18:33:35 2010 +0100
    62.3 @@ -0,0 +1,1379 @@
    62.4 +(*  Title:      Pure/raw_simplifier.ML
    62.5 +    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
    62.6 +
    62.7 +Higher-order Simplification.
    62.8 +*)
    62.9 +
   62.10 +infix 4
   62.11 +  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
   62.12 +  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   62.13 +  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
   62.14 +
   62.15 +signature BASIC_RAW_SIMPLIFIER =
   62.16 +sig
   62.17 +  val simp_depth_limit: int Config.T
   62.18 +  val simp_trace_depth_limit: int Config.T
   62.19 +  val simp_debug: bool Config.T
   62.20 +  val simp_trace: bool Config.T
   62.21 +  type rrule
   62.22 +  val eq_rrule: rrule * rrule -> bool
   62.23 +  type simpset
   62.24 +  type proc
   62.25 +  type solver
   62.26 +  val mk_solver': string -> (simpset -> int -> tactic) -> solver
   62.27 +  val mk_solver: string -> (thm list -> int -> tactic) -> solver
   62.28 +  val empty_ss: simpset
   62.29 +  val merge_ss: simpset * simpset -> simpset
   62.30 +  val dest_ss: simpset ->
   62.31 +   {simps: (string * thm) list,
   62.32 +    procs: (string * cterm list) list,
   62.33 +    congs: (string * thm) list,
   62.34 +    weak_congs: string list,
   62.35 +    loopers: string list,
   62.36 +    unsafe_solvers: string list,
   62.37 +    safe_solvers: string list}
   62.38 +  type simproc
   62.39 +  val eq_simproc: simproc * simproc -> bool
   62.40 +  val morph_simproc: morphism -> simproc -> simproc
   62.41 +  val make_simproc: {name: string, lhss: cterm list,
   62.42 +    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   62.43 +  val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
   62.44 +  val prems_of_ss: simpset -> thm list
   62.45 +  val addsimps: simpset * thm list -> simpset
   62.46 +  val delsimps: simpset * thm list -> simpset
   62.47 +  val addeqcongs: simpset * thm list -> simpset
   62.48 +  val deleqcongs: simpset * thm list -> simpset
   62.49 +  val addcongs: simpset * thm list -> simpset
   62.50 +  val delcongs: simpset * thm list -> simpset
   62.51 +  val addsimprocs: simpset * simproc list -> simpset
   62.52 +  val delsimprocs: simpset * simproc list -> simpset
   62.53 +  val mksimps: simpset -> thm -> thm list
   62.54 +  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
   62.55 +  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
   62.56 +  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
   62.57 +  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   62.58 +  val settermless: simpset * (term * term -> bool) -> simpset
   62.59 +  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   62.60 +  val setloop': simpset * (simpset -> int -> tactic) -> simpset
   62.61 +  val setloop: simpset * (int -> tactic) -> simpset
   62.62 +  val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
   62.63 +  val addloop: simpset * (string * (int -> tactic)) -> simpset
   62.64 +  val delloop: simpset * string -> simpset
   62.65 +  val setSSolver: simpset * solver -> simpset
   62.66 +  val addSSolver: simpset * solver -> simpset
   62.67 +  val setSolver: simpset * solver -> simpset
   62.68 +  val addSolver: simpset * solver -> simpset
   62.69 +
   62.70 +  val rewrite_rule: thm list -> thm -> thm
   62.71 +  val rewrite_goals_rule: thm list -> thm -> thm
   62.72 +  val rewrite_goals_tac: thm list -> tactic
   62.73 +  val rewrite_goal_tac: thm list -> int -> tactic
   62.74 +  val rewtac: thm -> tactic
   62.75 +  val prune_params_tac: tactic
   62.76 +  val fold_rule: thm list -> thm -> thm
   62.77 +  val fold_goals_tac: thm list -> tactic
   62.78 +  val norm_hhf: thm -> thm
   62.79 +  val norm_hhf_protect: thm -> thm
   62.80 +end;
   62.81 +
   62.82 +signature RAW_SIMPLIFIER =
   62.83 +sig
   62.84 +  include BASIC_RAW_SIMPLIFIER
   62.85 +  exception SIMPLIFIER of string * thm
   62.86 +  val internal_ss: simpset ->
   62.87 +   {rules: rrule Net.net,
   62.88 +    prems: thm list,
   62.89 +    bounds: int * ((string * typ) * string) list,
   62.90 +    depth: int * bool Unsynchronized.ref,
   62.91 +    context: Proof.context option} *
   62.92 +   {congs: (string * thm) list * string list,
   62.93 +    procs: proc Net.net,
   62.94 +    mk_rews:
   62.95 +     {mk: simpset -> thm -> thm list,
   62.96 +      mk_cong: simpset -> thm -> thm,
   62.97 +      mk_sym: simpset -> thm -> thm option,
   62.98 +      mk_eq_True: simpset -> thm -> thm option,
   62.99 +      reorient: theory -> term list -> term -> term -> bool},
  62.100 +    termless: term * term -> bool,
  62.101 +    subgoal_tac: simpset -> int -> tactic,
  62.102 +    loop_tacs: (string * (simpset -> int -> tactic)) list,
  62.103 +    solvers: solver list * solver list}
  62.104 +  val add_simp: thm -> simpset -> simpset
  62.105 +  val del_simp: thm -> simpset -> simpset
  62.106 +  val solver: simpset -> solver -> int -> tactic
  62.107 +  val simp_depth_limit_raw: Config.raw
  62.108 +  val clear_ss: simpset -> simpset
  62.109 +  val simproc_global_i: theory -> string -> term list
  62.110 +    -> (theory -> simpset -> term -> thm option) -> simproc
  62.111 +  val simproc_global: theory -> string -> string list
  62.112 +    -> (theory -> simpset -> term -> thm option) -> simproc
  62.113 +  val simp_trace_depth_limit_raw: Config.raw
  62.114 +  val simp_trace_depth_limit_default: int Unsynchronized.ref
  62.115 +  val simp_trace_default: bool Unsynchronized.ref
  62.116 +  val simp_trace_raw: Config.raw
  62.117 +  val simp_debug_raw: Config.raw
  62.118 +  val add_prems: thm list -> simpset -> simpset
  62.119 +  val inherit_context: simpset -> simpset -> simpset
  62.120 +  val the_context: simpset -> Proof.context
  62.121 +  val context: Proof.context -> simpset -> simpset
  62.122 +  val global_context: theory  -> simpset -> simpset
  62.123 +  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
  62.124 +  val debug_bounds: bool Unsynchronized.ref
  62.125 +  val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
  62.126 +  val set_solvers: solver list -> simpset -> simpset
  62.127 +  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
  62.128 +  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
  62.129 +  val rewrite_thm: bool * bool * bool ->
  62.130 +    (simpset -> thm -> thm option) -> simpset -> thm -> thm
  62.131 +  val rewrite_goal_rule: bool * bool * bool ->
  62.132 +    (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
  62.133 +  val asm_rewrite_goal_tac: bool * bool * bool ->
  62.134 +    (simpset -> tactic) -> simpset -> int -> tactic
  62.135 +  val rewrite: bool -> thm list -> conv
  62.136 +  val simplify: bool -> thm list -> thm -> thm
  62.137 +end;
  62.138 +
  62.139 +structure Raw_Simplifier: RAW_SIMPLIFIER =
  62.140 +struct
  62.141 +
  62.142 +(** datatype simpset **)
  62.143 +
  62.144 +(* rewrite rules *)
  62.145 +
  62.146 +type rrule =
  62.147 + {thm: thm,         (*the rewrite rule*)
  62.148 +  name: string,     (*name of theorem from which rewrite rule was extracted*)
  62.149 +  lhs: term,        (*the left-hand side*)
  62.150 +  elhs: cterm,      (*the etac-contracted lhs*)
  62.151 +  extra: bool,      (*extra variables outside of elhs*)
  62.152 +  fo: bool,         (*use first-order matching*)
  62.153 +  perm: bool};      (*the rewrite rule is permutative*)
  62.154 +
  62.155 +(*
  62.156 +Remarks:
  62.157 +  - elhs is used for matching,
  62.158 +    lhs only for preservation of bound variable names;
  62.159 +  - fo is set iff
  62.160 +    either elhs is first-order (no Var is applied),
  62.161 +      in which case fo-matching is complete,
  62.162 +    or elhs is not a pattern,
  62.163 +      in which case there is nothing better to do;
  62.164 +*)
  62.165 +
  62.166 +fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
  62.167 +  Thm.eq_thm_prop (thm1, thm2);
  62.168 +
  62.169 +
  62.170 +(* simplification sets, procedures, and solvers *)
  62.171 +
  62.172 +(*A simpset contains data required during conversion:
  62.173 +    rules: discrimination net of rewrite rules;
  62.174 +    prems: current premises;
  62.175 +    bounds: maximal index of bound variables already used
  62.176 +      (for generating new names when rewriting under lambda abstractions);
  62.177 +    depth: simp_depth and exceeded flag;
  62.178 +    congs: association list of congruence rules and
  62.179 +           a list of `weak' congruence constants.
  62.180 +           A congruence is `weak' if it avoids normalization of some argument.
  62.181 +    procs: discrimination net of simplification procedures
  62.182 +      (functions that prove rewrite rules on the fly);
  62.183 +    mk_rews:
  62.184 +      mk: turn simplification thms into rewrite rules;
  62.185 +      mk_cong: prepare congruence rules;
  62.186 +      mk_sym: turn == around;
  62.187 +      mk_eq_True: turn P into P == True;
  62.188 +    termless: relation for ordered rewriting;*)
  62.189 +
  62.190 +datatype simpset =
  62.191 +  Simpset of
  62.192 +   {rules: rrule Net.net,
  62.193 +    prems: thm list,
  62.194 +    bounds: int * ((string * typ) * string) list,
  62.195 +    depth: int * bool Unsynchronized.ref,
  62.196 +    context: Proof.context option} *
  62.197 +   {congs: (string * thm) list * string list,
  62.198 +    procs: proc Net.net,
  62.199 +    mk_rews:
  62.200 +     {mk: simpset -> thm -> thm list,
  62.201 +      mk_cong: simpset -> thm -> thm,
  62.202 +      mk_sym: simpset -> thm -> thm option,
  62.203 +      mk_eq_True: simpset -> thm -> thm option,
  62.204 +      reorient: theory -> term list -> term -> term -> bool},
  62.205 +    termless: term * term -> bool,
  62.206 +    subgoal_tac: simpset -> int -> tactic,
  62.207 +    loop_tacs: (string * (simpset -> int -> tactic)) list,
  62.208 +    solvers: solver list * solver list}
  62.209 +and proc =
  62.210 +  Proc of
  62.211 +   {name: string,
  62.212 +    lhs: cterm,
  62.213 +    proc: simpset -> cterm -> thm option,
  62.214 +    id: stamp * thm list}
  62.215 +and solver =
  62.216 +  Solver of
  62.217 +   {name: string,
  62.218 +    solver: simpset -> int -> tactic,
  62.219 +    id: stamp};
  62.220 +
  62.221 +
  62.222 +fun internal_ss (Simpset args) = args;
  62.223 +
  62.224 +fun make_ss1 (rules, prems, bounds, depth, context) =
  62.225 +  {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
  62.226 +
  62.227 +fun map_ss1 f {rules, prems, bounds, depth, context} =
  62.228 +  make_ss1 (f (rules, prems, bounds, depth, context));
  62.229 +
  62.230 +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
  62.231 +  {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
  62.232 +    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
  62.233 +
  62.234 +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
  62.235 +  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  62.236 +
  62.237 +fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
  62.238 +
  62.239 +fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
  62.240 +fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
  62.241 +
  62.242 +fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
  62.243 +
  62.244 +fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
  62.245 +  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
  62.246 +fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
  62.247 +
  62.248 +fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
  62.249 +fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
  62.250 +
  62.251 +fun solver_name (Solver {name, ...}) = name;
  62.252 +fun solver ss (Solver {solver = tac, ...}) = tac ss;
  62.253 +fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
  62.254 +
  62.255 +
  62.256 +(* simp depth *)
  62.257 +
  62.258 +val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
  62.259 +val simp_depth_limit = Config.int simp_depth_limit_raw;
  62.260 +
  62.261 +val simp_trace_depth_limit_default = Unsynchronized.ref 1;
  62.262 +val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
  62.263 +  (fn _ => Config.Int (! simp_trace_depth_limit_default));
  62.264 +val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
  62.265 +
  62.266 +fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
  62.267 +  | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
  62.268 +
  62.269 +fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
  62.270 +  if depth > simp_trace_depth_limit_of context then
  62.271 +    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
  62.272 +  else
  62.273 +    (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
  62.274 +
  62.275 +val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
  62.276 +  (rules, prems, bounds,
  62.277 +    (depth + 1,
  62.278 +      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
  62.279 +
  62.280 +fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
  62.281 +
  62.282 +
  62.283 +(* diagnostics *)
  62.284 +
  62.285 +exception SIMPLIFIER of string * thm;
  62.286 +
  62.287 +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
  62.288 +val simp_debug = Config.bool simp_debug_raw;
  62.289 +
  62.290 +val simp_trace_default = Unsynchronized.ref false;
  62.291 +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
  62.292 +val simp_trace = Config.bool simp_trace_raw;
  62.293 +
  62.294 +fun if_enabled (Simpset ({context, ...}, _)) flag f =
  62.295 +  (case context of
  62.296 +    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
  62.297 +  | NONE => ())
  62.298 +
  62.299 +fun if_visible (Simpset ({context, ...}, _)) f x =
  62.300 +  (case context of
  62.301 +    SOME ctxt => if Context_Position.is_visible ctxt then f x else ()
  62.302 +  | NONE => ());
  62.303 +
  62.304 +local
  62.305 +
  62.306 +fun prnt ss warn a = if warn then warning a else trace_depth ss a;
  62.307 +
  62.308 +fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
  62.309 +  let
  62.310 +    val names = Term.declare_term_names t Name.context;
  62.311 +    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
  62.312 +    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
  62.313 +  in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
  62.314 +
  62.315 +fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
  62.316 +  Syntax.string_of_term ctxt
  62.317 +    (if Config.get ctxt simp_debug then t else show_bounds ss t));
  62.318 +
  62.319 +in
  62.320 +
  62.321 +fun print_term_global ss warn a thy t =
  62.322 +  print_term ss warn (K a) t (ProofContext.init_global thy);
  62.323 +
  62.324 +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
  62.325 +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
  62.326 +
  62.327 +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
  62.328 +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
  62.329 +
  62.330 +fun trace_cterm warn a ss ct =
  62.331 +  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
  62.332 +
  62.333 +fun trace_thm a ss th =
  62.334 +  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
  62.335 +
  62.336 +fun trace_named_thm a ss (th, name) =
  62.337 +  if_enabled ss simp_trace (print_term ss false
  62.338 +    (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
  62.339 +    (Thm.full_prop_of th));
  62.340 +
  62.341 +fun warn_thm a ss th =
  62.342 +  print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
  62.343 +
  62.344 +fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
  62.345 +
  62.346 +end;
  62.347 +
  62.348 +
  62.349 +
  62.350 +(** simpset operations **)
  62.351 +
  62.352 +(* context *)
  62.353 +
  62.354 +fun eq_bound (x: string, (y, _)) = x = y;
  62.355 +
  62.356 +fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
  62.357 +  (rules, prems, (count + 1, bound :: bounds), depth, context));
  62.358 +
  62.359 +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  62.360 +  (rules, ths @ prems, bounds, depth, context));
  62.361 +
  62.362 +fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
  62.363 +  map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
  62.364 +
  62.365 +fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
  62.366 +  | the_context _ = raise Fail "Simplifier: no proof context in simpset";
  62.367 +
  62.368 +fun context ctxt =
  62.369 +  map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
  62.370 +
  62.371 +val global_context = context o ProofContext.init_global;
  62.372 +
  62.373 +fun activate_context thy ss =
  62.374 +  let
  62.375 +    val ctxt = the_context ss;
  62.376 +    val ctxt' = ctxt
  62.377 +      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
  62.378 +      |> Context_Position.set_visible false;
  62.379 +  in context ctxt' ss end;
  62.380 +
  62.381 +fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
  62.382 +
  62.383 +
  62.384 +(* maintain simp rules *)
  62.385 +
  62.386 +(* FIXME: it seems that the conditions on extra variables are too liberal if
  62.387 +prems are nonempty: does solving the prems really guarantee instantiation of
  62.388 +all its Vars? Better: a dynamic check each time a rule is applied.
  62.389 +*)
  62.390 +fun rewrite_rule_extra_vars prems elhs erhs =
  62.391 +  let
  62.392 +    val elhss = elhs :: prems;
  62.393 +    val tvars = fold Term.add_tvars elhss [];
  62.394 +    val vars = fold Term.add_vars elhss [];
  62.395 +  in
  62.396 +    erhs |> Term.exists_type (Term.exists_subtype
  62.397 +      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
  62.398 +    erhs |> Term.exists_subterm
  62.399 +      (fn Var v => not (member (op =) vars v) | _ => false)
  62.400 +  end;
  62.401 +
  62.402 +fun rrule_extra_vars elhs thm =
  62.403 +  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
  62.404 +
  62.405 +fun mk_rrule2 {thm, name, lhs, elhs, perm} =
  62.406 +  let
  62.407 +    val t = term_of elhs;
  62.408 +    val fo = Pattern.first_order t orelse not (Pattern.pattern t);
  62.409 +    val extra = rrule_extra_vars elhs thm;
  62.410 +  in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
  62.411 +
  62.412 +fun del_rrule (rrule as {thm, elhs, ...}) ss =
  62.413 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  62.414 +    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
  62.415 +  handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
  62.416 +
  62.417 +fun insert_rrule (rrule as {thm, name, ...}) ss =
  62.418 + (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
  62.419 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  62.420 +    let
  62.421 +      val rrule2 as {elhs, ...} = mk_rrule2 rrule;
  62.422 +      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
  62.423 +    in (rules', prems, bounds, depth, context) end)
  62.424 +  handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
  62.425 +
  62.426 +fun vperm (Var _, Var _) = true
  62.427 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  62.428 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  62.429 +  | vperm (t, u) = (t = u);
  62.430 +
  62.431 +fun var_perm (t, u) =
  62.432 +  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
  62.433 +
  62.434 +(*simple test for looping rewrite rules and stupid orientations*)
  62.435 +fun default_reorient thy prems lhs rhs =
  62.436 +  rewrite_rule_extra_vars prems lhs rhs
  62.437 +    orelse
  62.438 +  is_Var (head_of lhs)
  62.439 +    orelse
  62.440 +(* turns t = x around, which causes a headache if x is a local variable -
  62.441 +   usually it is very useful :-(
  62.442 +  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
  62.443 +  andalso not(exists_subterm is_Var lhs)
  62.444 +    orelse
  62.445 +*)
  62.446 +  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
  62.447 +    orelse
  62.448 +  null prems andalso Pattern.matches thy (lhs, rhs)
  62.449 +    (*the condition "null prems" is necessary because conditional rewrites
  62.450 +      with extra variables in the conditions may terminate although
  62.451 +      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
  62.452 +    orelse
  62.453 +  is_Const lhs andalso not (is_Const rhs);
  62.454 +
  62.455 +fun decomp_simp thm =
  62.456 +  let
  62.457 +    val thy = Thm.theory_of_thm thm;
  62.458 +    val prop = Thm.prop_of thm;
  62.459 +    val prems = Logic.strip_imp_prems prop;
  62.460 +    val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
  62.461 +    val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
  62.462 +      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
  62.463 +    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
  62.464 +    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
  62.465 +    val erhs = Envir.eta_contract (term_of rhs);
  62.466 +    val perm =
  62.467 +      var_perm (term_of elhs, erhs) andalso
  62.468 +      not (term_of elhs aconv erhs) andalso
  62.469 +      not (is_Var (term_of elhs));
  62.470 +  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
  62.471 +
  62.472 +fun decomp_simp' thm =
  62.473 +  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
  62.474 +    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
  62.475 +    else (lhs, rhs)
  62.476 +  end;
  62.477 +
  62.478 +fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
  62.479 +  (case mk_eq_True ss thm of
  62.480 +    NONE => []
  62.481 +  | SOME eq_True =>
  62.482 +      let
  62.483 +        val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
  62.484 +      in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
  62.485 +
  62.486 +(*create the rewrite rule and possibly also the eq_True variant,
  62.487 +  in case there are extra vars on the rhs*)
  62.488 +fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
  62.489 +  let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
  62.490 +    if rewrite_rule_extra_vars [] lhs rhs then
  62.491 +      mk_eq_True ss (thm2, name) @ [rrule]
  62.492 +    else [rrule]
  62.493 +  end;
  62.494 +
  62.495 +fun mk_rrule ss (thm, name) =
  62.496 +  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  62.497 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  62.498 +    else
  62.499 +      (*weak test for loops*)
  62.500 +      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
  62.501 +      then mk_eq_True ss (thm, name)
  62.502 +      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  62.503 +  end;
  62.504 +
  62.505 +fun orient_rrule ss (thm, name) =
  62.506 +  let
  62.507 +    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
  62.508 +    val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
  62.509 +  in
  62.510 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  62.511 +    else if reorient thy prems lhs rhs then
  62.512 +      if reorient thy prems rhs lhs
  62.513 +      then mk_eq_True ss (thm, name)
  62.514 +      else
  62.515 +        (case mk_sym ss thm of
  62.516 +          NONE => []
  62.517 +        | SOME thm' =>
  62.518 +            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
  62.519 +            in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
  62.520 +    else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  62.521 +  end;
  62.522 +
  62.523 +fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
  62.524 +  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
  62.525 +
  62.526 +fun extract_safe_rrules (ss, thm) =
  62.527 +  maps (orient_rrule ss) (extract_rews (ss, [thm]));
  62.528 +
  62.529 +
  62.530 +(* add/del rules explicitly *)
  62.531 +
  62.532 +fun comb_simps comb mk_rrule (ss, thms) =
  62.533 +  let
  62.534 +    val rews = extract_rews (ss, thms);
  62.535 +  in fold (fold comb o mk_rrule) rews ss end;
  62.536 +
  62.537 +fun ss addsimps thms =
  62.538 +  comb_simps insert_rrule (mk_rrule ss) (ss, thms);
  62.539 +
  62.540 +fun ss delsimps thms =
  62.541 +  comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
  62.542 +
  62.543 +fun add_simp thm ss = ss addsimps [thm];
  62.544 +fun del_simp thm ss = ss delsimps [thm];
  62.545 +
  62.546 +
  62.547 +(* congs *)
  62.548 +
  62.549 +fun cong_name (Const (a, _)) = SOME a
  62.550 +  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
  62.551 +  | cong_name _ = NONE;
  62.552 +
  62.553 +local
  62.554 +
  62.555 +fun is_full_cong_prems [] [] = true
  62.556 +  | is_full_cong_prems [] _ = false
  62.557 +  | is_full_cong_prems (p :: prems) varpairs =
  62.558 +      (case Logic.strip_assums_concl p of
  62.559 +        Const ("==", _) $ lhs $ rhs =>
  62.560 +          let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
  62.561 +            is_Var x andalso forall is_Bound xs andalso
  62.562 +            not (has_duplicates (op =) xs) andalso xs = ys andalso
  62.563 +            member (op =) varpairs (x, y) andalso
  62.564 +            is_full_cong_prems prems (remove (op =) (x, y) varpairs)
  62.565 +          end
  62.566 +      | _ => false);
  62.567 +
  62.568 +fun is_full_cong thm =
  62.569 +  let
  62.570 +    val prems = prems_of thm and concl = concl_of thm;
  62.571 +    val (lhs, rhs) = Logic.dest_equals concl;
  62.572 +    val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
  62.573 +  in
  62.574 +    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
  62.575 +    is_full_cong_prems prems (xs ~~ ys)
  62.576 +  end;
  62.577 +
  62.578 +fun add_cong (ss, thm) = ss |>
  62.579 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.580 +    let
  62.581 +      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
  62.582 +        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  62.583 +    (*val lhs = Envir.eta_contract lhs;*)
  62.584 +      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
  62.585 +        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
  62.586 +      val (xs, weak) = congs;
  62.587 +      val _ =
  62.588 +        if AList.defined (op =) xs a
  62.589 +        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
  62.590 +        else ();
  62.591 +      val xs' = AList.update (op =) (a, thm) xs;
  62.592 +      val weak' = if is_full_cong thm then weak else a :: weak;
  62.593 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  62.594 +
  62.595 +fun del_cong (ss, thm) = ss |>
  62.596 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.597 +    let
  62.598 +      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
  62.599 +        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  62.600 +    (*val lhs = Envir.eta_contract lhs;*)
  62.601 +      val a = the (cong_name (head_of lhs)) handle Option.Option =>
  62.602 +        raise SIMPLIFIER ("Congruence must start with a constant", thm);
  62.603 +      val (xs, _) = congs;
  62.604 +      val xs' = filter_out (fn (x : string, _) => x = a) xs;
  62.605 +      val weak' = xs' |> map_filter (fn (a, thm) =>
  62.606 +        if is_full_cong thm then NONE else SOME a);
  62.607 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  62.608 +
  62.609 +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
  62.610 +
  62.611 +in
  62.612 +
  62.613 +val (op addeqcongs) = Library.foldl add_cong;
  62.614 +val (op deleqcongs) = Library.foldl del_cong;
  62.615 +
  62.616 +fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
  62.617 +fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
  62.618 +
  62.619 +end;
  62.620 +
  62.621 +
  62.622 +(* simprocs *)
  62.623 +
  62.624 +datatype simproc =
  62.625 +  Simproc of
  62.626 +    {name: string,
  62.627 +     lhss: cterm list,
  62.628 +     proc: morphism -> simpset -> cterm -> thm option,
  62.629 +     id: stamp * thm list};
  62.630 +
  62.631 +fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
  62.632 +
  62.633 +fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
  62.634 +  Simproc
  62.635 +   {name = name,
  62.636 +    lhss = map (Morphism.cterm phi) lhss,
  62.637 +    proc = Morphism.transform phi proc,
  62.638 +    id = (s, Morphism.fact phi ths)};
  62.639 +
  62.640 +fun make_simproc {name, lhss, proc, identifier} =
  62.641 +  Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
  62.642 +
  62.643 +fun mk_simproc name lhss proc =
  62.644 +  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
  62.645 +    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
  62.646 +
  62.647 +(* FIXME avoid global thy and Logic.varify_global *)
  62.648 +fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
  62.649 +fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
  62.650 +
  62.651 +
  62.652 +local
  62.653 +
  62.654 +fun add_proc (proc as Proc {name, lhs, ...}) ss =
  62.655 + (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
  62.656 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.657 +    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
  62.658 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  62.659 +  handle Net.INSERT =>
  62.660 +    (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
  62.661 +
  62.662 +fun del_proc (proc as Proc {name, lhs, ...}) ss =
  62.663 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.664 +    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
  62.665 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  62.666 +  handle Net.DELETE =>
  62.667 +    (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
  62.668 +
  62.669 +fun prep_procs (Simproc {name, lhss, proc, id}) =
  62.670 +  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
  62.671 +
  62.672 +in
  62.673 +
  62.674 +fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
  62.675 +fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
  62.676 +
  62.677 +end;
  62.678 +
  62.679 +
  62.680 +(* mk_rews *)
  62.681 +
  62.682 +local
  62.683 +
  62.684 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
  62.685 +      termless, subgoal_tac, loop_tacs, solvers) =>
  62.686 +  let
  62.687 +    val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
  62.688 +      f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
  62.689 +    val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
  62.690 +      reorient = reorient'};
  62.691 +  in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
  62.692 +
  62.693 +in
  62.694 +
  62.695 +fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
  62.696 +
  62.697 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
  62.698 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  62.699 +
  62.700 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
  62.701 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  62.702 +
  62.703 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
  62.704 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  62.705 +
  62.706 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
  62.707 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  62.708 +
  62.709 +fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
  62.710 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  62.711 +
  62.712 +end;
  62.713 +
  62.714 +
  62.715 +(* termless *)
  62.716 +
  62.717 +fun ss settermless termless = ss |>
  62.718 +  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
  62.719 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  62.720 +
  62.721 +
  62.722 +(* tactics *)
  62.723 +
  62.724 +fun ss setsubgoaler subgoal_tac = ss |>
  62.725 +  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
  62.726 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  62.727 +
  62.728 +fun ss setloop' tac = ss |>
  62.729 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
  62.730 +   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
  62.731 +
  62.732 +fun ss setloop tac = ss setloop' (K tac);
  62.733 +
  62.734 +fun ss addloop' (name, tac) = ss |>
  62.735 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.736 +    (congs, procs, mk_rews, termless, subgoal_tac,
  62.737 +     (if AList.defined (op =) loop_tacs name
  62.738 +      then if_visible ss warning ("Overwriting looper " ^ quote name)
  62.739 +      else (); AList.update (op =) (name, tac) loop_tacs), solvers));
  62.740 +
  62.741 +fun ss addloop (name, tac) = ss addloop' (name, K tac);
  62.742 +
  62.743 +fun ss delloop name = ss |>
  62.744 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  62.745 +    (congs, procs, mk_rews, termless, subgoal_tac,
  62.746 +     (if AList.defined (op =) loop_tacs name then ()
  62.747 +      else if_visible ss warning ("No such looper in simpset: " ^ quote name);
  62.748 +      AList.delete (op =) name loop_tacs), solvers));
  62.749 +
  62.750 +fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  62.751 +  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
  62.752 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
  62.753 +
  62.754 +fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  62.755 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  62.756 +    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
  62.757 +
  62.758 +fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  62.759 +  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
  62.760 +    subgoal_tac, loop_tacs, ([solver], solvers)));
  62.761 +
  62.762 +fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  62.763 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  62.764 +    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
  62.765 +
  62.766 +fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
  62.767 +  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
  62.768 +  subgoal_tac, loop_tacs, (solvers, solvers)));
  62.769 +
  62.770 +
  62.771 +(* empty *)
  62.772 +
  62.773 +fun init_ss mk_rews termless subgoal_tac solvers =
  62.774 +  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
  62.775 +    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
  62.776 +
  62.777 +fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
  62.778 +  init_ss mk_rews termless subgoal_tac solvers
  62.779 +  |> inherit_context ss;
  62.780 +
  62.781 +val empty_ss =
  62.782 +  init_ss
  62.783 +    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
  62.784 +      mk_cong = K I,
  62.785 +      mk_sym = K (SOME o Drule.symmetric_fun),
  62.786 +      mk_eq_True = K (K NONE),
  62.787 +      reorient = default_reorient}
  62.788 +    Term_Ord.termless (K (K no_tac)) ([], []);
  62.789 +
  62.790 +
  62.791 +(* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
  62.792 +
  62.793 +fun merge_ss (ss1, ss2) =
  62.794 +  if pointer_eq (ss1, ss2) then ss1
  62.795 +  else
  62.796 +    let
  62.797 +      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
  62.798 +       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
  62.799 +        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
  62.800 +      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
  62.801 +       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
  62.802 +        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
  62.803 +
  62.804 +      val rules' = Net.merge eq_rrule (rules1, rules2);
  62.805 +      val prems' = Thm.merge_thms (prems1, prems2);
  62.806 +      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
  62.807 +      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
  62.808 +      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
  62.809 +      val weak' = merge (op =) (weak1, weak2);
  62.810 +      val procs' = Net.merge eq_proc (procs1, procs2);
  62.811 +      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
  62.812 +      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
  62.813 +      val solvers' = merge eq_solver (solvers1, solvers2);
  62.814 +    in
  62.815 +      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
  62.816 +        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
  62.817 +    end;
  62.818 +
  62.819 +
  62.820 +(* dest_ss *)
  62.821 +
  62.822 +fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
  62.823 + {simps = Net.entries rules
  62.824 +    |> map (fn {name, thm, ...} => (name, thm)),
  62.825 +  procs = Net.entries procs
  62.826 +    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
  62.827 +    |> partition_eq (eq_snd eq_procid)
  62.828 +    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
  62.829 +  congs = #1 congs,
  62.830 +  weak_congs = #2 congs,
  62.831 +  loopers = map fst loop_tacs,
  62.832 +  unsafe_solvers = map solver_name (#1 solvers),
  62.833 +  safe_solvers = map solver_name (#2 solvers)};
  62.834 +
  62.835 +
  62.836 +
  62.837 +(** rewriting **)
  62.838 +
  62.839 +(*
  62.840 +  Uses conversions, see:
  62.841 +    L C Paulson, A higher-order implementation of rewriting,
  62.842 +    Science of Computer Programming 3 (1983), pages 119-149.
  62.843 +*)
  62.844 +
  62.845 +fun check_conv msg ss thm thm' =
  62.846 +  let
  62.847 +    val thm'' = Thm.transitive thm thm' handle THM _ =>
  62.848 +     Thm.transitive thm (Thm.transitive
  62.849 +       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
  62.850 +  in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
  62.851 +  handle THM _ =>
  62.852 +    let
  62.853 +      val _ $ _ $ prop0 = Thm.prop_of thm;
  62.854 +    in
  62.855 +      trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
  62.856 +      trace_term false (fn () => "Should have proved:") ss prop0;
  62.857 +      NONE
  62.858 +    end;
  62.859 +
  62.860 +
  62.861 +(* mk_procrule *)
  62.862 +
  62.863 +fun mk_procrule ss thm =
  62.864 +  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
  62.865 +    if rewrite_rule_extra_vars prems lhs rhs
  62.866 +    then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
  62.867 +    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
  62.868 +  end;
  62.869 +
  62.870 +
  62.871 +(* rewritec: conversion to apply the meta simpset to a term *)
  62.872 +
  62.873 +(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  62.874 +  normalized terms by carrying around the rhs of the rewrite rule just
  62.875 +  applied. This is called the `skeleton'. It is decomposed in parallel
  62.876 +  with the term. Once a Var is encountered, the corresponding term is
  62.877 +  already in normal form.
  62.878 +  skel0 is a dummy skeleton that is to enforce complete normalization.*)
  62.879 +
  62.880 +val skel0 = Bound 0;
  62.881 +
  62.882 +(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  62.883 +  The latter may happen iff there are weak congruence rules for constants
  62.884 +  in the lhs.*)
  62.885 +
  62.886 +fun uncond_skel ((_, weak), (lhs, rhs)) =
  62.887 +  if null weak then rhs  (*optimization*)
  62.888 +  else if exists_Const (member (op =) weak o #1) lhs then skel0
  62.889 +  else rhs;
  62.890 +
  62.891 +(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  62.892 +  Otherwise those vars may become instantiated with unnormalized terms
  62.893 +  while the premises are solved.*)
  62.894 +
  62.895 +fun cond_skel (args as (_, (lhs, rhs))) =
  62.896 +  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
  62.897 +  else skel0;
  62.898 +
  62.899 +(*
  62.900 +  Rewriting -- we try in order:
  62.901 +    (1) beta reduction
  62.902 +    (2) unconditional rewrite rules
  62.903 +    (3) conditional rewrite rules
  62.904 +    (4) simplification procedures
  62.905 +
  62.906 +  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  62.907 +*)
  62.908 +
  62.909 +fun rewritec (prover, thyt, maxt) ss t =
  62.910 +  let
  62.911 +    val ctxt = the_context ss;
  62.912 +    val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  62.913 +    val eta_thm = Thm.eta_conversion t;
  62.914 +    val eta_t' = Thm.rhs_of eta_thm;
  62.915 +    val eta_t = term_of eta_t';
  62.916 +    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
  62.917 +      let
  62.918 +        val prop = Thm.prop_of thm;
  62.919 +        val (rthm, elhs') =
  62.920 +          if maxt = ~1 orelse not extra then (thm, elhs)
  62.921 +          else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
  62.922 +        val insts =
  62.923 +          if fo then Thm.first_order_match (elhs', eta_t')
  62.924 +          else Thm.match (elhs', eta_t');
  62.925 +        val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
  62.926 +        val prop' = Thm.prop_of thm';
  62.927 +        val unconditional = (Logic.count_prems prop' = 0);
  62.928 +        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
  62.929 +      in
  62.930 +        if perm andalso not (termless (rhs', lhs'))
  62.931 +        then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
  62.932 +              trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
  62.933 +        else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
  62.934 +           if unconditional
  62.935 +           then
  62.936 +             (trace_thm (fn () => "Rewriting:") ss thm';
  62.937 +              let
  62.938 +                val lr = Logic.dest_equals prop;
  62.939 +                val SOME thm'' = check_conv false ss eta_thm thm';
  62.940 +              in SOME (thm'', uncond_skel (congs, lr)) end)
  62.941 +           else
  62.942 +             (trace_thm (fn () => "Trying to rewrite:") ss thm';
  62.943 +              if simp_depth ss > Config.get ctxt simp_depth_limit
  62.944 +              then
  62.945 +                let
  62.946 +                  val s = "simp_depth_limit exceeded - giving up";
  62.947 +                  val _ = trace false (fn () => s) ss;
  62.948 +                  val _ = if_visible ss warning s;
  62.949 +                in NONE end
  62.950 +              else
  62.951 +              case prover ss thm' of
  62.952 +                NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
  62.953 +              | SOME thm2 =>
  62.954 +                  (case check_conv true ss eta_thm thm2 of
  62.955 +                     NONE => NONE |
  62.956 +                     SOME thm2' =>
  62.957 +                       let val concl = Logic.strip_imp_concl prop
  62.958 +                           val lr = Logic.dest_equals concl
  62.959 +                       in SOME (thm2', cond_skel (congs, lr)) end)))
  62.960 +      end
  62.961 +
  62.962 +    fun rews [] = NONE
  62.963 +      | rews (rrule :: rrules) =
  62.964 +          let val opt = rew rrule handle Pattern.MATCH => NONE
  62.965 +          in case opt of NONE => rews rrules | some => some end;
  62.966 +
  62.967 +    fun sort_rrules rrs =
  62.968 +      let
  62.969 +        fun is_simple ({thm, ...}: rrule) =
  62.970 +          (case Thm.prop_of thm of
  62.971 +            Const ("==", _) $ _ $ _ => true
  62.972 +          | _ => false);
  62.973 +        fun sort [] (re1, re2) = re1 @ re2
  62.974 +          | sort (rr :: rrs) (re1, re2) =
  62.975 +              if is_simple rr
  62.976 +              then sort rrs (rr :: re1, re2)
  62.977 +              else sort rrs (re1, rr :: re2);
  62.978 +      in sort rrs ([], []) end;
  62.979 +
  62.980 +    fun proc_rews [] = NONE
  62.981 +      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  62.982 +          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
  62.983 +            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
  62.984 +             case proc ss eta_t' of
  62.985 +               NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
  62.986 +             | SOME raw_thm =>
  62.987 +                 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
  62.988 +                   ss raw_thm;
  62.989 +                  (case rews (mk_procrule ss raw_thm) of
  62.990 +                    NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
  62.991 +                      " -- does not match") ss t; proc_rews ps)
  62.992 +                  | some => some)))
  62.993 +          else proc_rews ps;
  62.994 +  in
  62.995 +    (case eta_t of
  62.996 +      Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
  62.997 +    | _ =>
  62.998 +      (case rews (sort_rrules (Net.match_term rules eta_t)) of
  62.999 +        NONE => proc_rews (Net.match_term procs eta_t)
 62.1000 +      | some => some))
 62.1001 +  end;
 62.1002 +
 62.1003 +
 62.1004 +(* conversion to apply a congruence rule to a term *)
 62.1005 +
 62.1006 +fun congc prover ss maxt cong t =
 62.1007 +  let val rthm = Thm.incr_indexes (maxt + 1) cong;
 62.1008 +      val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
 62.1009 +      val insts = Thm.match (rlhs, t)
 62.1010 +      (* Thm.match can raise Pattern.MATCH;
 62.1011 +         is handled when congc is called *)
 62.1012 +      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
 62.1013 +      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
 62.1014 +      fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
 62.1015 +  in
 62.1016 +    (case prover thm' of
 62.1017 +      NONE => err ("Congruence proof failed.  Could not prove", thm')
 62.1018 +    | SOME thm2 =>
 62.1019 +        (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
 62.1020 +          NONE => err ("Congruence proof failed.  Should not have proved", thm2)
 62.1021 +        | SOME thm2' =>
 62.1022 +            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
 62.1023 +            then NONE else SOME thm2'))
 62.1024 +  end;
 62.1025 +
 62.1026 +val (cA, (cB, cC)) =
 62.1027 +  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
 62.1028 +
 62.1029 +fun transitive1 NONE NONE = NONE
 62.1030 +  | transitive1 (SOME thm1) NONE = SOME thm1
 62.1031 +  | transitive1 NONE (SOME thm2) = SOME thm2
 62.1032 +  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
 62.1033 +
 62.1034 +fun transitive2 thm = transitive1 (SOME thm);
 62.1035 +fun transitive3 thm = transitive1 thm o SOME;
 62.1036 +
 62.1037 +fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
 62.1038 +  let
 62.1039 +    fun botc skel ss t =
 62.1040 +          if is_Var skel then NONE
 62.1041 +          else
 62.1042 +          (case subc skel ss t of
 62.1043 +             some as SOME thm1 =>
 62.1044 +               (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
 62.1045 +                  SOME (thm2, skel2) =>
 62.1046 +                    transitive2 (Thm.transitive thm1 thm2)
 62.1047 +                      (botc skel2 ss (Thm.rhs_of thm2))
 62.1048 +                | NONE => some)
 62.1049 +           | NONE =>
 62.1050 +               (case rewritec (prover, thy, maxidx) ss t of
 62.1051 +                  SOME (thm2, skel2) => transitive2 thm2
 62.1052 +                    (botc skel2 ss (Thm.rhs_of thm2))
 62.1053 +                | NONE => NONE))
 62.1054 +
 62.1055 +    and try_botc ss t =
 62.1056 +          (case botc skel0 ss t of
 62.1057 +             SOME trec1 => trec1 | NONE => (Thm.reflexive t))
 62.1058 +
 62.1059 +    and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
 62.1060 +       (case term_of t0 of
 62.1061 +           Abs (a, T, _) =>
 62.1062 +             let
 62.1063 +                 val b = Name.bound (#1 bounds);
 62.1064 +                 val (v, t') = Thm.dest_abs (SOME b) t0;
 62.1065 +                 val b' = #1 (Term.dest_Free (Thm.term_of v));
 62.1066 +                 val _ =
 62.1067 +                   if b <> b' then
 62.1068 +                     warning ("Simplifier: renamed bound variable " ^
 62.1069 +                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
 62.1070 +                   else ();
 62.1071 +                 val ss' = add_bound ((b', T), a) ss;
 62.1072 +                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
 62.1073 +             in case botc skel' ss' t' of
 62.1074 +                  SOME thm => SOME (Thm.abstract_rule a v thm)
 62.1075 +                | NONE => NONE
 62.1076 +             end
 62.1077 +         | t $ _ => (case t of
 62.1078 +             Const ("==>", _) $ _  => impc t0 ss
 62.1079 +           | Abs _ =>
 62.1080 +               let val thm = Thm.beta_conversion false t0
 62.1081 +               in case subc skel0 ss (Thm.rhs_of thm) of
 62.1082 +                    NONE => SOME thm
 62.1083 +                  | SOME thm' => SOME (Thm.transitive thm thm')
 62.1084 +               end
 62.1085 +           | _  =>
 62.1086 +               let fun appc () =
 62.1087 +                     let
 62.1088 +                       val (tskel, uskel) = case skel of
 62.1089 +                           tskel $ uskel => (tskel, uskel)
 62.1090 +                         | _ => (skel0, skel0);
 62.1091 +                       val (ct, cu) = Thm.dest_comb t0
 62.1092 +                     in
 62.1093 +                     (case botc tskel ss ct of
 62.1094 +                        SOME thm1 =>
 62.1095 +                          (case botc uskel ss cu of
 62.1096 +                             SOME thm2 => SOME (Thm.combination thm1 thm2)
 62.1097 +                           | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
 62.1098 +                      | NONE =>
 62.1099 +                          (case botc uskel ss cu of
 62.1100 +                             SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
 62.1101 +                           | NONE => NONE))
 62.1102 +                     end
 62.1103 +                   val (h, ts) = strip_comb t
 62.1104 +               in case cong_name h of
 62.1105 +                    SOME a =>
 62.1106 +                      (case AList.lookup (op =) (fst congs) a of
 62.1107 +                         NONE => appc ()
 62.1108 +                       | SOME cong =>
 62.1109 +  (*post processing: some partial applications h t1 ... tj, j <= length ts,
 62.1110 +    may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
 62.1111 +                          (let
 62.1112 +                             val thm = congc (prover ss) ss maxidx cong t0;
 62.1113 +                             val t = the_default t0 (Option.map Thm.rhs_of thm);
 62.1114 +                             val (cl, cr) = Thm.dest_comb t
 62.1115 +                             val dVar = Var(("", 0), dummyT)
 62.1116 +                             val skel =
 62.1117 +                               list_comb (h, replicate (length ts) dVar)
 62.1118 +                           in case botc skel ss cl of
 62.1119 +                                NONE => thm
 62.1120 +                              | SOME thm' => transitive3 thm
 62.1121 +                                  (Thm.combination thm' (Thm.reflexive cr))
 62.1122 +                           end handle Pattern.MATCH => appc ()))
 62.1123 +                  | _ => appc ()
 62.1124 +               end)
 62.1125 +         | _ => NONE)
 62.1126 +
 62.1127 +    and impc ct ss =
 62.1128 +      if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
 62.1129 +
 62.1130 +    and rules_of_prem ss prem =
 62.1131 +      if maxidx_of_term (term_of prem) <> ~1
 62.1132 +      then (trace_cterm true
 62.1133 +        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
 62.1134 +          ss prem; ([], NONE))
 62.1135 +      else
 62.1136 +        let val asm = Thm.assume prem
 62.1137 +        in (extract_safe_rrules (ss, asm), SOME asm) end
 62.1138 +
 62.1139 +    and add_rrules (rrss, asms) ss =
 62.1140 +      (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
 62.1141 +
 62.1142 +    and disch r prem eq =
 62.1143 +      let
 62.1144 +        val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
 62.1145 +        val eq' = Thm.implies_elim (Thm.instantiate
 62.1146 +          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
 62.1147 +          (Thm.implies_intr prem eq)
 62.1148 +      in if not r then eq' else
 62.1149 +        let
 62.1150 +          val (prem', concl) = Thm.dest_implies lhs;
 62.1151 +          val (prem'', _) = Thm.dest_implies rhs
 62.1152 +        in Thm.transitive (Thm.transitive
 62.1153 +          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
 62.1154 +             Drule.swap_prems_eq) eq')
 62.1155 +          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
 62.1156 +             Drule.swap_prems_eq)
 62.1157 +        end
 62.1158 +      end
 62.1159 +
 62.1160 +    and rebuild [] _ _ _ _ eq = eq
 62.1161 +      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
 62.1162 +          let
 62.1163 +            val ss' = add_rrules (rev rrss, rev asms) ss;
 62.1164 +            val concl' =
 62.1165 +              Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
 62.1166 +            val dprem = Option.map (disch false prem)
 62.1167 +          in
 62.1168 +            (case rewritec (prover, thy, maxidx) ss' concl' of
 62.1169 +              NONE => rebuild prems concl' rrss asms ss (dprem eq)
 62.1170 +            | SOME (eq', _) => transitive2 (fold (disch false)
 62.1171 +                  prems (the (transitive3 (dprem eq) eq')))
 62.1172 +                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
 62.1173 +          end
 62.1174 +
 62.1175 +    and mut_impc0 prems concl rrss asms ss =
 62.1176 +      let
 62.1177 +        val prems' = strip_imp_prems concl;
 62.1178 +        val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
 62.1179 +      in
 62.1180 +        mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
 62.1181 +          (asms @ asms') [] [] [] [] ss ~1 ~1
 62.1182 +      end
 62.1183 +
 62.1184 +    and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
 62.1185 +        transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
 62.1186 +            (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
 62.1187 +          (if changed > 0 then
 62.1188 +             mut_impc (rev prems') concl (rev rrss') (rev asms')
 62.1189 +               [] [] [] [] ss ~1 changed
 62.1190 +           else rebuild prems' concl rrss' asms' ss
 62.1191 +             (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
 62.1192 +
 62.1193 +      | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
 62.1194 +          prems' rrss' asms' eqns ss changed k =
 62.1195 +        case (if k = 0 then NONE else botc skel0 (add_rrules
 62.1196 +          (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
 62.1197 +            NONE => mut_impc prems concl rrss asms (prem :: prems')
 62.1198 +              (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
 62.1199 +              (if k = 0 then 0 else k - 1)
 62.1200 +          | SOME eqn =>
 62.1201 +            let
 62.1202 +              val prem' = Thm.rhs_of eqn;
 62.1203 +              val tprems = map term_of prems;
 62.1204 +              val i = 1 + fold Integer.max (map (fn p =>
 62.1205 +                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
 62.1206 +              val (rrs', asm') = rules_of_prem ss prem'
 62.1207 +            in mut_impc prems concl rrss asms (prem' :: prems')
 62.1208 +              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
 62.1209 +                (take i prems)
 62.1210 +                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
 62.1211 +                  (drop i prems, concl))))) :: eqns)
 62.1212 +                  ss (length prems') ~1
 62.1213 +            end
 62.1214 +
 62.1215 +     (*legacy code - only for backwards compatibility*)
 62.1216 +    and nonmut_impc ct ss =
 62.1217 +      let
 62.1218 +        val (prem, conc) = Thm.dest_implies ct;
 62.1219 +        val thm1 = if simprem then botc skel0 ss prem else NONE;
 62.1220 +        val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
 62.1221 +        val ss1 =
 62.1222 +          if not useprem then ss
 62.1223 +          else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
 62.1224 +      in
 62.1225 +        (case botc skel0 ss1 conc of
 62.1226 +          NONE =>
 62.1227 +            (case thm1 of
 62.1228 +              NONE => NONE
 62.1229 +            | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
 62.1230 +        | SOME thm2 =>
 62.1231 +            let val thm2' = disch false prem1 thm2 in
 62.1232 +              (case thm1 of
 62.1233 +                NONE => SOME thm2'
 62.1234 +              | SOME thm1' =>
 62.1235 +                 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
 62.1236 +            end)
 62.1237 +      end
 62.1238 +
 62.1239 + in try_botc end;
 62.1240 +
 62.1241 +
 62.1242 +(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
 62.1243 +
 62.1244 +(*
 62.1245 +  Parameters:
 62.1246 +    mode = (simplify A,
 62.1247 +            use A in simplifying B,
 62.1248 +            use prems of B (if B is again a meta-impl.) to simplify A)
 62.1249 +           when simplifying A ==> B
 62.1250 +    prover: how to solve premises in conditional rewrites and congruences
 62.1251 +*)
 62.1252 +
 62.1253 +val debug_bounds = Unsynchronized.ref false;
 62.1254 +
 62.1255 +fun check_bounds ss ct =
 62.1256 +  if ! debug_bounds then
 62.1257 +    let
 62.1258 +      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
 62.1259 +      val bs = fold_aterms (fn Free (x, _) =>
 62.1260 +          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
 62.1261 +          then insert (op =) x else I
 62.1262 +        | _ => I) (term_of ct) [];
 62.1263 +    in
 62.1264 +      if null bs then ()
 62.1265 +      else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
 62.1266 +        (Thm.theory_of_cterm ct) (Thm.term_of ct)
 62.1267 +    end
 62.1268 +  else ();
 62.1269 +
 62.1270 +fun rewrite_cterm mode prover raw_ss raw_ct =
 62.1271 +  let
 62.1272 +    val thy = Thm.theory_of_cterm raw_ct;
 62.1273 +    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
 62.1274 +    val {maxidx, ...} = Thm.rep_cterm ct;
 62.1275 +    val ss = inc_simp_depth (activate_context thy raw_ss);
 62.1276 +    val depth = simp_depth ss;
 62.1277 +    val _ =
 62.1278 +      if depth mod 20 = 0 then
 62.1279 +        if_visible ss warning ("Simplification depth " ^ string_of_int depth)
 62.1280 +      else ();
 62.1281 +    val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
 62.1282 +    val _ = check_bounds ss ct;
 62.1283 +  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
 62.1284 +
 62.1285 +val simple_prover =
 62.1286 +  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
 62.1287 +
 62.1288 +fun rewrite _ [] ct = Thm.reflexive ct
 62.1289 +  | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
 62.1290 +      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 62.1291 +
 62.1292 +fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 62.1293 +val rewrite_rule = simplify true;
 62.1294 +
 62.1295 +(*simple term rewriting -- no proof*)
 62.1296 +fun rewrite_term thy rules procs =
 62.1297 +  Pattern.rewrite_term thy (map decomp_simp' rules) procs;
 62.1298 +
 62.1299 +fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
 62.1300 +
 62.1301 +(*Rewrite the subgoals of a proof state (represented by a theorem)*)
 62.1302 +fun rewrite_goals_rule thms th =
 62.1303 +  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
 62.1304 +    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 62.1305 +
 62.1306 +(*Rewrite the subgoal of a proof state (represented by a theorem)*)
 62.1307 +fun rewrite_goal_rule mode prover ss i thm =
 62.1308 +  if 0 < i andalso i <= Thm.nprems_of thm
 62.1309 +  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
 62.1310 +  else raise THM ("rewrite_goal_rule", i, [thm]);
 62.1311 +
 62.1312 +
 62.1313 +(** meta-rewriting tactics **)
 62.1314 +
 62.1315 +(*Rewrite all subgoals*)
 62.1316 +fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 62.1317 +fun rewtac def = rewrite_goals_tac [def];
 62.1318 +
 62.1319 +(*Rewrite one subgoal*)
 62.1320 +fun asm_rewrite_goal_tac mode prover_tac ss i thm =
 62.1321 +  if 0 < i andalso i <= Thm.nprems_of thm then
 62.1322 +    Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
 62.1323 +  else Seq.empty;
 62.1324 +
 62.1325 +fun rewrite_goal_tac rews =
 62.1326 +  let val ss = empty_ss addsimps rews in
 62.1327 +    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
 62.1328 +      (global_context (Thm.theory_of_thm st) ss) i st
 62.1329 +  end;
 62.1330 +
 62.1331 +(*Prunes all redundant parameters from the proof state by rewriting.
 62.1332 +  DOES NOT rewrite main goal, where quantification over an unused bound
 62.1333 +    variable is sometimes done to avoid the need for cut_facts_tac.*)
 62.1334 +val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
 62.1335 +
 62.1336 +
 62.1337 +(* for folding definitions, handling critical pairs *)
 62.1338 +
 62.1339 +(*The depth of nesting in a term*)
 62.1340 +fun term_depth (Abs (_, _, t)) = 1 + term_depth t
 62.1341 +  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
 62.1342 +  | term_depth _ = 0;
 62.1343 +
 62.1344 +val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
 62.1345 +
 62.1346 +(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
 62.1347 +  Returns longest lhs first to avoid folding its subexpressions.*)
 62.1348 +fun sort_lhs_depths defs =
 62.1349 +  let val keylist = AList.make (term_depth o lhs_of_thm) defs
 62.1350 +      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
 62.1351 +  in map (AList.find (op =) keylist) keys end;
 62.1352 +
 62.1353 +val rev_defs = sort_lhs_depths o map Thm.symmetric;
 62.1354 +
 62.1355 +fun fold_rule defs = fold rewrite_rule (rev_defs defs);
 62.1356 +fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 62.1357 +
 62.1358 +
 62.1359 +(* HHF normal form: !! before ==>, outermost !! generalized *)
 62.1360 +
 62.1361 +local
 62.1362 +
 62.1363 +fun gen_norm_hhf ss th =
 62.1364 +  (if Drule.is_norm_hhf (Thm.prop_of th) then th
 62.1365 +   else Conv.fconv_rule
 62.1366 +    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
 62.1367 +  |> Thm.adjust_maxidx_thm ~1
 62.1368 +  |> Drule.gen_all;
 62.1369 +
 62.1370 +val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 62.1371 +
 62.1372 +in
 62.1373 +
 62.1374 +val norm_hhf = gen_norm_hhf hhf_ss;
 62.1375 +val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
 62.1376 +
 62.1377 +end;
 62.1378 +
 62.1379 +end;
 62.1380 +
 62.1381 +structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
 62.1382 +open Basic_Meta_Simplifier;
    63.1 --- a/src/Pure/simplifier.ML	Fri Dec 17 18:24:44 2010 +0100
    63.2 +++ b/src/Pure/simplifier.ML	Fri Dec 17 18:33:35 2010 +0100
    63.3 @@ -7,7 +7,7 @@
    63.4  
    63.5  signature BASIC_SIMPLIFIER =
    63.6  sig
    63.7 -  include BASIC_META_SIMPLIFIER
    63.8 +  include BASIC_RAW_SIMPLIFIER
    63.9    val change_simpset: (simpset -> simpset) -> unit
   63.10    val global_simpset_of: theory -> simpset
   63.11    val Addsimprocs: simproc list -> unit
   63.12 @@ -33,6 +33,9 @@
   63.13    val pretty_ss: Proof.context -> simpset -> Pretty.T
   63.14    val clear_ss: simpset -> simpset
   63.15    val debug_bounds: bool Unsynchronized.ref
   63.16 +  val add_simp: thm -> simpset -> simpset
   63.17 +  val del_simp: thm -> simpset -> simpset
   63.18 +  val add_prems: thm list -> simpset -> simpset
   63.19    val inherit_context: simpset -> simpset -> simpset
   63.20    val the_context: simpset -> Proof.context
   63.21    val context: Proof.context -> simpset -> simpset
   63.22 @@ -72,7 +75,7 @@
   63.23  structure Simplifier: SIMPLIFIER =
   63.24  struct
   63.25  
   63.26 -open MetaSimplifier;
   63.27 +open Raw_Simplifier;
   63.28  
   63.29  
   63.30  (** pretty printing **)
   63.31 @@ -104,7 +107,7 @@
   63.32  (
   63.33    type T = simpset;
   63.34    val empty = empty_ss;
   63.35 -  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
   63.36 +  fun extend ss = Raw_Simplifier.inherit_context empty_ss ss;
   63.37    val merge = merge_ss;
   63.38  );
   63.39  
   63.40 @@ -127,7 +130,7 @@
   63.41  fun map_simpset f = Context.theory_map (map_ss f);
   63.42  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   63.43  fun global_simpset_of thy =
   63.44 -  MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
   63.45 +  Raw_Simplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
   63.46  
   63.47  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   63.48  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   63.49 @@ -135,7 +138,7 @@
   63.50  
   63.51  (* local simpset *)
   63.52  
   63.53 -fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
   63.54 +fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
   63.55  
   63.56  val _ = ML_Antiquote.value "simpset"
   63.57    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
   63.58 @@ -215,16 +218,16 @@
   63.59  
   63.60  fun solve_all_tac solvers ss =
   63.61    let
   63.62 -    val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
   63.63 -    val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   63.64 +    val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss ss;
   63.65 +    val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   63.66    in DEPTH_SOLVE (solve_tac 1) end;
   63.67  
   63.68  (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   63.69  fun generic_simp_tac safe mode ss =
   63.70    let
   63.71 -    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
   63.72 +    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = Raw_Simplifier.internal_ss ss;
   63.73      val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
   63.74 -    val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
   63.75 +    val solve_tac = FIRST' (map (Raw_Simplifier.solver ss)
   63.76        (rev (if safe then solvers else unsafe_solvers)));
   63.77  
   63.78      fun simp_loop_tac i =
   63.79 @@ -236,15 +239,15 @@
   63.80  
   63.81  fun simp rew mode ss thm =
   63.82    let
   63.83 -    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
   63.84 +    val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss ss;
   63.85      val tacf = solve_all_tac (rev unsafe_solvers);
   63.86      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   63.87    in rew mode prover ss thm end;
   63.88  
   63.89  in
   63.90  
   63.91 -val simp_thm = simp MetaSimplifier.rewrite_thm;
   63.92 -val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   63.93 +val simp_thm = simp Raw_Simplifier.rewrite_thm;
   63.94 +val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
   63.95  
   63.96  end;
   63.97  
   63.98 @@ -323,7 +326,7 @@
   63.99  
  63.100  val simplified = conv_mode -- Attrib.thms >>
  63.101    (fn (f, ths) => Thm.rule_attribute (fn context =>
  63.102 -    f ((if null ths then I else MetaSimplifier.clear_ss)
  63.103 +    f ((if null ths then I else Raw_Simplifier.clear_ss)
  63.104          (simpset_of (Context.proof_of context)) addsimps ths)));
  63.105  
  63.106  end;
  63.107 @@ -354,14 +357,14 @@
  63.108    Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
  63.109    Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
  63.110    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
  63.111 -    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
  63.112 +    >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)]
  63.113     @ cong_modifiers;
  63.114  
  63.115  val simp_modifiers' =
  63.116   [Args.add -- Args.colon >> K (I, simp_add),
  63.117    Args.del -- Args.colon >> K (I, simp_del),
  63.118    Args.$$$ onlyN -- Args.colon
  63.119 -    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
  63.120 +    >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)]
  63.121     @ cong_modifiers;
  63.122  
  63.123  val simp_options =
    64.1 --- a/src/Sequents/Sequents.thy	Fri Dec 17 18:24:44 2010 +0100
    64.2 +++ b/src/Sequents/Sequents.thy	Fri Dec 17 18:33:35 2010 +0100
    64.3 @@ -28,9 +28,7 @@
    64.4  
    64.5  (* concrete syntax *)
    64.6  
    64.7 -nonterminals
    64.8 -  seq seqobj seqcont
    64.9 -
   64.10 +nonterminal seq and seqobj and seqcont
   64.11  
   64.12  syntax
   64.13   "_SeqEmp"         :: seq                                  ("")
    65.1 --- a/src/Tools/Code/code_preproc.ML	Fri Dec 17 18:24:44 2010 +0100
    65.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Dec 17 18:33:35 2010 +0100
    65.3 @@ -83,10 +83,10 @@
    65.4  val map_pre = map_pre_post o apfst;
    65.5  val map_post = map_pre_post o apsnd;
    65.6  
    65.7 -val add_unfold = map_pre o MetaSimplifier.add_simp;
    65.8 -val del_unfold = map_pre o MetaSimplifier.del_simp;
    65.9 -val add_post = map_post o MetaSimplifier.add_simp;
   65.10 -val del_post = map_post o MetaSimplifier.del_simp;
   65.11 +val add_unfold = map_pre o Simplifier.add_simp;
   65.12 +val del_unfold = map_pre o Simplifier.del_simp;
   65.13 +val add_post = map_post o Simplifier.add_simp;
   65.14 +val del_post = map_post o Simplifier.del_simp;
   65.15  
   65.16  fun add_unfold_post raw_thm thy =
   65.17    let
   65.18 @@ -94,7 +94,7 @@
   65.19      val thm_sym = Thm.symmetric thm;
   65.20    in
   65.21      thy |> map_pre_post (fn (pre, post) =>
   65.22 -      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym))
   65.23 +      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
   65.24    end;
   65.25  
   65.26  fun add_functrans (name, f) = (map_data o apsnd)
    66.1 --- a/src/Tools/Code/code_simp.ML	Fri Dec 17 18:24:44 2010 +0100
    66.2 +++ b/src/Tools/Code/code_simp.ML	Fri Dec 17 18:33:35 2010 +0100
    66.3 @@ -24,7 +24,7 @@
    66.4  (
    66.5    type T = simpset;
    66.6    val empty = empty_ss;
    66.7 -  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
    66.8 +  fun extend ss = Simplifier.inherit_context empty_ss ss;
    66.9    val merge = merge_ss;
   66.10  );
   66.11  
    67.1 --- a/src/Tools/atomize_elim.ML	Fri Dec 17 18:24:44 2010 +0100
    67.2 +++ b/src/Tools/atomize_elim.ML	Fri Dec 17 18:33:35 2010 +0100
    67.3 @@ -60,7 +60,7 @@
    67.4  *)
    67.5  fun atomize_elim_conv ctxt ct =
    67.6      (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
    67.7 -    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
    67.8 +    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
    67.9      then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
   67.10                           then all_conv ct'
   67.11                           else raise CTERM ("atomize_elim", [ct', ct])))
    68.1 --- a/src/Tools/coherent.ML	Fri Dec 17 18:24:44 2010 +0100
    68.2 +++ b/src/Tools/coherent.ML	Fri Dec 17 18:33:35 2010 +0100
    68.3 @@ -45,7 +45,7 @@
    68.4    if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
    68.5    else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    68.6      (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
    68.7 -     MetaSimplifier.rewrite true (map Thm.symmetric
    68.8 +     Raw_Simplifier.rewrite true (map Thm.symmetric
    68.9         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
   68.10  
   68.11  fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
    69.1 --- a/src/Tools/induct.ML	Fri Dec 17 18:24:44 2010 +0100
    69.2 +++ b/src/Tools/induct.ML	Fri Dec 17 18:33:35 2010 +0100
    69.3 @@ -420,10 +420,10 @@
    69.4  
    69.5  fun mark_constraints n ctxt = Conv.fconv_rule
    69.6    (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
    69.7 -     (MetaSimplifier.rewrite false [equal_def']))) ctxt));
    69.8 +     (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
    69.9  
   69.10  val unmark_constraints = Conv.fconv_rule
   69.11 -  (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
   69.12 +  (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
   69.13  
   69.14  
   69.15  (* simplify *)
   69.16 @@ -514,10 +514,10 @@
   69.17  (* atomize *)
   69.18  
   69.19  fun atomize_term thy =
   69.20 -  MetaSimplifier.rewrite_term thy Induct_Args.atomize []
   69.21 +  Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
   69.22    #> Object_Logic.drop_judgment thy;
   69.23  
   69.24 -val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
   69.25 +val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
   69.26  
   69.27  val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
   69.28  
   69.29 @@ -528,8 +528,8 @@
   69.30  (* rulify *)
   69.31  
   69.32  fun rulify_term thy =
   69.33 -  MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   69.34 -  MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   69.35 +  Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   69.36 +  Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   69.37  
   69.38  fun rulified_term thm =
   69.39    let
   69.40 @@ -668,7 +668,7 @@
   69.41    end);
   69.42  
   69.43  fun miniscope_tac p = CONVERSION o
   69.44 -  Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   69.45 +  Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   69.46  
   69.47  in
   69.48  
    70.1 --- a/src/ZF/ZF.thy	Fri Dec 17 18:24:44 2010 +0100
    70.2 +++ b/src/ZF/ZF.thy	Fri Dec 17 18:33:35 2010 +0100
    70.3 @@ -102,7 +102,7 @@
    70.4    where "A -> B == Pi(A, %_. B)"
    70.5  
    70.6  
    70.7 -nonterminals "is" patterns
    70.8 +nonterminal "is" and patterns
    70.9  
   70.10  syntax
   70.11    ""          :: "i => is"                   ("_")
    71.1 --- a/src/ZF/func.thy	Fri Dec 17 18:24:44 2010 +0100
    71.2 +++ b/src/ZF/func.thy	Fri Dec 17 18:33:35 2010 +0100
    71.3 @@ -445,8 +445,7 @@
    71.4    update  :: "[i,i,i] => i"  where
    71.5     "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
    71.6  
    71.7 -nonterminals
    71.8 -  updbinds  updbind
    71.9 +nonterminal updbinds and updbind
   71.10  
   71.11  syntax
   71.12