# HG changeset patch # User haftmann # Date 1226588318 -3600 # Node ID 1b257449f804bb6e8dd50bfe0b50a3f45cb93b86 # Parent 22a8125d66fa4f1f55975b444c341dba3d32d2ed simproc for let diff -r 22a8125d66fa -r 1b257449f804 NEWS --- a/NEWS Thu Nov 13 15:58:37 2008 +0100 +++ b/NEWS Thu Nov 13 15:58:38 2008 +0100 @@ -117,6 +117,13 @@ *** HOL *** +* If methods "eval" and "evaluation" encounter a structured proof state +with !!/==>, only the conclusion is evaluated to True (if possible), +avoiding strange error messages. + +* Simplifier: simproc for let expressions now unfolds if bound variable +occurs at most one time in let expression body. INCOMPATIBILITY. + * New classes "top" and "bot" with corresponding operations "top" and "bot" in theory Orderings; instantiation of class "complete_lattice" requires instantiation of classes "top" and "bot". INCOMPATIBILITY. diff -r 22a8125d66fa -r 1b257449f804 src/HOL/Complex/ex/MIR.thy --- a/src/HOL/Complex/ex/MIR.thy Thu Nov 13 15:58:37 2008 +0100 +++ b/src/HOL/Complex/ex/MIR.thy Thu Nov 13 15:58:38 2008 +0100 @@ -3686,7 +3686,11 @@ ultimately show ?ths by auto qed next - case (3 a b) thus ?case by auto + case (3 a b) then show ?case + apply auto + apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all + apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all + done qed (auto simp add: Let_def split_def ring_simps conj_rl) lemma real_in_int_intervals: diff -r 22a8125d66fa -r 1b257449f804 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Nov 13 15:58:37 2008 +0100 +++ b/src/HOL/HOL.thy Thu Nov 13 15:58:38 2008 +0100 @@ -1322,55 +1322,63 @@ simproc_setup let_simp ("Let x f") = {* let val (f_Let_unfold, x_Let_unfold) = - let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold} + let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold} in (cterm_of @{theory} f, cterm_of @{theory} x) end val (f_Let_folded, x_Let_folded) = - let val [(_$(f$x)$_)] = prems_of @{thm Let_folded} + let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded} in (cterm_of @{theory} f, cterm_of @{theory} x) end; val g_Let_folded = - let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; - - fun proc _ ss ct = - let - val ctxt = Simplifier.the_context ss; - val thy = ProofContext.theory_of ctxt; - val t = Thm.term_of ct; - 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 is_Free x orelse is_Bound x orelse is_Const x - then SOME @{thm Let_def} - else - let - val n = case f of (Abs (x,_,_)) => x | _ => "x"; - val cx = cterm_of thy x; - val {T=xT,...} = rep_cterm cx; - val cf = cterm_of thy f; - val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); - val (_$_$g) = prop_of fx_g; - val g' = abstract_over (x,g); - in (if (g aconv g') - then - let - val rl = - cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold}; - in SOME (rl OF [fx_g]) end - else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) - else let - val abs_g'= Abs (n,xT,g'); - val g'x = abs_g'$x; - val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); - val rl = cterm_instantiate - [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx), - (g_Let_folded,cterm_of thy abs_g')] - @{thm Let_folded}; - in SOME (rl OF [transitive fx_g g_g'x]) - end) - end - | _ => NONE) - end -in proc end *} - + let val [(_ $ _ $ (g $ _))] = prems_of @{thm Let_folded} + in cterm_of @{theory} g end; + fun count_loose (Bound i) k = if i >= k then 1 else 0 + | count_loose (s $ t) k = count_loose s k + count_loose t k + | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) + | count_loose _ _ = 0; + fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = + case t + of Abs (_, _, t') => count_loose t' 0 <= 1 + | _ => true; +in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct) + then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*) + else let (*Norbert Schirmer's case*) + val ctxt = Simplifier.the_context ss; + val thy = ProofContext.theory_of ctxt; + val t = Thm.term_of ct; + val ([t'], ctxt') = Variable.import_terms false [t] ctxt; + in Option.map (hd o Variable.export ctxt' ctxt o single) + (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *) + if is_Free x orelse is_Bound x orelse is_Const x + then SOME @{thm Let_def} + else + let + val n = case f of (Abs (x, _, _)) => x | _ => "x"; + val cx = cterm_of thy x; + val {T = xT, ...} = rep_cterm cx; + val cf = cterm_of thy f; + val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); + val (_ $ _ $ g) = prop_of fx_g; + val g' = abstract_over (x,g); + in (if (g aconv g') + then + let + val rl = + cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold}; + in SOME (rl OF [fx_g]) end + else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*) + else let + val abs_g'= Abs (n,xT,g'); + val g'x = abs_g'$x; + val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); + val rl = cterm_instantiate + [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx), + (g_Let_folded, cterm_of thy abs_g')] + @{thm Let_folded}; + in SOME (rl OF [transitive fx_g g_g'x]) + end) + end + | _ => NONE) + end +end *} lemma True_implies_equals: "(True \ PROP P) \ PROP P" proof diff -r 22a8125d66fa -r 1b257449f804 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Thu Nov 13 15:58:37 2008 +0100 +++ b/src/HOL/Library/Ramsey.thy Thu Nov 13 15:58:38 2008 +0100 @@ -131,8 +131,8 @@ from dependent_choice [OF transr propr0 proprstep] obtain g where pg: "!!n::nat. ?propr (g n)" and rg: "!!n m. n (g n, g m) \ ?ramr" by blast - let ?gy = "(\n. let (y,Y,t) = g n in y)" - let ?gt = "(\n. let (y,Y,t) = g n in t)" + let ?gy = "fst o g" + let ?gt = "snd o snd o g" have rangeg: "\k. range ?gt \ {..