let_simproc: activate Variable.import;
authorwenzelm
Tue Jul 11 12:16:52 2006 +0200 (2006-07-11)
changeset 200703f31fb81b83a
parent 20069 77a6b62418bb
child 20071 8f3e1ddb50e6
let_simproc: activate Variable.import;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Jul 11 11:19:28 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Jul 11 12:16:52 2006 +0200
     1.3 @@ -176,27 +176,25 @@
     1.4  val Let_folded = thm "Let_folded";
     1.5  val Let_unfold = thm "Let_unfold";
     1.6  
     1.7 -val (f_Let_unfold,x_Let_unfold) = 
     1.8 -      let val [(_$(f$x)$_)] = prems_of Let_unfold 
     1.9 +val (f_Let_unfold,x_Let_unfold) =
    1.10 +      let val [(_$(f$x)$_)] = prems_of Let_unfold
    1.11        in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
    1.12 -val (f_Let_folded,x_Let_folded) = 
    1.13 -      let val [(_$(f$x)$_)] = prems_of Let_folded 
    1.14 +val (f_Let_folded,x_Let_folded) =
    1.15 +      let val [(_$(f$x)$_)] = prems_of Let_folded
    1.16        in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end;
    1.17 -val g_Let_folded = 
    1.18 +val g_Let_folded =
    1.19        let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
    1.20  in
    1.21  val let_simproc =
    1.22 -  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 
    1.23 +  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"]
    1.24     (fn sg => fn ss => fn t =>
    1.25 -(* FIXME: very slow (replace t by t' in case below)
    1.26       let val ctxt = Simplifier.the_context ss;
    1.27           val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
    1.28       in Option.map (hd o Variable.export ctxt' ctxt o single)
    1.29 -*)
    1.30 -      (case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
    1.31 +      (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
    1.32           if not (!use_let_simproc) then NONE
    1.33 -         else if is_Free x orelse is_Bound x orelse is_Const x 
    1.34 -         then SOME Let_def  
    1.35 +         else if is_Free x orelse is_Bound x orelse is_Const x
    1.36 +         then SOME Let_def
    1.37           else
    1.38            let
    1.39               val n = case f of (Abs (x,_,_)) => x | _ => "x";
    1.40 @@ -206,27 +204,25 @@
    1.41               val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    1.42               val (_$_$g) = prop_of fx_g;
    1.43               val g' = abstract_over (x,g);
    1.44 -           in (if (g aconv g') 
    1.45 +           in (if (g aconv g')
    1.46                 then
    1.47                    let
    1.48                      val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
    1.49 -                  in SOME (rl OF [fx_g]) end 
    1.50 +                  in SOME (rl OF [fx_g]) end
    1.51                 else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
    1.52 -               else let 
    1.53 +               else let
    1.54                       val abs_g'= Abs (n,xT,g');
    1.55                       val g'x = abs_g'$x;
    1.56                       val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
    1.57                       val rl = cterm_instantiate
    1.58                                 [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
    1.59                                  (g_Let_folded,cterm_of sg abs_g')]
    1.60 -                               Let_folded; 
    1.61 -                   in SOME (rl OF [transitive fx_g g_g'x]) 
    1.62 +                               Let_folded;
    1.63 +                   in SOME (rl OF [transitive fx_g g_g'x])
    1.64                     end)
    1.65             end
    1.66          | _ => NONE)
    1.67 - (*  FIXME: continue
    1.68 -  end*)
    1.69 - )
    1.70 +     end)
    1.71  end
    1.72  
    1.73  (*** Case splitting ***)