Theory Reordering_Quantifiers

theory Reordering_Quantifiers
  imports Main
begin

lemma
  assumes A: "finite A"
  shows "finite {(a,b,c) | a b c. a ∈ A ∧ b < (n :: nat) ∧ P c}"
  using assms [[simproc add: finite_Collect]] apply simp
  oops

lemma
  assumes A: "finite A"
  shows "finite {(d, c, a, b) | a b c d. d < n ∧ P c ∧ (a, b) ∈ A}"
  using assms
  using [[simproc add: finite_Collect]] apply simp
  oops
  
lemma
  "finite {x . x ∈ A}" if "finite A"
  using [[simp_trace]]
  using that by simp

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. a ∈ A ∧ c < n ∧ t = (a,c)}"
  apply simp
  using assms by simp

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {(a, c). a ∈ A ∧ c < n}"
  apply simp
  using assms by simp

(* Printing util *)
ML ‹
  fun pretty_cterm ctxt ctm = Syntax.pretty_term ctxt (Thm.term_of ctm)
  val string_of_cterm = Pretty.string_of oo pretty_cterm
  val string_of_term = Pretty.string_of oo Syntax.pretty_term
›

ML_val ‹tracing (Syntax.string_of_term @{context} @{term "a < b"})›

ML_val ‹tracing (ML_Syntax.print_term @{term "a < b"})›

ML ‹
  fun strip_prop (Const (@{const_name HOL.Trueprop}, _) $ t) = t
    | strip_prop t = t
›

declare [[ML_print_depth = 50]]

ML ‹
  signature QUANTIFIER1_DATA =
sig
  (*functionality*)
  (*terms to be moved around*)
  (*arguments: preceding quantifies, term under question, preceding terms*)
  val move: (term * string * typ) list -> term -> term list -> bool
  (*always move? if false then moves appear if a non-mover was encountered before*)
  val force_move: bool
  (*rotate quantifiers after moving*)
  val rotate: bool
  (*abstract syntax*)
  val dest_eq: term -> (term * term) option
  val dest_conj: term -> (term * term) option
  val dest_imp: term -> (term * term) option
  val conj: term
  val imp: term
  (*rules*)
  val iff_reflection: thm (* P <-> Q ==> P == Q *)
  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 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) *)
  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
end;

signature QUANTIFIER1 =
sig
  val prove_one_point_all_tac: Proof.context -> tactic
  val prove_one_point_ex_tac: Proof.context -> tactic
  val rearrange_all: Proof.context -> cterm -> thm option
  (* XXX Need to export this ?*)
  val rearrange_ex': Proof.context -> term -> thm option
  val rearrange_ex: Proof.context -> cterm -> thm option
  val rotate_ex: Proof.context -> cterm -> thm option
  val miniscope_ex: Proof.context -> cterm -> thm option
  val rotate_all: Proof.context -> cterm -> thm option
  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
end;

