gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;

--- a/src/HOL/Tools/Presburger/qelim.ML	Sun Jun 17 13:39:39 2007 +0200
+++ b/src/HOL/Tools/Presburger/qelim.ML	Sun Jun 17 13:39:45 2007 +0200
@@ -8,9 +8,9 @@
 
 signature QELIM =
  sig
- val standard_qelim_conv: (cterm list -> cterm -> thm) ->
+ val standard_qelim_conv: Proof.context -> (cterm list -> cterm -> thm) ->
    (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
- val gen_qelim_conv: Conv.conv -> Conv.conv -> Conv.conv ->
+ val gen_qelim_conv: Proof.context -> Conv.conv -> Conv.conv -> Conv.conv ->
    (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) ->
    ('a -> Conv.conv) -> ('a -> cterm -> thm) -> Conv.conv
 
@@ -20,29 +20,40 @@
 struct
 open Conv;
 
-val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
-
-fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv  = 
- let fun conv p =
-  case (term_of p) of 
-   Const(s,T)$_$_ => if domain_type T = HOLogic.boolT 
-                        andalso s mem ["op &","op |","op -->","op ="]
-                    then binop_conv conv p else atcv env p
- | Const("Not",_)$_ => arg_conv conv p
- | Const("Ex",_)$Abs(s,_,_) => 
-   let 
-    val (e,p0) = Thm.dest_comb p
-    val (x,p') = Thm.dest_abs (SOME s) p0
-    val th = Thm.abstract_rule s x 
-                  (((gen_qelim_conv precv postcv simpex_conv ins (ins x env) atcv ncv qcv) 
-                      then_conv (ncv (ins x env))) p')
-                  |> Drule.arg_cong_rule e
-    val th' = simpex_conv (Thm.rhs_of th)
-    val (l,r) = Thm.dest_equals (cprop_of th')
-   in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th))
-      else Thm.transitive (Thm.transitive th th') (conv r) end
- | _ => atcv env p
- in precv then_conv conv then_conv postcv end;
+local
+ val all_not_ex = mk_meta_eq @{thm "all_not_ex"}
+in
+fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv  = 
+ let 
+  val thy = ProofContext.theory_of ctxt
+  fun conv env p =
+   case (term_of p) of 
+    Const(s,T)$_$_ => if domain_type T = HOLogic.boolT 
+                         andalso s mem ["op &","op |","op -->","op ="]
+                     then binop_conv (conv env) p else atcv env p
+  | Const("Not",_)$_ => arg_conv (conv env) p
+  | Const("Ex",_)$Abs(s,_,_) => 
+    let 
+     val (e,p0) = Thm.dest_comb p
+     val (x,p') = Thm.dest_abs (SOME s) p0
+     val env' = ins x env
+     val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
+                   |> Drule.arg_cong_rule e
+     val th' = simpex_conv (Thm.rhs_of th)
+     val (l,r) = Thm.dest_equals (cprop_of th')
+    in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th))
+       else Thm.transitive (Thm.transitive th th') (conv env r) end
+  | Const("Ex",_)$ _ => (eta_conv thy then_conv conv env) p 
+  | Const("All",_)$_ => 
+    let 
+     val p = Thm.dest_arg p
+     val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
+     val th = instantiate' [SOME T] [SOME p] all_not_ex 
+    in transitive th (conv env (Thm.rhs_of th)) 
+    end
+  | _ => atcv env p
+ in precv then_conv (conv env) then_conv postcv end
+end;
 
 fun cterm_frees ct = 
  let fun h acc t = 
@@ -53,12 +64,13 @@
   | _ => acc
  in h [] ct end;
 
-val standard_qelim_conv = 
- let val pcv = Simplifier.rewrite 
-                 (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) 
-                     @ [not_all,ex_disj_distrib]))
- in fn atcv => fn ncv => fn qcv => fn p => 
-       gen_qelim_conv pcv pcv pcv (curry (op ::)) (cterm_frees p) atcv ncv qcv p 
- end;
+local
+val pcv = Simplifier.rewrite 
+                 (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) 
+                     @ [@{thm "all_not_ex"}, not_all,ex_disj_distrib])
+in 
+fun standard_qelim_conv ctxt atcv ncv qcv p = 
+    gen_qelim_conv ctxt pcv pcv pcv cons (cterm_frees p) atcv ncv qcv p 
+end;
 
 end;