1.1 --- a/src/HOL/HOL.thy	Thu Nov 13 15:58:37 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Nov 13 15:58:38 2008 +0100
     1.3 @@ -1322,55 +1322,63 @@
     1.4  simproc_setup let_simp ("Let x f") = {*
     1.5  let
     1.6    val (f_Let_unfold, x_Let_unfold) =
     1.7 -    let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold}
     1.8 +    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold}
     1.9      in (cterm_of @{theory} f, cterm_of @{theory} x) end
    1.10    val (f_Let_folded, x_Let_folded) =
    1.11 -    let val [(_$(f$x)$_)] = prems_of @{thm Let_folded}
    1.12 +    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded}
    1.13      in (cterm_of @{theory} f, cterm_of @{theory} x) end;
    1.14    val g_Let_folded =
    1.15 -    let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end;
    1.16 -
    1.17 -  fun proc _ ss ct =
    1.18 -    let
    1.19 -      val ctxt = Simplifier.the_context ss;
    1.20 -      val thy = ProofContext.theory_of ctxt;
    1.21 -      val t = Thm.term_of ct;
    1.22 -      val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    1.23 -    in Option.map (hd o Variable.export ctxt' ctxt o single)
    1.24 -      (case t' of Const ("Let",_) $ x $ f => (* x and f are already in normal form *)
    1.25 -        if is_Free x orelse is_Bound x orelse is_Const x
    1.26 -        then SOME @{thm Let_def}
    1.27 -        else
    1.28 -          let
    1.29 -            val n = case f of (Abs (x,_,_)) => x | _ => "x";
    1.30 -            val cx = cterm_of thy x;
    1.31 -            val {T=xT,...} = rep_cterm cx;
    1.32 -            val cf = cterm_of thy f;
    1.33 -            val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    1.34 -            val (_$_$g) = prop_of fx_g;
    1.35 -            val g' = abstract_over (x,g);
    1.36 -          in (if (g aconv g')
    1.37 -               then
    1.38 -                  let
    1.39 -                    val rl =
    1.40 -                      cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold};
    1.41 -                  in SOME (rl OF [fx_g]) end
    1.42 -               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
    1.43 -               else let
    1.44 -                     val abs_g'= Abs (n,xT,g');
    1.45 -                     val g'x = abs_g'$x;
    1.46 -                     val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
    1.47 -                     val rl = cterm_instantiate
    1.48 -                               [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx),
    1.49 -                                (g_Let_folded,cterm_of thy abs_g')]
    1.50 -                               @{thm Let_folded};
    1.51 -                   in SOME (rl OF [transitive fx_g g_g'x])
    1.52 -                   end)
    1.53 -          end
    1.54 -      | _ => NONE)
    1.55 -    end
    1.56 -in proc end *}
    1.57 -
    1.58 +    let val [(_ $ _ $ (g $ _))] = prems_of @{thm Let_folded}
    1.59 +    in cterm_of @{theory} g end;
    1.60 +  fun count_loose (Bound i) k = if i >= k then 1 else 0
    1.61 +    | count_loose (s $ t) k = count_loose s k + count_loose t k
    1.62 +    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    1.63 +    | count_loose _ _ = 0;
    1.64 +  fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
    1.65 +   case t
    1.66 +    of Abs (_, _, t') => count_loose t' 0 <= 1
    1.67 +     | _ => true;
    1.68 +in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
    1.69 +  then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*)
    1.70 +  else let (*Norbert Schirmer's case*)
    1.71 +    val ctxt = Simplifier.the_context ss;
    1.72 +    val thy = ProofContext.theory_of ctxt;
    1.73 +    val t = Thm.term_of ct;
    1.74 +    val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    1.75 +  in Option.map (hd o Variable.export ctxt' ctxt o single)
    1.76 +    (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
    1.77 +      if is_Free x orelse is_Bound x orelse is_Const x
    1.78 +      then SOME @{thm Let_def}
    1.79 +      else
    1.80 +        let
    1.81 +          val n = case f of (Abs (x, _, _)) => x | _ => "x";
    1.82 +          val cx = cterm_of thy x;
    1.83 +          val {T = xT, ...} = rep_cterm cx;
    1.84 +          val cf = cterm_of thy f;
    1.85 +          val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    1.86 +          val (_ $ _ $ g) = prop_of fx_g;
    1.87 +          val g' = abstract_over (x,g);
    1.88 +        in (if (g aconv g')
    1.89 +             then
    1.90 +                let
    1.91 +                  val rl =
    1.92 +                    cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.93 +                in SOME (rl OF [fx_g]) end
    1.94 +             else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*)
    1.95 +             else let
    1.96 +                   val abs_g'= Abs (n,xT,g');
    1.97 +                   val g'x = abs_g'$x;
    1.98 +                   val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
    1.99 +                   val rl = cterm_instantiate
   1.100 +                             [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
   1.101 +                              (g_Let_folded, cterm_of thy abs_g')]
   1.102 +                             @{thm Let_folded};
   1.103 +                 in SOME (rl OF [transitive fx_g g_g'x])
   1.104 +                 end)
   1.105 +        end
   1.106 +    | _ => NONE)
   1.107 +  end
   1.108 +end *}
   1.109  
   1.110  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.111  proof