src/HOL/simpdata.ML
changeset 15423 761a4f8e6ad6
parent 15184 d2c19aea17bc
child 15531 08c8dad8e399
     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)
    1.63 -     addsimprocs [defALL_regroup,defEX_regroup]
    1.64 +     addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
    1.65       addcongs [imp_cong]
    1.66       addsplits [split_if];
    1.67