# HG changeset patch # User paulson # Date 863015346 -7200 # Node ID d01d4c0c4b4400190ad21a93fee4795c4f358436 # Parent 4cc2fe62f7c321910ae23a6ebf5aa68518fe5088 New acknowledgements; fixed overfull lines and tables diff -r 4cc2fe62f7c3 -r d01d4c0c4b44 doc-src/Ref/goals.tex --- a/doc-src/Ref/goals.tex Wed May 07 16:26:28 1997 +0200 +++ b/doc-src/Ref/goals.tex Wed May 07 16:29:06 1997 +0200 @@ -393,13 +393,15 @@ \section{Executing batch proofs} -\index{batch execution} +\index{batch execution}% +To save space below, let type \texttt{tacfun} abbreviate \texttt{thm list -> + tactic list}, which is the type of a tactical proof. \begin{ttbox} -prove_goal : theory-> string->(thm list->tactic list)->thm -qed_goal : string->theory-> string->(thm list->tactic list)->unit -prove_goalw: theory->thm list->string->(thm list->tactic list)->thm -qed_goalw : string->theory->thm list->string->(thm list->tactic list)->unit -prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm +prove_goal : theory -> string -> tacfun -> thm +qed_goal : string -> theory -> string -> tacfun -> unit +prove_goalw: theory -> thm list -> string -> tacfun -> thm +qed_goalw : string -> theory -> thm list -> string -> tacfun -> unit +prove_goalw_cterm: thm list -> cterm -> tacfun -> thm \end{ttbox} These batch functions create an initial proof state, then apply a tactic to it, yielding a sequence of final proof states. The head of the sequence is diff -r 4cc2fe62f7c3 -r d01d4c0c4b44 doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Wed May 07 16:26:28 1997 +0200 +++ b/doc-src/Ref/ref.tex Wed May 07 16:29:06 1997 +0200 @@ -1,9 +1,8 @@ \documentclass[12pt]{report} -\usepackage{a4} +\usepackage{a4,proof} \makeatletter \input{../rail.sty} -\input{../proof.sty} \input{../iman.sty} \input{../extra.sty} \makeatother @@ -16,19 +15,19 @@ %%% needs chapter on Provers/typedsimp.ML? \title{The Isabelle Reference Manual} -\author{{\em Lawrence C. Paulson}% +\author{{\em Lawrence C. Paulson}\\ + Computer Laboratory \\ University of Cambridge \\ + \texttt{lcp@cl.cam.ac.uk}\\[3ex] + With Contributions by Tobias Nipkow and Markus Wenzel% \thanks{Tobias Nipkow, of T. U. Munich, wrote most of Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to Chapter~\protect\ref{theories}. Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others suggested changes - and corrections. The research has been funded by the SERC (grants - GR/G53279, GR/H40570) and by ESPRIT project 6453: Types.} -\\ -Computer Laboratory \\ University of Cambridge \\[2ex] -\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}\\[3cm] -Copyright \copyright{} \number\year{} by Lawrence C. Paulson} + and corrections. The research has been funded by the EPSRC (grants + GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453: + Types.}} \makeindex diff -r 4cc2fe62f7c3 -r d01d4c0c4b44 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Wed May 07 16:26:28 1997 +0200 +++ b/doc-src/Ref/simplifier.tex Wed May 07 16:29:06 1997 +0200 @@ -269,7 +269,7 @@ The solver is a pair of tactics that attempt to solve a subgoal after simplification. Typically it just proves trivial subgoals such as {\tt True} and $t=t$. It could use sophisticated means such as {\tt - fast_tac}, though that could make simplification expensive. + blast_tac}, though that could make simplification expensive. Rewriting does not instantiate unknowns. For example, rewriting cannot prove $a\in \Var{A}$ since this requires @@ -306,7 +306,7 @@ should call the simplifier at some point. The simplifier will then call the solver, which must therefore be prepared to solve goals of the form $t = \Var{x}$, usually by reflexivity. In particular, reflexivity should be -tried before any of the fancy tactics like {\tt fast_tac}. +tried before any of the fancy tactics like {\tt blast_tac}. It may even happen that due to simplification the subgoal is no longer an equality. For example $False \bimp \Var{Q}$ could be rewritten to @@ -366,14 +366,16 @@ \index{*Asm_full_simp_tac} \begin{ttbox} -infix 4 setsubgoaler setloop addloop setSSolver addSSolver setSolver addSolver +infix 4 setsubgoaler setloop addloop + setSSolver addSSolver setSolver addSolver setmksimps addsimps delsimps addeqcongs deleqcongs; signature SIMPLIFIER = sig type simpset val empty_ss: simpset - val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list, + val rep_ss: simpset -> {simps: thm list, procs: string list, + congs: thm list, subgoal_tac: simpset -> int -> tactic, loop_tac: int -> tactic, finish_tac: thm list -> int -> tactic, @@ -758,7 +760,7 @@ \begin{ttbox} 2 * sum (\%i. i) (Suc n) = n * Suc n 1. !!n1. n1 + sum (\%i. i) n1 + (n1 + sum (\%i. i) n1) = n1 + n1 * n1 - ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i. i) n1)) = + ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i.i) n1)) = n1 + (n1 + (n1 + n1 * n1)) \end{ttbox} Ordered rewriting proves this by sorting the left-hand side. Proving @@ -774,7 +776,7 @@ signs: \begin{ttbox} val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" - (fn _ => [fast_tac HOL_cs 1]); + (fn _ => [Blast_tac 1]); \end{ttbox} This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs in the conclusion but not~$s$, can often be brought into the right form. diff -r 4cc2fe62f7c3 -r d01d4c0c4b44 doc-src/Ref/substitution.tex --- a/doc-src/Ref/substitution.tex Wed May 07 16:26:28 1997 +0200 +++ b/doc-src/Ref/substitution.tex Wed May 07 16:29:06 1997 +0200 @@ -126,11 +126,11 @@ sig structure Simplifier : SIMPLIFIER val dest_eq : term -> term*term - val eq_reflection : thm (* a=b ==> a==b *) - val imp_intr : thm (* (P ==> Q) ==> P-->Q *) - val rev_mp : thm (* [| P; P-->Q |] ==> Q *) - val subst : thm (* [| a=b; P(a) |] ==> P(b) *) - val sym : thm (* a=b ==> b=a *) + val eq_reflection : thm (* a=b ==> a==b *) + val imp_intr : thm (* (P ==> Q) ==> P-->Q *) + val rev_mp : thm (* [| P; P-->Q |] ==> Q *) + val subst : thm (* [| a=b; P(a) |] ==> P(b) *) + val sym : thm (* a=b ==> b=a *) end; \end{ttbox} Thus, the functor requires the following items: diff -r 4cc2fe62f7c3 -r d01d4c0c4b44 doc-src/Ref/syntax.tex --- a/doc-src/Ref/syntax.tex Wed May 07 16:26:28 1997 +0200 +++ b/doc-src/Ref/syntax.tex Wed May 07 16:29:06 1997 +0200 @@ -813,7 +813,7 @@ if 0 mem (loose_bnos B) then let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in list_comb - (Const (q, dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts) + (Const (q,dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts) end else list_comb (Const (r, dummyT) $ A $ B, ts) | dependent_tr' _ _ = raise Match;