18537

1 


2 
(* $Id$ *)


3 


4 
theory "proof" imports base begin


5 


6 
chapter {* Structured reasoning *}


7 


8 
section {* Proof context *}


9 

20026

10 
subsection {* Local variables *}


11 

20064

12 
text FIXME


13 

20026

14 
text %mlref {*


15 
\begin{mldecls}


16 
@{index_ML Variable.declare_term: "term > Proof.context > Proof.context"} \\

20064

17 
@{index_ML Variable.add_fixes: "string list > Proof.context > string list * Proof.context"} \\

20026

18 
@{index_ML Variable.import: "bool > thm list > Proof.context > thm list * Proof.context"} \\


19 
@{index_ML Variable.export: "Proof.context > Proof.context > thm list > thm list"} \\


20 
@{index_ML Variable.trade: "Proof.context > (thm list > thm list) > thm list > thm list"} \\


21 
@{index_ML Variable.monomorphic: "Proof.context > term list > term list"} \\


22 
@{index_ML Variable.polymorphic: "Proof.context > term list > term list"} \\


23 
\end{mldecls}


24 


25 
\begin{description}


26 

20064

27 
\item @{ML Variable.declare_term}~@{text "t ctxt"} declares term


28 
@{text "t"} to belong to the context. This fixes free type


29 
variables, but not term variables. Constraints for type and term


30 
variables are declared uniformly.


31 


32 
\item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term


33 
variables @{text "xs"} and returns the internal names of the


34 
resulting Skolem constants. Note that term fixes refer to


35 
\emph{all} type instances that may occur in the future.


36 


37 
\item @{ML Variable.invent_fixes} is similar to @{ML


38 
Variable.add_fixes}, but the given names merely act as hints for


39 
internal fixes produced here.

20026

40 

20064

41 
\item @{ML Variable.import}~@{text "open ths ctxt"} augments the


42 
context by new fixes for the schematic type and term variables


43 
occurring in @{text "ths"}. The @{text "open"} flag indicates


44 
whether the fixed names should be accessible to the user, otherwise


45 
internal names are chosen.

20026

46 

20064

47 
\item @{ML Variable.export}~@{text "inner outer ths"} generalizes


48 
fixed type and term variables in @{text "ths"} according to the


49 
difference of the @{text "inner"} and @{text "outer"} context. Note


50 
that type variables occurring in term variables are still fixed.


51 


52 
@{ML Variable.export} essentially reverses the effect of @{ML


53 
Variable.import} (up to renaming of schematic variables.

20026

54 


55 
\item @{ML Variable.trade} composes @{ML Variable.import} and @{ML

20041

56 
Variable.export}, i.e.\ it provides a view on facts with all


57 
variables being fixed in the current context.

20026

58 

20064

59 
\item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed


60 
type variables for the schematic ones in @{text "ts"}.

20026

61 

20064

62 
\item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type


63 
variables in @{text "ts"} as far as possible, even those occurring


64 
in fixed term variables. This operation essentially reverses the


65 
default policy of typeinference to introduce local polymorphism as


66 
fixed types.

20026

67 


68 
\end{description}


69 
*}


70 

18537

71 
text FIXME


72 


73 
section {* Proof state *}


74 


75 
text {*


76 
FIXME


77 


78 
\glossary{Proof state}{The whole configuration of a structured proof,


79 
consisting of a \seeglossary{proof context} and an optional


80 
\seeglossary{structured goal}. Internally, an Isar proof state is


81 
organized as a stack to accomodate block structure of proof texts.


82 
For historical reasons, a lowlevel \seeglossary{tactical goal} is


83 
occasionally called ``proof state'' as well.}


84 


85 
\glossary{Structured goal}{FIXME}


86 


87 
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}


88 


89 


90 
*}


91 


92 
section {* Methods *}


93 


94 
text FIXME


95 


96 
section {* Attributes *}


97 


98 
text FIXME


99 


100 
end
