"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
authornipkow
Sat May 16 11:28:02 2009 +0200 (2009-05-16)
changeset 31166a90fe83f58ea
parent 31159 bac0d673b6d6
child 31167 8741df04d1ae
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".
src/HOL/Bali/Example.thy
src/HOL/HOL.thy
src/HOL/Library/Binomial.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Set.thy
src/Provers/quantifier1.ML
     1.1 --- a/src/HOL/Bali/Example.thy	Fri May 15 10:01:57 2009 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Sat May 16 11:28:02 2009 +0200
     1.3 @@ -1075,10 +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 -apply (unfold max_spec_def)
     1.8 -apply (simp (no_asm) add: appl_methds_Base_foo)
     1.9 -apply auto
    1.10 -done
    1.11 +by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
    1.12  
    1.13  section "well-typedness"
    1.14  
     2.1 --- a/src/HOL/HOL.thy	Fri May 15 10:01:57 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat May 16 11:28:02 2009 +0200
     2.3 @@ -1050,8 +1050,7 @@
     2.4      "(P | False) = P"  "(False | P) = P"
     2.5      "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
     2.6      "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
     2.7 -    -- {* needed for the one-point-rule quantifier simplification procs *}
     2.8 -    -- {* essential for termination!! *} and
     2.9 +  and
    2.10      "!!P. (EX x. x=t & P(x)) = P(t)"
    2.11      "!!P. (EX x. t=x & P(x)) = P(t)"
    2.12      "!!P. (ALL x. x=t --> P(x)) = P(t)"
     3.1 --- a/src/HOL/Library/Binomial.thy	Fri May 15 10:01:57 2009 +0200
     3.2 +++ b/src/HOL/Library/Binomial.thy	Sat May 16 11:28:02 2009 +0200
     3.3 @@ -88,9 +88,7 @@
     3.4  
     3.5  lemma card_s_0_eq_empty:
     3.6      "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
     3.7 -  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
     3.8 -  apply (simp cong add: rev_conj_cong)
     3.9 -  done
    3.10 +by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
    3.11  
    3.12  lemma choose_deconstruct: "finite M ==> x \<notin> M
    3.13    ==> {s. s <= insert x M & card(s) = Suc k}
     4.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Fri May 15 10:01:57 2009 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 11:28:02 2009 +0200
     4.3 @@ -69,10 +69,11 @@
     4.4  lemma subcls1:
     4.5    "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
     4.6                  (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
     4.7 -  apply (simp add: subcls1_def2)
     4.8 -  apply (simp add: name_defs class_defs system_defs E_def class_def)
     4.9 -  apply (auto simp: expand_fun_eq split: split_if_asm)
    4.10 -  done
    4.11 +apply (simp add: subcls1_def2)
    4.12 +apply (simp add: name_defs class_defs system_defs E_def class_def)
    4.13 +apply (auto simp: expand_fun_eq name_defs[symmetric] class_defs split:split_if_asm)
    4.14 +apply(simp add:name_defs)+
    4.15 +done
    4.16  
    4.17  text {* The subclass relation is acyclic; hence its converse is well founded: *}
    4.18  lemma notin_rtrancl:
     5.1 --- a/src/HOL/NanoJava/TypeRel.thy	Fri May 15 10:01:57 2009 +0200
     5.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sat May 16 11:28:02 2009 +0200
     5.3 @@ -56,7 +56,7 @@
     5.4    "subcls1 = 
     5.5      (SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     5.6  apply (unfold subcls1_def is_class_def)
     5.7 -apply auto
     5.8 +apply (auto split:split_if_asm)
     5.9  done
    5.10  
    5.11  lemma finite_subcls1: "finite subcls1"
     6.1 --- a/src/HOL/Set.thy	Fri May 15 10:01:57 2009 +0200
     6.2 +++ b/src/HOL/Set.thy	Sat May 16 11:28:02 2009 +0200
     6.3 @@ -1034,6 +1034,29 @@
     6.4  
     6.5  subsubsection {* Set reasoning tools *}
     6.6  
     6.7 +text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
     6.8 +
     6.9 +lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
    6.10 +by auto
    6.11 +
    6.12 +lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
    6.13 +by auto
    6.14 +
    6.15 +ML{*
    6.16 +  local
    6.17 +    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    6.18 +    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    6.19 +                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    6.20 +  in
    6.21 +    val defColl_regroup = Simplifier.simproc (the_context ())
    6.22 +      "defined Collect" ["{x. P x & Q x}"]
    6.23 +      (Quantifier1.rearrange_Coll Coll_perm_tac)
    6.24 +  end;
    6.25 +
    6.26 +  Addsimprocs [defColl_regroup];
    6.27 +
    6.28 +*}
    6.29 +
    6.30  text {*
    6.31    Rewrite rules for boolean case-splitting: faster than @{text
    6.32    "split_if [split]"}.
     7.1 --- a/src/Provers/quantifier1.ML	Fri May 15 10:01:57 2009 +0200
     7.2 +++ b/src/Provers/quantifier1.ML	Sat May 16 11:28:02 2009 +0200
     7.3 @@ -21,11 +21,21 @@
     7.4          "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
     7.5          "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
     7.6          As must be "? x. t=x & P(x)".
     7.7 -
     7.8          
     7.9       And similarly for the bounded quantifiers.
    7.10  
    7.11  Gries etc call this the "1 point rules"
    7.12 +
    7.13 +The above also works for !x1..xn. and ?x1..xn by moving the defined
    7.14 +qunatifier inside first, but not for nested bounded quantifiers.
    7.15 +
    7.16 +For set comprehensions the basic permutations
    7.17 +      ... & x = t & ...  ->  x = t & (... & ...)
    7.18 +      ... & t = x & ...  ->  t = x & (... & ...)
    7.19 +are also exported.
    7.20 +
    7.21 +To avoid looping, NONE is returned if the term cannot be rearranged,
    7.22 +esp if x=t/t=x sits at the front already.
    7.23  *)
    7.24  
    7.25  signature QUANTIFIER1_DATA =
    7.26 @@ -61,6 +71,7 @@
    7.27    val rearrange_ex:  theory -> simpset -> term -> thm option
    7.28    val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
    7.29    val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
    7.30 +  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
    7.31  end;
    7.32  
    7.33  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    7.34 @@ -70,29 +81,28 @@
    7.35  
    7.36  (* FIXME: only test! *)
    7.37  fun def xs eq =
    7.38 -  let val n = length xs
    7.39 -  in case dest_eq eq of
    7.40 -      SOME(c,s,t) =>
    7.41 -        s = Bound n andalso not(loose_bvar1(t,n)) orelse
    7.42 -        t = Bound n andalso not(loose_bvar1(s,n))
    7.43 -    | NONE => false
    7.44 -  end;
    7.45 +  (case dest_eq eq of
    7.46 +     SOME(c,s,t) =>
    7.47 +       let val n = length xs
    7.48 +       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
    7.49 +          t = Bound n andalso not(loose_bvar1(s,n)) end
    7.50 +   | NONE => false);
    7.51  
    7.52 -fun extract_conj xs t = case dest_conj t of NONE => NONE
    7.53 +fun extract_conj fst xs t = case dest_conj t of NONE => NONE
    7.54      | SOME(conj,P,Q) =>
    7.55 -        (if def xs P then SOME(xs,P,Q) else
    7.56 +        (if not fst andalso def xs P then SOME(xs,P,Q) else
    7.57           if def xs Q then SOME(xs,Q,P) else
    7.58 -         (case extract_conj xs P of
    7.59 +         (case extract_conj false xs P of
    7.60              SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
    7.61 -          | NONE => (case extract_conj xs Q of
    7.62 +          | NONE => (case extract_conj false xs Q of
    7.63                         SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q')
    7.64                       | NONE => NONE)));
    7.65  
    7.66 -fun extract_imp xs t = case dest_imp t of NONE => NONE
    7.67 -    | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
    7.68 -                       else (case extract_conj xs P of
    7.69 +fun extract_imp fst xs t = case dest_imp t of NONE => NONE
    7.70 +    | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
    7.71 +                       else (case extract_conj false xs P of
    7.72                                 SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
    7.73 -                             | NONE => (case extract_imp xs Q of
    7.74 +                             | NONE => (case extract_imp false xs Q of
    7.75                                            NONE => NONE
    7.76                                          | SOME(xs,eq,Q') =>
    7.77                                              SOME(xs,eq,imp$P$Q')));
    7.78 @@ -100,8 +110,8 @@
    7.79  fun extract_quant extract q =
    7.80    let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
    7.81              if qa = q then exqu ((qC,x,T)::xs) Q else NONE
    7.82 -        | exqu xs P = extract xs P
    7.83 -  in exqu end;
    7.84 +        | exqu xs P = extract (null xs) xs P
    7.85 +  in exqu [] end;
    7.86  
    7.87  fun prove_conv tac thy tu =
    7.88    Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
    7.89 @@ -147,7 +157,7 @@
    7.90    in quant xs (qC $ Abs(x,T,Q)) end;
    7.91  
    7.92  fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
    7.93 -     (case extract_quant extract_imp q [] P of
    7.94 +     (case extract_quant extract_imp q P of
    7.95          NONE => NONE
    7.96        | SOME(xs,eq,Q) =>
    7.97            let val R = quantify all x T xs (imp $ eq $ Q)
    7.98 @@ -155,7 +165,7 @@
    7.99    | rearrange_all _ _ _ = NONE;
   7.100  
   7.101  fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
   7.102 -     (case extract_imp [] P of
   7.103 +     (case extract_imp true [] P of
   7.104          NONE => NONE
   7.105        | SOME(xs,eq,Q) => if not(null xs) then NONE else
   7.106            let val R = imp $ eq $ Q
   7.107 @@ -163,7 +173,7 @@
   7.108    | rearrange_ball _ _ _ _ = NONE;
   7.109  
   7.110  fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
   7.111 -     (case extract_quant extract_conj q [] P of
   7.112 +     (case extract_quant extract_conj q P of
   7.113          NONE => NONE
   7.114        | SOME(xs,eq,Q) =>
   7.115            let val R = quantify ex x T xs (conj $ eq $ Q)
   7.116 @@ -171,10 +181,17 @@
   7.117    | rearrange_ex _ _ _ = NONE;
   7.118  
   7.119  fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
   7.120 -     (case extract_conj [] P of
   7.121 +     (case extract_conj true [] P of
   7.122          NONE => NONE
   7.123        | SOME(xs,eq,Q) => if not(null xs) then NONE else
   7.124            SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   7.125    | rearrange_bex _ _ _ _ = NONE;
   7.126  
   7.127 +fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
   7.128 +     (case extract_conj true [] P of
   7.129 +        NONE => NONE
   7.130 +      | SOME(_,eq,Q) =>
   7.131 +          let val R = Coll $ Abs(x,T, conj $ eq $ Q)
   7.132 +          in SOME(prove_conv tac thy (F,R)) end);
   7.133 +
   7.134  end;