added Isar command 'define';
authorwenzelm
Sun Apr 24 21:31:14 2016 +0200 (2016-04-24)
changeset 630391a20fd9cf281
parent 63038 1fbad761c1ba
child 63040 eb4ddd18d635
added Isar command 'define';
NEWS
src/Doc/Isar_Ref/Framework.thy
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Quick_Reference.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/Isar_Ref/Synopsis.thy
src/Pure/Isar/proof.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sun Apr 24 20:37:24 2016 +0200
     1.2 +++ b/NEWS	Sun Apr 24 21:31:14 2016 +0200
     1.3 @@ -59,6 +59,10 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 +* Command 'define' introduces a local (non-polymorphic) definition, with
     1.8 +optional abstraction over local parameters. The syntax resembles
     1.9 +'obtain' and fits better into the Isar language than old 'def'.
    1.10 +
    1.11  * Command '\<proof>' is an alias for 'sorry', with different
    1.12  typesetting. E.g. to produce proof holes in examples and documentation.
    1.13  
     2.1 --- a/src/Doc/Isar_Ref/Framework.thy	Sun Apr 24 20:37:24 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Framework.thy	Sun Apr 24 21:31:14 2016 +0200
     2.3 @@ -577,8 +577,8 @@
     2.4    i.e.\ it may only occur internally when derived commands are defined in ML.
     2.5  
     2.6    The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below.
     2.7 -  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>
     2.8 -  a\<close>, with the subsequent inference @{inference expand}.
     2.9 +  The derived element \<^theory_text>\<open>define x where "x \<equiv> a"\<close> is defined as \<^theory_text>\<open>fix x assume
    2.10 +  \<guillemotleft>expand\<guillemotright> x \<equiv> a\<close>, with the subsequent inference @{inference expand}.
    2.11  
    2.12    \[
    2.13    \infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
    2.14 @@ -649,7 +649,7 @@
    2.15    note \<open>A \<Longrightarrow> B\<close>
    2.16    text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    2.17    {
    2.18 -    def x \<equiv> a
    2.19 +    define x where "x \<equiv> a"
    2.20      have "B x" \<proof>
    2.21    }
    2.22    note \<open>B a\<close>
     3.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sun Apr 24 20:37:24 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sun Apr 24 21:31:14 2016 +0200
     3.3 @@ -127,6 +127,7 @@
     3.4      @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     3.5      @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     3.6      @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     3.7 +    @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     3.8      @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     3.9    \end{matharray}
    3.10  
    3.11 @@ -151,7 +152,7 @@
    3.12    "presume"} leaves the subgoal unchanged in order to be proved later by the
    3.13    user.
    3.14  
    3.15 -  Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv> t\<close>'', are achieved
    3.16 +  Local definitions, introduced by ``\<^theory_text>\<open>define x where x = t\<close>'', are achieved
    3.17    by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption
    3.18    that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
    3.19    reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
    3.20 @@ -166,6 +167,9 @@
    3.21      ;
    3.22      prems: (@'if' (@{syntax props'} + @'and'))?
    3.23      ;
    3.24 +    @@{command define} (@{syntax "fixes"} + @'and')
    3.25 +      @'where' (@{syntax props} + @'and') @{syntax for_fixes}
    3.26 +    ;
    3.27      @@{command def} (def + @'and')
    3.28      ;
    3.29      def: @{syntax thmdecl}? \<newline>
    3.30 @@ -189,14 +193,23 @@
    3.31    to \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
    3.32    for-context only effects propositions according to actual use of variables.
    3.33  
    3.34 -  \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
    3.35 -  In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
    3.36 -  ``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command
    3.37 -  "assume"}~\<open>x \<equiv> t\<close>'', with the resulting hypothetical equation solved by
    3.38 -  reflexivity.
    3.39 +  \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.
    3.40 +  In results that are exported from the context, \<open>x\<close> is replaced by \<open>t\<close>.
    3.41 +
    3.42 +  Internally, equational assumptions are added to the context in Pure form,
    3.43 +  using \<open>x \<equiv> t\<close> instead of \<open>x = t\<close> or \<open>x \<longleftrightarrow> t\<close> from the object-logic. When
    3.44 +  exporting results from the context, \<open>x\<close> is generalized and the assumption
    3.45 +  discharged by reflexivity, causing the replacement by \<open>t\<close>.
    3.46  
    3.47 -  The default name for the definitional equation is \<open>x_def\<close>. Several
    3.48 -  simultaneous definitions may be given at the same time.
    3.49 +  The default name for the definitional fact is \<open>x_def\<close>. Several simultaneous
    3.50 +  definitions may be given as well, with a collective default name.
    3.51 +
    3.52 +  \<^medskip>
    3.53 +  It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
    3.54 +  :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
    3.55 +
    3.56 +  \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an
    3.57 +  old form of \<^theory_text>\<open>define x where "x = t"\<close>.
    3.58  \<close>
    3.59  
    3.60  
    3.61 @@ -227,10 +240,10 @@
    3.62  
    3.63    \<^medskip>
    3.64    Term abbreviations are quite different from local definitions as introduced
    3.65 -  via @{command "def"} (see \secref{sec:proof-context}). The latter are
    3.66 +  via @{command "define"} (see \secref{sec:proof-context}). The latter are
    3.67    visible within the logic as actual equations, while abbreviations disappear
    3.68    during the input process just after type checking. Also note that @{command
    3.69 -  "def"} does not support polymorphism.
    3.70 +  "define"} does not support polymorphism.
    3.71  
    3.72    @{rail \<open>
    3.73      @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
     4.1 --- a/src/Doc/Isar_Ref/Quick_Reference.thy	Sun Apr 24 20:37:24 2016 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Sun Apr 24 21:31:14 2016 +0200
     4.3 @@ -88,7 +88,7 @@
     4.4      \<^theory_text>\<open>moreover\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = calculation this\<close> \\
     4.5      \<^theory_text>\<open>ultimately\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>moreover from calculation\<close> \\[0.5ex]
     4.6      \<^theory_text>\<open>presume a: A\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>assume a: A\<close> \\
     4.7 -    \<^theory_text>\<open>def "x \<equiv> t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x \<equiv> t"\<close> \\
     4.8 +    \<^theory_text>\<open>define x where "x = t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x = t"\<close> \\
     4.9      \<^theory_text>\<open>consider x where A | \<dots>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>have thesis\<close> \\
    4.10      & & \quad \<^theory_text>\<open>if "\<And>x. A \<Longrightarrow> thesis" and \<dots> for thesis\<close> \\
    4.11      \<^theory_text>\<open>obtain x where a: A \<proof>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>consider x where A \<proof>\<close> \\
     5.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sun Apr 24 20:37:24 2016 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun Apr 24 21:31:14 2016 +0200
     5.3 @@ -538,11 +538,12 @@
     5.4      to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}).
     5.5  
     5.6      \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter.
     5.7 -    This is similar to \<^theory_text>\<open>def\<close> within a proof (cf.\
     5.8 -    \secref{sec:proof-context}), but @{element "defines"} takes an equational
     5.9 -    proposition instead of variable-term pair. The left-hand side of the
    5.10 -    equation may have additional arguments, e.g.\ ``@{element "defines"}~\<open>f
    5.11 -    x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>''.
    5.12 +    This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\
    5.13 +    \secref{sec:proof-context}), but @{element "defines"} is restricted to
    5.14 +    Pure equalities and the defined variable needs to be declared beforehand
    5.15 +    via @{element "fixes"}. The left-hand side of the equation may have
    5.16 +    additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'',
    5.17 +    which need to be free in the context.
    5.18  
    5.19      \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local
    5.20      context. Most notably, this may include arbitrary declarations in any
     6.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Sun Apr 24 20:37:24 2016 +0200
     6.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Sun Apr 24 21:31:14 2016 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4    assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>
     6.5  
     6.6    txt \<open>Definitions (non-polymorphic):\<close>
     6.7 -  def x \<equiv> "t::'a"
     6.8 +  define x :: 'a where "x = t"
     6.9  
    6.10    txt \<open>Abbreviations (polymorphic):\<close>
    6.11    let ?f = "\<lambda>x. x"
    6.12 @@ -635,7 +635,7 @@
    6.13  next
    6.14  
    6.15    {
    6.16 -    def x \<equiv> t
    6.17 +    define x where "x = t"
    6.18      have "B x" \<proof>
    6.19    }
    6.20    have "B t" by fact
     7.1 --- a/src/Pure/Isar/proof.ML	Sun Apr 24 20:37:24 2016 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Sun Apr 24 21:31:14 2016 +0200
     7.3 @@ -86,6 +86,12 @@
     7.4    val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
     7.5    val case_: Thm.binding * ((string * Position.T) * binding option list) -> state -> state
     7.6    val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) -> state -> state
     7.7 +  val define: (binding * typ option * mixfix) list ->
     7.8 +    (binding * typ option * mixfix) list ->
     7.9 +    (Thm.binding * (term * term list) list) list -> state -> state
    7.10 +  val define_cmd: (binding * string option * mixfix) list ->
    7.11 +    (binding * string option * mixfix) list ->
    7.12 +    (Attrib.binding * (string * string list) list) list -> state -> state
    7.13    val begin_block: state -> state
    7.14    val next_block: state -> state
    7.15    val end_block: state -> state
    7.16 @@ -883,6 +889,70 @@
    7.17  end;
    7.18  
    7.19  
    7.20 +(* define *)
    7.21 +
    7.22 +local
    7.23 +
    7.24 +fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
    7.25 +      if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
    7.26 +      else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
    7.27 +  | match_defs [] [] = []
    7.28 +  | match_defs more_decls more_defs =
    7.29 +      error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
    7.30 +        (if null more_decls then "" else " ") ^
    7.31 +        "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
    7.32 +
    7.33 +fun invisible_fixes vars ctxt = ctxt
    7.34 +  |> Context_Position.set_visible false
    7.35 +  |> Proof_Context.add_fixes vars |> #2
    7.36 +  |> Context_Position.restore_visible ctxt;
    7.37 +
    7.38 +fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
    7.39 +  let
    7.40 +    val _ = assert_forward state;
    7.41 +    val ctxt = context_of state;
    7.42 +
    7.43 +    (*vars*)
    7.44 +    val n_vars = length raw_vars;
    7.45 +    val (((all_vars, _, all_params), defss, _, binds'), _) =
    7.46 +      prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
    7.47 +    val (vars, fixes) = chop n_vars all_vars;
    7.48 +    val (params, _) = chop n_vars all_params;
    7.49 +
    7.50 +    (*defs*)
    7.51 +    val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
    7.52 +    val defs1 = map derived_def (flat defss);
    7.53 +    val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
    7.54 +    val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
    7.55 +
    7.56 +    (*fixes*)
    7.57 +    val fixes_ctxt = invisible_fixes fixes defs_ctxt;
    7.58 +    val export = singleton (Variable.export fixes_ctxt defs_ctxt);
    7.59 +
    7.60 +    (*notes*)
    7.61 +    val def_thmss =
    7.62 +      map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
    7.63 +        (defs1 ~~ defs2 ~~ defs3)
    7.64 +      |> unflat (map snd raw_defs);
    7.65 +    val notes =
    7.66 +      map2 (fn ((a, raw_atts), _) => fn def_thms =>
    7.67 +        ((Binding.reset_pos (Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a),
    7.68 +          map (prep_att defs_ctxt) raw_atts), map (fn (_, th) => ([th], [])) def_thms))
    7.69 +        raw_defs def_thmss;
    7.70 +  in
    7.71 +    state
    7.72 +    |> map_context (K defs_ctxt #> fold Variable.bind_term binds')
    7.73 +    |> note_thmss notes
    7.74 +  end;
    7.75 +
    7.76 +in
    7.77 +
    7.78 +val define = gen_define Proof_Context.cert_spec (K I);
    7.79 +val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
    7.80 +
    7.81 +end;
    7.82 +
    7.83 +
    7.84  
    7.85  (** proof structure **)
    7.86  
     8.1 --- a/src/Pure/Pure.thy	Sun Apr 24 20:37:24 2016 +0200
     8.2 +++ b/src/Pure/Pure.thy	Sun Apr 24 21:31:14 2016 +0200
     8.3 @@ -54,7 +54,7 @@
     8.4    and "note" :: prf_decl % "proof"
     8.5    and "supply" :: prf_script % "proof"
     8.6    and "using" "unfolding" :: prf_decl % "proof"
     8.7 -  and "fix" "assume" "presume" "def" :: prf_asm % "proof"
     8.8 +  and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
     8.9    and "consider" :: prf_goal % "proof"
    8.10    and "obtain" :: prf_asm_goal % "proof"
    8.11    and "guess" :: prf_script_asm_goal % "proof"
    8.12 @@ -739,6 +739,11 @@
    8.13      (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
    8.14  
    8.15  val _ =
    8.16 +  Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
    8.17 +    ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
    8.18 +      >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
    8.19 +
    8.20 +val _ =
    8.21    Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
    8.22      (Parse.and_list1
    8.23        (Parse_Spec.opt_thm_name ":" --