functor Quantifier(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
struct

fun extract_conj trms fst xs t =
  (case Data.dest_conj t of
    NONE => NONE
  | SOME (P, Q) =>
      let
        val mover = Data.move xs P trms
      in
        if Data.force_move andalso mover then (if fst then NONE else SOME (xs, P, Q))
        else if Data.force_move andalso Data.move xs Q (P :: trms) then SOME (xs, Q, P)
        else if mover andalso not fst then SOME (xs, P, Q)
        else if
          not Data.force_move andalso (not mover orelse not fst) andalso Data.move xs Q (P :: trms)
          then SOME (xs, Q, P)
        else
          (case extract_conj trms (if Data.force_move then false else fst) xs P of
            SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
          | NONE =>
              (case extract_conj (P :: trms)
                    (if Data.force_move then false else (fst andalso mover)) xs Q
               of
                SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
              | NONE => NONE))
      end);
(* XXX This is not regularized with respect to term context *)
fun extract_imp fst xs t =
  (case Data.dest_imp t of
    NONE => NONE
  | SOME (P, Q) =>
      if Data.move 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 (if Data.force_move then null xs else true) xs P
  in exqu [] end;

fun prove_conv ctxt tu tac =
  let
    val (goal, ctxt') =
      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
    val thm =
      Goal.prove ctxt' [] [] goal
        (fn {context = ctxt'', ...} =>
          resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt'');
  in singleton (Variable.export ctxt' ctxt) thm end;

fun maybe_tac tac = if Data.rotate then tac else K all_tac;

fun qcomm_tac ctxt qcomm qI i =
  REPEAT_DETERM (maybe_tac (resolve_tac ctxt [qcomm]) i THEN resolve_tac ctxt [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;
in
  fun prove_rotate_ex_tac ctxt i = qcomm_tac ctxt excomm Data.iff_exI i
  fun prove_one_point_ex_tac ctxt =
    prove_rotate_ex_tac ctxt 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
    ALLGOALS
      (EVERY' [maybe_tac (eresolve_tac ctxt [Data.exE]),
        REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
        maybe_tac (resolve_tac ctxt [Data.exI]),
        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
end;

(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
*)
local
  fun tac ctxt =
    SELECT_GOAL
      (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry],
        REPEAT o resolve_tac ctxt [Data.impI],
        eresolve_tac ctxt [Data.mp],
        REPEAT o eresolve_tac ctxt [Data.conjE],
        REPEAT o ares_tac ctxt [Data.conjI]]);
  val allcomm = Data.all_comm RS Data.iff_trans;
in
  fun prove_one_point_all_tac ctxt =
    EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI,
      resolve_tac ctxt [Data.iff_allI],
      resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt];
end

(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
*)
local
  val allcomm = Data.all_comm RS Data.iff_trans;
in
  fun prove_one_point_all_tac2 ctxt =
    EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI,
      resolve_tac ctxt [Data.iff_allI],
      resolve_tac ctxt [Data.iffI], blast_tac ctxt, blast_tac ctxt];
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)
  | 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 if Data.rotate then quant xs (qC $ Abs (x, T, Q)) else qC $ Abs (x, T, quant xs P) end;

fun rearrange_all ctxt ct =
  (case Thm.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 ctxt (F, R) prove_one_point_all_tac) end)
  | _ => NONE);

fun rotate_all ctxt ct =
  let
    fun extract fst xs P =
      if fst then NONE else SOME (xs, P, P)
    in
  (case strip_prop (Thm.term_of ct) of
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
      (case extract_quant extract q P of
        NONE => NONE
      | SOME (xs, _, Q) =>
          let val R = quantify ex x T xs Q
          in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac2) end)
  | _ => NONE) end;

fun rearrange_ball tac ctxt ct =
  (case Thm.term_of ct of
    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 ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
  | _ => NONE);

fun rearrange_ex' ctxt trm =
  (case strip_prop trm 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 ctxt (F, R) prove_one_point_ex_tac) end)
  | _ => NONE);

fun rearrange_ex ctxt = rearrange_ex' ctxt o Thm.term_of

fun rotate_ex ctxt ct =
  let
    fun extract fst xs P =
      if fst then NONE else SOME (xs, P, P)
    in
  (case strip_prop (Thm.term_of ct) of
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
      (case extract_quant extract q P of
        NONE => NONE
      | SOME (xs, _, Q) =>
          let val R = quantify ex x T xs Q
          in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
  | _ => NONE) end;

fun miniscope_ex ctxt ct =
  let
    fun extract fst xs t =
      case Data.dest_conj t of
        SOME (P, _) => if Data.move xs P [] andalso not fst then SOME (xs, t, t) else NONE
      | NONE => NONE
    in
  (case strip_prop (Thm.term_of ct) of
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
      (case extract_quant extract q P of
        NONE => NONE
      | SOME (xs, _, Q) =>
          let val R = quantify ex x T xs Q
          in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
  | _ => NONE) end;

fun rearrange_bex tac ctxt ct =
  (case Thm.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 ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
  | _ => NONE);

fun rearrange_Collect tac ctxt ct =
  (case Thm.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 ctxt (F, R) tac) end)
  | _ => NONE);

end;

