# HG changeset patch # User wenzelm # Date 1461526274 -7200 # Node ID 1a20fd9cf28166c706af0f75e1c6dc6a2331d58e # Parent 1fbad761c1bad8d9987a75a37cee8d9f9032de2d added Isar command 'define'; diff -r 1fbad761c1ba -r 1a20fd9cf281 NEWS --- 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 '\' is an alias for 'sorry', with different typesetting. E.g. to produce proof holes in examples and documentation. diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Doc/Isar_Ref/Framework.thy --- 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>\assume\ is @{inference export} as given below. - The derived element \<^theory_text>\def x \ a\ is defined as \<^theory_text>\fix x assume \expand\ x \ - a\, with the subsequent inference @{inference expand}. + The derived element \<^theory_text>\define x where "x \ a"\ is defined as \<^theory_text>\fix x assume + \expand\ x \ a\, with the subsequent inference @{inference expand}. \[ \infer[(@{inference_def export})]{\\\ - A \ A \ B\}{\\\ \ B\} @@ -649,7 +649,7 @@ note \A \ B\ text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { - def x \ a + define x where "x \ a" have "B x" \ } note \B a\ diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Doc/Isar_Ref/Proof.thy --- 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"} & : & \proof(state) \ proof(state)\ \\ @{command_def "assume"} & : & \proof(state) \ proof(state)\ \\ @{command_def "presume"} & : & \proof(state) \ proof(state)\ \\ + @{command_def "define"} & : & \proof(state) \ proof(state)\ \\ @{command_def "def"} & : & \proof(state) \ proof(state)\ \\ \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"}~\x \ t\'', are achieved + Local definitions, introduced by ``\<^theory_text>\define x where x = t\'', are achieved by combining ``@{command "fix"}~\x\'' with another version of assumption that causes any hypothetical equation \x \ t\ to be eliminated by the reflexivity rule. Thus, exporting some result \x \ t \ \[x]\ yields \\ @@ -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}? \ @@ -189,14 +193,23 @@ to \<^theory_text>\assume "\x. A x \ B x"\, but vacuous quantification is avoided: a for-context only effects propositions according to actual use of variables. - \<^descr> @{command "def"}~\x \ t\ introduces a local (non-polymorphic) definition. - In results exported from the context, \x\ is replaced by \t\. Basically, - ``@{command "def"}~\x \ t\'' abbreviates ``@{command "fix"}~\x\~@{command - "assume"}~\x \ t\'', with the resulting hypothetical equation solved by - reflexivity. + \<^descr> \<^theory_text>\define x where "x = t"\ introduces a local (non-polymorphic) definition. + In results that are exported from the context, \x\ is replaced by \t\. + + Internally, equational assumptions are added to the context in Pure form, + using \x \ t\ instead of \x = t\ or \x \ t\ from the object-logic. When + exporting results from the context, \x\ is generalized and the assumption + discharged by reflexivity, causing the replacement by \t\. - The default name for the definitional equation is \x_def\. Several - simultaneous definitions may be given at the same time. + The default name for the definitional fact is \x_def\. 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>\define f + :: "'a \ 'b" where "f x = t" for x :: 'a\. + + \<^descr> \<^theory_text>\def x \ t\ introduces a local (non-polymorphic) definition. This is an + old form of \<^theory_text>\define x where "x = t"\. \ @@ -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 \ @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and') diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Doc/Isar_Ref/Quick_Reference.thy --- 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>\moreover\ & \\\ & \<^theory_text>\note calculation = calculation this\ \\ \<^theory_text>\ultimately\ & \\\ & \<^theory_text>\moreover from calculation\ \\[0.5ex] \<^theory_text>\presume a: A\ & \\\ & \<^theory_text>\assume a: A\ \\ - \<^theory_text>\def "x \ t"\ & \\\ & \<^theory_text>\fix x assume x_def: "x \ t"\ \\ + \<^theory_text>\define x where "x = t"\ & \\\ & \<^theory_text>\fix x assume x_def: "x = t"\ \\ \<^theory_text>\consider x where A | \\ & \\\ & \<^theory_text>\have thesis\ \\ & & \quad \<^theory_text>\if "\x. A \ thesis" and \ for thesis\ \\ \<^theory_text>\obtain x where a: A \\ & \\\ & \<^theory_text>\consider x where A \\ \\ diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Doc/Isar_Ref/Spec.thy --- 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>\assume\ within a proof (cf.\ \secref{sec:proof-context}). \<^descr> @{element "defines"}~\a: x \ t\ defines a previously declared parameter. - This is similar to \<^theory_text>\def\ 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"}~\f - x\<^sub>1 \ x\<^sub>n \ t\''. + This is similar to \<^theory_text>\define\ 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"}~\f x\<^sub>1 \ x\<^sub>n \ t\'', + which need to be free in the context. \<^descr> @{element "notes"}~\a = b\<^sub>1 \ b\<^sub>n\ reconsiders facts within a local context. Most notably, this may include arbitrary declarations in any diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Doc/Isar_Ref/Synopsis.thy --- 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" \ \type assignment at first occurrence in concrete term\ txt \Definitions (non-polymorphic):\ - def x \ "t::'a" + define x :: 'a where "x = t" txt \Abbreviations (polymorphic):\ let ?f = "\x. x" @@ -635,7 +635,7 @@ next { - def x \ t + define x where "x = t" have "B x" \ } have "B t" by fact diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Pure/Isar/proof.ML --- 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 **) diff -r 1fbad761c1ba -r 1a20fd9cf281 src/Pure/Pure.thy --- 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 ":" --