fixed let-simproc
authorschirmer
Wed Jul 05 11:32:38 2006 +0200 (2006-07-05)
changeset 20014729a45534001
parent 20013 57505678692d
child 20015 1ffcf4802802
fixed let-simproc
----------------------------------------------------------------------
src/HOL/Bali/AxSem.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Bali/AxSem.thy	Tue Jul 04 21:26:26 2006 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Jul 05 11:32:38 2006 +0200
     1.3 @@ -1079,7 +1079,7 @@
     1.4  apply (rule ax_escape, clarsimp)
     1.5  apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
     1.6  apply (drule spec,drule spec,drule spec, erule conseq12)
     1.7 -apply (force simp add: init_lvars_def)
     1.8 +apply (force simp add: init_lvars_def Let_def)
     1.9  done
    1.10  
    1.11  lemma ax_Methd1: 
     2.1 --- a/src/HOL/simpdata.ML	Tue Jul 04 21:26:26 2006 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Wed Jul 05 11:32:38 2006 +0200
     2.3 @@ -176,16 +176,23 @@
     2.4  val Let_folded = thm "Let_folded";
     2.5  val Let_unfold = thm "Let_unfold";
     2.6  
     2.7 -val f_Let_unfold = 
     2.8 -      let val [(_$(f$_)$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end
     2.9 -val f_Let_folded = 
    2.10 -      let val [(_$(f$_)$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end;
    2.11 +val (f_Let_unfold,x_Let_unfold) = 
    2.12 +      let val [(_$(f$x)$_)] = prems_of Let_unfold 
    2.13 +      in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
    2.14 +val (f_Let_folded,x_Let_folded) = 
    2.15 +      let val [(_$(f$x)$_)] = prems_of Let_folded 
    2.16 +      in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end;
    2.17  val g_Let_folded = 
    2.18        let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
    2.19  in
    2.20  val let_simproc =
    2.21    Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 
    2.22     (fn sg => fn ss => fn t =>
    2.23 +(* FIXME: very slow (replace t by t' in case below)
    2.24 +     let val ctxt = Simplifier.the_context ss;
    2.25 +         val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
    2.26 +     in Option.map (hd o Variable.export ctxt' ctxt o single)
    2.27 +*)
    2.28        (case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
    2.29           if not (!use_let_simproc) then NONE
    2.30           else if is_Free x orelse is_Bound x orelse is_Const x 
    2.31 @@ -202,7 +209,7 @@
    2.32             in (if (g aconv g') 
    2.33                 then
    2.34                    let
    2.35 -                    val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
    2.36 +                    val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
    2.37                    in SOME (rl OF [fx_g]) end 
    2.38                 else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
    2.39                 else let 
    2.40 @@ -210,12 +217,16 @@
    2.41                       val g'x = abs_g'$x;
    2.42                       val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
    2.43                       val rl = cterm_instantiate
    2.44 -                               [(f_Let_folded,cterm_of sg f),
    2.45 +                               [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
    2.46                                  (g_Let_folded,cterm_of sg abs_g')]
    2.47                                 Let_folded; 
    2.48 -                   in SOME (rl OF [transitive fx_g g_g'x]) end)
    2.49 +                   in SOME (rl OF [transitive fx_g g_g'x]) 
    2.50 +                   end)
    2.51             end
    2.52 -        | _ => NONE))
    2.53 +        | _ => NONE)
    2.54 + (*  FIXME: continue
    2.55 +  end*)
    2.56 + )
    2.57  end
    2.58  
    2.59  (*** Case splitting ***)