1.1 --- a/src/HOL/Bali/Example.thy Mon May 18 15:45:42 2009 +0200
1.2 +++ b/src/HOL/Bali/Example.thy Mon May 18 23:15:56 2009 +0200
1.3 @@ -1075,7 +1075,7 @@
1.4 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> =
1.5 {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
1.6 , [Class Base])}"
1.7 -by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
1.8 +by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
1.9
1.10 section "well-typedness"
1.11
2.1 --- a/src/HOL/Library/Pocklington.thy Mon May 18 15:45:42 2009 +0200
2.2 +++ b/src/HOL/Library/Pocklington.thy Mon May 18 23:15:56 2009 +0200
2.3 @@ -382,8 +382,9 @@
2.4 (* Euler totient function. *)
2.5
2.6 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
2.7 +
2.8 lemma phi_0[simp]: "\<phi> 0 = 0"
2.9 - unfolding phi_def by (auto simp add: card_eq_0_iff)
2.10 + unfolding phi_def by auto
2.11
2.12 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
2.13 proof-
3.1 --- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 18 15:45:42 2009 +0200
3.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon May 18 23:15:56 2009 +0200
3.3 @@ -69,9 +69,9 @@
3.4 lemma subcls1:
3.5 "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
3.6 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
3.7 -apply (simp add: subcls1_def2 del:singleton_conj_conv2)
3.8 +apply (simp add: subcls1_def2)
3.9 apply (simp add: name_defs class_defs system_defs E_def class_def)
3.10 -apply (auto simp: expand_fun_eq split: split_if_asm)
3.11 +apply (auto simp: expand_fun_eq)
3.12 done
3.13
3.14 text {* The subclass relation is acyclic; hence its converse is well founded: *}
4.1 --- a/src/HOL/Set.thy Mon May 18 15:45:42 2009 +0200
4.2 +++ b/src/HOL/Set.thy Mon May 18 23:15:56 2009 +0200
4.3 @@ -1036,12 +1036,17 @@
4.4
4.5 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
4.6
4.7 -lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
4.8 +lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
4.9 by auto
4.10
4.11 -lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
4.12 +lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
4.13 by auto
4.14
4.15 +text {*
4.16 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
4.17 +to the front (and similarly for @{text "t=x"}):
4.18 +*}
4.19 +
4.20 ML{*
4.21 local
4.22 val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
4.23 @@ -1054,7 +1059,6 @@
4.24 end;
4.25
4.26 Addsimprocs [defColl_regroup];
4.27 -
4.28 *}
4.29
4.30 text {*
5.1 --- a/src/Provers/quantifier1.ML Mon May 18 15:45:42 2009 +0200
5.2 +++ b/src/Provers/quantifier1.ML Mon May 18 23:15:56 2009 +0200
5.3 @@ -90,7 +90,7 @@
5.4
5.5 fun extract_conj fst xs t = case dest_conj t of NONE => NONE
5.6 | SOME(conj,P,Q) =>
5.7 - (if not fst andalso def xs P then SOME(xs,P,Q) else
5.8 + (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
5.9 if def xs Q then SOME(xs,Q,P) else
5.10 (case extract_conj false xs P of
5.11 SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
5.12 @@ -99,7 +99,7 @@
5.13 | NONE => NONE)));
5.14
5.15 fun extract_imp fst xs t = case dest_imp t of NONE => NONE
5.16 - | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
5.17 + | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
5.18 else (case extract_conj false xs P of
5.19 SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
5.20 | NONE => (case extract_imp false xs Q of