added 'split' method;
authorwenzelm
Mon Aug 28 20:29:56 2000 +0200 (2000-08-28)
changeset 9703bf65780eed02
parent 9702 f23bee3c0682
child 9704 c2f2f70bbb60
added 'split' method;
doc-src/IsarRef/generic.tex
src/Provers/splitter.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:19 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:56 2000 +0200
     1.3 @@ -620,16 +620,19 @@
     1.4  
     1.5  \section{Basic equational reasoning}
     1.6  
     1.7 -\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisaratt{symmetric}
     1.8 +\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
     1.9  \begin{matharray}{rcl}
    1.10    subst & : & \isarmeth \\
    1.11    hypsubst^* & : & \isarmeth \\
    1.12 +  split & : & \isarmeth \\
    1.13    symmetric & : & \isaratt \\
    1.14  \end{matharray}
    1.15  
    1.16  \begin{rail}
    1.17    'subst' thmref
    1.18    ;
    1.19 +  'split' thmrefs
    1.20 +  ;
    1.21  \end{rail}
    1.22  
    1.23  These methods and attributes provide basic facilities for equational reasoning
    1.24 @@ -642,6 +645,9 @@
    1.25  \item [$subst~thm$] performs a single substitution step using rule $thm$,
    1.26    which may be either a meta or object equality.
    1.27  \item [$hypsubst$] performs substitution using some assumption.
    1.28 +\item [$split~thms$] performs single-step case splitting using rules $thms$.
    1.29 +  Note that the $simp$ method already involves repeated application of split
    1.30 +  rules as declared in the current context (see \S\ref{sec:simp}).
    1.31  \item [$symmetric$] applies the symmetry rule of meta or object equality.
    1.32  \end{descr}
    1.33  
     2.1 --- a/src/Provers/splitter.ML	Mon Aug 28 20:29:19 2000 +0200
     2.2 +++ b/src/Provers/splitter.ML	Mon Aug 28 20:29:56 2000 +0200
     2.3 @@ -412,21 +412,22 @@
     2.4   (Attrib.add_del_args split_add_global split_del_global,
     2.5    Attrib.add_del_args split_add_local split_del_local);
     2.6  
     2.7 -val setup_attrs =
     2.8 -  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
     2.9  
    2.10 -
    2.11 -(* method modifiers *)
    2.12 +(* methods *)
    2.13  
    2.14  val split_modifiers =
    2.15   [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
    2.16    Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
    2.17    Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
    2.18  
    2.19 +val split_meth = Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o split_tac);
    2.20 +
    2.21  
    2.22  
    2.23  (** theory setup **)
    2.24  
    2.25 -val setup = [setup_attrs];
    2.26 +val setup =
    2.27 + [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
    2.28 +  Method.add_methods [(splitN, split_meth, "apply splitter rule")]];
    2.29  
    2.30  end;