1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Tue May 06 00:12:03 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Tue May 06 00:13:01 2008 +0200
1.3 @@ -62,8 +62,8 @@
1.4 given as @{text eq}, which is then turned into a proven fact. The
1.5 given proposition may deviate from internal meta-level equality
1.6 according to the rewrite rules declared as @{attribute defn} by the
1.7 - object-logic. This typically covers object-level equality @{text "x
1.8 - = t"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
1.9 + object-logic. This usually covers object-level equality @{text "x =
1.10 + y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
1.11 change the @{attribute defn} setup.
1.12
1.13 Definitions may be presented with explicit arguments on the LHS, as
1.14 @@ -193,8 +193,9 @@
1.15 "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
1.16 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
1.17 global theory context; the current target context will be suspended
1.18 - for this command only. Note that @{text "(\<IN> -)"} will always
1.19 - produce a global result independently of the current target context.
1.20 + for this command only. Note that ``@{text "(\<IN> -)"}'' will
1.21 + always produce a global result independently of the current target
1.22 + context.
1.23
1.24 \end{descr}
1.25
1.26 @@ -213,8 +214,8 @@
1.27
1.28 Theorems are exported by discharging the assumptions and
1.29 generalizing the parameters of the context. For example, @{text "a:
1.30 - B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"} (again for arbitrary
1.31 - @{text "?x"}).
1.32 + B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
1.33 + @{text "?x"}.
1.34 *}
1.35
1.36
1.37 @@ -313,7 +314,7 @@
1.38 proof (cf.\ \secref{sec:proof-context}).
1.39
1.40 \item [@{element "defines"}~@{text "a: x \<equiv> t"}] defines a previously
1.41 - declared parameter. This is close to @{command "def"} within a
1.42 + declared parameter. This is similar to @{command "def"} within a
1.43 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
1.44 takes an equational proposition instead of variable-term pair. The
1.45 left-hand side of the equation may have additional arguments, e.g.\
1.46 @@ -398,7 +399,7 @@
1.47 context. This requires a proof of the instantiated specification
1.48 and is called \emph{locale interpretation}. Interpretation is
1.49 possible in theories and locales (command @{command
1.50 - "interpretation"}) and also within a proof body (@{command
1.51 + "interpretation"}) and also within a proof body (command @{command
1.52 "interpret"}).
1.53
1.54 \begin{matharray}{rcl}
1.55 @@ -432,7 +433,6 @@
1.56 instantiation term --- with the exception of defined parameters.
1.57 These are, if omitted, derived from the defining equation and other
1.58 instantiations. Use ``@{text _}'' to omit an instantiation term.
1.59 - Free variables are automatically generalized.
1.60
1.61 The command generates proof obligations for the instantiated
1.62 specifications (assumes and defines elements). Once these are
1.63 @@ -498,8 +498,7 @@
1.64
1.65 \item [@{command "interpret"}~@{text "expr insts \<WHERE> eqns"}]
1.66 interprets @{text expr} in the proof context and is otherwise
1.67 - similar to interpretation in theories. Free variables in
1.68 - instantiations are not generalized, however.
1.69 + similar to interpretation in theories.
1.70
1.71 \item [@{command "print_interps"}~@{text loc}] prints the
1.72 interpretations of a particular locale @{text loc} that are active
1.73 @@ -594,7 +593,7 @@
1.74 \secref{sec:target}) which allows to specify class operations @{text
1.75 "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding to sort @{text s} at the
1.76 particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
1.77 - \<alpha>\<^sub>n :: s\<^sub>n) t"}. An plain @{command "instance"} command
1.78 + \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command
1.79 in the target body poses a goal stating these type arities. The
1.80 target is concluded by an @{command_ref "end"} command.
1.81
1.82 @@ -727,7 +726,7 @@
1.83 \begin{descr}
1.84
1.85 \item [@{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 ::
1.86 - \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n} \<BEGIN>"}]
1.87 + \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}]
1.88 opens a theory target (cf.\ \secref{sec:target}) which allows to
1.89 specify constants with overloaded definitions. These are identified
1.90 by an explicitly given mapping from variable names @{text
1.91 @@ -819,8 +818,7 @@
1.92 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
1.93 facts indicated for forward chaining).
1.94 \begin{matharray}{l}
1.95 - @{text "\<langle>facts b\<^sub>1 \<dots> b\<^sub>k\<rangle>"} \\
1.96 - @{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]
1.97 + @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]
1.98 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
1.99 \quad @{command "proof"}~@{text succeed} \\
1.100 \qquad @{command "fix"}~@{text thesis} \\
1.101 @@ -1396,7 +1394,7 @@
1.102 'simplified' opt? thmrefs?
1.103 ;
1.104
1.105 - opt: '(' (noasm | noasmsimp | noasmuse) ')'
1.106 + opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
1.107 ;
1.108 \end{rail}
1.109
1.110 @@ -1669,7 +1667,7 @@
1.111 Non-conditional rules result in a ``safe'' introduction and
1.112 elimination pair; conditional ones are considered ``unsafe''. Rules
1.113 with negative conclusion are automatically inverted (using @{text
1.114 - "\<not>"} elimination internally).
1.115 + "\<not>"}-elimination internally).
1.116
1.117 The ``@{text "?"}'' version of @{attribute iff} declares rules to
1.118 the Isabelle/Pure context only, and omits the Simplifier
1.119 @@ -1720,11 +1718,11 @@
1.120 The @{command "case"} command provides a shorthand to refer to a
1.121 local context symbolically: certain proof methods provide an
1.122 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
1.123 - x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of
1.124 - ``@{command "case"}@{text c}'' is then equivalent to ``@{command
1.125 - "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text
1.126 - "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''. Term bindings may be
1.127 - covered as well, notably @{variable ?case} for the main conclusion.
1.128 + x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
1.129 + "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
1.130 + "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1.131 + \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
1.132 + @{variable ?case} for the main conclusion.
1.133
1.134 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
1.135 a case value is marked as hidden, i.e.\ there is no way to refer to
1.136 @@ -1885,11 +1883,11 @@
1.137
1.138 \medskip
1.139 \begin{tabular}{llll}
1.140 - facts & & arguments & rule \\\hline
1.141 - & @{method cases} & & classical case split \\
1.142 - & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1.143 + facts & & arguments & rule \\\hline
1.144 + & @{method cases} & & classical case split \\
1.145 + & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1.146 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
1.147 - @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1.148 + @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1.149 \end{tabular}
1.150 \medskip
1.151
1.152 @@ -1905,10 +1903,10 @@
1.153
1.154 \medskip
1.155 \begin{tabular}{llll}
1.156 - facts & & arguments & rule \\\hline
1.157 - & @{method induct} & @{text "P x \<dots>"} & datatype induction (type of @{text x}) \\
1.158 - @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1.159 - @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1.160 + facts & & arguments & rule \\\hline
1.161 + & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
1.162 + @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1.163 + @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1.164 \end{tabular}
1.165 \medskip
1.166
1.167 @@ -1947,10 +1945,10 @@
1.168
1.169 \medskip
1.170 \begin{tabular}{llll}
1.171 - goal & & arguments & rule \\\hline
1.172 - & @{method coinduct} & @{text "x \<dots>"} & type coinduction (type of @{text x}) \\
1.173 + goal & & arguments & rule \\\hline
1.174 + & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
1.175 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
1.176 - @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> R"} & explicit rule @{text R} \\
1.177 + @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1.178 \end{tabular}
1.179
1.180 Coinduction is the dual of induction. Induction essentially