--- a/doc-src/IsarImplementation/Thy/document/logic.tex Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Fri Sep 15 22:56:08 2006 +0200
@@ -134,6 +134,8 @@
\indexmltype{typ}\verb|type typ| \\
\indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
\indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
\indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
\indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
@@ -317,10 +319,12 @@
\begin{mldecls}
\indexmltype{term}\verb|type term| \\
\indexml{op aconv}\verb|op aconv: term * term -> bool| \\
- \indexml{map-term-types}\verb|map_term_types: (typ -> typ) -> term -> term| \\ %FIXME rename map_types
+ \indexml{map-types}\verb|map_types: (typ -> typ) -> term -> term| \\
\indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
\indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
\indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexml{fastype-of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
@@ -341,7 +345,7 @@
on type \verb|term|; raw datatype equality should only be used
for operations related to parsing or printing!
- \item \verb|map_term_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
+ \item \verb|map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
\item \verb|fold_types|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term
structure is traversed from left to right.
@@ -574,10 +578,12 @@
\begin{mldecls}
\indexmltype{ctyp}\verb|type ctyp| \\
\indexmltype{cterm}\verb|type cterm| \\
+ \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
+ \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{thm}\verb|type thm| \\
\indexml{proofs}\verb|proofs: int ref| \\
- \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
- \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
\indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
\indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
\indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
@@ -587,6 +593,8 @@
\indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
\indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
\indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
\indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
\indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
@@ -601,9 +609,13 @@
well-typedness) checks, relative to the declarations of type
constructors, constants etc. in the theory.
- This representation avoids syntactic rechecking in tight loops of
- inferences. There are separate operations to decompose certified
- entities (including actual theorems).
+ \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|cterm_of|~\isa{thy\ t} explicitly checks types and terms, respectively. This also
+ involves some basic normalizations, such expansion of type and term
+ abbreviations from the theory context.
+
+ Re-certification is relatively slow and should be avoided in tight
+ reasoning loops. There are separate operations to decompose
+ certified entities (including actual theorems).
\item \verb|thm| represents proven propositions. This is an
abstract datatype that guarantees that its values have been
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Sep 15 22:56:08 2006 +0200
@@ -177,7 +177,9 @@
\indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
\indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
\indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
- \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
+ \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{theory-ref}\verb|type theory_ref| \\
\indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
\indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
@@ -555,7 +557,9 @@
\indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
\indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
+ \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
\indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
\end{mldecls}
@@ -634,7 +638,9 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{Name.internal}\verb|Name.internal: string -> string| \\
- \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
+ \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{Name.context}\verb|type Name.context| \\
\indexml{Name.context}\verb|Name.context: Name.context| \\
\indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
@@ -805,11 +811,15 @@
\indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
\indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
\indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
- \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
+ \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
\indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
\indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
- \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
+ \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
\indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
\indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 15 22:56:08 2006 +0200
@@ -329,10 +329,14 @@
\indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
\indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
+ \end{mldecls}
+ \begin{mldecls}
\indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Fri Sep 15 22:56:08 2006 +0200
@@ -76,7 +76,7 @@
\[
\infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
- \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
+ \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{C}}{\isa{{\isacharhash}C}}
\]
\medskip The following low-level variants admit general reasoning
--- a/doc-src/IsarImplementation/Thy/logic.thy Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Fri Sep 15 22:56:08 2006 +0200
@@ -123,6 +123,8 @@
@{index_ML_type typ} \\
@{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
@{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
@{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
@@ -315,10 +317,12 @@
\begin{mldecls}
@{index_ML_type term} \\
@{index_ML "op aconv": "term * term -> bool"} \\
- @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\ %FIXME rename map_types
+ @{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"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
@@ -341,7 +345,7 @@
on type @{ML_type term}; raw datatype equality should only be used
for operations related to parsing or printing!
- \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
+ \item @{ML 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
@@ -576,10 +580,12 @@
\begin{mldecls}
@{index_ML_type ctyp} \\
@{index_ML_type cterm} \\
+ @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
+ @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type thm} \\
@{index_ML proofs: "int ref"} \\
- @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
- @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
@{index_ML Thm.assume: "cterm -> thm"} \\
@{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
@{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
@@ -589,6 +595,8 @@
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
@{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
@{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
@{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
@{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
@@ -603,9 +611,14 @@
well-typedness) checks, relative to the declarations of type
constructors, constants etc. in the theory.
- This representation avoids syntactic rechecking in tight loops of
- inferences. There are separate operations to decompose certified
- entities (including actual theorems).
+ \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
+ t"} explicitly checks types and terms, respectively. This also
+ involves some basic normalizations, such expansion of type and term
+ abbreviations from the theory context.
+
+ Re-certification is relatively slow and should be avoided in tight
+ reasoning loops. There are separate operations to decompose
+ certified entities (including actual theorems).
\item @{ML_type thm} represents proven propositions. This is an
abstract datatype that guarantees that its values have been
--- a/doc-src/IsarImplementation/Thy/prelim.thy Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Fri Sep 15 22:56:08 2006 +0200
@@ -152,7 +152,9 @@
@{index_ML Theory.subthy: "theory * theory -> bool"} \\
@{index_ML Theory.merge: "theory * theory -> theory"} \\
@{index_ML Theory.checkpoint: "theory -> theory"} \\
- @{index_ML Theory.copy: "theory -> theory"} \\[1ex]
+ @{index_ML Theory.copy: "theory -> theory"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type theory_ref} \\
@{index_ML Theory.self_ref: "theory -> theory_ref"} \\
@{index_ML Theory.deref: "theory_ref -> theory"} \\
@@ -480,7 +482,9 @@
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
- @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
+ @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type "Symbol.sym"} \\
@{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
\end{mldecls}
@@ -552,7 +556,9 @@
text %mlref {*
\begin{mldecls}
@{index_ML Name.internal: "string -> string"} \\
- @{index_ML Name.skolem: "string -> string"} \\[1ex]
+ @{index_ML Name.skolem: "string -> string"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type Name.context} \\
@{index_ML Name.context: Name.context} \\
@{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
@@ -697,11 +703,15 @@
@{index_ML NameSpace.qualifier: "string -> string"} \\
@{index_ML NameSpace.append: "string -> string -> string"} \\
@{index_ML NameSpace.pack: "string list -> string"} \\
- @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
+ @{index_ML NameSpace.unpack: "string -> string list"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type NameSpace.naming} \\
@{index_ML NameSpace.default_naming: NameSpace.naming} \\
@{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
- @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
+ @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML_type NameSpace.T} \\
@{index_ML NameSpace.empty: NameSpace.T} \\
@{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
--- a/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 15 22:56:08 2006 +0200
@@ -290,10 +290,14 @@
"({context: Proof.context, schematics: ctyp list * cterm list,
params: cterm list, asms: cterm list, concl: cterm,
prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
@{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
+ \end{mldecls}
+ \begin{mldecls}
@{index_ML Obtain.result: "(Proof.context -> tactic) ->
thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/tactic.thy Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Fri Sep 15 22:56:08 2006 +0200
@@ -61,7 +61,7 @@
\[
\infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
- \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
+ \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
\]
\medskip The following low-level variants admit general reasoning
--- a/doc-src/IsarImplementation/style.sty Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/style.sty Fri Sep 15 22:56:08 2006 +0200
@@ -37,7 +37,7 @@
\renewcommand{\isadigit}[1]{\isamath{#1}}
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
+\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
\isafoldtag{FIXME}
\isakeeptag{mlref}
--- a/src/HOL/Algebra/ringsimp.ML Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Fri Sep 15 22:56:08 2006 +0200
@@ -8,7 +8,7 @@
signature ALGEBRA =
sig
val print_structures: Context.generic -> unit
- val setup: Theory.theory -> Theory.theory
+ val setup: theory -> theory
end;
structure Algebra: ALGEBRA =
@@ -17,7 +17,7 @@
(** Theory and context data **)
-fun struct_eq ((s1, ts1), (s2, ts2)) =
+fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
structure AlgebraData = GenericDataFun
--- a/src/HOL/Real/Float.ML Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Real/Float.ML Fri Sep 15 22:56:08 2006 +0200
@@ -458,7 +458,7 @@
end
| _ => raise exn
)
-val th = ref ([]: Theory.theory list)
+val th = ref ([]: theory list)
val sg = ref ([]: Sign.sg list)
fun invoke_float_op c =
@@ -507,4 +507,4 @@
invoke_oracle th "nat_op" (sg, Nat_op_oracle_data c)
end
*)
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/cnf_funcs.ML Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Sep 15 22:56:08 2006 +0200
@@ -42,8 +42,8 @@
val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *)
- val make_cnf_thm : Theory.theory -> Term.term -> Thm.thm
- val make_cnfx_thm : Theory.theory -> Term.term -> Thm.thm
+ val make_cnf_thm : theory -> Term.term -> Thm.thm
+ val make_cnfx_thm : theory -> Term.term -> Thm.thm
val cnf_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to CNF *)
val cnfx_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to (almost) definitional CNF *)
end;
@@ -176,8 +176,6 @@
(* inst_thm: instantiates a theorem with a list of terms *)
(* ------------------------------------------------------------------------- *)
-(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
-
fun inst_thm thy ts thm =
instantiate' [] (map (SOME o cterm_of thy) ts) thm;
--- a/src/HOL/Tools/res_atpset.ML Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Tools/res_atpset.ML Fri Sep 15 22:56:08 2006 +0200
@@ -84,7 +84,7 @@
val extend = copy;
fun merge _ (ref atpst1, ref atpst2) =
ref (merge_atpset (atpst1, atpst2));
- fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
+ fun print _ (ref atpst) = print_atpset atpst;
end);
val print_AtpSet = GlobalAtpSet.print;
@@ -138,4 +138,4 @@
val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
-end;
\ No newline at end of file
+end;