# HG changeset patch
# User schirmer
# Date 1152091958 -7200
# Node ID 729a4553400188214590d39f45736fd0877c9414
# Parent  57505678692d6737d3c25c25d3ae524e568f83e9
fixed let-simproc
----------------------------------------------------------------------

diff -r 57505678692d -r 729a45534001 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Tue Jul 04 21:26:26 2006 +0200
+++ b/src/HOL/Bali/AxSem.thy	Wed Jul 05 11:32:38 2006 +0200
@@ -1079,7 +1079,7 @@
 apply (rule ax_escape, clarsimp)
 apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
 apply (drule spec,drule spec,drule spec, erule conseq12)
-apply (force simp add: init_lvars_def)
+apply (force simp add: init_lvars_def Let_def)
 done
 
 lemma ax_Methd1: 
diff -r 57505678692d -r 729a45534001 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Jul 04 21:26:26 2006 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 05 11:32:38 2006 +0200
@@ -176,16 +176,23 @@
 val Let_folded = thm "Let_folded";
 val Let_unfold = thm "Let_unfold";
 
-val f_Let_unfold = 
-      let val [(_$(f$_)$_)] = prems_of Let_unfold in cterm_of (sign_of (the_context ())) f end
-val f_Let_folded = 
-      let val [(_$(f$_)$_)] = prems_of Let_folded in cterm_of (sign_of (the_context ())) f end;
+val (f_Let_unfold,x_Let_unfold) = 
+      let val [(_$(f$x)$_)] = prems_of Let_unfold 
+      in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
+val (f_Let_folded,x_Let_folded) = 
+      let val [(_$(f$x)$_)] = prems_of Let_folded 
+      in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end;
 val g_Let_folded = 
       let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
 in
 val let_simproc =
   Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 
    (fn sg => fn ss => fn t =>
+(* FIXME: very slow (replace t by t' in case below)
+     let val ctxt = Simplifier.the_context ss;
+         val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
+     in Option.map (hd o Variable.export ctxt' ctxt o single)
+*)
       (case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
          if not (!use_let_simproc) then NONE
          else if is_Free x orelse is_Bound x orelse is_Const x 
@@ -202,7 +209,7 @@
            in (if (g aconv g') 
                then
                   let
-                    val rl = cterm_instantiate [(f_Let_unfold,cf)] Let_unfold;
+                    val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
                   in SOME (rl OF [fx_g]) end 
                else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
                else let 
@@ -210,12 +217,16 @@
                      val g'x = abs_g'$x;
                      val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
                      val rl = cterm_instantiate
-                               [(f_Let_folded,cterm_of sg f),
+                               [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
                                 (g_Let_folded,cterm_of sg abs_g')]
                                Let_folded; 
-                   in SOME (rl OF [transitive fx_g g_g'x]) end)
+                   in SOME (rl OF [transitive fx_g g_g'x]) 
+                   end)
            end
-        | _ => NONE))
+        | _ => NONE)
+ (*  FIXME: continue
+  end*)
+ )
 end
 
 (*** Case splitting ***)