# HG changeset patch
# User nipkow
# Date 985867194 -7200
# Node ID 558a4feebb049d981b47726ed8de977047563e0f
# Parent  30d96882f91565a9269f7e7bbcfd4b45bcce518c
generalization of 1 point rules for ALL

diff -r 30d96882f915 -r 558a4feebb04 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/FOL/simpdata.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -218,6 +218,15 @@
     "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
 
 
+local
+val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
+              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
+
+val iff_allI = allI RS
+    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
+               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+in
+
 (** make simplification procedures for quantifier elimination **)
 structure Quantifier1 = Quantifier1Fun(
 struct
@@ -226,30 +235,32 @@
     | dest_eq _ = None;
   fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
     | dest_conj _ = None;
+  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
+    | dest_imp _ = None;
   val conj = FOLogic.conj
   val imp  = FOLogic.imp
   (*rules*)
   val iff_reflection = iff_reflection
   val iffI = iffI
-  val sym  = sym
   val conjI= conjI
   val conjE= conjE
   val impI = impI
-  val impE = impE
   val mp   = mp
+  val uncurry = uncurry
   val exI  = exI
   val exE  = exE
-  val allI = allI
-  val allE = allE
+  val iff_allI = iff_allI
 end);
 
+end;
+
 local
 
 val ex_pattern =
   read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
 
 val all_pattern =
-  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
+  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
 
 in
 val defEX_regroup =
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -93,7 +93,6 @@
 by (Simp_tac 1);
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
 by (rename_tac "vss lrst" 1);  
@@ -116,7 +115,6 @@
 by (Simp_tac 1);
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
@@ -155,7 +153,6 @@
 by (Simp_tac 1);
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
 by (rename_tac "vss lrst" 1);  
