--- a/src/HOL/Bali/Example.thy Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Bali/Example.thy Mon May 18 23:15:56 2009 +0200
@@ -1075,7 +1075,7 @@
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> =
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
, [Class Base])}"
-by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
+by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
section "well-typedness"
--- a/src/HOL/Library/Pocklington.thy Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy Mon May 18 23:15:56 2009 +0200
@@ -382,8 +382,9 @@
(* Euler totient function. *)
definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
+
lemma phi_0[simp]: "\<phi> 0 = 0"
- unfolding phi_def by (auto simp add: card_eq_0_iff)
+ unfolding phi_def by auto
lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
proof-
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon May 18 23:15:56 2009 +0200
@@ -69,9 +69,9 @@
lemma subcls1:
"subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
-apply (simp add: subcls1_def2 del:singleton_conj_conv2)
+apply (simp add: subcls1_def2)
apply (simp add: name_defs class_defs system_defs E_def class_def)
-apply (auto simp: expand_fun_eq split: split_if_asm)
+apply (auto simp: expand_fun_eq)
done
text {* The subclass relation is acyclic; hence its converse is well founded: *}
--- a/src/HOL/Set.thy Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Set.thy Mon May 18 23:15:56 2009 +0200
@@ -1036,11 +1036,16 @@
text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
-lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
+lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
+by auto
+
+lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
by auto
-lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
-by auto
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
ML{*
local
@@ -1054,7 +1059,6 @@
end;
Addsimprocs [defColl_regroup];
-
*}
text {*
--- a/src/Provers/quantifier1.ML Mon May 18 15:45:42 2009 +0200
+++ b/src/Provers/quantifier1.ML Mon May 18 23:15:56 2009 +0200
@@ -90,7 +90,7 @@
fun extract_conj fst xs t = case dest_conj t of NONE => NONE
| SOME(conj,P,Q) =>
- (if not fst andalso def xs P then SOME(xs,P,Q) else
+ (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
if def xs Q then SOME(xs,Q,P) else
(case extract_conj false xs P of
SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
@@ -99,7 +99,7 @@
| NONE => NONE)));
fun extract_imp fst xs t = case dest_imp t of NONE => NONE
- | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
+ | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
else (case extract_conj false xs P of
SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
| NONE => (case extract_imp false xs Q of