structure Quantifier1 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move xs eq _ =
  (case dest_eq eq of
    SOME (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);
  val force_move = true
  val rotate = true
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

(* loose_bvar2(t,k) iff t contains a 'loose' bound variable referring to
   a level below k. *)
fun loose_bvar2(Bound i,k) = i < k
  | loose_bvar2(f$t, k) = loose_bvar2(f,k) orelse loose_bvar2(t,k)
  | loose_bvar2(Abs(_,_,t),k) = loose_bvar2(t,k+1)
  | loose_bvar2 _ = false;

structure Quantifier2 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move xs t _ =  
      let val n = length xs in
        loose_bvar1 (t, n) andalso not (loose_bvar2 (t, n))
      end
  val force_move = false
  val rotate = false
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

structure Quantifier3 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move xs t _ =  
      let val n = length xs in
        loose_bvar1 (t, n) andalso not (loose_bvar (t, n + 1))
      end
  val force_move = false
  val rotate = false
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

signature Int_Param =
  sig
    val x : int
  end;

fun is_conj (Const(@{const_name HOL.conj},_) $ _ $ _) = true
    | is_conj _ = false;

functor Quantifier4 (to_move: Int_Param) = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move _ P trms = length trms + 1 = to_move.x andalso not (is_conj P)
  val force_move = true
  val rotate = false
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

structure Quantifier5 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move _ t _ = is_conj t
  val force_move = true
  val rotate = false
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

structure Quantifier6 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move xs t _ =  
      let val n = length xs in
        not (loose_bvar1 (t, n))
      end
  val force_move = true
  val rotate = true
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

structure Quantifier7 = Quantifier
(
  (*abstract syntax*)
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    | dest_eq _ = NONE;
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    | dest_conj _ = NONE;
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    | dest_imp _ = NONE;
  val conj = HOLogic.conj
  val imp  = HOLogic.imp
  fun move xs t _ =  
      let val n = length xs in
        not (loose_bvar1 (t, n))
      end
  val force_move = true
  val rotate = true
  (*rules*)
  val iff_reflection = @{thm eq_reflection}
  val iffI = @{thm iffI}
  val iff_trans = @{thm trans}
  val conjI= @{thm conjI}
  val conjE= @{thm conjE}
  val impI = @{thm impI}
  val mp   = @{thm mp}
  val uncurry = @{thm uncurry}
  val exI  = @{thm exI}
  val exE  = @{thm exE}
  val iff_allI = @{thm iff_allI}
  val iff_exI = @{thm iff_exI}
  val all_comm = @{thm all_comm}
  val ex_comm = @{thm ex_comm}
);

›

ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a ∈ A"}›
ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a = b"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. a = b ∧ c < n"}›
ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∃ a c. a = b ∧ c < n"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a = b"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. a < n ∧ a = b"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. a < n ∧ c < n ∧ a = b"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a > c"}›
ML_val ‹Quantifier3.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a > c"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ a > b"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "∃ a c. c < n ∧ (P a c ∧ a > b) ∧ Q c"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "finite {(a, c) | a c. c < n ∧ a ∈ A}"}›
ML_val ‹Quantifier2.rearrange_ex @{context} @{cterm "finite {t. ∃ a c. a ∈ A ∧ c < n ∧ t = (a,c)}"}›
ML_val ‹Quantifier1.rotate_ex @{context} @{cterm "∃ a c. c < n ∧ a > b"}›
ML_val ‹Quantifier1.rotate_ex @{context} @{cterm "∃ a c d. c < n ∧ a > b ∧ P d"}›
ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∃ a c. a < n ∧ c = b"}›
ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∀ a. ∃ c. a < n ∧ c = b"}›
ML_val ‹Quantifier1.rearrange_ex @{context} @{cterm "∀ a c. a < n ∧ c = b"}›
ML_val ‹Quantifier6.rearrange_ex @{context} @{cterm "∃ a b c. a < n ∧ b < 3 ∧ b > c"}›
ML_val ‹Quantifier6.rearrange_ex @{context} @{cterm "∃b c. a < n ∧ b < 3 ∧ b > c"}›
ML_val ‹Quantifier7.miniscope_ex @{context} @{cterm "∃ a b c. a < n ∧ b < 3 ∧ b > c"}›
ML_val ‹Quantifier7.miniscope_ex @{context} @{cterm "∃b c. a < n ∧ b < 3 ∧ b > c"}›