@@ -193,7 +190,6 @@
 by (Simp_tac 1);
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A list (next A a st)" 1);
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -396,7 +396,7 @@
 \  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
 \          (? s. (start R,s) : steps R v & q = False#s))))";
 by (blast_tac (claset() addDs [True_steps_concD]
-     addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
+     addIs [True_True_steps_concI,in_steps_epsclosure]) 1);
 qed "True_steps_conc";
 
 (** starting from the start **)
@@ -537,7 +537,7 @@
 by (induct_tac "us" 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
-by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,in_epsclosure_steps]) 1);
 qed_spec_mp "steps_star_cycle";
 
 (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
@@ -578,7 +578,7 @@
  by (Blast_tac 1);
 by (etac disjE 1);
  by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [in_steps_epsclosure]) 1);
 qed "start_steps_star";
 
 Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -317,63 +317,61 @@
 (* case Let e1 e2 *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 by (strip_tac 1);
-by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
+(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
+by (rename_tac "S1 t1 m1 S2" 1); 
 by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
-by (simp_tac (simpset() addsimps [o_def]) 1);
-by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
-by (rtac (has_type_cl_sub RS spec) 1);
-by (dres_inst_tac [("x","A")] spec 1);
-by (dres_inst_tac [("x","S1")] spec 1);
-by (dres_inst_tac [("x","t1")] spec 1);
-by (dres_inst_tac [("x","m2")] spec 1);
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x","m1")] spec 1);
-by (mp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+ by (simp_tac (simpset() addsimps [o_def]) 1);
+ by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+ by (rtac (has_type_cl_sub RS spec) 1);
+ by (dres_inst_tac [("x","A")] spec 1);
+ by (dres_inst_tac [("x","S1")] spec 1);
+ by (dres_inst_tac [("x","t1")] spec 1);
+ by (dres_inst_tac [("x","m1")] spec 1);
+ by (dres_inst_tac [("x","n")] spec 1);
+ by (mp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 by (simp_tac (simpset() addsimps [o_def]) 1);
 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
 by (rtac (gen_subst_commutes RS sym RS subst) 1);
-by (rtac (app_subst_Cons RS subst) 2);
-by (etac thin_rl 2);
-by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
-by (dres_inst_tac [("x","S2")] spec 2);
-by (dres_inst_tac [("x","t")] spec 2);
-by (dres_inst_tac [("x","n2")] spec 2);
-by (dres_inst_tac [("x","m2")] spec 2);
-by (ftac new_tv_W 2);
-by (assume_tac 2);
-by (dtac conjunct1 2);
-by (dtac conjunct1 2);
-by (ftac new_tv_subst_scheme_list 2);
-by (rtac new_scheme_list_le 2);
-by (rtac W_var_ge 2);
-by (assume_tac 2);
-by (assume_tac 2);
-by (etac impE 2);
-by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
-by (Simp_tac 2);
-by (Fast_tac 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
+ by (rtac (app_subst_Cons RS subst) 2);
+ by (etac thin_rl 2);
+ by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
+ by (dres_inst_tac [("x","S2")] spec 2);
+ by (dres_inst_tac [("x","t")] spec 2);
+ by (dres_inst_tac [("x","m")] spec 2);
+ by (dres_inst_tac [("x","m1")] spec 2);
+ by (ftac new_tv_W 2);
+  by (assume_tac 2);
+ by (dtac conjunct1 2);
+ by (ftac new_tv_subst_scheme_list 2);
+  by (rtac new_scheme_list_le 2);
+   by (rtac W_var_ge 2);
+   by (assume_tac 2);
+  by (assume_tac 2);
+ by (etac impE 2);
+  by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
+   by (Simp_tac 2);
+   by (Fast_tac 2);
+  by (assume_tac 2);
+ by (Asm_full_simp_tac 2);
 by (rtac weaken_A_Int_B_eq_empty 1);
 by (rtac allI 1);
 by (strip_tac 1);
 by (rtac weaken_not_elem_A_minus_B 1);
-by (case_tac "x < m2" 1);
-by (rtac disjI2 1);
-by (rtac (free_tv_gen_cons RS subst) 1);
-by (rtac free_tv_W 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (assume_tac 1);
+by (case_tac "x < m1" 1);
+ by (rtac disjI2 1);
+ by (rtac (free_tv_gen_cons RS subst) 1);
+ by (rtac free_tv_W 1);
+   by (assume_tac 1);
+  by (Asm_full_simp_tac 1);
+ by (assume_tac 1);
 by (rtac disjI1 1);
 by (dtac new_tv_W 1);
 by (assume_tac 1);
 by (dtac conjunct2 1);
-by (dtac conjunct2 1);
 by (rtac new_tv_not_free_tv 1);
 by (rtac new_tv_le 1);
-by (assume_tac 2);
+ by (assume_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
 qed_spec_mp "W_correct_lemma";
 
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Set.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -100,6 +100,17 @@
 
 Addsimps [ball_triv, bex_triv];
 
+(* Blast cannot prove these (yet?).
+   Move somewhere else?
+Goal "(ALL x:A. x=a) = (A = {a})";
+by(Blast_tac 1);
+qed "ball_triv_one_point1";
+
+Goal "(ALL x:A. a=x) = (A = {a})";
+by(Blast_tac 1);
+qed "ball_triv_one_point2";
+*)
+
 Goal "(EX x:A. x=a) = (a:A)";
 by(Blast_tac 1);
 qed "bex_triv_one_point1";
@@ -112,6 +123,10 @@
 by(Blast_tac 1);
 qed "bex_one_point1";
 
+Goal "(EX x:A. a=x & P x) = (a:A & P a)";
+by(Blast_tac 1);
+qed "bex_one_point2";
+
 Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
 by(Blast_tac 1);
 qed "ball_one_point1";
@@ -120,7 +135,8 @@
 by(Blast_tac 1);
 qed "ball_one_point2";
 
-Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1,
+Addsimps [bex_triv_one_point1,bex_triv_one_point2,
+          bex_one_point1,bex_one_point2,
           ball_one_point1,ball_one_point2];
 
 let
@@ -133,14 +149,9 @@
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
-    ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+    ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT)
 
-val swap = prove_goal thy
-  "((!x. A x & EP x --> Q x) = (!x. E x --> A x & P x --> Q x)) ==> \
-\  ((!x. A x --> EP x --> Q x) = (!x. A x --> E x --> P x --> Q x))"
-  (fn ths => [cut_facts_tac ths 1, Blast_tac 1]);
-
-val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN
+val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
                      Quantifier1.prove_one_point_all_tac;
 
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/W0/I.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -58,10 +58,12 @@
 (** LEVEL 34 **)
 by (rtac conjI 1);
  by (strip_tac 1);
- by (mp_tac 1);
+ by (rtac notI 1);
+ by (Asm_full_simp_tac 1);
+(* by (mp_tac 1);
  by (mp_tac 1);
  by (etac exE 1);
- by (etac conjE 1);
+ by (etac conjE 1);*)
  by (etac impE 1);
   by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
   by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
@@ -73,10 +75,13 @@
 by (rename_tac "s2 t2' n2'" 1);
 by (rtac conjI 1);
  by (strip_tac 1);
+ by (rtac notI 1);
+ by (Asm_full_simp_tac 1);
+(*
  by (mp_tac 1);
  by (mp_tac 1);
  by (etac exE 1);
- by (etac conjE 1);
+ by (etac conjE 1);*)
  by (etac impE 1);
   by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
   by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/W0/W.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -50,7 +50,7 @@
 (* case App e1 e2 *)
 by (simp_tac (simpset() addsplits [split_bind]) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "s t na sa ta nb sb" 1);
 by (eres_inst_tac [("x","a")] allE 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","$ s a")] allE 1);
@@ -59,7 +59,6 @@
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (etac conjE 1);
 by (eres_inst_tac [("x","sa")] allE 1);
 by (eres_inst_tac [("x","ta")] allE 1);
 by (eres_inst_tac [("x","nb")] allE 1);
@@ -99,7 +98,7 @@
 (* case App e1 e2 *)
 by (simp_tac (simpset() addsplits [split_bind]) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "s t na sa ta nb sb" 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","a")] allE 1);
 by (eres_inst_tac [("x","s")] allE 1);
diff -r 30d96882f915 -r 558a4feebb04 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/simpdata.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -66,9 +66,12 @@
    "(P | ~P) = True",    "(~P | P) = True",
    "((~P) = (~Q)) = (P=Q)",
    "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
-(*two needed for the one-point-rule quantifier simplification procs*)
-   "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
-   "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
+(* needed for the one-point-rule quantifier simplification procs*)
+(*essential for termination!!*)
+   "(? x. x=t & P(x)) = P(t)",
+   "(? x. t=x & P(x)) = P(t)",
+   "(! x. x=t --> P(x)) = P(t)",
+   "(! x. t=x --> P(x)) = P(t)" ];
 
 val imp_cong = standard(impI RSN
     (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
@@ -256,6 +259,14 @@
 by (Blast_tac 1);
 qed "if_bool_eq_disj";
 
+local
+val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
+              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
+
+val iff_allI = allI RS
+    prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)"
+               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+in
 
 (*** make simplification procedures for quantifier elimination ***)
 
@@ -266,28 +277,30 @@
     | dest_eq _ = None;
   fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
     | dest_conj _ = None;
+  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
+    | dest_imp _ = None;
   val conj = HOLogic.conj
   val imp  = HOLogic.imp
   (*rules*)
   val iff_reflection = eq_reflection
   val iffI = iffI
-  val sym  = sym
   val conjI= conjI
   val conjE= conjE
   val impI = impI
-  val impE = impE
   val mp   = mp
+  val uncurry = uncurry
   val exI  = exI
   val exE  = exE
-  val allI = allI
-  val allE = allE
+  val iff_allI = iff_allI
 end);
 
+end;
+
 local
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
     ("EX x. P(x) & Q(x)",HOLogic.boolT)
 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
-    ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+    ("ALL x. P(x) --> Q(x)",HOLogic.boolT)
 in
 val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
       Quantifier1.rearrange_ex
diff -r 30d96882f915 -r 558a4feebb04 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Thu Mar 29 12:26:37 2001 +0200
+++ b/src/Provers/quantifier1.ML	Thu Mar 29 13:59:54 2001 +0200
@@ -7,7 +7,7 @@
 
             ? x. ... & x = t & ...
      into   ? x. x = t & ... & ...
-     where the `? x. x = t &' in the latter formula is eliminated
+     where the `? x. x = t &' in the latter formula must be eliminated
            by ordinary simplification. 
 
      and   ! x. (... & x = t & ...) --> P x
@@ -15,10 +15,14 @@
      where the `!x. x=t -->' in the latter formula is eliminated
            by ordinary simplification.
 
+     And analogously for t=x, but the eqn is not turned around!
+
      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
         "!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"
@@ -29,21 +33,20 @@
   (*abstract syntax*)
   val dest_eq: term -> (term*term*term)option
   val dest_conj: term -> (term*term*term)option
+  val dest_imp:  term -> (term*term*term)option
   val conj: term
   val imp:  term
   (*rules*)
   val iff_reflection: thm (* P <-> Q ==> P == Q *)
   val iffI:  thm
-  val sym:   thm
   val conjI: thm
   val conjE: thm
   val impI:  thm
-  val impE:  thm
   val mp:    thm
   val exI:   thm
   val exE:   thm
-  val allI:  thm
-  val allE:  thm
+  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
+  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
 end;
 
 signature QUANTIFIER1 =
@@ -61,28 +64,31 @@
 
 open Data;
 
+(* FIXME: only test! *)
 fun def eq = case dest_eq eq of
       Some(c,s,t) =>
-        if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
-        if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
-        else None
-    | None => None;
+        s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
+        t = Bound 0 andalso not(loose_bvar1(s,0))
+    | None => false;
 
-fun extract conj = case dest_conj conj of
-      Some(conj,P,Q) =>
-        (case def P of
-           Some eq => Some(eq,Q)
-         | None =>
-             (case def Q of
-                Some eq => Some(eq,P)
-              | None =>
-                 (case extract P of
-                    Some(eq,P') => Some(eq, conj $ P' $ Q)
-                  | None =>
-                      (case extract Q of
-                         Some(eq,Q') => Some(eq,conj $ P $ Q')
-                       | None => None))))
-    | None => None;
+fun extract_conj t = case dest_conj t of None => None
+    | Some(conj,P,Q) =>
+        (if def P then Some(P,Q) else
+         if def Q then Some(Q,P) else
+         (case extract_conj P of
+            Some(eq,P') => Some(eq, conj $ P' $ Q)
+          | None => (case extract_conj Q of
+                       Some(eq,Q') => Some(eq,conj $ P $ Q')
+                     | None => None)));
+
+fun extract_imp t = case dest_imp t of None => None
+    | Some(imp,P,Q) => if def P then Some(P,Q)
+                       else (case extract_conj P of
+                               Some(eq,P') => Some(eq, imp $ P' $ Q)
+                             | None => (case extract_imp Q of
+                                          None => None
+                                        | Some(eq,Q') => Some(eq, imp$P$Q')));
+    
 
 fun prove_conv tac sg tu =
   let val meta_eq = cterm_of sg (Logic.mk_equals tu)
@@ -97,44 +103,44 @@
 *)
 val prove_one_point_ex_tac = rtac iffI 1 THEN
     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
-                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
+                    DEPTH_SOLVE_1 o (ares_tac [conjI])]);
 
 (* Proves (! x. (... & x = t & ...) --> P x) =
           (! x. x = t --> (... & ...) --> P x)
 *)
-val prove_one_point_all_tac = EVERY1[rtac iffI,
-                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
-                          REPEAT o (etac conjE),
-                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
-                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
-                          etac impE, atac ORELSE' etac sym, etac mp,
-                          REPEAT o (ares_tac [conjI])];
+local
+val tac = SELECT_GOAL
+          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
+                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
+in
+val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
+end
 
-fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
-     (case extract P of
+fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
+     (case extract_imp P of
         None => None
-      | Some(eq,P') =>
-          let val R = imp $ eq $ (imp $ P' $ Q)
+      | Some(eq,Q) =>
+          let val R = imp $ eq $ Q
           in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
   | rearrange_all _ _ _ = None;
 
-fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* --> *)_ $ P $ Q)) =
-     (case extract P of
+fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
+     (case extract_imp P of
         None => None
-      | Some(eq,P') =>
-          let val R = imp $ eq $ (imp $ P' $ Q)
+      | Some(eq,Q) =>
+          let val R = imp $ eq $ Q
           in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   | rearrange_ball _ _ _ _ = None;
 
 fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
-     (case extract P of
+     (case extract_conj P of
         None => None
       | Some(eq,Q) =>
           Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
   | rearrange_ex _ _ _ = None;
 
 fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
-     (case extract P of
+     (case extract_conj P of
         None => None
       | Some(eq,Q) =>
           Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))