simproc for let
authorhaftmann
Thu Nov 13 15:58:38 2008 +0100 (2008-11-13)
changeset 287411b257449f804
parent 28740 22a8125d66fa
child 28742 07073b1087dd
simproc for let
NEWS
src/HOL/Complex/ex/MIR.thy
src/HOL/HOL.thy
src/HOL/Library/Ramsey.thy
     1.1 --- a/NEWS	Thu Nov 13 15:58:37 2008 +0100
     1.2 +++ b/NEWS	Thu Nov 13 15:58:38 2008 +0100
     1.3 @@ -117,6 +117,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* If methods "eval" and "evaluation" encounter a structured proof state
     1.8 +with !!/==>, only the conclusion is evaluated to True (if possible),
     1.9 +avoiding strange error messages.
    1.10 +
    1.11 +* Simplifier: simproc for let expressions now unfolds if bound variable
    1.12 +occurs at most one time in let expression body.  INCOMPATIBILITY.
    1.13 +
    1.14  * New classes "top" and "bot" with corresponding operations "top" and "bot"
    1.15  in theory Orderings;  instantiation of class "complete_lattice" requires
    1.16  instantiation of classes "top" and "bot".  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Complex/ex/MIR.thy	Thu Nov 13 15:58:37 2008 +0100
     2.2 +++ b/src/HOL/Complex/ex/MIR.thy	Thu Nov 13 15:58:38 2008 +0100
     2.3 @@ -3686,7 +3686,11 @@
     2.4        ultimately show ?ths by auto
     2.5      qed
     2.6  next
     2.7 -  case (3 a b) thus ?case by auto
     2.8 +  case (3 a b) then show ?case
     2.9 +  apply auto
    2.10 +  apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all
    2.11 +  apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all
    2.12 +  done
    2.13  qed (auto simp add: Let_def split_def ring_simps conj_rl)
    2.14  
    2.15  lemma real_in_int_intervals: 
     3.1 --- a/src/HOL/HOL.thy	Thu Nov 13 15:58:37 2008 +0100
     3.2 +++ b/src/HOL/HOL.thy	Thu Nov 13 15:58:38 2008 +0100
     3.3 @@ -1322,55 +1322,63 @@
     3.4  simproc_setup let_simp ("Let x f") = {*
     3.5  let
     3.6    val (f_Let_unfold, x_Let_unfold) =
     3.7 -    let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold}
     3.8 +    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold}
     3.9      in (cterm_of @{theory} f, cterm_of @{theory} x) end
    3.10    val (f_Let_folded, x_Let_folded) =
    3.11 -    let val [(_$(f$x)$_)] = prems_of @{thm Let_folded}
    3.12 +    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded}
    3.13      in (cterm_of @{theory} f, cterm_of @{theory} x) end;
    3.14    val g_Let_folded =
    3.15 -    let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end;
    3.16 -
    3.17 -  fun proc _ ss ct =
    3.18 -    let
    3.19 -      val ctxt = Simplifier.the_context ss;
    3.20 -      val thy = ProofContext.theory_of ctxt;
    3.21 -      val t = Thm.term_of ct;
    3.22 -      val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    3.23 -    in Option.map (hd o Variable.export ctxt' ctxt o single)
    3.24 -      (case t' of Const ("Let",_) $ x $ f => (* x and f are already in normal form *)
    3.25 -        if is_Free x orelse is_Bound x orelse is_Const x
    3.26 -        then SOME @{thm Let_def}
    3.27 -        else
    3.28 -          let
    3.29 -            val n = case f of (Abs (x,_,_)) => x | _ => "x";
    3.30 -            val cx = cterm_of thy x;
    3.31 -            val {T=xT,...} = rep_cterm cx;
    3.32 -            val cf = cterm_of thy f;
    3.33 -            val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    3.34 -            val (_$_$g) = prop_of fx_g;
    3.35 -            val g' = abstract_over (x,g);
    3.36 -          in (if (g aconv g')
    3.37 -               then
    3.38 -                  let
    3.39 -                    val rl =
    3.40 -                      cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold};
    3.41 -                  in SOME (rl OF [fx_g]) end
    3.42 -               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
    3.43 -               else let
    3.44 -                     val abs_g'= Abs (n,xT,g');
    3.45 -                     val g'x = abs_g'$x;
    3.46 -                     val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
    3.47 -                     val rl = cterm_instantiate
    3.48 -                               [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx),
    3.49 -                                (g_Let_folded,cterm_of thy abs_g')]
    3.50 -                               @{thm Let_folded};
    3.51 -                   in SOME (rl OF [transitive fx_g g_g'x])
    3.52 -                   end)
    3.53 -          end
    3.54 -      | _ => NONE)
    3.55 -    end
    3.56 -in proc end *}
    3.57 -
    3.58 +    let val [(_ $ _ $ (g $ _))] = prems_of @{thm Let_folded}
    3.59 +    in cterm_of @{theory} g end;
    3.60 +  fun count_loose (Bound i) k = if i >= k then 1 else 0
    3.61 +    | count_loose (s $ t) k = count_loose s k + count_loose t k
    3.62 +    | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    3.63 +    | count_loose _ _ = 0;
    3.64 +  fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
    3.65 +   case t
    3.66 +    of Abs (_, _, t') => count_loose t' 0 <= 1
    3.67 +     | _ => true;
    3.68 +in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
    3.69 +  then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*)
    3.70 +  else let (*Norbert Schirmer's case*)
    3.71 +    val ctxt = Simplifier.the_context ss;
    3.72 +    val thy = ProofContext.theory_of ctxt;
    3.73 +    val t = Thm.term_of ct;
    3.74 +    val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    3.75 +  in Option.map (hd o Variable.export ctxt' ctxt o single)
    3.76 +    (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
    3.77 +      if is_Free x orelse is_Bound x orelse is_Const x
    3.78 +      then SOME @{thm Let_def}
    3.79 +      else
    3.80 +        let
    3.81 +          val n = case f of (Abs (x, _, _)) => x | _ => "x";
    3.82 +          val cx = cterm_of thy x;
    3.83 +          val {T = xT, ...} = rep_cterm cx;
    3.84 +          val cf = cterm_of thy f;
    3.85 +          val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
    3.86 +          val (_ $ _ $ g) = prop_of fx_g;
    3.87 +          val g' = abstract_over (x,g);
    3.88 +        in (if (g aconv g')
    3.89 +             then
    3.90 +                let
    3.91 +                  val rl =
    3.92 +                    cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    3.93 +                in SOME (rl OF [fx_g]) end
    3.94 +             else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*)
    3.95 +             else let
    3.96 +                   val abs_g'= Abs (n,xT,g');
    3.97 +                   val g'x = abs_g'$x;
    3.98 +                   val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
    3.99 +                   val rl = cterm_instantiate
   3.100 +                             [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
   3.101 +                              (g_Let_folded, cterm_of thy abs_g')]
   3.102 +                             @{thm Let_folded};
   3.103 +                 in SOME (rl OF [transitive fx_g g_g'x])
   3.104 +                 end)
   3.105 +        end
   3.106 +    | _ => NONE)
   3.107 +  end
   3.108 +end *}
   3.109  
   3.110  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   3.111  proof
     4.1 --- a/src/HOL/Library/Ramsey.thy	Thu Nov 13 15:58:37 2008 +0100
     4.2 +++ b/src/HOL/Library/Ramsey.thy	Thu Nov 13 15:58:38 2008 +0100
     4.3 @@ -131,8 +131,8 @@
     4.4      from dependent_choice [OF transr propr0 proprstep]
     4.5      obtain g where pg: "!!n::nat.  ?propr (g n)"
     4.6        and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
     4.7 -    let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"
     4.8 -    let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"
     4.9 +    let ?gy = "fst o g"
    4.10 +    let ?gt = "snd o snd o g"
    4.11      have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    4.12      proof (intro exI subsetI)
    4.13        fix x