# HG changeset patch
# User wenzelm
# Date 1303477504 -7200
# Node ID 38b9f023cc34330f75d36a6f0024a3e007239ffd
# Parent  5dfae6d348fdcb0443fb1f5af096aa2a0758ef09
misc tuning and simplification;

diff -r 5dfae6d348fd -r 38b9f023cc34 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/FOL/FOL.thy	Fri Apr 22 15:05:04 2011 +0200
@@ -306,13 +306,8 @@
 
 use "simpdata.ML"
 
-simproc_setup defined_Ex ("EX x. P(x)") = {*
-  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
-*}
-
-simproc_setup defined_All ("ALL x. P(x)") = {*
-  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
-*}
+simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
+simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
 
 ML {*
 (*intuitionistic simprules only*)
diff -r 5dfae6d348fd -r 38b9f023cc34 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 22 15:05:04 2011 +0200
@@ -1212,13 +1212,8 @@
 
 setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
 
-simproc_setup defined_Ex ("EX x. P x") = {*
-  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
-*}
-
-simproc_setup defined_All ("ALL x. P x") = {*
-  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
-*}
+simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
+simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
 
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
diff -r 5dfae6d348fd -r 38b9f023cc34 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/HOL/Set.thy	Fri Apr 22 15:05:04 2011 +0200
@@ -76,14 +76,12 @@
 *}
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
-  let
-    val Collect_perm_tac =
-      rtac @{thm Collect_cong} 1 THEN
+  fn _ =>
+    Quantifier1.rearrange_Collect
+     (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 @{thms conjI}]);
-  in
-    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
-  end
+      ALLGOALS
+        (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
 *}
 
 lemmas CollectE = CollectD [elim_format]
@@ -331,18 +329,14 @@
   let
     val unfold_bex_tac = unfold_tac @{thms Bex_def};
     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
 *}
 
 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
   let
     val unfold_ball_tac = unfold_tac @{thms Ball_def};
     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
 *}
 
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
diff -r 5dfae6d348fd -r 38b9f023cc34 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/Provers/quantifier1.ML	Fri Apr 22 15:05:04 2011 +0200
@@ -66,11 +66,11 @@
 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
-  val rearrange_all: simpset -> term -> thm option
-  val rearrange_ex: simpset -> term -> thm option
-  val rearrange_ball: tactic -> simpset -> term -> thm option
-  val rearrange_bex: tactic -> simpset -> term -> thm option
-  val rearrange_Collect: tactic -> simpset -> term -> thm option
+  val rearrange_all: simpset -> cterm -> thm option
+  val rearrange_ex: simpset -> cterm -> thm option
+  val rearrange_ball: tactic -> simpset -> cterm -> thm option
+  val rearrange_bex: tactic -> simpset -> cterm -> thm option
+  val rearrange_Collect: tactic -> simpset -> cterm -> thm option
 end;
 
 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -172,15 +172,19 @@
     val Q = if n = 0 then P else renumber 0 n P;
   in quant xs (qC $ Abs (x, T, Q)) end;
 
-fun rearrange_all ss (F as (all as Const (q, _)) $ Abs (x, T, P)) =
+fun rearrange_all ss ct =
+  (case term_of ct of
+    F as (all as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_imp q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify all x T xs (Data.imp $ eq $ Q)
           in SOME (prove_conv prove_one_point_all_tac ss (F, R)) end)
-  | rearrange_all _ _ = NONE;
+  | _ => NONE);
 
-fun rearrange_ball tac ss (F as Ball $ A $ Abs (x, T, P)) =
+fun rearrange_ball tac ss ct =
+  (case term_of ct of
+    F as Ball $ A $ Abs (x, T, P) =>
       (case extract_imp true [] P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
@@ -188,30 +192,36 @@
           else
             let val R = Data.imp $ eq $ Q
             in SOME (prove_conv tac ss (F, Ball $ A $ Abs (x, T, R))) end)
-  | rearrange_ball _ _ _ = NONE;
+  | _ => NONE);
 
-fun rearrange_ex ss (F as (ex as Const (q, _)) $ Abs (x, T, P)) =
+fun rearrange_ex ss ct =
+  (case term_of ct of
+    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_conj q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify ex x T xs (Data.conj $ eq $ Q)
           in SOME (prove_conv prove_one_point_ex_tac ss (F, R)) end)
-  | rearrange_ex _ _ = NONE;
+  | _ => NONE);
 
-fun rearrange_bex tac ss (F as Bex $ A $ Abs (x, T, P)) =
+fun rearrange_bex tac ss ct =
+  (case term_of ct of
+    F as Bex $ A $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
           else SOME (prove_conv tac ss (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
-  | rearrange_bex _ _ _ = NONE;
+  | _ => NONE);
 
-fun rearrange_Collect tac ss (F as Collect $ Abs (x, T, P)) =
+fun rearrange_Collect tac ss ct =
+  (case term_of ct of
+    F as Collect $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (_, eq, Q) =>
           let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
           in SOME (prove_conv tac ss (F, R)) end)
-  | rearrange_Collect _ _ _ = NONE;
+  | _ => NONE);
 
 end;
diff -r 5dfae6d348fd -r 38b9f023cc34 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/ZF/OrdQuant.thy	Fri Apr 22 15:05:04 2011 +0200
@@ -372,18 +372,14 @@
   let
     val unfold_rex_tac = unfold_tac @{thms rex_def};
     fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss end
 *}
 
 simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {*
   let
     val unfold_rall_tac = unfold_tac @{thms rall_def};
     fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss end
 *}
 
 end
diff -r 5dfae6d348fd -r 38b9f023cc34 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri Apr 22 14:53:11 2011 +0200
+++ b/src/ZF/pair.thy	Fri Apr 22 15:05:04 2011 +0200
@@ -14,18 +14,14 @@
   let
     val unfold_bex_tac = unfold_tac @{thms Bex_def};
     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
 *}
 
 simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
   let
     val unfold_ball_tac = unfold_tac @{thms Ball_def};
     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in
-    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
-  end
+  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
 *}