simproc_setup ex_reorder ("∃x. P x") = ‹fn _ => Quantifier2.rearrange_ex›
declare [[simproc del: ex_reorder]]
simproc_setup ex_reorder2 ("∃x. P x") = ‹fn _ => Quantifier3.rearrange_ex›
declare [[simproc del: ex_reorder2]]
simproc_setup ex_reorder3 ("∃x. P x") = ‹fn _ => Quantifier6.rearrange_ex›
declare [[simproc del: ex_reorder3]]
simproc_setup ex_reorder4 ("∃x. P x") = ‹fn _ => Quantifier7.miniscope_ex›
declare [[simproc del: ex_reorder4]]

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {(a, c). c < n ∧ a ∈ A}"
  using assms
    using [[simproc add: finite_Collect]]
    by simp

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {(a, c) | a c. c < n ∧ a ∈ A}"
  using assms
  using [[simproc add: ex_reorder]]
    by simp

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. a ∈ A ∧ c < n ∧ t = (a,c)}"
  apply simp
  using assms apply simp
  oops

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. (t = (a,c) ∧ c < n) ∧ a ∈ A}"
      using [[simproc add: ex_reorder]]
  using [[simp_trace]] apply simp
  using assms by simp

lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. (t = (a,c) ∧ a ∈ A) ∧ c < n}"
  using [[simp_trace]] apply (simp del: Product_Type.Collect_case_prod)
  using assms by simp
  
lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. (a ∈ A ∧ t = (a,c)) ∧ c < n}"
  using [[simp_trace]] apply simp
  using assms by simp
  
lemma
  fixes n :: nat
  assumes A: "finite A"
  shows "finite {t. ∃ a c. a ∈ A ∧ c < n ∧ t = (a,c)}"
  using [[simp_trace]] apply simp
  using assms by simp
  
lemma
  assumes A: "finite A"
  shows "finite {t. ∃ a c. a ∈ A ∧ P c ∧ t = (a,c)}"
  using [[simp_trace]] apply simp
  using assms apply simp
  oops

ML ‹
  fun rotate_quant reorder_thm n ctxt =
    let
      fun subst j =
        if j > n then K all_tac else
          (
            EqSubst.eqsubst_tac ctxt [j] [reorder_thm]
          ) THEN' subst (j + 1)
    in subst 1 end;
›

ML ‹
  fun rotate_ex_tac ctxt =
    let
      fun foc_tac {concl, ...} =
        case Quantifier1.rotate_ex ctxt concl of
          NONE => no_tac
        | SOME thm => rewrite_goals_tac ctxt [thm]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;
›

ML ‹
  fun rotate_all_tac ctxt =
    let
      fun foc_tac {concl, ...} =
        case Quantifier1.rotate_all ctxt concl of
          NONE => no_tac
        | SOME thm => rewrite_goals_tac ctxt [thm]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;
›

ML ‹
  fun rearrange_ex_tac ctxt =
    let
      fun foc_tac {concl, ...} =
        case Quantifier2.rearrange_ex ctxt concl of
          NONE => no_tac
        | SOME thm => rewrite_goals_tac ctxt [thm]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;
›

ML ‹
  fun rearrange_ex_tac2 ctxt =
    let
      fun foc_tac {concl, ...} =
        case Quantifier3.rearrange_ex ctxt concl of
          NONE => no_tac
        | SOME thm => rewrite_goals_tac ctxt [thm]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;
›

