# HG changeset patch # User nipkow # Date 1242466103 -7200 # Node ID 8741df04d1aea480b4b772f5c7a23a867e63aefb # Parent 8448ba49d6816e5666fbbb4ab3846a5e06694c82# Parent a90fe83f58ea5dc1c666a5e488768863b4898a7e merged diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/Bali/Example.thy Sat May 16 11:28:23 2009 +0200 @@ -1075,10 +1075,7 @@ lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \name=foo,parTs=[NT]\ = {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) , [Class Base])}" -apply (unfold max_spec_def) -apply (simp (no_asm) add: appl_methds_Base_foo) -apply auto -done +by (simp (no_asm) add: max_spec_def appl_methds_Base_foo) section "well-typedness" diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/HOL.thy Sat May 16 11:28:23 2009 +0200 @@ -1050,8 +1050,7 @@ "(P | False) = P" "(False | P) = P" "(P | P) = P" "(P | (P | Q)) = (P | Q)" and "(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" - -- {* needed for the one-point-rule quantifier simplification procs *} - -- {* essential for termination!! *} and + and "!!P. (EX x. x=t & P(x)) = P(t)" "!!P. (EX x. t=x & P(x)) = P(t)" "!!P. (ALL x. x=t --> P(x)) = P(t)" diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/Library/Binomial.thy Sat May 16 11:28:23 2009 +0200 @@ -88,9 +88,7 @@ lemma card_s_0_eq_empty: "finite A ==> card {B. B \ A & card B = 0} = 1" - apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) - apply (simp cong add: rev_conj_cong) - done +by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) lemma choose_deconstruct: "finite M ==> x \ M ==> {s. s <= insert x M & card(s) = Suc k} diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/MicroJava/BV/BVExample.thy Sat May 16 11:28:23 2009 +0200 @@ -69,10 +69,11 @@ lemma subcls1: "subcls1 E = (\C D. (C, D) \ {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})" - 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) - done +apply (simp add: subcls1_def2) +apply (simp add: name_defs class_defs system_defs E_def class_def) +apply (auto simp: expand_fun_eq name_defs[symmetric] class_defs split:split_if_asm) +apply(simp add:name_defs)+ +done text {* The subclass relation is acyclic; hence its converse is well founded: *} lemma notin_rtrancl: diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/NanoJava/TypeRel.thy --- a/src/HOL/NanoJava/TypeRel.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/NanoJava/TypeRel.thy Sat May 16 11:28:23 2009 +0200 @@ -56,7 +56,7 @@ "subcls1 = (SIGMA C: {C. is_class C} . {D. C\Object \ super (the (class C)) = D})" apply (unfold subcls1_def is_class_def) -apply auto +apply (auto split:split_if_asm) done lemma finite_subcls1: "finite subcls1" diff -r 8448ba49d681 -r 8741df04d1ae src/HOL/Set.thy --- a/src/HOL/Set.thy Fri May 15 15:13:09 2009 -0700 +++ b/src/HOL/Set.thy Sat May 16 11:28:23 2009 +0200 @@ -1034,6 +1034,29 @@ subsubsection {* Set reasoning tools *} +text{* Elimination of @{text"{x. \ & x=t & \}"}. *} + +lemma singleton_conj_conv[simp]: "{x. x=a & 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 + +ML{* + local + val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN + ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}), + DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])]) + in + val defColl_regroup = Simplifier.simproc (the_context ()) + "defined Collect" ["{x. P x & Q x}"] + (Quantifier1.rearrange_Coll Coll_perm_tac) + end; + + Addsimprocs [defColl_regroup]; + +*} + text {* Rewrite rules for boolean case-splitting: faster than @{text "split_if [split]"}. diff -r 8448ba49d681 -r 8741df04d1ae src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Fri May 15 15:13:09 2009 -0700 +++ b/src/Provers/quantifier1.ML Sat May 16 11:28:23 2009 +0200 @@ -21,11 +21,21 @@ "!x. x=t --> P(x)" is covered by the congreunce rule for -->; "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. As must be "? x. t=x & P(x)". - And similarly for the bounded quantifiers. Gries etc call this the "1 point rules" + +The above also works for !x1..xn. and ?x1..xn by moving the defined +qunatifier inside first, but not for nested bounded quantifiers. + +For set comprehensions the basic permutations + ... & x = t & ... -> x = t & (... & ...) + ... & t = x & ... -> t = x & (... & ...) +are also exported. + +To avoid looping, NONE is returned if the term cannot be rearranged, +esp if x=t/t=x sits at the front already. *) signature QUANTIFIER1_DATA = @@ -61,6 +71,7 @@ val rearrange_ex: theory -> simpset -> term -> thm option val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option + val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option end; functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = @@ -70,29 +81,28 @@ (* FIXME: only test! *) fun def xs eq = - let val n = length xs - in case dest_eq eq of - SOME(c,s,t) => - s = Bound n andalso not(loose_bvar1(t,n)) orelse - t = Bound n andalso not(loose_bvar1(s,n)) - | NONE => false - end; + (case dest_eq eq of + SOME(c,s,t) => + let val n = length xs + in s = Bound n andalso not(loose_bvar1(t,n)) orelse + t = Bound n andalso not(loose_bvar1(s,n)) end + | NONE => false); -fun extract_conj xs t = case dest_conj t of NONE => NONE +fun extract_conj fst xs t = case dest_conj t of NONE => NONE | SOME(conj,P,Q) => - (if def xs P then SOME(xs,P,Q) else + (if not fst andalso def xs P then SOME(xs,P,Q) else if def xs Q then SOME(xs,Q,P) else - (case extract_conj xs P of + (case extract_conj false xs P of SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) - | NONE => (case extract_conj xs Q of + | NONE => (case extract_conj false xs Q of SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q') | NONE => NONE))); -fun extract_imp xs t = case dest_imp t of NONE => NONE - | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q) - else (case extract_conj xs P of +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) + else (case extract_conj false xs P of SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) - | NONE => (case extract_imp xs Q of + | NONE => (case extract_imp false xs Q of NONE => NONE | SOME(xs,eq,Q') => SOME(xs,eq,imp$P$Q'))); @@ -100,8 +110,8 @@ fun extract_quant extract q = let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) = if qa = q then exqu ((qC,x,T)::xs) Q else NONE - | exqu xs P = extract xs P - in exqu end; + | exqu xs P = extract (null xs) xs P + in exqu [] end; fun prove_conv tac thy tu = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) @@ -147,7 +157,7 @@ in quant xs (qC $ Abs(x,T,Q)) end; fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) = - (case extract_quant extract_imp q [] P of + (case extract_quant extract_imp q P of NONE => NONE | SOME(xs,eq,Q) => let val R = quantify all x T xs (imp $ eq $ Q) @@ -155,7 +165,7 @@ | rearrange_all _ _ _ = NONE; fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) = - (case extract_imp [] P of + (case extract_imp true [] P of NONE => NONE | SOME(xs,eq,Q) => if not(null xs) then NONE else let val R = imp $ eq $ Q @@ -163,7 +173,7 @@ | rearrange_ball _ _ _ _ = NONE; fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) = - (case extract_quant extract_conj q [] P of + (case extract_quant extract_conj q P of NONE => NONE | SOME(xs,eq,Q) => let val R = quantify ex x T xs (conj $ eq $ Q) @@ -171,10 +181,17 @@ | rearrange_ex _ _ _ = NONE; fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) = - (case extract_conj [] P of + (case extract_conj true [] P of NONE => NONE | SOME(xs,eq,Q) => if not(null xs) then NONE else SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q)))) | rearrange_bex _ _ _ _ = NONE; +fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) = + (case extract_conj true [] P of + NONE => NONE + | SOME(_,eq,Q) => + let val R = Coll $ Abs(x,T, conj $ eq $ Q) + in SOME(prove_conv tac thy (F,R)) end); + end;