# HG changeset patch
# User wenzelm
# Date 1303476791 -7200
# Node ID 5dfae6d348fdcb0443fb1f5af096aa2a0758ef09
# Parent  de868abd131ef8e55ec343e807d6bca0cc4a5de2
misc tuning;

diff -r de868abd131e -r 5dfae6d348fd src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 22 14:38:49 2011 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 22 14:53:11 2011 +0200
@@ -52,8 +52,8 @@
 
 
 (** make simplification procedures for quantifier elimination **)
-structure Quantifier1 = Quantifier1Fun(
-struct
+structure Quantifier1 = Quantifier1
+(
   (*abstract syntax*)
   fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
     | dest_eq _ = NONE;
@@ -78,7 +78,7 @@
   val iff_exI = @{thm iff_exI}
   val all_comm = @{thm all_comm}
   val ex_comm = @{thm ex_comm}
-end);
+);
 
 
 (*** Case splitting ***)
diff -r de868abd131e -r 5dfae6d348fd src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 14:38:49 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 14:53:11 2011 +0200
@@ -7,8 +7,8 @@
 
 (** tools setup **)
 
-structure Quantifier1 = Quantifier1Fun
-(struct
+structure Quantifier1 = Quantifier1
+(
   (*abstract syntax*)
   fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
     | dest_eq _ = NONE;
@@ -33,7 +33,7 @@
   val iff_exI = @{thm iff_exI}
   val all_comm = @{thm all_comm}
   val ex_comm = @{thm ex_comm}
-end);
+);
 
 structure Simpdata =
 struct
