# HG changeset patch # User wenzelm # Date 1301512068 -7200 # Node ID a7570c66d74606b62683b0ae5cdb44583c0630c7 # Parent 3164e7263b53cd82c7efc540ef5fece9bc279605 inline lemmas instead of accidental physical addressing -- explicit is better than implicit; diff -r 3164e7263b53 -r a7570c66d746 src/HOL/Tools/list_to_set_comprehension.ML --- a/src/HOL/Tools/list_to_set_comprehension.ML Wed Mar 30 20:21:40 2011 +0200 +++ b/src/HOL/Tools/list_to_set_comprehension.ML Wed Mar 30 21:07:48 2011 +0200 @@ -51,7 +51,7 @@ fun conjunct_assoc_conv ct = Conv.try_conv - ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct + (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv @@ -107,7 +107,7 @@ end (* returns condition continuing term option *) fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = - SOME (cond, then_t) + SOME (cond, then_t) | dest_if _ = NONE fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 | tac ctxt (If :: cont) = @@ -117,13 +117,14 @@ THEN Subgoal.FOCUS (fn {prems, context, ...} => CONVERSION (right_hand_set_comprehension_conv (K (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv - then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1 + then_conv + rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1 THEN tac ctxt cont THEN rtac @{thm impI} 1 THEN Subgoal.FOCUS (fn {prems, context, ...} => CONVERSION (right_hand_set_comprehension_conv (K (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv - then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1 + then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1 THEN rtac set_Nil_I 1 | tac ctxt (Case (T, i) :: cont) = let @@ -148,22 +149,26 @@ then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => Conv.repeat_conv (all_but_last_exists_conv - (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 + (K (rewr_conv' + @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 THEN tac ctxt cont else Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION ((right_hand_set_comprehension_conv (K - (conj_conv - ((eq_conv Conv.all_conv - (rewr_conv' (List.last prems))) then_conv - (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) - Conv.all_conv then_conv - (rewr_conv' @{thm simp_thms(24)}))) context) then_conv - (Trueprop_conv - (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv - (Conv.bottom_conv - (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1 + CONVERSION + (right_hand_set_comprehension_conv (K + (conj_conv + ((eq_conv Conv.all_conv + (rewr_conv' (List.last prems))) then_conv + (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) + Conv.all_conv then_conv + (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv + Trueprop_conv + (eq_conv Conv.all_conv + (Collect_conv (fn (_, ctxt) => + Conv.repeat_conv + (Conv.bottom_conv + (K (rewr_conv' + @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 THEN rtac set_Nil_I 1)) (#case_rewrites info)) end fun make_inner_eqs bound_vs Tis eqs t =