ML ‹

  fun strip_fin (Const (@{const_name "finite"}, _) $ (Const (@{const_name "Collect"}, _) $ t)) = t
    | strip_fin t = t

  fun wrap_fin tac ctxt = tac ctxt o strip_fin

  structure Quant2 = Quantifier4(val x = 2);
  structure Quant3 = Quantifier4(val x = 3);
  structure Quant4 = Quantifier4(val x = 4);
  structure Quant5 = Quantifier4(val x = 5);

  fun rearrange_ex_fixed_n rearrange_n ctxt =
    let
      fun foc_tac {concl, ...} =
        case rearrange_n ctxt concl of
          NONE => no_tac
        | SOME thm => rewrite_goals_tac ctxt [thm, @{thm HOL.conj_assoc} RS @{thm HOL.eq_reflection}]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;
  
  val rearrange_ex_fixed_2 = rearrange_ex_fixed_n Quant2.rearrange_ex;
  val rearrange_ex_fixed_3 = rearrange_ex_fixed_n Quant3.rearrange_ex;
  val rearrange_ex_fixed_4 = rearrange_ex_fixed_n Quant4.rearrange_ex;
  val rearrange_ex_fixed_5 = rearrange_ex_fixed_n Quant5.rearrange_ex;

  (* val defer_ex = rearrange_ex_fixed_n (wrap_fin Quantifier5.rearrange_ex); *)

  fun CONV conv ctxt =
    let
      fun foc_tac {concl, ...} =
        rewrite_goals_tac ctxt [conv ctxt concl]
    in
      Subgoal.FOCUS foc_tac ctxt
    end;

  fun mk_conv f ctxt ct =
    case (f ctxt ct) of
      SOME thm => thm
    | _ => raise CTERM ("no conversion", [])

  fun success_conv cv ct =
    let
      val eq = cv ct
    in
      if Thm.is_reflexive eq then raise CTERM ("no conversion", []) else eq
    end

  fun mk_conv' f ctxt ct = the_default (Thm.reflexive ct) (f ctxt ct)
  val assoc_conv = Conv.rewr_conv (@{thm HOL.conj_assoc} RS @{thm HOL.eq_reflection})
  val comm_conv = Conv.rewr_conv (@{thm HOL.conj_commute} RS @{thm HOL.eq_reflection})
  fun wrap_conv f ctxt =
    success_conv (
      Conv.top_sweep_conv (fn ctxt => mk_conv f ctxt then_conv Conv.repeat_conv assoc_conv) ctxt
    )
  fun mk_tac conv ctxt = CONVERSION (Conv.concl_conv ~1 (Object_Logic.judgment_conv ctxt (conv ctxt)))

  val defer_conv = mk_conv Quantifier5.rearrange_ex
  val conv = wrap_conv Quantifier5.rearrange_ex
  fun defer_ex_tac ctxt i =
    CHANGED (mk_tac (fn ctxt => wrap_conv Quantifier5.rearrange_ex ctxt else_conv Conv.top_sweep_conv (K comm_conv) ctxt) ctxt i)
  val mini_ex_tac = mk_tac (wrap_conv Quantifier6.rearrange_ex)
  val mini_ex_tac2 = mk_tac (wrap_conv Quantifier7.miniscope_ex)

  val rearrange_ex_fixed_2 = mk_tac (wrap_conv Quant2.rearrange_ex);
  val rearrange_ex_fixed_3 = mk_tac (wrap_conv Quant3.rearrange_ex);
  val rearrange_ex_fixed_4 = mk_tac (wrap_conv Quant4.rearrange_ex);
  val rearrange_ex_fixed_5 = mk_tac (wrap_conv Quant5.rearrange_ex);
›

ML_val ‹defer_conv @{context} @{cterm "∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"}›
ML_val ‹assoc_conv @{cterm "(a < 1 ∧ b < 2) ∧ c < 3 ∧ d < 4"}›
ML_val ‹Conv.binder_conv (K assoc_conv) @{context} @{cterm "∃ a. (a < 1 ∧ b < 2) ∧ c < 3 ∧ d < 4"}›
ML_val ‹Conv.top_sweep_conv (K assoc_conv) @{context} @{cterm "∃ a b c d. (a < 1 ∧ b < 2) ∧ c < 3 ∧ d < 4"}›
ML_val ‹Conv.bottom_conv (K (Conv.try_conv assoc_conv)) @{context} @{cterm "∃ a b c d. (a < 1 ∧ b < 2) ∧ c < 3 ∧ d < 4"}›
ML_val ‹Conv.every_conv [defer_conv @{context}, Conv.try_conv assoc_conv] @{cterm "∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"}›
ML_val ‹conv @{context} @{cterm "∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"}›
ML_val ‹conv @{context} @{cterm "finite {t. ∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4}"}›
ML_val ‹conv @{context} @{cterm "∃a b c d. d = 4 ∧ c = 3 ∧ b < 2 ∧ a < 1"}›

ML_val ‹Quantifier1.rotate_ex @{context} @{cterm "∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"}›

ML_val ‹Quantifier1.rotate_all @{context} @{cterm "∀ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"}›

lemma
  "∀ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  apply (tactic ‹rotate_all_tac @{context} 1›)
  apply (tactic ‹rotate_all_tac @{context} 1›)
  apply (tactic ‹rotate_all_tac @{context} 1›)
  apply (tactic ‹rotate_all_tac @{context} 1›)
  apply (tactic ‹rotate_all_tac @{context} 1›)
  oops

lemma
  "∃ a b c d. a < 1 ∧ b < 2 ∧ c = 3 ∧ d = 4"
  apply (tactic ‹rearrange_ex_fixed_2 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_3 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_4 @{context} 1›)
  apply (tactic ‹defer_ex_tac @{context} 1›)
  apply (subst conj_assoc)+
  oops