diff -r de868abd131e -r 5dfae6d348fd src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Apr 22 14:38:49 2011 +0200
+++ b/src/Provers/quantifier1.ML	Fri Apr 22 14:53:11 2011 +0200
@@ -7,7 +7,7 @@
             ? x. ... & x = t & ...
      into   ? x. x = t & ... & ...
      where the `? x. x = t &' in the latter formula must be eliminated
-           by ordinary simplification. 
+           by ordinary simplification.
 
      and   ! x. (... & x = t & ...) --> P x
      into  ! x. x = t --> (... & ...) --> P x
@@ -20,7 +20,7 @@
         "!x. x=t --> P(x)" is covered by the congruence 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"
@@ -40,21 +40,21 @@
 signature QUANTIFIER1_DATA =
 sig
   (*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 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
+  val imp: term
   (*rules*)
   val iff_reflection: thm (* P <-> Q ==> P == Q *)
-  val iffI:  thm
+  val iffI: thm
   val iff_trans: thm
   val conjI: thm
   val conjE: thm
-  val impI:  thm
-  val mp:    thm
-  val exI:   thm
-  val exE:   thm
+  val impI: thm
+  val mp: thm
+  val exI: thm
+  val exE: 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) *)
   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
@@ -73,41 +73,51 @@
   val rearrange_Collect: tactic -> simpset -> term -> thm option
 end;
 
-functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
+functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
 struct
 
 (* FIXME: only test! *)
 fun def xs eq =
   (case Data.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);
+    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 fst xs t = case Data.dest_conj t of NONE => NONE
-    | SOME(conj,P,Q) =>
-        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
-         if def xs Q then SOME(xs,Q,P) else
-         (case extract_conj false xs P of
-            SOME(xs,eq,P') => SOME(xs,eq, Data.conj $ P' $ Q)
-          | NONE => (case extract_conj false xs Q of
-                       SOME(xs,eq,Q') => SOME(xs,eq,Data.conj $ P $ Q')
-                     | NONE => NONE)));
+fun extract_conj fst xs t =
+  (case Data.dest_conj t of
+    NONE => NONE
+  | SOME (conj, P, Q) =>
+      if def xs P then (if fst then NONE else SOME (xs, P, Q))
+      else if def xs Q then SOME (xs, Q, P)
+      else
+        (case extract_conj false xs P of
+          SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
+        | NONE =>
+            (case extract_conj false xs Q of
+              SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
+            | NONE => NONE)));
 
-fun extract_imp fst xs t = case Data.dest_imp t of NONE => NONE
-    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
-                       else (case extract_conj false xs P of
-                               SOME(xs,eq,P') => SOME(xs, eq, Data.imp $ P' $ Q)
-                             | NONE => (case extract_imp false xs Q of
-                                          NONE => NONE
-                                        | SOME(xs,eq,Q') =>
-                                            SOME(xs,eq,Data.imp$P$Q')));
+fun extract_imp fst xs t =
+  (case Data.dest_imp t of
+    NONE => NONE
+  | SOME (imp, P, Q) =>
+      if def xs P then (if fst then NONE else SOME (xs, P, Q))
+      else
+        (case extract_conj false xs P of
+          SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q)
+        | NONE =>
+            (case extract_imp false xs Q of
+              NONE => NONE
+            | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q'))));
 
 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 (null xs) xs P
+  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 (null xs) xs P
   in exqu [] end;
 
 fun prove_conv tac ss tu =
@@ -119,81 +129,89 @@
       Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
   in singleton (Variable.export ctxt' ctxt) thm end;
 
-fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
+fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
 
 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
    Better: instantiate exI
 *)
 local
-val excomm = Data.ex_comm RS Data.iff_trans
+  val excomm = Data.ex_comm RS Data.iff_trans;
 in
-val prove_one_point_ex_tac = qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
-    ALLGOALS(EVERY'[etac Data.exE, REPEAT_DETERM o (etac Data.conjE), rtac Data.exI,
-                    DEPTH_SOLVE_1 o (ares_tac [Data.conjI])])
+  val prove_one_point_ex_tac =
+    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
+    ALLGOALS
+      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
+        DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
 end;
 
 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
 *)
 local
-val tac = SELECT_GOAL
-          (EVERY1[REPEAT o (dtac Data.uncurry), REPEAT o (rtac Data.impI), etac Data.mp,
-                  REPEAT o (etac Data.conjE), REPEAT o (ares_tac [Data.conjI])])
-val allcomm = Data.all_comm RS Data.iff_trans
+  val tac =
+    SELECT_GOAL
+      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
+        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
+  val allcomm = Data.all_comm RS Data.iff_trans;
 in
-val prove_one_point_all_tac =
-      EVERY1[qcomm_tac allcomm Data.iff_allI,rtac Data.iff_allI, rtac Data.iffI, tac, tac]
+  val prove_one_point_all_tac =
+    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
 end
 
-fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
-                                   if i=u then l else i+1)
-  | renumber l u (s$t) = renumber l u s $ renumber l u t
-  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
+fun renumber l u (Bound i) =
+      Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
+  | renumber l u (s $ t) = renumber l u s $ renumber l u t
+  | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
   | renumber _ _ atom = atom;
 
 fun quantify qC x T xs P =
-  let fun quant [] P = P
-        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
-      val n = length xs
-      val Q = if n=0 then P else renumber 0 n P
-  in quant xs (qC $ Abs(x,T,Q)) end;
+  let
+    fun quant [] P = P
+      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
+    val n = length xs;
+    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)) =
-     (case extract_quant extract_imp q P of
+fun rearrange_all ss (F as (all as Const (q, _)) $ Abs (x, T, P)) =
+      (case extract_quant extract_imp q P of
         NONE => NONE
-      | SOME(xs,eq,Q) =>
+      | 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)
+          in SOME (prove_conv prove_one_point_all_tac ss (F, R)) end)
   | rearrange_all _ _ = NONE;
 
-fun rearrange_ball tac ss (F as Ball $ A $ Abs(x,T,P)) =
-     (case extract_imp true [] P of
+fun rearrange_ball tac ss (F as Ball $ A $ Abs (x, T, P)) =
+      (case extract_imp true [] P of
         NONE => NONE
-      | SOME(xs,eq,Q) => if not(null xs) then NONE else
-          let val R = Data.imp $ eq $ Q
-          in SOME (prove_conv tac ss (F,Ball $ A $ Abs(x,T,R))) end)
+      | SOME (xs, eq, Q) =>
+          if not (null xs) then NONE
+          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;
 
-fun rearrange_ex ss (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
-     (case extract_quant extract_conj q P of
+fun rearrange_ex ss (F as (ex as Const (q, _)) $ Abs (x, T, P)) =
+      (case extract_quant extract_conj q P of
         NONE => NONE
-      | SOME(xs,eq,Q) =>
+      | 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)
+          in SOME (prove_conv prove_one_point_ex_tac ss (F, R)) end)
   | rearrange_ex _ _ = NONE;
 
-fun rearrange_bex tac ss (F as Bex $ A $ Abs(x,T,P)) =
-     (case extract_conj true [] P of
+fun rearrange_bex tac ss (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))))
+      | 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;
 
-fun rearrange_Collect tac ss (F as Coll $ Abs(x,T,P)) =
-     (case extract_conj true [] P of
+fun rearrange_Collect tac ss (F as Collect $ Abs (x, T, P)) =
+      (case extract_conj true [] P of
         NONE => NONE
-      | SOME(_,eq,Q) =>
-          let val R = Coll $ Abs(x,T, Data.conj $ eq $ Q)
-          in SOME(prove_conv tac ss (F,R)) end);
+      | 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;
 
 end;