summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 07 Sep 2016 22:28:40 +0200 | |

changeset 63822 | c575a3814a76 |

parent 63820 | 9f004fbf9d5c (current diff) |

parent 63821 | 52235c27538c (diff) |

child 63823 | ca8b737b08cf |

merged

--- a/NEWS Wed Sep 07 11:59:09 2016 +0200 +++ b/NEWS Wed Sep 07 22:28:40 2016 +0200 @@ -66,7 +66,15 @@ is relevant to avoid confusion of Pure.simp vs. HOL.simp. * Commands 'prf' and 'full_prf' are somewhat more informative (again): -proof terms are reconstructed and cleaned from administrative thm nodes. +proof terms are reconstructed and cleaned from administrative thm +nodes. + +* The command 'unfolding' and proof method "unfold" include a second +stage where given equations are passed through the attribute "abs_def" +before rewriting. This ensures that definitions are fully expanded, +regardless of the actual parameters that are provided. Rare +INCOMPATIBILITY in some corner cases: use proof method (simp only:) +instead, or declare [[unfold_abs_def = false]] in the proof context. *** Prover IDE -- Isabelle/Scala/jEdit ***

--- a/src/Doc/Isar_Ref/Generic.thy Wed Sep 07 11:59:09 2016 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Wed Sep 07 22:28:40 2016 +0200 @@ -84,6 +84,11 @@ fold back) the given definitions throughout all goals; any chained facts provided are inserted into the goal and subject to rewriting as well. + Unfolding works in two stages: first, the given equations are used directly + for rewriting; second, the equations are passed through the attribute + @{attribute_ref abs_def} before rewriting --- to ensure that definitions are + fully expanded, regardless of the actual parameters that are provided. + \<^descr> @{method insert}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> inserts theorems as facts into all goals of the proof state. Note that current facts indicated for forward chaining are ignored. @@ -155,8 +160,8 @@ expand and fold back again the given definitions throughout a rule. \<^descr> @{attribute abs_def} turns an equation of the form @{prop "f x y \<equiv> t"} - into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} or @{method - unfold} steps always expand it. This also works for object-logic equality. + into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} steps always + expand it. This also works for object-logic equality. \<^descr> @{attribute rotated}~\<open>n\<close> rotate the premises of a theorem by \<open>n\<close> (default 1).

--- a/src/Doc/Isar_Ref/Proof.thy Wed Sep 07 11:59:09 2016 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Wed Sep 07 22:28:40 2016 +0200 @@ -332,8 +332,8 @@ "proof"}). \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command - "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the - goal state and facts. + "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal + state and facts. See also the proof method @{method_ref unfold}. \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method expression. The facts provided by the proof state (via @{command "using"}

--- a/src/Pure/Isar/local_defs.ML Wed Sep 07 11:59:09 2016 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Sep 07 22:28:40 2016 +0200 @@ -207,7 +207,7 @@ (* unfold object-level rules *) -val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool false)); +val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool true)); val unfold_abs_def = Config.bool unfold_abs_def_raw; local