lemma
  "finite {t. ∃ a b c d. a < 1 ∧ b < 2 ∧ c = 3 ∧ d = 4}"
  apply (tactic ‹rearrange_ex_fixed_2 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_3 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_4 @{context} 1›)
  apply (tactic ‹defer_ex_tac @{context} 1›)
  oops
  
lemma
  "finite S ⟹ finite {t. ∃ a b c d. a < 1 ∧ b < 2 ∧ c = 3 ∧ d = 4}"
  apply (tactic ‹rearrange_ex_fixed_2 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_3 @{context} 1›)
  apply (tactic ‹rearrange_ex_fixed_4 @{context} 1›)
  apply (tactic ‹defer_ex_tac @{context} 1›, simp only: conj_assoc)
  oops

lemma
  "finite S ⟹ finite {t. ∃ a b c d. P a b d ∧ c > 3}"
  apply (tactic ‹defer_ex_tac @{context} 1›)
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply (simp only: ex_simps)
  oops

lemma
  "∃ a b c d. d < 4 ∧ a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  using [[simproc add: ex_reorder3]]
  apply simp
  oops

lemma
  "∃ a b c d. d < 4 ∧ a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  using [[simproc add: ex_reorder4]]
  apply simp
  oops

lemma
  "∃ a b c d. d < 4 ∧ a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  oops

lemma
  "∃ a b c d. d < 4 ∧ a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  apply (tactic ‹mini_ex_tac2 @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac2 @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac2 @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  apply (tactic ‹mini_ex_tac @{context} 1›)
  apply simp
  oops
  
lemma
  "∃ a c b d. d < 4 ∧ a < 1 ∧ b < 2 ∧ c < 3"
  apply simp
  oops
  
lemma
  "∃ a b c d. a < 1 ∧ b < 2 ∧ c < 3 ∧ d < 4"
  apply (tactic ‹rotate_ex_tac @{context} 1›)
  apply (tactic ‹rotate_ex_tac @{context} 1›)
  apply (tactic ‹rotate_ex_tac @{context} 1›)
  apply (tactic ‹rotate_ex_tac @{context} 1›)
  apply (tactic ‹rotate_ex_tac @{context} 1›)
  oops

lemma
  "∃ a b c d. b < 2 ∧ c < 3 ∧ d < 4 ∧ a < 1"
  apply (tactic ‹rearrange_ex_tac @{context} 1›)
  oops

lemma
  "∃ a b c d. b < 2 ∧ c < 3 ∧ d < 4 ∧ a < c"
  apply (tactic ‹rearrange_ex_tac2 @{context} 1›; simp only: conj_assoc)+
  oops

lemma
  "∃ a b c d. b < 2 ∧ c < 3 ∧ d < 4 ∧ a < c"
  apply (tactic ‹rearrange_ex_tac2 @{context} 1›; simp del: ex_simps)+
  oops

lemma
  "∃ a b c d. b < 2 ∧ c < 3 ∧ d < 4 ∧ a < c"
  apply (tactic ‹rearrange_ex_tac2 @{context} 1›)
  apply (simp del: ex_simps)
  apply (tactic ‹rearrange_ex_tac2 @{context} 1›)
  apply (simp del: ex_simps)
  apply (tactic ‹rearrange_ex_tac2 @{context} 1›)
  using [[simp_trace]]
  apply (simp del: ex_simps)
  oops

lemma finite_Collect_bounded_ex_4:
  assumes "finite {(a,b,c,d) . P a b c d}"
  shows
    "finite {x. ∃a b c d. P a b c d ∧ Q x a b c d}
    ⟷ (∀ a b c d. P a b c d ⟶ finite {x. Q x a b c d})"
proof -
  have *:
    "{x. ∃a b c d. P a b c d ∧ Q x a b c d}
    = {x. ∃ t. t ∈ {(a,b,c,d). P a b c d} ∧ (∃a b c d. t = (a, b, c, d) ∧ Q x a b c d)}"
    by simp
  show ?thesis apply (subst *)
    apply (subst finite_Collect_bounded_ex)
    using assms by simp+
oops
  
lemma finite_Collect_bounded_ex_4':
  assumes "finite {(a,b,c,d) | a b c d. P a b c d}"
  shows
    "finite {x. ∃a b c d. P a b c d ∧ Q x a b c d}
    ⟷ (∀ a b c d. P a b c d ⟶ finite {x. Q x a b c d})"
proof -
  have *:
    "{x. ∃a b c d. P a b c d ∧ Q x a b c d}
    = {x. ∃ t. t ∈ {(a,b,c,d) | a b c d. P a b c d} ∧ (∃a b c d. t = (a, b, c, d) ∧ Q x a b c d)}"
    by simp
  show ?thesis apply (subst *)
    apply (subst finite_Collect_bounded_ex)
    using assms by simp+
qed

lemma finite_Collect_bounded_ex_2 [simp]:
  assumes "finite {(a,b). P a b}"
  shows
    "finite {x. ∃a b. P a b ∧ Q x a b}
    ⟷ (∀ a b. P a b ⟶ finite {x. Q x a b})"
  using assms finite_Collect_bounded_ex[OF assms, where Q = "λ x. λ (a, b). Q x a b"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_3 [simp]:
  assumes "finite {(a,b,c) . P a b c}"
  shows
    "finite {x. ∃a b c. P a b c ∧ Q x a b c}
    ⟷ (∀ a b c. P a b c ⟶ finite {x. Q x a b c})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c). Q x a b c"]
  by clarsimp

lemma finite_Collect_bounded_ex_4 [simp]:
  assumes "finite {(a,b,c,d) . P a b c d}"
  shows
    "finite {x. ∃a b c d. P a b c d ∧ Q x a b c d}
    ⟷ (∀ a b c d. P a b c d ⟶ finite {x. Q x a b c d})"
  using assms finite_Collect_bounded_ex[OF assms, where Q = "λ x. λ (a, b, c, d). Q x a b c d"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_5 [simp]:
  assumes "finite {(a,b,c,d,e) . P a b c d e}"
  shows
    "finite {x. ∃a b c d e. P a b c d e ∧ Q x a b c d e}
    ⟷ (∀ a b c d e. P a b c d e ⟶ finite {x. Q x a b c d e})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e). Q x a b c d e"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_6 [simp]:
  assumes "finite {(a,b,c,d,e,f) . P a b c d e f}"
  shows
    "finite {x. ∃a b c d e f. P a b c d e f ∧ Q x a b c d e f}
    ⟷ (∀ a b c d e f. P a b c d e f ⟶ finite {x. Q x a b c d e f})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e, f). Q x a b c d e f"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_7 [simp]:
  assumes "finite {(a,b,c,d,e,f,g) . P a b c d e f g}"
  shows
    "finite {x. ∃a b c d e f g. P a b c d e f g ∧ Q x a b c d e f g}
    ⟷ (∀ a b c d e f g. P a b c d e f g ⟶ finite {x. Q x a b c d e f g})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e, f, g). Q x a b c d e f g"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_8 [simp]:
  assumes "finite {(a,b,c,d,e,f,g,h) . P a b c d e f g h}"
  shows
    "finite {x. ∃a b c d e f g h. P a b c d e f g h ∧ Q x a b c d e f g h}
    ⟷ (∀ a b c d e f g h. P a b c d e f g h ⟶ finite {x. Q x a b c d e f g h})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e, f, g, h). Q x a b c d e f g h"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_9 [simp]:
  assumes "finite {(a,b,c,d,e,f,g,h,i) . P a b c d e f g h i}"
  shows
    "finite {x. ∃a b c d e f g h i. P a b c d e f g h i ∧ Q x a b c d e f g h i}
    ⟷ (∀ a b c d e f g h i. P a b c d e f g h i ⟶ finite {x. Q x a b c d e f g h i})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e, f, g, h, i). Q x a b c d e f g h i"]
  by clarsimp (* force, simp *)

lemma finite_Collect_bounded_ex_10 [simp]:
  assumes "finite {(a,b,c,d,e,f,g,h,i,j) . P a b c d e f g h i j}"
  shows
    "finite {x. ∃a b c d e f g h i j. P a b c d e f g h i j ∧ Q x a b c d e f g h i j}
    ⟷ (∀ a b c d e f g h i j. P a b c d e f g h i j ⟶ finite {x. Q x a b c d e f g h i j})"
  using assms finite_Collect_bounded_ex
    [OF assms, where Q = "λ x. λ (a, b, c, d, e, f, g, h, i, j). Q x a b c d e f g h i j"]
  by clarsimp (* force, simp *)

end