author schirmer Sat, 18 Dec 2004 17:14:33 +0100 changeset 15423 761a4f8e6ad6 parent 15422 cbdddc0efadf child 15424 7a91490c1b04
 NEWS file | annotate | diff | comparison | revisions src/HOL/HOL.thy file | annotate | diff | comparison | revisions src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
--- a/NEWS	Sat Dec 18 17:12:45 2004 +0100
+++ b/NEWS	Sat Dec 18 17:14:33 2004 +0100
@@ -247,6 +247,14 @@
all partial orders (class "order"), in particular numbers and sets. For
linear orders (e.g. numbers) it treats ~ x < y just like y <= x.

+  - Simproc for "let x = a in f x"
+  If a is a free or bound variable or a constant then the let is unfolded.
+  Otherwise first a is simplified to a', and then f a' is simplified to
+  g. If possible we abstract a' from g arriving at "let x = a' in g' x",
+  otherwise we unfold the let and arrive at g. The simproc can be
+  enabled/disabled by the reference use_let_simproc. Potential
+  INCOMPATIBILITY since simplification is more powerful by default.
+
* HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
(containing Boolean satisfiability problems) into Isabelle/HOL theories.

--- a/src/HOL/HOL.thy	Sat Dec 18 17:12:45 2004 +0100
+++ b/src/HOL/HOL.thy	Sat Dec 18 17:14:33 2004 +0100
@@ -1098,6 +1098,14 @@
lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules

+text {* \medskip let rules for simproc *}
+
+lemma Let_folded: "f x \<equiv> g x \<Longrightarrow>  Let x f \<equiv> Let x g"
+  by (unfold Let_def)
+
+lemma Let_unfold: "f x \<equiv> g \<Longrightarrow>  Let x f \<equiv> g"
+  by (unfold Let_def)
+
subsubsection {* Actual Installation of the Simplifier *}

use "simpdata.ML"
--- a/src/HOL/simpdata.ML	Sat Dec 18 17:12:45 2004 +0100
+++ b/src/HOL/simpdata.ML	Sat Dec 18 17:14:33 2004 +0100
@@ -131,6 +131,55 @@
Simplifier.simproc (Theory.sign_of (the_context ()))
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;

+(*** Simproc for Let ***)
+
+val use_let_simproc = ref true;
+
+local
+val Let_folded = thm "Let_folded";
+val Let_unfold = thm "Let_unfold";
+
+val f_Let_unfold =
+      let val [(_\$(f\$_)\$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end
+val f_Let_folded =
+      let val [(_\$(f\$_)\$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end;
+val g_Let_folded =
+      let val [(_\$_\$(g\$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
+in
+val let_simproc =
+  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"]
+   (fn sg => fn ss => fn t =>
+      (case t of (Const ("Let",_)\$x\$f) => (* x and f are already in normal form *)
+         if not (!use_let_simproc) then None
+         else if is_Free x orelse is_Bound x orelse is_Const x
+         then Some Let_def
+         else
+          let
+             val n = case f of (Abs (x,_,_)) => x | _ => "x";
+             val cx = cterm_of sg x;
+             val {T=xT,...} = rep_cterm cx;
+             val cf = cterm_of sg f;
+             val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
+             val (_\$_\$g) = prop_of fx_g;
+             val g' = abstract_over (x,g);
+           in (if (g aconv g')
+               then
+                  let
+                    val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
+                  in Some (rl OF [fx_g]) end
+               else if betapply (f,x) aconv g then None (* avoid identity conversion *)
+               else let
+                     val abs_g'= Abs (n,xT,g');
+                     val g'x = abs_g'\$x;
+                     val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
+                     val rl = cterm_instantiate
+                               [(f_Let_folded,cterm_of sg f),
+                                (g_Let_folded,cterm_of sg abs_g')]
+                               Let_folded;
+                   in Some (rl OF [transitive fx_g g_g'x]) end)
+           end
+        | _ => None))
+end

(*** Case splitting ***)

@@ -248,7 +297,7 @@
disj_not1, not_all, not_ex, cases_simp,
thm "the_eq_trivial", the_sym_eq_trivial]
@ ex_simps @ all_simps @ simp_thms)