--- a/NEWS Sun Apr 24 20:37:24 2016 +0200
+++ b/NEWS Sun Apr 24 21:31:14 2016 +0200
@@ -59,6 +59,10 @@
*** Isar ***
+* Command 'define' introduces a local (non-polymorphic) definition, with
+optional abstraction over local parameters. The syntax resembles
+'obtain' and fits better into the Isar language than old 'def'.
+
* Command '\<proof>' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.
--- a/src/Doc/Isar_Ref/Framework.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Sun Apr 24 21:31:14 2016 +0200
@@ -577,8 +577,8 @@
i.e.\ it may only occur internally when derived commands are defined in ML.
The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below.
- The derived element \<^theory_text>\<open>def x \<equiv> a\<close> is defined as \<^theory_text>\<open>fix x assume \<guillemotleft>expand\<guillemotright> x \<equiv>
- a\<close>, with the subsequent inference @{inference expand}.
+ The derived element \<^theory_text>\<open>define x where "x \<equiv> a"\<close> is defined as \<^theory_text>\<open>fix x assume
+ \<guillemotleft>expand\<guillemotright> x \<equiv> a\<close>, with the subsequent inference @{inference expand}.
\[
\infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
@@ -649,7 +649,7 @@
note \<open>A \<Longrightarrow> B\<close>
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
- def x \<equiv> a
+ define x where "x \<equiv> a"
have "B x" \<proof>
}
note \<open>B a\<close>
--- a/src/Doc/Isar_Ref/Proof.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sun Apr 24 21:31:14 2016 +0200
@@ -127,6 +127,7 @@
@{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
\end{matharray}
@@ -151,7 +152,7 @@
"presume"} leaves the subgoal unchanged in order to be proved later by the
user.
- Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv> t\<close>'', are achieved
+ Local definitions, introduced by ``\<^theory_text>\<open>define x where x = t\<close>'', are achieved
by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption
that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
@@ -166,6 +167,9 @@
;
prems: (@'if' (@{syntax props'} + @'and'))?
;
+ @@{command define} (@{syntax "fixes"} + @'and')
+ @'where' (@{syntax props} + @'and') @{syntax for_fixes}
+ ;
@@{command def} (def + @'and')
;
def: @{syntax thmdecl}? \<newline>
@@ -189,14 +193,23 @@
to \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
for-context only effects propositions according to actual use of variables.
- \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
- In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
- ``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command
- "assume"}~\<open>x \<equiv> t\<close>'', with the resulting hypothetical equation solved by
- reflexivity.
+ \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.
+ In results that are exported from the context, \<open>x\<close> is replaced by \<open>t\<close>.
+
+ Internally, equational assumptions are added to the context in Pure form,
+ using \<open>x \<equiv> t\<close> instead of \<open>x = t\<close> or \<open>x \<longleftrightarrow> t\<close> from the object-logic. When
+ exporting results from the context, \<open>x\<close> is generalized and the assumption
+ discharged by reflexivity, causing the replacement by \<open>t\<close>.
- The default name for the definitional equation is \<open>x_def\<close>. Several
- simultaneous definitions may be given at the same time.
+ The default name for the definitional fact is \<open>x_def\<close>. Several simultaneous
+ definitions may be given as well, with a collective default name.
+
+ \<^medskip>
+ It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
+ :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
+
+ \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an
+ old form of \<^theory_text>\<open>define x where "x = t"\<close>.
\<close>
@@ -227,10 +240,10 @@
\<^medskip>
Term abbreviations are quite different from local definitions as introduced
- via @{command "def"} (see \secref{sec:proof-context}). The latter are
+ via @{command "define"} (see \secref{sec:proof-context}). The latter are
visible within the logic as actual equations, while abbreviations disappear
during the input process just after type checking. Also note that @{command
- "def"} does not support polymorphism.
+ "define"} does not support polymorphism.
@{rail \<open>
@@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
--- a/src/Doc/Isar_Ref/Quick_Reference.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy Sun Apr 24 21:31:14 2016 +0200
@@ -88,7 +88,7 @@
\<^theory_text>\<open>moreover\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = calculation this\<close> \\
\<^theory_text>\<open>ultimately\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>moreover from calculation\<close> \\[0.5ex]
\<^theory_text>\<open>presume a: A\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>assume a: A\<close> \\
- \<^theory_text>\<open>def "x \<equiv> t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x \<equiv> t"\<close> \\
+ \<^theory_text>\<open>define x where "x = t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x = t"\<close> \\
\<^theory_text>\<open>consider x where A | \<dots>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>have thesis\<close> \\
& & \quad \<^theory_text>\<open>if "\<And>x. A \<Longrightarrow> thesis" and \<dots> for thesis\<close> \\
\<^theory_text>\<open>obtain x where a: A \<proof>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>consider x where A \<proof>\<close> \\
--- a/src/Doc/Isar_Ref/Spec.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sun Apr 24 21:31:14 2016 +0200
@@ -538,11 +538,12 @@
to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}).
\<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter.
- This is similar to \<^theory_text>\<open>def\<close> within a proof (cf.\
- \secref{sec:proof-context}), but @{element "defines"} takes an equational
- proposition instead of variable-term pair. The left-hand side of the
- equation may have additional arguments, e.g.\ ``@{element "defines"}~\<open>f
- x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>''.
+ This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\
+ \secref{sec:proof-context}), but @{element "defines"} is restricted to
+ Pure equalities and the defined variable needs to be declared beforehand
+ via @{element "fixes"}. The left-hand side of the equation may have
+ additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'',
+ which need to be free in the context.
\<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local
context. Most notably, this may include arbitrary declarations in any
--- a/src/Doc/Isar_Ref/Synopsis.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Apr 24 21:31:14 2016 +0200
@@ -26,7 +26,7 @@
assume "a = b" \<comment> \<open>type assignment at first occurrence in concrete term\<close>
txt \<open>Definitions (non-polymorphic):\<close>
- def x \<equiv> "t::'a"
+ define x :: 'a where "x = t"
txt \<open>Abbreviations (polymorphic):\<close>
let ?f = "\<lambda>x. x"
@@ -635,7 +635,7 @@
next
{
- def x \<equiv> t
+ define x where "x = t"
have "B x" \<proof>
}
have "B t" by fact
--- a/src/Pure/Isar/proof.ML Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Pure/Isar/proof.ML Sun Apr 24 21:31:14 2016 +0200
@@ -86,6 +86,12 @@
val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val case_: Thm.binding * ((string * Position.T) * binding option list) -> state -> state
val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) -> state -> state
+ val define: (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list -> state -> state
+ val define_cmd: (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (Attrib.binding * (string * string list) list) list -> state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
@@ -883,6 +889,70 @@
end;
+(* define *)
+
+local
+
+fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
+ if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+ else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
+ | match_defs [] [] = []
+ | match_defs more_decls more_defs =
+ error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
+ (if null more_decls then "" else " ") ^
+ "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
+
+fun invisible_fixes vars ctxt = ctxt
+ |> Context_Position.set_visible false
+ |> Proof_Context.add_fixes vars |> #2
+ |> Context_Position.restore_visible ctxt;
+
+fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
+ let
+ val _ = assert_forward state;
+ val ctxt = context_of state;
+
+ (*vars*)
+ val n_vars = length raw_vars;
+ val (((all_vars, _, all_params), defss, _, binds'), _) =
+ prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
+ val (vars, fixes) = chop n_vars all_vars;
+ val (params, _) = chop n_vars all_params;
+
+ (*defs*)
+ val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
+ val defs1 = map derived_def (flat defss);
+ val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
+ val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
+
+ (*fixes*)
+ val fixes_ctxt = invisible_fixes fixes defs_ctxt;
+ val export = singleton (Variable.export fixes_ctxt defs_ctxt);
+
+ (*notes*)
+ val def_thmss =
+ map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
+ (defs1 ~~ defs2 ~~ defs3)
+ |> unflat (map snd raw_defs);
+ val notes =
+ map2 (fn ((a, raw_atts), _) => fn def_thms =>
+ ((Binding.reset_pos (Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a),
+ map (prep_att defs_ctxt) raw_atts), map (fn (_, th) => ([th], [])) def_thms))
+ raw_defs def_thmss;
+ in
+ state
+ |> map_context (K defs_ctxt #> fold Variable.bind_term binds')
+ |> note_thmss notes
+ end;
+
+in
+
+val define = gen_define Proof_Context.cert_spec (K I);
+val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
+
+end;
+
+
(** proof structure **)
--- a/src/Pure/Pure.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Pure/Pure.thy Sun Apr 24 21:31:14 2016 +0200
@@ -54,7 +54,7 @@
and "note" :: prf_decl % "proof"
and "supply" :: prf_script % "proof"
and "using" "unfolding" :: prf_decl % "proof"
- and "fix" "assume" "presume" "def" :: prf_asm % "proof"
+ and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
and "guess" :: prf_script_asm_goal % "proof"
@@ -739,6 +739,11 @@
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
val _ =
+ Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
+ ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
+ >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
+
+val _ =
Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --