src/HOL/simpdata.ML
changeset 20014 729a45534001
parent 19472 896eb8056e97
child 20046 9c8909fc5865
     1.1 --- a/src/HOL/simpdata.ML	Tue Jul 04 21:26:26 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Jul 05 11:32:38 2006 +0200
     1.3 @@ -176,16 +176,23 @@
     1.4  val Let_folded = thm "Let_folded";
     1.5  val Let_unfold = thm "Let_unfold";
     1.6  
     1.7 -val f_Let_unfold = 
     1.8 -      let val [(_$(f$_)$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end
     1.9 -val f_Let_folded = 
    1.10 -      let val [(_$(f$_)$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end;
    1.11 +val (f_Let_unfold,x_Let_unfold) = 
    1.12 +      let val [(_$(f$x)$_)] = prems_of Let_unfold 
    1.13 +      in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
    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        let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
    1.19  in
    1.20  val let_simproc =
    1.21    Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 
    1.22     (fn sg => fn ss => fn t =>
    1.23 +(* FIXME: very slow (replace t by t' in case below)
    1.24 +     let val ctxt = Simplifier.the_context ss;
    1.25 +         val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
    1.26 +     in Option.map (hd o Variable.export ctxt' ctxt o single)
    1.27 +*)
    1.28        (case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
    1.29           if not (!use_let_simproc) then NONE
    1.30           else if is_Free x orelse is_Bound x orelse is_Const x 
    1.31 @@ -202,7 +209,7 @@
    1.32             in (if (g aconv g') 
    1.33                 then
    1.34                    let
    1.35 -                    val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
    1.36 +                    val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
    1.37                    in SOME (rl OF [fx_g]) end 
    1.38                 else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
    1.39                 else let 
    1.40 @@ -210,12 +217,16 @@
    1.41                       val g'x = abs_g'$x;
    1.42                       val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
    1.43                       val rl = cterm_instantiate
    1.44 -                               [(f_Let_folded,cterm_of sg f),
    1.45 +                               [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
    1.46                                  (g_Let_folded,cterm_of sg abs_g')]
    1.47                                 Let_folded; 
    1.48 -                   in SOME (rl OF [transitive fx_g g_g'x]) end)
    1.49 +                   in SOME (rl OF [transitive fx_g g_g'x]) 
    1.50 +                   end)
    1.51             end
    1.52 -        | _ => NONE))
    1.53 +        | _ => NONE)
    1.54 + (*  FIXME: continue
    1.55 +  end*)
    1.56 + )
    1.57  end
    1.58  
    1.59  (*** Case splitting ***)