--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu May 08 22:05:15 2008 +0200
@@ -4,7 +4,7 @@
imports HOLCF
begin
-chapter {* HOLCF specific elements *}
+chapter {* Isabelle/HOLCF \label{ch:holcf} *}
section {* Mixfix syntax for continuous operations *}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 08 22:05:15 2008 +0200
@@ -4,7 +4,7 @@
imports Main
begin
-chapter {* HOL specific elements \label{ch:logics} *}
+chapter {* Isabelle/HOL \label{ch:hol} *}
section {* Primitive types \label{sec:hol-typedef} *}
@@ -151,7 +151,7 @@
the literature. The more part of a record scheme may be
instantiated by zero or more further components. For example, the
previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
- c, \<dots> = m'"}, where @{text m'} refers to a different more part.
+ c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
Fixed records are special instances of record schemes, where
``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
@@ -165,8 +165,8 @@
\item the more part is internalized, as a free term or type
variable,
- \item field names are externalized, they cannot be accessed within the logic
- as first-class values.
+ \item field names are externalized, they cannot be accessed within
+ the logic as first-class values.
\end{enumerate}
@@ -243,8 +243,8 @@
any field (including ``@{text more}''):
\begin{matharray}{lll}
- @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
- @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
+ @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
+ @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
\end{matharray}
There is special syntax for application of updates: @{text "r\<lparr>x :=
@@ -262,7 +262,7 @@
constructor function:
\begin{matharray}{lll}
- @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
+ @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
\end{matharray}
\medskip We now reconsider the case of non-root records, which are
@@ -275,29 +275,32 @@
fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
the above record operations will get the following types:
- \begin{matharray}{lll}
- @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
+ \medskip
+ \begin{tabular}{lll}
+ @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
@{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
- \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
- \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
- @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
- \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
- \end{matharray}
- \noindent
+ \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
+ \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
+ @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
+ \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
+ \end{tabular}
+ \medskip
- \medskip Some further operations address the extension aspect of a
+ \noindent Some further operations address the extension aspect of a
derived record scheme specifically: @{text "t.fields"} produces a
record fragment consisting of exactly the new fields introduced here
(the result may serve as a more part elsewhere); @{text "t.extend"}
takes a fixed record and adds a given more part; @{text
"t.truncate"} restricts a record scheme to a fixed record.
- \begin{matharray}{lll}
- @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
- @{text "t.extend"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr> \<Rightarrow>
- \<zeta> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
- @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
- \end{matharray}
+ \medskip
+ \begin{tabular}{lll}
+ @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
+ @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
+ \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
+ @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
+ \end{tabular}
+ \medskip
\noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
for root records.
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Thu May 08 22:05:15 2008 +0200
@@ -4,7 +4,7 @@
imports Main
begin
-chapter {* ML tactic expressions \label{sec:conv-tac} *}
+chapter {* ML tactic expressions *}
text {*
Isar Proof methods closely resemble traditional tactics, when used
--- a/doc-src/IsarRef/Thy/Quick_Reference.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Thu May 08 22:05:15 2008 +0200
@@ -20,65 +20,78 @@
@{command "using"}~@{text a} & indicate use of additional facts \\
@{command "unfolding"}~@{text a} & unfold definitional equations \\
@{command "proof"}~@{text "m\<^sub>1"}~\dots~@{command "qed"}~@{text "m\<^sub>2"} & indicate proof structure and refinements \\
- @{command "{"}~\dots~@{command "}"} & indicate explicit blocks \\
+ @{command "{"}~@{text "\<dots>"}~@{command "}"} & indicate explicit blocks \\
@{command "next"} & switch blocks \\
@{command "note"}~@{text "a = b"} & reconsider facts \\
@{command "let"}~@{text "p = t"} & abbreviate terms by higher-order matching \\
\end{tabular}
- \begin{matharray}{rcl}
- @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
+ \medskip
+
+ \begin{tabular}{rcl}
+ @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
@{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
- & \Or & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
+ & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
@{text prfx} & = & @{command "apply"}~@{text method} \\
- & \Or & @{command "using"}~@{text "facts"} \\
- & \Or & @{command "unfolding"}~@{text "facts"} \\
+ & @{text "|"} & @{command "using"}~@{text "facts"} \\
+ & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
@{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
- & \Or & @{command "next"} \\
- & \Or & @{command "note"}~@{text "name = facts"} \\
- & \Or & @{command "let"}~@{text "term = term"} \\
- & \Or & @{command "fix"}~@{text "var\<^sup>+"} \\
- & \Or & @{command "assume"}~@{text "name: props"} \\
- & \Or & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
+ & @{text "|"} & @{command "next"} \\
+ & @{text "|"} & @{command "note"}~@{text "name = facts"} \\
+ & @{text "|"} & @{command "let"}~@{text "term = term"} \\
+ & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\
+ & @{text "|"} & @{command "assume"}~@{text "name: props"} \\
+ & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
@{text goal} & = & @{command "have"}~@{text "name: props proof"} \\
- & \Or & @{command "show"}~@{text "name: props proof"} \\
- \end{matharray}
+ & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\
+ \end{tabular}
*}
subsection {* Abbreviations and synonyms *}
text {*
- \begin{matharray}{rcl}
- @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & \equiv & @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
- @{command ".."} & \equiv & @{command "by"}~@{text rule} \\
- @{command "."} & \equiv & @{command "by"}~@{text this} \\
- @{command "hence"} & \equiv & @{command "then"}~@{command "have"} \\
- @{command "thus"} & \equiv & @{command "then"}~@{command "show"} \\
- @{command "from"}~@{text a} & \equiv & @{command "note"}~@{text a}~@{command "then"} \\
- @{command "with"}~@{text a} & \equiv & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
- @{command "from"}~@{text this} & \equiv & @{command "then"} \\
- @{command "from"}~@{text this}~@{command "have"} & \equiv & @{command "hence"} \\
- @{command "from"}~@{text this}~@{command "show"} & \equiv & @{command "thus"} \\
- \end{matharray}
+ \begin{tabular}{rcl}
+ @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & @{text "\<equiv>"} &
+ @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
+ @{command ".."} & @{text "\<equiv>"} & @{command "by"}~@{text rule} \\
+ @{command "."} & @{text "\<equiv>"} & @{command "by"}~@{text this} \\
+ @{command "hence"} & @{text "\<equiv>"} & @{command "then"}~@{command "have"} \\
+ @{command "thus"} & @{text "\<equiv>"} & @{command "then"}~@{command "show"} \\
+ @{command "from"}~@{text a} & @{text "\<equiv>"} & @{command "note"}~@{text a}~@{command "then"} \\
+ @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
+ @{command "from"}~@{text this} & @{text "\<equiv>"} & @{command "then"} \\
+ @{command "from"}~@{text this}~@{command "have"} & @{text "\<equiv>"} & @{command "hence"} \\
+ @{command "from"}~@{text this}~@{command "show"} & @{text "\<equiv>"} & @{command "thus"} \\
+ \end{tabular}
*}
subsection {* Derived elements *}
text {*
- \begin{matharray}{rcl}
- @{command "also"}@{text "\<^sub>0"} & \approx & @{command "note"}~@{text "calculation = this"} \\
- @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \approx & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
- @{command "finally"} & \approx & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
- @{command "moreover"} & \approx & @{command "note"}~@{text "calculation = calculation this"} \\
- @{command "ultimately"} & \approx & @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
- @{command "presume"}~@{text "a: \<phi>"} & \approx & @{command "assume"}~@{text "a: \<phi>"} \\
- @{command "def"}~@{text "a: x \<equiv> t"} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
- @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & \approx & \dots~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
- @{command "case"}~@{text c} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
- @{command "sorry"} & \approx & @{command "by"}~@{text cheating} \\
- \end{matharray}
+ \begin{tabular}{rcl}
+ @{command "also"}@{text "\<^sub>0"} & @{text "\<approx>"} &
+ @{command "note"}~@{text "calculation = this"} \\
+ @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & @{text "\<approx>"} &
+ @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
+ @{command "finally"} & @{text "\<approx>"} &
+ @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
+ @{command "moreover"} & @{text "\<approx>"} &
+ @{command "note"}~@{text "calculation = calculation this"} \\
+ @{command "ultimately"} & @{text "\<approx>"} &
+ @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
+ @{command "presume"}~@{text "a: \<phi>"} & @{text "\<approx>"} &
+ @{command "assume"}~@{text "a: \<phi>"} \\
+ @{command "def"}~@{text "a: x \<equiv> t"} & @{text "\<approx>"} &
+ @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
+ @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & @{text "\<approx>"} &
+ @{text "\<dots>"}~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
+ @{command "case"}~@{text c} & @{text "\<approx>"} &
+ @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
+ @{command "sorry"} & @{text "\<approx>"} &
+ @{command "by"}~@{text cheating} \\
+ \end{tabular}
*}
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Thu May 08 22:05:15 2008 +0200
@@ -4,7 +4,7 @@
imports ZF
begin
-chapter {* ZF specific elements *}
+chapter {* Isabelle/ZF \label{ch:zf} *}
section {* Type checking *}
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Thu May 08 22:05:15 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{HOLCF specific elements%
+\isamarkupchapter{Isabelle/HOLCF \label{ch:holcf}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 22:05:15 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{HOL specific elements \label{ch:logics}%
+\isamarkupchapter{Isabelle/HOL \label{ch:hol}%
}
\isamarkuptrue%
%
@@ -166,7 +166,7 @@
variable, which is occasionally referred to as ``row variable'' in
the literature. The more part of a record scheme may be
instantiated by zero or more further components. For example, the
- previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
+ previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isasymrparr}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
Fixed records are special instances of record schemes, where
``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}
element. In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation
@@ -180,8 +180,8 @@
\item the more part is internalized, as a free term or type
variable,
- \item field names are externalized, they cannot be accessed within the logic
- as first-class values.
+ \item field names are externalized, they cannot be accessed within
+ the logic as first-class values.
\end{enumerate}
@@ -254,8 +254,8 @@
any field (including ``\isa{more}''):
\begin{matharray}{lll}
- \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
- \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
\end{matharray}
There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}. Further notation for
@@ -270,7 +270,7 @@
constructor function:
\begin{matharray}{lll}
- \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
\end{matharray}
\medskip We now reconsider the case of non-root records, which are
@@ -283,24 +283,27 @@
fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}},
the above record operations will get the following types:
- \begin{matharray}{lll}
- \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
- \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
- \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
- \end{matharray}
- \noindent
+ \medskip
+ \begin{tabular}{lll}
+ \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
+ \end{tabular}
+ \medskip
- \medskip Some further operations address the extension aspect of a
+ \noindent Some further operations address the extension aspect of a
derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a
record fragment consisting of exactly the new fields introduced here
(the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}
takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.
- \begin{matharray}{lll}
- \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
- \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
- \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
- \end{matharray}
+ \medskip
+ \begin{tabular}{lll}
+ \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
+ \end{tabular}
+ \medskip
\noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide
for root records.%
--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Thu May 08 22:05:15 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{ML tactic expressions \label{sec:conv-tac}%
+\isamarkupchapter{ML tactic expressions%
}
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Thu May 08 22:05:15 2008 +0200
@@ -42,29 +42,31 @@
\mbox{\isa{\isacommand{using}}}~\isa{a} & indicate use of additional facts \\
\mbox{\isa{\isacommand{unfolding}}}~\isa{a} & unfold definitional equations \\
\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\dots~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & indicate proof structure and refinements \\
- \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\dots~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\
+ \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\
\mbox{\isa{\isacommand{next}}} & switch blocks \\
\mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b{\isachardoublequote}} & reconsider facts \\
\mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isacharequal}\ t{\isachardoublequote}} & abbreviate terms by higher-order matching \\
\end{tabular}
- \begin{matharray}{rcl}
- \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex]
+ \medskip
+
+ \begin{tabular}{rcl}
+ \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof\ \ {\isacharbar}{\isachardoublequote}}~~\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}{\isasymdots}\ \ {\isacharbar}\ \ {\isasymdots}{\isachardoublequote}} \\[1ex]
\isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}method\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\
- & \Or & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
\isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\
- & \Or & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
\isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\
- & \Or & \mbox{\isa{\isacommand{next}}} \\
- & \Or & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{next}}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\
\isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
- & \Or & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
- \end{matharray}%
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
+ \end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -73,18 +75,19 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\
- \mbox{\isa{\isacommand{{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{this} \\
- \mbox{\isa{\isacommand{hence}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\
- \mbox{\isa{\isacommand{thus}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\
- \mbox{\isa{\isacommand{from}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\
- \mbox{\isa{\isacommand{with}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex]
- \mbox{\isa{\isacommand{from}}}~\isa{this} & \equiv & \mbox{\isa{\isacommand{then}}} \\
- \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \equiv & \mbox{\isa{\isacommand{hence}}} \\
- \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \equiv & \mbox{\isa{\isacommand{thus}}} \\
- \end{matharray}%
+\begin{tabular}{rcl}
+ \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\
+ \mbox{\isa{\isacommand{{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{this} \\
+ \mbox{\isa{\isacommand{hence}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\
+ \mbox{\isa{\isacommand{thus}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\
+ \mbox{\isa{\isacommand{from}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\
+ \mbox{\isa{\isacommand{with}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex]
+ \mbox{\isa{\isacommand{from}}}~\isa{this} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}} \\
+ \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{hence}}} \\
+ \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{thus}}} \\
+ \end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -93,18 +96,28 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{finally}}} & \approx & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
- \mbox{\isa{\isacommand{moreover}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{ultimately}}} & \approx & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
- \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \dots~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{case}}}~\isa{c} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{sorry}}} & \approx & \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\
- \end{matharray}%
+\begin{tabular}{rcl}
+ \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{finally}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
+ \mbox{\isa{\isacommand{moreover}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{ultimately}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
+ \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{case}}}~\isa{c} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
+ \mbox{\isa{\isacommand{sorry}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
+ \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\
+ \end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 08 22:05:15 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{ZF specific elements%
+\isamarkupchapter{Isabelle/ZF \label{ch:zf}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/intro.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex Thu May 08 22:05:15 2008 +0200
@@ -318,10 +318,8 @@
\medskip The present text really is only a reference manual on
Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
give some clues of how the concepts introduced here may be put into
- practice. \Appref{ap:refcard} provides a quick reference card of
- the most common Isabelle/Isar language elements. \Appref{ap:conv}
- offers some practical hints on converting existing Isabelle theories
- and proof scripts to the new format (without restructuring proofs).
+ practice. Especially note that \appref{ap:refcard} provides a quick
+ reference card of the most common Isabelle/Isar language elements.
Further issues concerning the Isar concepts are covered in the
literature
--- a/doc-src/IsarRef/Thy/document/pure.tex Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex Thu May 08 22:05:15 2008 +0200
@@ -30,8 +30,11 @@
\Chref{ch:gen-tools} describes further Isar elements provided by
generic tools and packages (such as the Simplifier) that are either
part of Pure Isabelle or pre-installed in most object logics.
- \Chref{ch:logics} refers to object-logic specific elements (mainly
- for HOL and ZF).
+ Specific language elements introduced by the major object-logics are
+ described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
+ (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
+ examples given in the generic parts will usually refer to
+ Isabelle/HOL as well.
\medskip Isar commands may be either \emph{proper} document
constructors, or \emph{improper commands}. Some proof methods and
@@ -1172,7 +1175,7 @@
The following proof methods and attributes refer to basic logical
operations of Isar. Further methods and attributes are provided by
several generic and object-logic specific tools and packages (see
- \chref{ch:gen-tools} and \chref{ch:logics}).
+ \chref{ch:gen-tools} and \chref{ch:hol}).
\begin{matharray}{rcl}
\indexdef{}{method}{-}\mbox{\isa{{\isacharminus}}} & : & \isarmeth \\
--- a/doc-src/IsarRef/Thy/intro.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/intro.thy Thu May 08 22:05:15 2008 +0200
@@ -287,10 +287,8 @@
\medskip The present text really is only a reference manual on
Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
give some clues of how the concepts introduced here may be put into
- practice. \Appref{ap:refcard} provides a quick reference card of
- the most common Isabelle/Isar language elements. \Appref{ap:conv}
- offers some practical hints on converting existing Isabelle theories
- and proof scripts to the new format (without restructuring proofs).
+ practice. Especially note that \appref{ap:refcard} provides a quick
+ reference card of the most common Isabelle/Isar language elements.
Further issues concerning the Isar concepts are covered in the
literature
--- a/doc-src/IsarRef/Thy/pure.thy Thu May 08 14:52:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy Thu May 08 22:05:15 2008 +0200
@@ -12,8 +12,11 @@
\Chref{ch:gen-tools} describes further Isar elements provided by
generic tools and packages (such as the Simplifier) that are either
part of Pure Isabelle or pre-installed in most object logics.
- \Chref{ch:logics} refers to object-logic specific elements (mainly
- for HOL and ZF).
+ Specific language elements introduced by the major object-logics are
+ described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
+ (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
+ examples given in the generic parts will usually refer to
+ Isabelle/HOL as well.
\medskip Isar commands may be either \emph{proper} document
constructors, or \emph{improper commands}. Some proof methods and
@@ -1172,7 +1175,7 @@
The following proof methods and attributes refer to basic logical
operations of Isar. Further methods and attributes are provided by
several generic and object-logic specific tools and packages (see
- \chref{ch:gen-tools} and \chref{ch:logics}).
+ \chref{ch:gen-tools} and \chref{ch:hol}).
\begin{matharray}{rcl}
@{method_def "-"} & : & \isarmeth \\