src/HOL/simpdata.ML
```     1.1 --- a/src/HOL/simpdata.ML	Sat Dec 18 17:12:45 2004 +0100
1.2 +++ b/src/HOL/simpdata.ML	Sat Dec 18 17:14:33 2004 +0100
1.3 @@ -131,6 +131,55 @@
1.4    Simplifier.simproc (Theory.sign_of (the_context ()))
1.5      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
1.6
1.7 +(*** Simproc for Let ***)
1.8 +
1.9 +val use_let_simproc = ref true;
1.10 +
1.11 +local
1.12 +val Let_folded = thm "Let_folded";
1.13 +val Let_unfold = thm "Let_unfold";
1.14 +
1.15 +val f_Let_unfold =
1.16 +      let val [(_\$(f\$_)\$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end
1.17 +val f_Let_folded =
1.18 +      let val [(_\$(f\$_)\$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end;
1.19 +val g_Let_folded =
1.20 +      let val [(_\$_\$(g\$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
1.21 +in
1.22 +val let_simproc =
1.23 +  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"]
1.24 +   (fn sg => fn ss => fn t =>
1.25 +      (case t of (Const ("Let",_)\$x\$f) => (* x and f are already in normal form *)
1.26 +         if not (!use_let_simproc) then None
1.27 +         else if is_Free x orelse is_Bound x orelse is_Const x
1.28 +         then Some Let_def
1.29 +         else
1.30 +          let
1.31 +             val n = case f of (Abs (x,_,_)) => x | _ => "x";
1.32 +             val cx = cterm_of sg x;
1.33 +             val {T=xT,...} = rep_cterm cx;
1.34 +             val cf = cterm_of sg f;
1.35 +             val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
1.36 +             val (_\$_\$g) = prop_of fx_g;
1.37 +             val g' = abstract_over (x,g);
1.38 +           in (if (g aconv g')
1.39 +               then
1.40 +                  let
1.41 +                    val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
1.42 +                  in Some (rl OF [fx_g]) end
1.43 +               else if betapply (f,x) aconv g then None (* avoid identity conversion *)
1.44 +               else let
1.45 +                     val abs_g'= Abs (n,xT,g');
1.46 +                     val g'x = abs_g'\$x;
1.47 +                     val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
1.48 +                     val rl = cterm_instantiate
1.49 +                               [(f_Let_folded,cterm_of sg f),
1.50 +                                (g_Let_folded,cterm_of sg abs_g')]
1.51 +                               Let_folded;
1.52 +                   in Some (rl OF [transitive fx_g g_g'x]) end)
1.53 +           end
1.54 +        | _ => None))
1.55 +end
1.56
1.57  (*** Case splitting ***)
1.58
1.59 @@ -248,7 +297,7 @@
1.60         disj_not1, not_all, not_ex, cases_simp,
1.61         thm "the_eq_trivial", the_sym_eq_trivial]
1.62       @ ex_simps @ all_simps @ simp_thms)