# HG changeset patch # User wenzelm # Date 1286971523 -3600 # Node ID cb6634eb89263f123691d4b4c15b5b9fb409e1a2 # Parent 50f42116ebdb9dd1d5bd3f378cfb167aa99d840f examples in Isabelle/HOL; tuned; diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/IsaMakefile --- a/doc-src/IsarImplementation/IsaMakefile Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/IsaMakefile Wed Oct 13 13:05:23 2010 +0100 @@ -19,13 +19,13 @@ ## sessions -Thy: $(LOG)/Pure-Thy.gz +Thy: $(LOG)/HOL-Thy.gz -$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \ +$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \ Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy \ Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy \ Thy/ML_old.thy ../antiquote_setup.ML - @$(USEDIR) Pure Thy + @$(USEDIR) HOL Thy @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ Thy/document/pdfsetup.sty Thy/document/session.tex @@ -33,4 +33,4 @@ ## clean clean: - @rm -f $(LOG)/Pure-Thy.gz + @rm -f $(LOG)/HOL-Thy.gz diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Base.thy --- a/doc-src/IsarImplementation/Thy/Base.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Base.thy Wed Oct 13 13:05:23 2010 +0100 @@ -1,5 +1,5 @@ theory Base -imports Pure +imports Main uses "../../antiquote_setup.ML" begin diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 13:05:23 2010 +0100 @@ -5,8 +5,6 @@ chapter {* Isar language elements *} text {* - %FIXME proper formal markup of methods!? - The Isar proof language (see also \cite[\S2]{isabelle-isar-ref}) consists of three main categories of language elements: @@ -23,7 +21,7 @@ \item Proof \emph{methods} define a secondary language of mixed forward-backward refinement steps involving facts and goals. - Typical examples are @{method rule}, @{method unfold}, and @{text + Typical examples are @{method rule}, @{method unfold}, and @{method simp}. Methods can occur in certain well-defined parts of the Isar proof @@ -103,7 +101,7 @@ \item @{ML Proof.simple_goal}~@{text "state"} returns the structured Isar goal (if available) in the form seen by ``simple'' methods - (like @{text simp} or @{text blast}). The Isar goal facts are + (like @{method simp} or @{method blast}). The Isar goal facts are already inserted as premises into the subgoals, which are presented individually as in @{ML Proof.goal}. @@ -114,9 +112,9 @@ \item @{ML Proof.raw_goal}~@{text "state"} returns the structured Isar goal (if available) in the raw internal form seen by ``raw'' - methods (like @{text induct}). This form is rarely appropriate for - dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} should - be used in most situations. + methods (like @{method induct}). This form is rarely appropriate + for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} + should be used in most situations. \item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"} initializes a toplevel Isar proof state within a given context. @@ -162,7 +160,7 @@ text %mlex {* The following example peeks at a certain goal configuration. *} example_proof - have "PROP A" and "PROP B" and "PROP C" + have A and B and C ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *} oops @@ -228,13 +226,14 @@ \begin{enumerate} - \item structured method with cases, e.g.\ @{text "induct"} + \item structured method with cases, e.g.\ @{method "induct"} - \item regular method: strong emphasis on facts, e.g.\ @{text "rule"} + \item regular method: strong emphasis on facts, e.g.\ @{method "rule"} - \item simple method: weak emphasis on facts, merely inserted into subgoals, e.g.\ @{text "simp"} + \item simple method: weak emphasis on facts, merely inserted into + subgoals, e.g.\ @{method "simp"} - \item old-style tactic emulation, e.g. @{text "rule_tac"} + \item old-style tactic emulation, e.g. @{method "rule_tac"} \begin{itemize} diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Oct 13 13:05:23 2010 +0100 @@ -121,8 +121,8 @@ @{index_ML_type sort: "class list"} \\ @{index_ML_type arity: "string * sort list * sort"} \\ @{index_ML_type typ} \\ - @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\ - @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ + @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\ + @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ \end{mldecls} \begin{mldecls} @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ @@ -149,13 +149,14 @@ \item @{ML_type typ} represents types; this is a datatype with constructors @{ML TFree}, @{ML TVar}, @{ML Type}. - \item @{ML map_atyps}~@{text "f \"} applies the mapping @{text "f"} - to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text - "\"}. + \item @{ML Term.map_atyps}~@{text "f \"} applies the mapping @{text + "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in + @{text "\"}. - \item @{ML fold_atyps}~@{text "f \"} iterates the operation @{text - "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar}) - in @{text "\"}; the type structure is traversed from left to right. + \item @{ML Term.fold_atyps}~@{text "f \"} iterates the operation + @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML + TVar}) in @{text "\"}; the type structure is traversed from left to + right. \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"} tests the subsort relation @{text "s\<^isub>1 \ s\<^isub>2"}. @@ -354,10 +355,10 @@ \begin{mldecls} @{index_ML_type term} \\ @{index_ML "op aconv": "term * term -> bool"} \\ - @{index_ML map_types: "(typ -> typ) -> term -> term"} \\ - @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ - @{index_ML map_aterms: "(term -> term) -> term -> term"} \\ - @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\ + @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\ + @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ + @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\ + @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\ \end{mldecls} \begin{mldecls} @{index_ML fastype_of: "term -> typ"} \\ @@ -383,20 +384,20 @@ on type @{ML_type term}; raw datatype equality should only be used for operations related to parsing or printing! - \item @{ML map_types}~@{text "f t"} applies the mapping @{text + \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text "f"} to all types occurring in @{text "t"}. - \item @{ML fold_types}~@{text "f t"} iterates the operation @{text - "f"} over all occurrences of types in @{text "t"}; the term + \item @{ML Term.fold_types}~@{text "f t"} iterates the operation + @{text "f"} over all occurrences of types in @{text "t"}; the term structure is traversed from left to right. - \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"} - to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML + \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text + "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}) occurring in @{text "t"}. - \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text - "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free}, - @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is + \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation + @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML + Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is traversed from left to right. \item @{ML fastype_of}~@{text "t"} determines the type of a diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 13:05:23 2010 +0100 @@ -1081,8 +1081,8 @@ ML {* Binding.pos_of @{binding here} *} -text {* \medskip That position can be also printed in a message as - follows. *} +text {* \medskip\noindent That position can be also printed in a + message as follows. *} ML_command {* writeln diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Wed Oct 13 13:05:23 2010 +0100 @@ -159,12 +159,8 @@ \end{description} *} -text %mlex {* The following example (in theory @{theory Pure}) shows - how to work with fixed term and type parameters and with - type-inference. -*} - -typedecl foo -- {* some basic type for testing purposes *} +text %mlex {* The following example shows how to work with fixed term + and type parameters and with type-inference. *} ML {* (*static compile-time context -- for testing only*) @@ -178,11 +174,11 @@ val t1' = singleton (Variable.polymorphic ctxt1) t1; (*term u enforces specific type assignment*) - val u = Syntax.read_term ctxt1 "(x::foo) \ y"; + val u = Syntax.read_term ctxt1 "(x::nat) \ y"; (*official declaration of u -- propagates constraints etc.*) val ctxt2 = ctxt1 |> Variable.declare_term u; - val t2 = Syntax.read_term ctxt2 "x"; (*x::foo is enforced*) + val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*) *} text {* In the above example, the starting context had been derived