diff --git a/src/FOL/FOL.thy b/src/FOL/FOL.thy
--- a/src/FOL/FOL.thy
+++ b/src/FOL/FOL.thy
@@ -1,455 +1,455 @@
 (*  Title:      FOL/FOL.thy
     Author:     Lawrence C Paulson and Markus Wenzel
 *)
 
 section \<open>Classical first-order logic\<close>
 
 theory FOL
 imports IFOL
 keywords "print_claset" "print_induct_rules" :: diag
 begin
 
 ML_file \<open>~~/src/Provers/classical.ML\<close>
 ML_file \<open>~~/src/Provers/blast.ML\<close>
 ML_file \<open>~~/src/Provers/clasimp.ML\<close>
 
 
 subsection \<open>The classical axiom\<close>
 
 axiomatization where
   classical: \<open>(\<not> P \<Longrightarrow> P) \<Longrightarrow> P\<close>
 
 
 subsection \<open>Lemmas and proof tools\<close>
 
 lemma ccontr: \<open>(\<not> P \<Longrightarrow> False) \<Longrightarrow> P\<close>
   by (erule FalseE [THEN classical])
 
 
 subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
 
 lemma disjCI: \<open>(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q\<close>
   apply (rule classical)
   apply (assumption | erule meta_mp | rule disjI1 notI)+
   apply (erule notE disjI2)+
   done
 
 text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
 lemma ex_classical:
   assumes r: \<open>\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)\<close>
   shows \<open>\<exists>x. P(x)\<close>
   apply (rule classical)
   apply (rule exI, erule r)
   done
 
 text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
 lemma exCI:
   assumes r: \<open>\<forall>x. \<not> P(x) \<Longrightarrow> P(a)\<close>
   shows \<open>\<exists>x. P(x)\<close>
   apply (rule ex_classical)
   apply (rule notI [THEN allI, THEN r])
   apply (erule notE)
   apply (erule exI)
   done
 
 lemma excluded_middle: \<open>\<not> P \<or> P\<close>
   apply (rule disjCI)
   apply assumption
   done
 
 lemma case_split [case_names True False]:
   assumes r1: \<open>P \<Longrightarrow> Q\<close>
     and r2: \<open>\<not> P \<Longrightarrow> Q\<close>
   shows \<open>Q\<close>
   apply (rule excluded_middle [THEN disjE])
   apply (erule r2)
   apply (erule r1)
   done
 
 ML \<open>
   fun case_tac ctxt a fixes =
     Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
 \<close>
 
 method_setup case_tac = \<open>
   Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
     (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
 \<close> "case_tac emulation (dynamic instantiation!)"
 
 
 subsection \<open>Special elimination rules\<close>
 
 text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
 lemma impCE:
   assumes major: \<open>P \<longrightarrow> Q\<close>
     and r1: \<open>\<not> P \<Longrightarrow> R\<close>
     and r2: \<open>Q \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   apply (rule excluded_middle [THEN disjE])
    apply (erule r1)
   apply (rule r2)
   apply (erule major [THEN mp])
   done
 
 text \<open>
   This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''.
   Can't install as default: would break old proofs.
 \<close>
 lemma impCE':
   assumes major: \<open>P \<longrightarrow> Q\<close>
     and r1: \<open>Q \<Longrightarrow> R\<close>
     and r2: \<open>\<not> P \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   apply (rule excluded_middle [THEN disjE])
    apply (erule r2)
   apply (rule r1)
   apply (erule major [THEN mp])
   done
 
 text \<open>Double negation law.\<close>
 lemma notnotD: \<open>\<not> \<not> P \<Longrightarrow> P\<close>
   apply (rule classical)
   apply (erule notE)
   apply assumption
   done
 
 lemma contrapos2:  \<open>\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P\<close>
   apply (rule classical)
   apply (drule (1) meta_mp)
   apply (erule (1) notE)
   done
 
 
 subsubsection \<open>Tactics for implication and contradiction\<close>
 
 text \<open>
   Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in
   \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>.
 \<close>
 lemma iffCE:
   assumes major: \<open>P \<longleftrightarrow> Q\<close>
     and r1: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
     and r2: \<open>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   apply (rule major [unfolded iff_def, THEN conjE])
   apply (elim impCE)
      apply (erule (1) r2)
     apply (erule (1) notE)+
   apply (erule (1) r1)
   done
 
 
 (*Better for fast_tac: needs no quantifier duplication!*)
 lemma alt_ex1E:
   assumes major: \<open>\<exists>! x. P(x)\<close>
     and r: \<open>\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   using major
 proof (rule ex1E)
   fix x
   assume * : \<open>\<forall>y. P(y) \<longrightarrow> y = x\<close>
   assume \<open>P(x)\<close>
   then show \<open>R\<close>
   proof (rule r)
     {
       fix y y'
       assume \<open>P(y)\<close> and \<open>P(y')\<close>
       with * have \<open>x = y\<close> and \<open>x = y'\<close>
         by - (tactic "IntPr.fast_tac \<^context> 1")+
       then have \<open>y = y'\<close> by (rule subst)
     } note r' = this
     show \<open>\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<close>
       by (intro strip, elim conjE) (rule r')
   qed
 qed
 
 lemma imp_elim: \<open>P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R\<close>
   by (rule classical) iprover
 
 lemma swap: \<open>\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R\<close>
   by (rule classical) iprover
 
 
 section \<open>Classical Reasoner\<close>
 
 ML \<open>
 structure Cla = Classical
 (
   val imp_elim = @{thm imp_elim}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val classical = @{thm classical}
   val sizef = size_of_thm
   val hyp_subst_tacs = [hyp_subst_tac]
 );
 
 structure Basic_Classical: BASIC_CLASSICAL = Cla;
 open Basic_Classical;
 \<close>
 
 (*Propositional rules*)
 lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
   and [elim!] = conjE disjE impCE FalseE iffCE
 ML \<open>val prop_cs = claset_of \<^context>\<close>
 
 (*Quantifier rules*)
 lemmas [intro!] = allI ex_ex1I
   and [intro] = exI
   and [elim!] = exE alt_ex1E
   and [elim] = allE
 ML \<open>val FOL_cs = claset_of \<^context>\<close>
 
 ML \<open>
   structure Blast = Blast
   (
     structure Classical = Cla
     val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   );
   val blast_tac = Blast.blast_tac;
 \<close>
 
 
 lemma ex1_functional: \<open>\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c\<close>
   by blast
 
 text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
 lemma True_implies_equals: \<open>(True \<Longrightarrow> PROP P) \<equiv> PROP P\<close>
 proof
   assume \<open>True \<Longrightarrow> PROP P\<close>
   from this and TrueI show \<open>PROP P\<close> .
 next
   assume \<open>PROP P\<close>
   then show \<open>PROP P\<close> .
 qed
 
 lemma uncurry: \<open>P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R\<close>
   by blast
 
 lemma iff_allI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close>
   by blast
 
 lemma iff_exI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close>
   by blast
 
 lemma all_comm: \<open>(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))\<close>
   by blast
 
 lemma ex_comm: \<open>(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))\<close>
   by blast
 
 
 
 subsection \<open>Classical simplification rules\<close>
 
 text \<open>
   Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and
   false cases boil down to the same thing.
 \<close>
 
 lemma cases_simp: \<open>(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q\<close>
   by blast
 
 
 subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
 
 text \<open>
   We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of
   \<open>\<exists>\<close> over \<open>\<or>\<close>.
 
   Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
   this step can increase proof length!
 \<close>
 
 text \<open>Existential miniscoping.\<close>
 lemma int_ex_simps:
   \<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close>
   \<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close>
   \<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close>
   \<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close>
   by iprover+
 
 text \<open>Classical rules.\<close>
 lemma cla_ex_simps:
   \<open>\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close>
   \<open>\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))\<close>
   by blast+
 
 lemmas ex_simps = int_ex_simps cla_ex_simps
 
 text \<open>Universal miniscoping.\<close>
 lemma int_all_simps:
   \<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close>
   \<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close>
   \<open>\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q\<close>
   \<open>\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))\<close>
   by iprover+
 
 text \<open>Classical rules.\<close>
 lemma cla_all_simps:
   \<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close>
   \<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close>
   by blast+
 
 lemmas all_simps = int_all_simps cla_all_simps
 
 
 subsubsection \<open>Named rewrite rules proved for IFOL\<close>
 
 lemma imp_disj1: \<open>(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
 lemma imp_disj2: \<open>Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
 
 lemma de_Morgan_conj: \<open>(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)\<close> by blast
 
 lemma not_imp: \<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> by blast
 lemma not_iff: \<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)\<close> by blast
 
 lemma not_all: \<open>(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> by blast
 lemma imp_all: \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close> by blast
 
 
 lemmas meta_simps =
   triv_forall_equality  \<comment> \<open>prunes params\<close>
   True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
 
 lemmas IFOL_simps =
   refl [THEN P_iff_T] conj_simps disj_simps not_simps
   imp_simps iff_simps quant_simps
 
 lemma notFalseI: \<open>\<not> False\<close> by iprover
 
 lemma cla_simps_misc:
   \<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close>
   \<open>P \<or> \<not> P\<close>
   \<open>\<not> P \<or> P\<close>
   \<open>\<not> \<not> P \<longleftrightarrow> P\<close>
   \<open>(\<not> P \<longrightarrow> P) \<longleftrightarrow> P\<close>
   \<open>(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)\<close> by blast+
 
 lemmas cla_simps =
   de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
   not_imp not_all not_ex cases_simp cla_simps_misc
 
 
 ML_file \<open>simpdata.ML\<close>
 
-simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
 
 ML \<open>
 (*intuitionistic simprules only*)
 val IFOL_ss =
   put_simpset FOL_basic_ss \<^context>
   addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
   addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
   |> Simplifier.add_cong @{thm imp_cong}
   |> simpset_of;
 
 (*classical simprules too*)
 val FOL_ss =
   put_simpset IFOL_ss \<^context>
   addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
   |> simpset_of;
 \<close>
 
 setup \<open>
   map_theory_simpset (put_simpset FOL_ss) #>
   Simplifier.method_setup Splitter.split_modifiers
 \<close>
 
 ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
 
 
 subsection \<open>Other simple lemmas\<close>
 
 lemma [simp]: \<open>((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)\<close>
   by blast
 
 lemma [simp]: \<open>((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))\<close>
   by blast
 
 lemma not_disj_iff_imp: \<open>\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close>
   by blast
 
 
 subsubsection \<open>Monotonicity of implications\<close>
 
 lemma conj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)\<close>
   by fast (*or (IntPr.fast_tac 1)*)
 
 lemma disj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)\<close>
   by fast (*or (IntPr.fast_tac 1)*)
 
 lemma imp_mono: \<open>\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)\<close>
   by fast (*or (IntPr.fast_tac 1)*)
 
 lemma imp_refl: \<open>P \<longrightarrow> P\<close>
   by (rule impI)
 
 text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
 lemma ex_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close>
   by blast
 
 lemma all_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))\<close>
   by blast
 
 
 subsection \<open>Proof by cases and induction\<close>
 
 text \<open>Proper handling of non-atomic rule statements.\<close>
 
 context
 begin
 
 qualified definition \<open>induct_forall(P) \<equiv> \<forall>x. P(x)\<close>
 qualified definition \<open>induct_implies(A, B) \<equiv> A \<longrightarrow> B\<close>
 qualified definition \<open>induct_equal(x, y) \<equiv> x = y\<close>
 qualified definition \<open>induct_conj(A, B) \<equiv> A \<and> B\<close>
 
 lemma induct_forall_eq: \<open>(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))\<close>
   unfolding atomize_all induct_forall_def .
 
 lemma induct_implies_eq: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))\<close>
   unfolding atomize_imp induct_implies_def .
 
 lemma induct_equal_eq: \<open>(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))\<close>
   unfolding atomize_eq induct_equal_def .
 
 lemma induct_conj_eq: \<open>(A &&& B) \<equiv> Trueprop(induct_conj(A, B))\<close>
   unfolding atomize_conj induct_conj_def .
 
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric] = induct_atomize
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
 
 text \<open>Method setup.\<close>
 
 ML_file \<open>~~/src/Tools/induct.ML\<close>
 ML \<open>
   structure Induct = Induct
   (
     val cases_default = @{thm case_split}
     val atomize = @{thms induct_atomize}
     val rulify = @{thms induct_rulify}
     val rulify_fallback = @{thms induct_rulify_fallback}
     val equal_def = @{thm induct_equal_def}
     fun dest_def _ = NONE
     fun trivial_tac _ _ = no_tac
   );
 \<close>
 
 declare case_split [cases type: o]
 
 end
 
 ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
 
 hide_const (open) eq
 
 end
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -1,2141 +1,2141 @@
 (*  Title:      HOL/HOL.thy
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
 section \<open>The basis of Higher-Order Logic\<close>
 
 theory HOL
 imports Pure Tools.Code_Generator
 keywords
   "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
     "print_induct_rules" :: diag and
   "quickcheck_params" :: thy_decl
 abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/try.ML\<close>
 ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
 ML_file \<open>~~/src/Tools/solve_direct.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/classical.ML\<close>
 ML_file \<open>~~/src/Provers/blast.ML\<close>
 ML_file \<open>~~/src/Provers/clasimp.ML\<close>
 ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
 ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
 ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
 ML_file \<open>~~/src/Tools/cong_tac.ML\<close>
 ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
 ML_file \<open>~~/src/Tools/project_rule.ML\<close>
 ML_file \<open>~~/src/Tools/subtyping.ML\<close>
 ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
 
 ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
 
 ML \<open>
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_random\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_exhaustive\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_bounded_forall\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_full_exhaustive\<close>;
   Plugin_Name.declare_setup \<^binding>\<open>quickcheck_narrowing\<close>;
 \<close>
 ML \<open>
   Plugin_Name.define_setup \<^binding>\<open>quickcheck\<close>
    [\<^plugin>\<open>quickcheck_exhaustive\<close>,
     \<^plugin>\<open>quickcheck_random\<close>,
     \<^plugin>\<open>quickcheck_bounded_forall\<close>,
     \<^plugin>\<open>quickcheck_full_exhaustive\<close>,
     \<^plugin>\<open>quickcheck_narrowing\<close>]
 \<close>
 
 
 subsection \<open>Primitive logic\<close>
 
 text \<open>
 The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that
 describes the first implementation of HOL. However, there are a number of differences.
 In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
 only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
 axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
 line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
 \<close>
 
 subsubsection \<open>Core syntax\<close>
 
 setup \<open>Axclass.class_axiomatization (\<^binding>\<open>type\<close>, [])\<close>
 default_sort type
 setup \<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close>
 
 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
 instance "fun" :: (type, type) type by (rule fun_arity)
 
 axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
 instance itself :: (type) type by (rule itself_arity)
 
 typedecl bool
 
 judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
 
 axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
   and eq :: "['a, 'a] \<Rightarrow> bool"
   and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 notation (input)
   eq  (infixl "=" 50)
 notation (output)
   eq  (infix "=" 50)
 
 text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax
 because of the large amount of material that relies on infixl.\<close>
 
 subsubsection \<open>Defined connectives and quantifiers\<close>
 
 definition True :: bool
   where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
 
 definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
   where "All P \<equiv> (P = (\<lambda>x. True))"
 
 definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
   where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
 
 definition False :: bool
   where "False \<equiv> (\<forall>P. P)"
 
 definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
   where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
 definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
   where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
 
 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
 
 definition Uniq :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Uniq P \<equiv> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> y = x)"
 
 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
 syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(4?< _./ _)" [0, 10] 10)
 syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
 syntax (ASCII)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
 syntax (input)
   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
 syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
 translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Ex1\<close> \<^syntax_const>\<open>_Ex1\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
 syntax
   "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
   "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
 translations
   "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
   "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
 
 
 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infix "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 notation (ASCII)
   Not  ("~ _" [40] 40) and
   conj  (infixr "&" 35) and
   disj  (infixr "|" 30) and
   implies  (infixr "-->" 25) and
   not_equal  (infix "~=" 50)
 
 abbreviation (iff)
   iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
   where "A \<longleftrightarrow> B \<equiv> A = B"
 
 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
 print_translation \<open>
   [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 
 nonterminal letbinds and letbind
 syntax
   "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              ("(2_ =/ _)" 10)
   ""            :: "letbind \<Rightarrow> letbinds"                 ("_")
   "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     ("_;/ _")
   "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
 syntax (ASCII)
   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
 
 notation (ASCII)
   All  (binder "ALL " 10) and
   Ex  (binder "EX " 10)
 
 notation (input)
   All  (binder "! " 10) and
   Ex  (binder "? " 10)
 
 
 subsubsection \<open>Axioms and basic definitions\<close>
 
 axiomatization where
   refl: "t = (t::'a)" and
   subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
   ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
     \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses
          a related property.  It is an eta-expanded version of the traditional
          rule, and similar to the ABS rule of HOL\<close> and
 
   the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
 axiomatization where
   impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
   mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
 
   True_or_False: "(P = True) \<or> (P = False)"
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
 
 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   where "Let s f \<equiv> f s"
 
 translations
   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
 
 axiomatization undefined :: 'a
 
 class default = fixes default :: 'a
 
 
 subsection \<open>Fundamental rules\<close>
 
 subsubsection \<open>Equality\<close>
 
 lemma sym: "s = t \<Longrightarrow> t = s"
   by (erule subst) (rule refl)
 
 lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t"
   by (drule sym) (erule subst)
 
 lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t"
   by (erule subst)
 
 lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t"
   by (rule trans [OF _ sym])
 
 lemma meta_eq_to_obj_eq:
   assumes "A \<equiv> B"
   shows "A = B"
   unfolding assms by (rule refl)
 
 text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
      (* a = b
         |   |
         c = d   *)
 lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
   by (iprover intro: sym trans)
 
 text \<open>For calculational reasoning:\<close>
 
 lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a"
   by (rule ssubst)
 
 lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b"
   by (rule subst)
 
 
 subsubsection \<open>Congruence rules for application\<close>
 
 text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
 lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
   by (iprover intro: refl elim: subst)
 
 text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
 lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
   by (iprover intro: refl elim: subst)
 
 lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
   by (iprover intro: refl elim: subst)
 
 lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
   by (iprover intro: refl elim: subst)
 
 ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
 
 
 subsubsection \<open>Equality of booleans -- iff\<close>
 
 lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
   by (erule ssubst)
 
 lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> P"
   by (erule iffD2)
 
 lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
   by (drule sym) (rule iffD2)
 
 lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P"
   by (drule sym) (rule rev_iffD2)
 
 lemma iffE:
   assumes major: "P = Q"
     and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R"
   shows R
   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
 subsubsection \<open>True (1)\<close>
 
 lemma TrueI: True
   unfolding True_def by (rule refl)
 
 lemma eqTrueE: "P = True \<Longrightarrow> P"
   by (erule iffD2) (rule TrueI)
 
 
 subsubsection \<open>Universal quantifier (1)\<close>
 
 lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
   unfolding All_def by (iprover intro: eqTrueE fun_cong)
 
 lemma allE:
   assumes major: "\<forall>x. P x" and minor: "P x \<Longrightarrow> R"
   shows R
   by (iprover intro: minor major [THEN spec])
 
 lemma all_dupE:
   assumes major: "\<forall>x. P x" and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R"
   shows R
   by (iprover intro: minor major major [THEN spec])
 
 
 subsubsection \<open>False\<close>
 
 text \<open>
   Depends upon \<open>spec\<close>; it is impossible to do propositional
   logic before quantifiers!
 \<close>
 
 lemma FalseE: "False \<Longrightarrow> P"
   unfolding False_def by (erule spec)
 
 lemma False_neq_True: "False = True \<Longrightarrow> P"
   by (erule eqTrueE [THEN FalseE])
 
 
 subsubsection \<open>Negation\<close>
 
 lemma notI:
   assumes "P \<Longrightarrow> False"
   shows "\<not> P"
   unfolding not_def by (iprover intro: impI assms)
 
 lemma False_not_True: "False \<noteq> True"
   by (iprover intro: notI elim: False_neq_True)
 
 lemma True_not_False: "True \<noteq> False"
   by (iprover intro: notI dest: sym elim: False_neq_True)
 
 lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R"
   unfolding not_def
   by (iprover intro: mp [THEN FalseE])
 
 
 subsubsection \<open>Implication\<close>
 
 lemma impE:
   assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
   shows R
   by (iprover intro: assms mp)
 
 text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   by (rule mp)
 
 lemma contrapos_nn:
   assumes major: "\<not> Q"
     and minor: "P \<Longrightarrow> Q"
   shows "\<not> P"
   by (iprover intro: notI minor major [THEN notE])
 
 text \<open>Not used at all, but we already have the other 3 combinations.\<close>
 lemma contrapos_pn:
   assumes major: "Q"
     and minor: "P \<Longrightarrow> \<not> Q"
   shows "\<not> P"
   by (iprover intro: notI minor major notE)
 
 lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
   by (erule contrapos_nn) (erule sym)
 
 lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y"
   by (erule subst, erule ssubst, assumption)
 
 
 subsubsection \<open>Disjunction (1)\<close>
 
 lemma disjE:
   assumes major: "P \<or> Q"
     and minorP: "P \<Longrightarrow> R"
     and minorQ: "Q \<Longrightarrow> R"
   shows R
   by (iprover intro: minorP minorQ impI
       major [unfolded or_def, THEN spec, THEN mp, THEN mp])
 
 
 subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
 
 text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
 
 lemma iffI:
   assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
   shows "P = Q"
 proof (rule disjE[OF True_or_False[of P]])
   assume 1: "P = True"
   note Q = assms(1)[OF eqTrueE[OF this]]
   from 1 show ?thesis
   proof (rule ssubst)
     from True_or_False[of Q] show "True = Q"
     proof (rule disjE)
       assume "Q = True"
       thus ?thesis by(rule sym)
     next
       assume "Q = False"
       with Q have False by (rule rev_iffD1)
       thus ?thesis by (rule FalseE)
     qed
   qed
 next
   assume 2: "P = False"
   thus ?thesis
   proof (rule ssubst)
     from True_or_False[of Q] show "False = Q"
     proof (rule disjE)
       assume "Q = True"
       from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
       thus ?thesis by (rule FalseE)
     next
       assume "Q = False"
       thus ?thesis by(rule sym)
     qed
   qed
 qed
 
 
 subsubsection \<open>True (2)\<close>
 
 lemma eqTrueI: "P \<Longrightarrow> P = True"
   by (iprover intro: iffI TrueI)
 
 
 subsubsection \<open>Universal quantifier (2)\<close>
 
 lemma allI:
   assumes "\<And>x::'a. P x"
   shows "\<forall>x. P x"
   unfolding All_def by (iprover intro: ext eqTrueI assms)
 
 
 subsubsection \<open>Existential quantifier\<close>
 
 lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   unfolding Ex_def by (iprover intro: allI allE impI mp)
 
 lemma exE:
   assumes major: "\<exists>x::'a. P x"
     and minor: "\<And>x. P x \<Longrightarrow> Q"
   shows "Q"
   by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
 
 
 subsubsection \<open>Conjunction\<close>
 
 lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
   unfolding and_def by (iprover intro: impI [THEN allI] mp)
 
 lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
   unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
   unfolding and_def by (iprover intro: impI dest: spec mp)
 
 lemma conjE:
   assumes major: "P \<and> Q"
     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule minor)
   show P by (rule major [THEN conjunct1])
   show Q by (rule major [THEN conjunct2])
 qed
 
 lemma context_conjI:
   assumes P "P \<Longrightarrow> Q"
   shows "P \<and> Q"
   by (iprover intro: conjI assms)
 
 
 subsubsection \<open>Disjunction (2)\<close>
 
 lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
 
 lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
 
 
 subsubsection \<open>Classical logic\<close>
 
 lemma classical:
   assumes "\<not> P \<Longrightarrow> P"
   shows P
 proof (rule True_or_False [THEN disjE])
   show P if "P = True"
     using that by (iprover intro: eqTrueE)
   show P if "P = False"
   proof (intro notI assms)
     assume P
     with that show False
       by (iprover elim: subst)
   qed
 qed
 
 lemmas ccontr = FalseE [THEN classical]
 
 text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
   make elimination rules.\<close>
 lemma rev_notE:
   assumes premp: P
     and premnot: "\<not> R \<Longrightarrow> \<not> P"
   shows R
   by (iprover intro: ccontr notE [OF premnot premp])
 
 
 text \<open>Double negation law.\<close>
 lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
   by (iprover intro: ccontr notE )
 
 lemma contrapos_pp:
   assumes p1: Q
     and p2: "\<not> P \<Longrightarrow> \<not> Q"
   shows P
   by (iprover intro: classical p1 p2 notE)
 
 
 subsubsection \<open>Unique existence\<close>
 
 lemma Uniq_I [intro?]:
   assumes "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> y = x"
   shows "Uniq P"
   unfolding Uniq_def by (iprover intro: assms allI impI)
 
 lemma Uniq_D [dest?]: "\<lbrakk>Uniq P; P a; P b\<rbrakk> \<Longrightarrow> a=b"
   unfolding Uniq_def by (iprover dest: spec mp)
 
 lemma ex1I:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   shows "\<exists>!x. P x"
   unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
 
 text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
 lemma ex_ex1I:
   assumes ex_prem: "\<exists>x. P x"
     and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   shows "\<exists>!x. P x"
   by (iprover intro: ex_prem [THEN exE] ex1I eq)
 
 lemma ex1E:
   assumes major: "\<exists>!x. P x" and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule major [unfolded Ex1_def, THEN exE])
   show "\<And>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<Longrightarrow> R"
     by (iprover intro: minor elim: conjE)
 qed
 
 lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
   by (iprover intro: exI elim: ex1E)
 
 subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
 
 lemma disjCI:
   assumes "\<not> Q \<Longrightarrow> P"
   shows "P \<or> Q"
   by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
 
 lemma excluded_middle: "\<not> P \<or> P"
   by (iprover intro: disjCI)
 
 text \<open>
   case distinction as a natural deduction rule.
   Note that \<open>\<not> P\<close> is the second case, not the first.
 \<close>
 lemma case_split [case_names True False]:
   assumes "P \<Longrightarrow> Q" "\<not> P \<Longrightarrow> Q"
   shows Q
   using excluded_middle [of P]
     by (iprover intro: assms elim: disjE)
 
 text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
 lemma impCE:
   assumes major: "P \<longrightarrow> Q"
     and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   shows R
   using excluded_middle [of P]
   by (iprover intro: minor major [THEN mp] elim: disjE)+
 
 text \<open>
   This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
   those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
   default: would break old proofs.
 \<close>
 lemma impCE':
   assumes major: "P \<longrightarrow> Q"
     and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   shows R
   using assms by (elim impCE)
 
 
 text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
 lemma iffCE:
   assumes major: "P = Q"
     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   shows R
   by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
 
 lemma exCI:
   assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
   shows "\<exists>x. P x"
   by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 
 
 subsubsection \<open>Intuitionistic Reasoning\<close>
 
 lemma impE':
   assumes 1: "P \<longrightarrow> Q"
     and 2: "Q \<Longrightarrow> R"
     and 3: "P \<longrightarrow> Q \<Longrightarrow> P"
   shows R
 proof -
   from 3 and 1 have P .
   with 1 have Q by (rule impE)
   with 2 show R .
 qed
 
 lemma allE':
   assumes 1: "\<forall>x. P x"
     and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q"
   shows Q
 proof -
   from 1 have "P x" by (rule spec)
   from this and 1 show Q by (rule 2)
 qed
 
 lemma notE':
   assumes 1: "\<not> P"
     and 2: "\<not> P \<Longrightarrow> P"
   shows R
 proof -
   from 2 and 1 have P .
   with 1 show R by (rule notE)
 qed
 
 lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" .
 lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" .
 
 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE
   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
 lemmas [trans] = trans
   and [sym] = sym not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
 
 subsubsection \<open>Atomizing meta-level connectives\<close>
 
 axiomatization where
   eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
 
 lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
 proof
   assume "\<And>x. P x"
   then show "\<forall>x. P x" ..
 next
   assume "\<forall>x. P x"
   then show "\<And>x. P x" by (rule allE)
 qed
 
 lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
 proof
   assume r: "A \<Longrightarrow> B"
   show "A \<longrightarrow> B" by (rule impI) (rule r)
 next
   assume "A \<longrightarrow> B" and A
   then show B by (rule mp)
 qed
 
 lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)"
 proof
   assume r: "A \<Longrightarrow> False"
   show "\<not> A" by (rule notI) (rule r)
 next
   assume "\<not> A" and A
   then show False by (rule notE)
 qed
 
 lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)"
 proof
   assume "x \<equiv> y"
   show "x = y" by (unfold \<open>x \<equiv> y\<close>) (rule refl)
 next
   assume "x = y"
   then show "x \<equiv> y" by (rule eq_reflection)
 qed
 
 lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)"
 proof
   assume conj: "A &&& B"
   show "A \<and> B"
   proof (rule conjI)
     from conj show A by (rule conjunctionD1)
     from conj show B by (rule conjunctionD2)
   qed
 next
   assume conj: "A \<and> B"
   show "A &&& B"
   proof -
     from conj show A ..
     from conj show B ..
   qed
 qed
 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
 
 
 subsubsection \<open>Atomizing elimination rules\<close>
 
 lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)"
   by rule iprover+
 
 lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
   by rule iprover+
 
 lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
   by rule iprover+
 
 lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" ..
 
 
 subsection \<open>Package setup\<close>
 
 ML_file \<open>Tools/hologic.ML\<close>
 ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
 
 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)\<close>
 
 
 subsubsection \<open>Sledgehammer setup\<close>
 
 text \<open>
   Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   that are prolific (match too many equality or membership literals) and relate to
   seldom-used facts. Some duplicate other rules.
 \<close>
 
 named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
 
 
 subsubsection \<open>Classical Reasoner setup\<close>
 
 lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by (rule classical) iprover
 
 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   by (rule classical) iprover
 
 lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
 
 ML \<open>
 structure Hypsubst = Hypsubst
 (
   val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = @{thm eq_reflection}
   val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
   val imp_intr = @{thm impI}
   val rev_mp = @{thm rev_mp}
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl};
 );
 open Hypsubst;
 
 structure Classical = Classical
 (
   val imp_elim = @{thm imp_elim}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
   val classical = @{thm classical}
   val sizef = Drule.size_of_thm
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 );
 
 structure Basic_Classical: BASIC_CLASSICAL = Classical;
 open Basic_Classical;
 \<close>
 
 setup \<open>
   (*prevent substitution on bool*)
   let
     fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close>
       | non_bool_eq _ = false;
     fun hyp_subst_tac' ctxt =
       SUBGOAL (fn (goal, i) =>
         if Term.exists_Const non_bool_eq goal
         then Hypsubst.hyp_subst_tac ctxt i
         else no_tac);
   in
     Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   end
 \<close>
 
 declare iffI [intro!]
   and notI [intro!]
   and impI [intro!]
   and disjCI [intro!]
   and conjI [intro!]
   and TrueI [intro!]
   and refl [intro!]
 
 declare iffCE [elim!]
   and FalseE [elim!]
   and impCE [elim!]
   and disjE [elim!]
   and conjE [elim!]
 
 declare ex_ex1I [intro!]
   and allI [intro!]
   and exI [intro]
 
 declare exE [elim!]
   allE [elim]
 
 ML \<open>val HOL_cs = claset_of \<^context>\<close>
 
 lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P"
   by (erule swap)
 
 declare ex_ex1I [rule del, intro! 2]
   and ex1I [intro]
 
 declare ext [intro]
 
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 
 text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
 lemma alt_ex1E [elim!]:
   assumes major: "\<exists>!x. P x"
     and minor: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   shows R
 proof (rule ex1E [OF major minor])
   show "\<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'" if "P x" and \<section>: "\<forall>y. P y \<longrightarrow> y = x" for x
     using \<open>P x\<close> \<section> \<section> by fast
 qed assumption
 
 text \<open>And again using Uniq\<close>
 lemma alt_ex1E':
   assumes  "\<exists>!x. P x" "\<And>x. \<lbrakk>P x; \<exists>\<^sub>\<le>\<^sub>1x. P x\<rbrakk> \<Longrightarrow> R"
   shows R
   using assms unfolding Uniq_def by fast
 
 lemma ex1_iff_ex_Uniq: "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x) \<and> (\<exists>\<^sub>\<le>\<^sub>1x. P x)"
   unfolding Uniq_def by fast
 
 
 ML \<open>
   structure Blast = Blast
   (
     structure Classical = Classical
     val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>HOL.eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   );
   val blast_tac = Blast.blast_tac;
 \<close>
 
 
 subsubsection \<open>THE: definite description operator\<close>
 
 lemma the_equality [intro]:
   assumes "P a"
     and "\<And>x. P x \<Longrightarrow> x = a"
   shows "(THE x. P x) = a"
   by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
 
 lemma theI:
   assumes "P a"
     and "\<And>x. P x \<Longrightarrow> x = a"
   shows "P (THE x. P x)"
   by (iprover intro: assms the_equality [THEN ssubst])
 
 lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   by (blast intro: theI)
 
 text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
 lemma theI2:
   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE x. P x)"
   by (iprover intro: assms theI)
 
 lemma the1I2:
   assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE x. P x)"
   by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
 
 lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   by blast
 
 lemma the1_equality': "\<lbrakk>\<exists>\<^sub>\<le>\<^sub>1x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   unfolding Uniq_def by blast
 
 lemma the_sym_eq_trivial: "(THE y. x = y) = x"
   by blast
 
 
 subsubsection \<open>Simplifier\<close>
 
 lemma eta_contract_eq: "(\<lambda>s. f s) = f" ..
 
 lemma simp_thms:
   shows not_not: "(\<not> \<not> P) = P"
   and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)"
   and
     "(P \<noteq> Q) = (P = (\<not> Q))"
     "(P \<or> \<not>P) = True"    "(\<not> P \<or> P) = True"
     "(x = x) = True"
   and not_True_eq_False [code]: "(\<not> True) = False"
   and not_False_eq_True [code]: "(\<not> False) = True"
   and
     "(\<not> P) \<noteq> P"  "P \<noteq> (\<not> P)"
     "(True = P) = P"
   and eq_True: "(P = True) = P"
   and "(False = P) = (\<not> P)"
   and eq_False: "(P = False) = (\<not> P)"
   and
     "(True \<longrightarrow> P) = P"  "(False \<longrightarrow> P) = True"
     "(P \<longrightarrow> True) = True"  "(P \<longrightarrow> P) = True"
     "(P \<longrightarrow> False) = (\<not> P)"  "(P \<longrightarrow> \<not> P) = (\<not> P)"
     "(P \<and> True) = P"  "(True \<and> P) = P"
     "(P \<and> False) = False"  "(False \<and> P) = False"
     "(P \<and> P) = P"  "(P \<and> (P \<and> Q)) = (P \<and> Q)"
     "(P \<and> \<not> P) = False"    "(\<not> P \<and> P) = False"
     "(P \<or> True) = True"  "(True \<or> P) = True"
     "(P \<or> False) = P"  "(False \<or> P) = P"
     "(P \<or> P) = P"  "(P \<or> (P \<or> Q)) = (P \<or> Q)" and
     "(\<forall>x. P) = P"  "(\<exists>x. P) = P"  "\<exists>x. x = t"  "\<exists>x. t = x"
   and
     "\<And>P. (\<exists>x. x = t \<and> P x) = P t"
     "\<And>P. (\<exists>x. t = x \<and> P x) = P t"
     "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
     "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
     "(\<forall>x. x \<noteq> t) = False"  "(\<forall>x. t \<noteq> x) = False"
   by (blast, blast, blast, blast, blast, iprover+)
 
 lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   by blast
 
 lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
   by blast
 
 lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   by blast
 
 lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
   by blast
 
 lemma eq_ac:
   shows eq_commute: "a = b \<longleftrightarrow> b = a"
     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
     and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   by (iprover, blast+)
 
 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
 
 lemma conj_comms:
   shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
     and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
 lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
 
 lemmas conj_ac = conj_commute conj_left_commute conj_assoc
 
 lemma disj_comms:
   shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
     and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
 lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
 
 lemmas disj_ac = disj_commute disj_left_commute disj_assoc
 
 lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
 lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
 
 lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
 lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
 
 lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
 lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
 lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
 
 text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
 lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
 lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
 
 lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 
 lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
   by iprover
 
 lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
 lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
 lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
 lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
 lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
 lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
 lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
 lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
 
 lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
 
 
 lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
   \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
   \<comment> \<open>cases boil down to the same thing.\<close>
   by blast
 
 lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
 lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
 lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
 lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
 lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
 
 declare All_def [no_atp]
 
 lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
 lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
 
 text \<open>
   \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
   May slow rewrite proofs down by as much as 50\%\<close>
 
 lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
 lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
   by iprover
 
 text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
 
 lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
   by blast
 
 
 text \<open>\<^medskip> if-then-else rules\<close>
 
 lemma if_True [code]: "(if True then x else y) = x"
   unfolding If_def by blast
 
 lemma if_False [code]: "(if False then x else y) = y"
   unfolding If_def by blast
 
 lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
   unfolding If_def by blast
 
 lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
   unfolding If_def by blast
 
 lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
 proof (rule case_split [of Q])
   show ?thesis if Q
     using that by (simplesubst if_P) blast+
   show ?thesis if "\<not> Q"
     using that by (simplesubst if_not_P) blast+
 qed
 
 lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
   by (simplesubst if_split) blast
 
 lemmas if_splits [no_atp] = if_split if_split_asm
 
 lemma if_cancel: "(if c then x else x) = x"
   by (simplesubst if_split) blast
 
 lemma if_eq_cancel: "(if x = y then y else x) = x"
   by (simplesubst if_split) blast
 
 lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
   \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
   by (rule if_split)
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
   \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
   by (simplesubst if_split) blast
 
 lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
 lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
 
 text \<open>\<^medskip> let rules for simproc\<close>
 
 lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
   by (unfold Let_def)
 
 lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g"
   by (unfold Let_def)
 
 text \<open>
   The following copy of the implication operator is useful for
   fine-tuning congruence rules.  It instructs the simplifier to simplify
   its premise.
 \<close>
 
 definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
   where "simp_implies \<equiv> (\<Longrightarrow>)"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   shows "PROP P =simp=> PROP Q"
   unfolding simp_implies_def
   by (iprover intro: PQ)
 
 lemma simp_impliesE:
   assumes PQ: "PROP P =simp=> PROP Q"
     and P: "PROP P"
     and QR: "PROP Q \<Longrightarrow> PROP R"
   shows "PROP R"
   by (iprover intro: QR P PQ [unfolded simp_implies_def])
 
 lemma simp_implies_cong:
   assumes PP' :"PROP P \<equiv> PROP P'"
     and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
   shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
   unfolding simp_implies_def
 proof (rule equal_intr_rule)
   assume PQ: "PROP P \<Longrightarrow> PROP Q"
     and P': "PROP P'"
   from PP' [symmetric] and P' have "PROP P"
     by (rule equal_elim_rule1)
   then have "PROP Q" by (rule PQ)
   with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
 next
   assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
     and P: "PROP P"
   from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
   then have "PROP Q'" by (rule P'Q')
   with P'QQ' [OF P', symmetric] show "PROP Q"
     by (rule equal_elim_rule1)
 qed
 
 lemma uncurry:
   assumes "P \<longrightarrow> Q \<longrightarrow> R"
   shows "P \<and> Q \<longrightarrow> R"
   using assms by blast
 
 lemma iff_allI:
   assumes "\<And>x. P x = Q x"
   shows "(\<forall>x. P x) = (\<forall>x. Q x)"
   using assms by blast
 
 lemma iff_exI:
   assumes "\<And>x. P x = Q x"
   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
   using assms by blast
 
 lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
   by blast
 
 lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
 ML_file \<open>Tools/simpdata.ML\<close>
 ML \<open>open Simpdata\<close>
 
 setup \<open>
   map_theory_simpset (put_simpset HOL_basic_ss) #>
   Simplifier.method_setup Splitter.split_modifiers
 \<close>
 
-simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
 
 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
 
 simproc_setup neq ("x = y") = \<open>fn _ =>
   let
     val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
     fun is_neq eq lhs rhs thm =
       (case Thm.prop_of thm of
         _ $ (Not $ (eq' $ l' $ r')) =>
           Not = HOLogic.Not andalso eq' = eq andalso
           r' aconv lhs andalso l' aconv rhs
       | _ => false);
     fun proc ss ct =
       (case Thm.term_of ct of
         eq $ lhs $ rhs =>
           (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
             SOME thm => SOME (thm RS neq_to_EQ_False)
           | NONE => NONE)
        | _ => NONE);
   in proc end
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
   let
     fun count_loose (Bound i) k = if i >= k then 1 else 0
       | count_loose (s $ t) k = count_loose s k + count_loose t k
       | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
       | count_loose _ _ = 0;
     fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) =
       (case t of
         Abs (_, _, t') => count_loose t' 0 <= 1
       | _ => true);
   in
     fn _ => fn ctxt => fn ct =>
       if is_trivial_let (Thm.term_of ct)
       then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
       else
         let (*Norbert Schirmer's case*)
           val t = Thm.term_of ct;
           val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
             (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
               if is_Free x orelse is_Bound x orelse is_Const x
               then SOME @{thm Let_def}
               else
                 let
                   val n = case f of (Abs (x, _, _)) => x | _ => "x";
                   val cx = Thm.cterm_of ctxt x;
                   val xT = Thm.typ_of_cterm cx;
                   val cf = Thm.cterm_of ctxt f;
                   val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
                   val (_ $ _ $ g) = Thm.prop_of fx_g;
                   val g' = abstract_over (x, g);
                   val abs_g'= Abs (n, xT, g');
                 in
                   if g aconv g' then
                     let
                       val rl =
                         infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
                     in SOME (rl OF [fx_g]) end
                   else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
                   then NONE (*avoid identity conversion*)
                   else
                     let
                       val g'x = abs_g' $ x;
                       val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
                       val rl =
                         @{thm Let_folded} |> infer_instantiate ctxt
                           [(("f", 0), Thm.cterm_of ctxt f),
                            (("x", 0), cx),
                            (("g", 0), Thm.cterm_of ctxt abs_g')];
                     in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
                 end
             | _ => NONE)
         end
   end
 \<close>
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
   assume "True \<Longrightarrow> PROP P"
   from this [OF TrueI] show "PROP P" .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
 lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
   by standard (intro TrueI)
 
 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
   by standard simp_all
 
 (* It seems that making this a simp rule is slower than using the simproc below *)
 lemma implies_False_swap:
   "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   by (rule swap_prems_eq)
 
 ML \<open>
 fun eliminate_false_implies ct =
   let
     val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
     fun go n =
       if n > 1 then
         Conv.rewr_conv @{thm Pure.swap_prems_eq}
         then_conv Conv.arg_conv (go (n - 1))
         then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
       else
         Conv.rewr_conv @{thm HOL.False_implies_equals}
   in
     case concl of
       Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
     | _ => NONE
   end
 \<close>
 
 simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>K (K eliminate_false_implies)\<close>
 
 
 lemma ex_simps:
   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
   "\<And>P Q. (\<exists>x. P \<and> Q x)   = (P \<and> (\<exists>x. Q x))"
   "\<And>P Q. (\<exists>x. P x \<or> Q)   = ((\<exists>x. P x) \<or> Q)"
   "\<And>P Q. (\<exists>x. P \<or> Q x)   = (P \<or> (\<exists>x. Q x))"
   "\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
   "\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))"
   \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close>
   by (iprover | blast)+
 
 lemma all_simps:
   "\<And>P Q. (\<forall>x. P x \<and> Q)   = ((\<forall>x. P x) \<and> Q)"
   "\<And>P Q. (\<forall>x. P \<and> Q x)   = (P \<and> (\<forall>x. Q x))"
   "\<And>P Q. (\<forall>x. P x \<or> Q)   = ((\<forall>x. P x) \<or> Q)"
   "\<And>P Q. (\<forall>x. P \<or> Q x)   = (P \<or> (\<forall>x. Q x))"
   "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
   "\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))"
   \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close>
   by (iprover | blast)+
 
 lemmas [simp] =
   triv_forall_equality  \<comment> \<open>prunes params\<close>
   True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
   False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
   if_True
   if_False
   if_cancel
   if_eq_cancel
   imp_disjL \<comment> \<open>In general it seems wrong to add distributive laws by default: they
     might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
     and cannot be removed without affecting existing proofs.  Moreover,
     rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
     grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
   conj_assoc
   disj_assoc
   de_Morgan_conj
   de_Morgan_disj
   imp_disj1
   imp_disj2
   not_imp
   disj_not1
   not_all
   not_ex
   cases_simp
   the_eq_trivial
   the_sym_eq_trivial
   ex_simps
   all_simps
   simp_thms
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = if_split
 
 ML \<open>val HOL_ss = simpset_of \<^context>\<close>
 
 text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
 lemma if_cong:
   assumes "b = c"
     and "c \<Longrightarrow> x = u"
     and "\<not> c \<Longrightarrow> y = v"
   shows "(if b then x else y) = (if c then u else v)"
   using assms by simp
 
 text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
   faster and allows the execution of functional programs.\<close>
 lemma if_weak_cong [cong]:
   assumes "b = c"
   shows "(if b then x else y) = (if c then x else y)"
   using assms by (rule arg_cong)
 
 text \<open>Prevents simplification of t: much faster\<close>
 lemma let_weak_cong:
   assumes "a = b"
   shows "(let x = a in t x) = (let x = b in t x)"
   using assms by (rule arg_cong)
 
 text \<open>To tidy up the result of a simproc.  Only the RHS will be simplified.\<close>
 lemma eq_cong2:
   assumes "u = u'"
   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
   using assms by simp
 
 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
 lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)"
   by simp
 
 lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)"
   by auto
 
 lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)"
   by auto
 
 lemma if_if_eq_conj: "(if P then if Q then x else y else y) = (if P \<and> Q then x else y)"
   by simp
 
 text \<open>As a simplification rule, it replaces all function equalities by
   first-order equalities.\<close>
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
   by auto
 
 
 subsubsection \<open>Generic cases and induction\<close>
 
 text \<open>Rule projections:\<close>
 ML \<open>
 structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
 );
 \<close>
 
 context
 begin
 
 qualified definition "induct_forall P \<equiv> \<forall>x. P x"
 qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
 qualified definition "induct_equal x y \<equiv> x = y"
 qualified definition "induct_conj A B \<equiv> A \<and> B"
 qualified definition "induct_true \<equiv> True"
 qualified definition "induct_false \<equiv> False"
 
 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
 
 lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
   by (unfold atomize_imp induct_implies_def)
 
 lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
   by (unfold atomize_eq induct_equal_def)
 
 lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
 lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
 lemmas induct_atomize = induct_atomize' induct_equal_eq
 lemmas induct_rulify' [symmetric] = induct_atomize'
 lemmas induct_rulify [symmetric] = induct_atomize
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_true_def induct_false_def
 
 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
     induct_conj (induct_forall A) (induct_forall B)"
   by (unfold induct_forall_def induct_conj_def) iprover
 
 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
     induct_conj (induct_implies C A) (induct_implies C B)"
   by (unfold induct_implies_def induct_conj_def) iprover
 
 lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
 proof
   assume r: "induct_conj A B \<Longrightarrow> PROP C"
   assume ab: A B
   show "PROP C" by (rule r) (simp add: induct_conj_def ab)
 next
   assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
   assume ab: "induct_conj A B"
   show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
 qed
 
 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
 
 lemma induct_trueI: "induct_true"
   by (simp add: induct_true_def)
 
 text \<open>Method setup.\<close>
 
 ML_file \<open>~~/src/Tools/induct.ML\<close>
 ML \<open>
 structure Induct = Induct
 (
   val cases_default = @{thm case_split}
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
   val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
 \<close>
 
 ML_file \<open>~~/src/Tools/induction.ML\<close>
 
 declaration \<open>
   fn _ => Induct.map_simpset (fn ss => ss
     addsimprocs
       [Simplifier.make_simproc \<^context> "swap_induct_false"
         {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
               if P <> Q then SOME Drule.swap_prems_eq else NONE
           | _ => NONE)},
        Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
         {lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             _ $ (_ $ P) $ _ =>
               let
                 fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) =
                       is_conj P andalso is_conj Q
                   | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true
                   | is_conj \<^const>\<open>induct_true\<close> = true
                   | is_conj \<^const>\<open>induct_false\<close> = true
                   | is_conj _ = false
               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
             | _ => NONE)}]
     |> Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
         map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
 \<close>
 
 text \<open>Pre-simplification of induction and cases rules\<close>
 
 lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
   assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
   show "PROP P t" by (rule r [OF refl])
 next
   fix x
   assume "PROP P t" "x = t"
   then show "PROP P x" by simp
 qed
 
 lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   unfolding induct_equal_def
 proof
   assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
   show "PROP P t" by (rule r [OF refl])
 next
   fix x
   assume "PROP P t" "t = x"
   then show "PROP P x" by simp
 qed
 
 lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
   unfolding induct_false_def induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
   unfolding induct_true_def
 proof
   assume "True \<Longrightarrow> PROP P"
   then show "PROP P" using TrueI .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
 lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
   unfolding induct_true_def
   by (iprover intro: equal_intr_rule)
 
 lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
   by (simp add: induct_implies_def induct_true_def)
 
 lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   by (rule simp_thms)
 
 end
 
 ML_file \<open>~~/src/Tools/induct_tacs.ML\<close>
 
 
 subsubsection \<open>Coherent logic\<close>
 
 ML_file \<open>~~/src/Tools/coherent.ML\<close>
 ML \<open>
 structure Coherent = Coherent
 (
   val atomize_elimL = @{thm atomize_elimL};
   val atomize_exL = @{thm atomize_exL};
   val atomize_conjL = @{thm atomize_conjL};
   val atomize_disjL = @{thm atomize_disjL};
   val operator_names = [\<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>Ex\<close>];
 );
 \<close>
 
 
 subsubsection \<open>Reorienting equalities\<close>
 
 ML \<open>
 signature REORIENT_PROC =
 sig
   val add : (term -> bool) -> theory -> theory
   val proc : morphism -> Proof.context -> cterm -> thm option
 end;
 
 structure Reorient_Proc : REORIENT_PROC =
 struct
   structure Data = Theory_Data
   (
     type T = ((term -> bool) * stamp) list;
     val empty = [];
     val extend = I;
     fun merge data : T = Library.merge (eq_snd (op =)) data;
   );
   fun add m = Data.map (cons (m, stamp ()));
   fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
 
   val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
   fun proc phi ctxt ct =
     let
       val thy = Proof_Context.theory_of ctxt;
     in
       case Thm.term_of ct of
         (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
       | _ => NONE
     end;
 end;
 \<close>
 
 
 subsection \<open>Other simple lemmas and lemma duplicates\<close>
 
 lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)"
   by auto
 
 lemma ex_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. P' x)"
   by auto
 
 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<forall>x. Q x \<longrightarrow> P x) = (\<forall>x. Q x \<longrightarrow> P' x)"
   by auto
 
 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> (\<exists>x. Q x \<and> P x) = (\<exists>x. Q x \<and> P' x)"
   by auto
 
 lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
   by blast+
 
 lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))" (is "?lhs = ?rhs")
 proof (intro iffI allI)
   assume L: ?lhs
   then have \<section>: "\<forall>x. P x (THE y. P x y)"
     by (best intro: theI')
   show ?rhs
     by (rule ex1I) (use L \<section> in \<open>fast+\<close>)
 next
   fix x
   assume R: ?rhs
   then obtain f where f: "\<forall>x. P x (f x)" and f1: "\<And>y. (\<forall>x. P x (y x)) \<Longrightarrow> y = f"
     by (blast elim: ex1E)
   show "\<exists>!y. P x y"
   proof (rule ex1I)
     show "P x (f x)"
       using f by blast
     show "y = f x" if "P x y" for y
     proof -
       have "P z (if z = x then y else f z)" for z
         using f that by (auto split: if_split)
       with f1 [of "\<lambda>z. if z = x then y else f z"] f
       show ?thesis
         by (auto simp add: split: if_split_asm dest: fun_cong)
     qed
   qed
 qed
 
 lemmas eq_sym_conv = eq_commute
 
 lemma nnf_simps:
   "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
   "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
   "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
   "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
   "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
   "(\<not> \<not> P) = P"
   by blast+
 
 
 subsection \<open>Basic ML bindings\<close>
 
 ML \<open>
 val FalseE = @{thm FalseE}
 val Let_def = @{thm Let_def}
 val TrueI = @{thm TrueI}
 val allE = @{thm allE}
 val allI = @{thm allI}
 val all_dupE = @{thm all_dupE}
 val arg_cong = @{thm arg_cong}
 val box_equals = @{thm box_equals}
 val ccontr = @{thm ccontr}
 val classical = @{thm classical}
 val conjE = @{thm conjE}
 val conjI = @{thm conjI}
 val conjunct1 = @{thm conjunct1}
 val conjunct2 = @{thm conjunct2}
 val disjCI = @{thm disjCI}
 val disjE = @{thm disjE}
 val disjI1 = @{thm disjI1}
 val disjI2 = @{thm disjI2}
 val eq_reflection = @{thm eq_reflection}
 val ex1E = @{thm ex1E}
 val ex1I = @{thm ex1I}
 val ex1_implies_ex = @{thm ex1_implies_ex}
 val exE = @{thm exE}
 val exI = @{thm exI}
 val excluded_middle = @{thm excluded_middle}
 val ext = @{thm ext}
 val fun_cong = @{thm fun_cong}
 val iffD1 = @{thm iffD1}
 val iffD2 = @{thm iffD2}
 val iffI = @{thm iffI}
 val impE = @{thm impE}
 val impI = @{thm impI}
 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
 val mp = @{thm mp}
 val notE = @{thm notE}
 val notI = @{thm notI}
 val not_all = @{thm not_all}
 val not_ex = @{thm not_ex}
 val not_iff = @{thm not_iff}
 val not_not = @{thm not_not}
 val not_sym = @{thm not_sym}
 val refl = @{thm refl}
 val rev_mp = @{thm rev_mp}
 val spec = @{thm spec}
 val ssubst = @{thm ssubst}
 val subst = @{thm subst}
 val sym = @{thm sym}
 val trans = @{thm trans}
 \<close>
 
 locale cnf
 begin
 
 lemma clause2raw_notE: "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto
 lemma clause2raw_not_disj: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto
 lemma clause2raw_not_not: "P \<Longrightarrow> \<not>\<not> P" by auto
 
 lemma iff_refl: "(P::bool) = P" by auto
 lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto
 lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P \<and> Q) = (P' \<and> Q')" by auto
 lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto
 
 lemma make_nnf_imp: "[| (\<not>P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto
 lemma make_nnf_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> Q'))" by auto
 lemma make_nnf_not_false: "(\<not>False) = True" by auto
 lemma make_nnf_not_true: "(\<not>True) = False" by auto
 lemma make_nnf_not_conj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<and> Q)) = (P' \<or> Q')" by auto
 lemma make_nnf_not_disj: "[| (\<not>P) = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<or> Q)) = (P' \<and> Q')" by auto
 lemma make_nnf_not_imp: "[| P = P'; (\<not>Q) = Q' |] ==> (\<not>(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto
 lemma make_nnf_not_iff: "[| P = P'; (\<not>P) = NP; Q = Q'; (\<not>Q) = NQ |] ==> (\<not>(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> NQ))" by auto
 lemma make_nnf_not_not: "P = P' ==> (\<not>\<not>P) = P'" by auto
 
 lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P \<and> Q) = Q'" by auto
 lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto
 lemma simp_TF_conj_False_l: "P = False ==> (P \<and> Q) = False" by auto
 lemma simp_TF_conj_False_r: "Q = False ==> (P \<and> Q) = False" by auto
 lemma simp_TF_disj_True_l: "P = True ==> (P \<or> Q) = True" by auto
 lemma simp_TF_disj_True_r: "Q = True ==> (P \<or> Q) = True" by auto
 lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto
 lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto
 
 lemma make_cnf_disj_conj_l: "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto
 lemma make_cnf_disj_conj_r: "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto
 
 lemma make_cnfx_disj_ex_l: "((\<exists>(x::bool). P x) \<or> Q) = (\<exists>x. P x \<or> Q)" by auto
 lemma make_cnfx_disj_ex_r: "(P \<or> (\<exists>(x::bool). Q x)) = (\<exists>x. P \<or> Q x)" by auto
 lemma make_cnfx_newlit: "(P \<or> Q) = (\<exists>x. (P \<or> x) \<and> (Q \<or> \<not>x))" by auto
 lemma make_cnfx_ex_cong: "(\<forall>(x::bool). P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>x. Q x)" by auto
 
 lemma weakening_thm: "[| P; Q |] ==> Q" by auto
 
 lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto
 
 end
 
 ML_file \<open>Tools/cnf.ML\<close>
 
 
 section \<open>\<open>NO_MATCH\<close> simproc\<close>
 
 text \<open>
   The simplification procedure can be used to avoid simplification of terms
   of a certain form.
 \<close>
 
 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   where "NO_MATCH pat val \<equiv> True"
 
 lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
   by (rule refl)
 
 declare [[coercion_args NO_MATCH - -]]
 
 simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt
     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
     val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
   in if m then NONE else SOME @{thm NO_MATCH_def} end
 \<close>
 
 text \<open>
   This setup ensures that a rewrite rule of the form \<^term>\<open>NO_MATCH pat val \<Longrightarrow> t\<close>
   is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
 \<close>
 
 
 text\<open>
   Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
   not to simplify the argument and to solve it by an assumption.
 \<close>
 
 definition ASSUMPTION :: "bool \<Rightarrow> bool"
   where "ASSUMPTION A \<equiv> A"
 
 lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
   by (rule refl)
 
 lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
   by (simp add: ASSUMPTION_def)
 
 lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
   by (simp add: ASSUMPTION_def)
 
 setup \<open>
 let
   val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
     resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
     resolve_tac ctxt (Simplifier.prems_of ctxt))
 in
   map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
 end
 \<close>
 
 
 subsection \<open>Code generator setup\<close>
 
 subsubsection \<open>Generic code generator preprocessor setup\<close>
 
 lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
   by (fact arg_cong)
 
 lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
   by (fact arg_cong)
 
 setup \<open>
   Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   Simplifier.add_cong @{thm conj_left_cong} #>
   Simplifier.add_cong @{thm disj_left_cong})
 \<close>
 
 
 subsubsection \<open>Equality\<close>
 
 class equal =
   fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin
 
 lemma equal: "equal = (=)"
   by (rule ext equal_eq)+
 
 lemma equal_refl: "equal x x \<longleftrightarrow> True"
   unfolding equal by rule+
 
 lemma eq_equal: "(=) \<equiv> equal"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
 
 end
 
 declare eq_equal [symmetric, code_post]
 declare eq_equal [code]
 
 setup \<open>
   Code_Preproc.map_pre (fn ctxt =>
     ctxt addsimprocs
       [Simplifier.make_simproc \<^context> "equal"
         {lhss = [\<^term>\<open>HOL.eq\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
           | _ => NONE)}])
 \<close>
 
 
 subsubsection \<open>Generic code generator foundation\<close>
 
 text \<open>Datatype \<^typ>\<open>bool\<close>\<close>
 
 code_datatype True False
 
 lemma [code]:
   shows "False \<and> P \<longleftrightarrow> False"
     and "True \<and> P \<longleftrightarrow> P"
     and "P \<and> False \<longleftrightarrow> False"
     and "P \<and> True \<longleftrightarrow> P"
   by simp_all
 
 lemma [code]:
   shows "False \<or> P \<longleftrightarrow> P"
     and "True \<or> P \<longleftrightarrow> True"
     and "P \<or> False \<longleftrightarrow> P"
     and "P \<or> True \<longleftrightarrow> True"
   by simp_all
 
 lemma [code]:
   shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
     and "(True \<longrightarrow> P) \<longleftrightarrow> P"
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
     and "(P \<longrightarrow> True) \<longleftrightarrow> True"
   by simp_all
 
 text \<open>More about \<^typ>\<open>prop\<close>\<close>
 
 lemma [code nbe]:
   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
     and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
   by (auto intro!: equal_intr_rule)
 
 lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
   by (auto intro!: equal_intr_rule holds)
 
 declare Trueprop_code [symmetric, code_post]
 
 text \<open>Equality\<close>
 
 declare simp_thms(6) [code nbe]
 
 instantiation itself :: (type) equal
 begin
 
 definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
   where "equal_itself x y \<longleftrightarrow> x = y"
 
 instance
   by standard (fact equal_itself_def)
 
 end
 
 lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::type \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close>
 
 lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> (((=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
   (is "?ofclass \<equiv> ?equal")
 proof
   assume "PROP ?ofclass"
   show "PROP ?equal"
     by (tactic \<open>ALLGOALS (resolve_tac \<^context> [Thm.unconstrainT @{thm eq_equal}])\<close>)
       (fact \<open>PROP ?ofclass\<close>)
 next
   assume "PROP ?equal"
   show "PROP ?ofclass" proof
   qed (simp add: \<open>PROP ?equal\<close>)
 qed
 
 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>equal\<close>, SOME \<^typ>\<open>'a::equal \<Rightarrow> 'a \<Rightarrow> bool\<close>)\<close>
 
 setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
 
 text \<open>Cases\<close>
 
 lemma Let_case_cert:
   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   shows "CASE x \<equiv> f x"
   using assms by simp_all
 
 setup \<open>
   Code.declare_case_global @{thm Let_case_cert} #>
   Code.declare_undefined_global \<^const_name>\<open>undefined\<close>
 \<close>
 
 declare [[code abort: undefined]]
 
 
 subsubsection \<open>Generic code generator target languages\<close>
 
 text \<open>type \<^typ>\<open>bool\<close>\<close>
 
 code_printing
   type_constructor bool \<rightharpoonup>
     (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
 | constant True \<rightharpoonup>
     (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
 | constant False \<rightharpoonup>
     (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
 
 code_reserved SML
   bool true false
 
 code_reserved OCaml
   bool
 
 code_reserved Scala
   Boolean
 
 code_printing
   constant Not \<rightharpoonup>
     (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
 | constant HOL.conj \<rightharpoonup>
     (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
 | constant HOL.disj \<rightharpoonup>
     (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
 | constant HOL.implies \<rightharpoonup>
     (SML) "!(if (_)/ then (_)/ else true)"
     and (OCaml) "!(if (_)/ then (_)/ else true)"
     and (Haskell) "!(if (_)/ then (_)/ else True)"
     and (Scala) "!(if ((_))/ (_)/ else true)"
 | constant If \<rightharpoonup>
     (SML) "!(if (_)/ then (_)/ else (_))"
     and (OCaml) "!(if (_)/ then (_)/ else (_))"
     and (Haskell) "!(if (_)/ then (_)/ else (_))"
     and (Scala) "!(if ((_))/ (_)/ else (_))"
 
 code_reserved SML
   not
 
 code_reserved OCaml
   not
 
 code_identifier
   code_module Pure \<rightharpoonup>
     (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
 
 text \<open>Using built-in Haskell equality.\<close>
 code_printing
   type_class equal \<rightharpoonup> (Haskell) "Eq"
 | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
 | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
 
 text \<open>\<open>undefined\<close>\<close>
 code_printing
   constant undefined \<rightharpoonup>
     (SML) "!(raise/ Fail/ \"undefined\")"
     and (OCaml) "failwith/ \"undefined\""
     and (Haskell) "error/ \"undefined\""
     and (Scala) "!sys.error(\"undefined\")"
 
 
 subsubsection \<open>Evaluation and normalization by evaluation\<close>
 
 method_setup eval = \<open>
   let
     fun eval_tac ctxt =
       let val conv = Code_Runtime.dynamic_holds_conv ctxt
       in
         CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
         resolve_tac ctxt [TrueI]
       end
   in
     Scan.succeed (SIMPLE_METHOD' o eval_tac)
   end
 \<close> "solve goal by evaluation"
 
 method_setup normalization = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD'
       (CHANGED_PROP o
         (CONVERSION (Nbe.dynamic_conv ctxt)
           THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
 \<close> "solve goal by normalization"
 
 
 subsection \<open>Counterexample Search Units\<close>
 
 subsubsection \<open>Quickcheck\<close>
 
 quickcheck_params [size = 5, iterations = 50]
 
 
 subsubsection \<open>Nitpick setup\<close>
 
 named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
   and nitpick_simp "equational specification of constants as needed by Nitpick"
   and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
   and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
   and if_bool_eq_disj [no_atp]
 
 
 subsection \<open>Preprocessing for the predicate compiler\<close>
 
 named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
   and code_pred_inline "inlining definitions for the Predicate Compiler"
   and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
 
 
 subsection \<open>Legacy tactics and ML bindings\<close>
 
 ML \<open>
   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   local
     fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
   in
     fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
   end;
 
   local
     val nnf_ss =
       simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps});
   in
     fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   end
 \<close>
 
 hide_const (open) eq equal
 
 end
diff --git a/src/HOL/Library/Quantified_Premise_Simproc.thy b/src/HOL/Library/Quantified_Premise_Simproc.thy
--- a/src/HOL/Library/Quantified_Premise_Simproc.thy
+++ b/src/HOL/Library/Quantified_Premise_Simproc.thy
@@ -1,9 +1,9 @@
 (* Author: Florian Haftmann, TU München *)
 
 theory Quantified_Premise_Simproc
   imports Main
 begin
 
-simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
+simproc_setup defined_all ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
 
 end
diff --git a/src/HOL/Set.thy b/src/HOL/Set.thy
--- a/src/HOL/Set.thy
+++ b/src/HOL/Set.thy
@@ -1,2032 +1,2028 @@
 (*  Title:      HOL/Set.thy
     Author:     Tobias Nipkow
     Author:     Lawrence C Paulson
     Author:     Markus Wenzel
 *)
 
 section \<open>Set theory for higher-order logic\<close>
 
 theory Set
   imports Lattices
 begin
 
 subsection \<open>Sets as predicates\<close>
 
 typedecl 'a set
 
 axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> \<open>comprehension\<close>
   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> \<open>membership\<close>
   where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
     and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
 
 notation
   member  ("'(\<in>')") and
   member  ("(_/ \<in> _)" [51, 51] 50)
 
 abbreviation not_member
   where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> \<open>non-membership\<close>
 notation
   not_member  ("'(\<notin>')") and
   not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 notation (ASCII)
   member  ("'(:')") and
   member  ("(_/ : _)" [51, 51] 50) and
   not_member  ("'(~:')") and
   not_member  ("(_/ ~: _)" [51, 51] 50)
 
 
 text \<open>Set comprehensions\<close>
 
 syntax
   "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_./ _})")
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
 syntax (ASCII)
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/: _)./ _})")
 syntax
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/ \<in> _)./ _})")
 translations
   "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
 lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
   by simp
 
 lemma CollectD: "a \<in> {x. P x} \<Longrightarrow> P a"
   by simp
 
 lemma Collect_cong: "(\<And>x. P x = Q x) \<Longrightarrow> {x. P x} = {x. Q x}"
   by simp
 
 text \<open>
   Simproc for pulling \<open>x = t\<close> in \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>
   to the front (and similarly for \<open>t = x\<close>):
 \<close>
 
 simproc_setup defined_Collect ("{x. P x \<and> Q x}") = \<open>
   fn _ => Quantifier1.rearrange_Collect
     (fn ctxt =>
       resolve_tac ctxt @{thms Collect_cong} 1 THEN
       resolve_tac ctxt @{thms iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
           DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
 \<close>
 
 lemmas CollectE = CollectD [elim_format]
 
 lemma set_eqI:
   assumes "\<And>x. x \<in> A \<longleftrightarrow> x \<in> B"
   shows "A = B"
 proof -
   from assms have "{x. x \<in> A} = {x. x \<in> B}"
     by simp
   then show ?thesis by simp
 qed
 
 lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
   by (auto intro:set_eqI)
 
 lemma Collect_eqI:
   assumes "\<And>x. P x = Q x"
   shows "Collect P = Collect Q"
   using assms by (auto intro: set_eqI)
 
 text \<open>Lifting of predicate class instances\<close>
 
 instantiation set :: (type) boolean_algebra
 begin
 
 definition less_eq_set
   where "A \<le> B \<longleftrightarrow> (\<lambda>x. member x A) \<le> (\<lambda>x. member x B)"
 
 definition less_set
   where "A < B \<longleftrightarrow> (\<lambda>x. member x A) < (\<lambda>x. member x B)"
 
 definition inf_set
   where "A \<sqinter> B = Collect ((\<lambda>x. member x A) \<sqinter> (\<lambda>x. member x B))"
 
 definition sup_set
   where "A \<squnion> B = Collect ((\<lambda>x. member x A) \<squnion> (\<lambda>x. member x B))"
 
 definition bot_set
   where "\<bottom> = Collect \<bottom>"
 
 definition top_set
   where "\<top> = Collect \<top>"
 
 definition uminus_set
   where "- A = Collect (- (\<lambda>x. member x A))"
 
 definition minus_set
   where "A - B = Collect ((\<lambda>x. member x A) - (\<lambda>x. member x B))"
 
 instance
   by standard
     (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
       bot_set_def top_set_def uminus_set_def minus_set_def
       less_le_not_le sup_inf_distrib1 diff_eq set_eqI fun_eq_iff
       del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)
 
 end
 
 text \<open>Set enumerations\<close>
 
 abbreviation empty :: "'a set" ("{}")
   where "{} \<equiv> bot"
 
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
 
 
 subsection \<open>Subsets and bounded quantifiers\<close>
 
 abbreviation subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "subset \<equiv> less"
 
 abbreviation subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "subset_eq \<equiv> less_eq"
 
 notation
   subset  ("'(\<subset>')") and
   subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("'(\<subseteq>')") and
   subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
 abbreviation (input)
   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset \<equiv> greater"
 
 abbreviation (input)
   supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset_eq \<equiv> greater_eq"
 
 notation
   supset  ("'(\<supset>')") and
   supset  ("(_/ \<supset> _)" [51, 51] 50) and
   supset_eq  ("'(\<supseteq>')") and
   supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
 
 notation (ASCII output)
   subset  ("'(<')") and
   subset  ("(_/ < _)" [51, 51] 50) and
   subset_eq  ("'(<=')") and
   subset_eq  ("(_/ <= _)" [51, 51] 50)
 
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> \<open>bounded universal quantifiers\<close>
 
 definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> \<open>bounded existential quantifiers\<close>
 
 syntax (ASCII)
   "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3ALL (_/:_)./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX (_/:_)./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX! (_/:_)./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST (_/:_)./ _)" [0, 0, 10] 10)
 
 syntax (input)
   "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3! (_/:_)./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3? (_/:_)./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3?! (_/:_)./ _)" [0, 0, 10] 10)
 
 syntax
   "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/\<in>_)./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/\<in>_)./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
 
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
   "\<exists>!x\<in>A. P" \<rightharpoonup> "\<exists>!x. x \<in> A \<and> P"
   "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
 
 syntax (ASCII output)
   "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
 
 syntax
   "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
 
 translations
  "\<forall>A\<subset>B. P" \<rightharpoonup> "\<forall>A. A \<subset> B \<longrightarrow> P"
  "\<exists>A\<subset>B. P" \<rightharpoonup> "\<exists>A. A \<subset> B \<and> P"
  "\<forall>A\<subseteq>B. P" \<rightharpoonup> "\<forall>A. A \<subseteq> B \<longrightarrow> P"
  "\<exists>A\<subseteq>B. P" \<rightharpoonup> "\<exists>A. A \<subseteq> B \<and> P"
  "\<exists>!A\<subseteq>B. P" \<rightharpoonup> "\<exists>!A. A \<subseteq> B \<and> P"
 
 print_translation \<open>
   let
     val All_binder = Mixfix.binder_name \<^const_syntax>\<open>All\<close>;
     val Ex_binder = Mixfix.binder_name \<^const_syntax>\<open>Ex\<close>;
     val impl = \<^const_syntax>\<open>HOL.implies\<close>;
     val conj = \<^const_syntax>\<open>HOL.conj\<close>;
     val sbset = \<^const_syntax>\<open>subset\<close>;
     val sbset_eq = \<^const_syntax>\<open>subset_eq\<close>;
 
     val trans =
      [((All_binder, impl, sbset), \<^syntax_const>\<open>_setlessAll\<close>),
       ((All_binder, impl, sbset_eq), \<^syntax_const>\<open>_setleAll\<close>),
       ((Ex_binder, conj, sbset), \<^syntax_const>\<open>_setlessEx\<close>),
       ((Ex_binder, conj, sbset_eq), \<^syntax_const>\<open>_setleEx\<close>)];
 
     fun mk v (v', T) c n P =
       if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
       then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
       else raise Match;
 
     fun tr' q = (q, fn _ =>
       (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, Type (\<^type_name>\<open>set\<close>, _)),
           Const (c, _) $
             (Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
           (case AList.lookup (=) trans (q, c, d) of
             NONE => raise Match
           | SOME l => mk v (v', T) l n P)
         | _ => raise Match));
   in
     [tr' All_binder, tr' Ex_binder]
   end
 \<close>
 
 
 text \<open>
   \<^medskip>
   Translate between \<open>{e | x1\<dots>xn. P}\<close> and \<open>{u. \<exists>x1\<dots>xn. u = e \<and> P}\<close>;
   \<open>{y. \<exists>x1\<dots>xn. y = e \<and> P}\<close> is only translated if \<open>[0..n] \<subseteq> bvs e\<close>.
 \<close>
 
 syntax
   "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_ |/_./ _})")
 
 parse_translation \<open>
   let
     val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", \<^const_syntax>\<open>Ex\<close>));
 
     fun nvars (Const (\<^syntax_const>\<open>_idts\<close>, _) $ _ $ idts) = nvars idts + 1
       | nvars _ = 1;
 
     fun setcompr_tr ctxt [e, idts, b] =
       let
         val eq = Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Bound (nvars idts) $ e;
         val P = Syntax.const \<^const_syntax>\<open>HOL.conj\<close> $ eq $ b;
         val exP = ex_tr ctxt [idts, P];
       in Syntax.const \<^const_syntax>\<open>Collect\<close> $ absdummy dummyT exP end;
 
   in [(\<^syntax_const>\<open>_Setcompr\<close>, setcompr_tr)] end
 \<close>
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Ball\<close> \<^syntax_const>\<open>_Ball\<close>,
   Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Bex\<close> \<^syntax_const>\<open>_Bex\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 print_translation \<open>
 let
   val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>\<open>Ex\<close>, "DUMMY"));
 
   fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
     let
       fun check (Const (\<^const_syntax>\<open>Ex\<close>, _) $ Abs (_, _, P), n) = check (P, n + 1)
         | check (Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
               (Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
             subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
         | check _ = false;
 
         fun tr' (_ $ abs) =
           let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
           in Syntax.const \<^syntax_const>\<open>_Setcompr\<close> $ e $ idts $ Q end;
     in
       if check (P, 0) then tr' P
       else
         let
           val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
           val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
         in
           case t of
             Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
               (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
                 (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P =>
             if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
           | _ => M
         end
     end;
   in [(\<^const_syntax>\<open>Collect\<close>, setcompr_tr')] end
 \<close>
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
-  fn _ => Quantifier1.rearrange_bex
-    (fn ctxt =>
-      unfold_tac ctxt @{thms Bex_def} THEN
-      Quantifier1.prove_one_point_ex_tac ctxt)
+  fn _ => Quantifier1.rearrange_Bex
+    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
 \<close>
 
 simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
-  fn _ => Quantifier1.rearrange_ball
-    (fn ctxt =>
-      unfold_tac ctxt @{thms Ball_def} THEN
-      Quantifier1.prove_one_point_all_tac ctxt)
+  fn _ => Quantifier1.rearrange_Ball
+    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
 \<close>
 
 lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
   by (simp add: Ball_def)
 
 lemmas strip = impI allI ballI
 
 lemma bspec [dest?]: "\<forall>x\<in>A. P x \<Longrightarrow> x \<in> A \<Longrightarrow> P x"
   by (simp add: Ball_def)
 
 text \<open>Gives better instantiation for bound:\<close>
 setup \<open>
   map_theory_claset (fn ctxt =>
     ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt'))
 \<close>
 
 ML \<open>
 structure Simpdata =
 struct
   open Simpdata;
   val mksimps_pairs = [(\<^const_name>\<open>Ball\<close>, @{thms bspec})] @ mksimps_pairs;
 end;
 
 open Simpdata;
 \<close>
 
 declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))\<close>
 
 lemma ballE [elim]: "\<forall>x\<in>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
   unfolding Ball_def by blast
 
 lemma bexI [intro]: "P x \<Longrightarrow> x \<in> A \<Longrightarrow> \<exists>x\<in>A. P x"
   \<comment> \<open>Normally the best argument order: \<open>P x\<close> constrains the choice of \<open>x \<in> A\<close>.\<close>
   unfolding Bex_def by blast
 
 lemma rev_bexI [intro?]: "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x"
   \<comment> \<open>The best argument order when there is only one \<open>x \<in> A\<close>.\<close>
   unfolding Bex_def by blast
 
 lemma bexCI: "(\<forall>x\<in>A. \<not> P x \<Longrightarrow> P a) \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>x\<in>A. P x"
   unfolding Bex_def by blast
 
 lemma bexE [elim!]: "\<exists>x\<in>A. P x \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P x \<Longrightarrow> Q) \<Longrightarrow> Q"
   unfolding Bex_def by blast
 
 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<longrightarrow> P)"
   \<comment> \<open>Trival rewrite rule.\<close>
   by (simp add: Ball_def)
 
 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<and> P)"
   \<comment> \<open>Dual form for existentials.\<close>
   by (simp add: Bex_def)
 
 lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x = a) \<longleftrightarrow> a \<in> A"
   by blast
 
 lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a = x) \<longleftrightarrow> a \<in> A"
   by blast
 
 lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x = a \<and> P x) \<longleftrightarrow> a \<in> A \<and> P a"
   by blast
 
 lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a = x \<and> P x) \<longleftrightarrow> a \<in> A \<and> P a"
   by blast
 
 lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x = a \<longrightarrow> P x) \<longleftrightarrow> (a \<in> A \<longrightarrow> P a)"
   by blast
 
 lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a = x \<longrightarrow> P x) \<longleftrightarrow> (a \<in> A \<longrightarrow> P a)"
   by blast
 
 lemma ball_conj_distrib: "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> (\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x)"
   by blast
 
 lemma bex_disj_distrib: "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> (\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x)"
   by blast
 
 
 text \<open>Congruence rules\<close>
 
 lemma ball_cong:
   "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
 by (simp add: Ball_def)
 
 lemma ball_cong_simp [cong]:
   "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
 by (simp add: simp_implies_def Ball_def)
 
 lemma bex_cong:
   "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
 by (simp add: Bex_def cong: conj_cong)
 
 lemma bex_cong_simp [cong]:
   "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
 by (simp add: simp_implies_def Bex_def cong: conj_cong)
 
 lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
   by auto
 
 
 subsection \<open>Basic operations\<close>
 
 subsubsection \<open>Subsets\<close>
 
 lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
   by (simp add: less_eq_set_def le_fun_def)
 
 text \<open>
   \<^medskip>
   Map the type \<open>'a set \<Rightarrow> anything\<close> to just \<open>'a\<close>; for overloading constants
   whose first argument has type \<open>'a set\<close>.
 \<close>
 
 lemma subsetD [elim, intro?]: "A \<subseteq> B \<Longrightarrow> c \<in> A \<Longrightarrow> c \<in> B"
   by (simp add: less_eq_set_def le_fun_def)
   \<comment> \<open>Rule in Modus Ponens style.\<close>
 
 lemma rev_subsetD [intro?,no_atp]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
   \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
   by (rule subsetD)
 
 lemma subsetCE [elim,no_atp]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
 lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   by blast
 
 lemma contra_subsetD [no_atp]: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
   by blast
 
 lemma subset_refl: "A \<subseteq> A"
   by (fact order_refl) (* already [iff] *)
 
 lemma subset_trans: "A \<subseteq> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<subseteq> C"
   by (fact order_trans)
 
 lemma subset_not_subset_eq [code]: "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
   by (fact less_le_not_le)
 
 lemma eq_mem_trans: "a = b \<Longrightarrow> b \<in> A \<Longrightarrow> a \<in> A"
   by simp
 
 lemmas basic_trans_rules [trans] =
   order_trans_rules rev_subsetD subsetD eq_mem_trans
 
 
 subsubsection \<open>Equality\<close>
 
 lemma subset_antisym [intro!]: "A \<subseteq> B \<Longrightarrow> B \<subseteq> A \<Longrightarrow> A = B"
   \<comment> \<open>Anti-symmetry of the subset relation.\<close>
   by (iprover intro: set_eqI subsetD)
 
 text \<open>\<^medskip> Equality rules from ZF set theory -- are they appropriate here?\<close>
 
 lemma equalityD1: "A = B \<Longrightarrow> A \<subseteq> B"
   by simp
 
 lemma equalityD2: "A = B \<Longrightarrow> B \<subseteq> A"
   by simp
 
 text \<open>
   \<^medskip>
   Be careful when adding this to the claset as \<open>subset_empty\<close> is in the
   simpset: \<^prop>\<open>A = {}\<close> goes to \<^prop>\<open>{} \<subseteq> A\<close> and \<^prop>\<open>A \<subseteq> {}\<close>
   and then back to \<^prop>\<open>A = {}\<close>!
 \<close>
 
 lemma equalityE: "A = B \<Longrightarrow> (A \<subseteq> B \<Longrightarrow> B \<subseteq> A \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
 lemma equalityCE [elim]: "A = B \<Longrightarrow> (c \<in> A \<Longrightarrow> c \<in> B \<Longrightarrow> P) \<Longrightarrow> (c \<notin> A \<Longrightarrow> c \<notin> B \<Longrightarrow> P) \<Longrightarrow> P"
   by blast
 
 lemma eqset_imp_iff: "A = B \<Longrightarrow> x \<in> A \<longleftrightarrow> x \<in> B"
   by simp
 
 lemma eqelem_imp_iff: "x = y \<Longrightarrow> x \<in> A \<longleftrightarrow> y \<in> A"
   by simp
 
 
 subsubsection \<open>The empty set\<close>
 
 lemma empty_def: "{} = {x. False}"
   by (simp add: bot_set_def bot_fun_def)
 
 lemma empty_iff [simp]: "c \<in> {} \<longleftrightarrow> False"
   by (simp add: empty_def)
 
 lemma emptyE [elim!]: "a \<in> {} \<Longrightarrow> P"
   by simp
 
 lemma empty_subsetI [iff]: "{} \<subseteq> A"
   \<comment> \<open>One effect is to delete the ASSUMPTION \<^prop>\<open>{} \<subseteq> A\<close>\<close>
   by blast
 
 lemma equals0I: "(\<And>y. y \<in> A \<Longrightarrow> False) \<Longrightarrow> A = {}"
   by blast
 
 lemma equals0D: "A = {} \<Longrightarrow> a \<notin> A"
   \<comment> \<open>Use for reasoning about disjointness: \<open>A \<inter> B = {}\<close>\<close>
   by blast
 
 lemma ball_empty [simp]: "Ball {} P \<longleftrightarrow> True"
   by (simp add: Ball_def)
 
 lemma bex_empty [simp]: "Bex {} P \<longleftrightarrow> False"
   by (simp add: Bex_def)
 
 
 subsubsection \<open>The universal set -- UNIV\<close>
 
 abbreviation UNIV :: "'a set"
   where "UNIV \<equiv> top"
 
 lemma UNIV_def: "UNIV = {x. True}"
   by (simp add: top_set_def top_fun_def)
 
 lemma UNIV_I [simp]: "x \<in> UNIV"
   by (simp add: UNIV_def)
 
 declare UNIV_I [intro]  \<comment> \<open>unsafe makes it less likely to cause problems\<close>
 
 lemma UNIV_witness [intro?]: "\<exists>x. x \<in> UNIV"
   by simp
 
 lemma subset_UNIV: "A \<subseteq> UNIV"
   by (fact top_greatest) (* already simp *)
 
 text \<open>
   \<^medskip>
   Eta-contracting these two rules (to remove \<open>P\<close>) causes them
   to be ignored because of their interaction with congruence rules.
 \<close>
 
 lemma ball_UNIV [simp]: "Ball UNIV P \<longleftrightarrow> All P"
   by (simp add: Ball_def)
 
 lemma bex_UNIV [simp]: "Bex UNIV P \<longleftrightarrow> Ex P"
   by (simp add: Bex_def)
 
 lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
   by auto
 
 lemma UNIV_not_empty [iff]: "UNIV \<noteq> {}"
   by (blast elim: equalityE)
 
 lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
   by blast
 
 
 subsubsection \<open>The Powerset operator -- Pow\<close>
 
 definition Pow :: "'a set \<Rightarrow> 'a set set"
   where Pow_def: "Pow A = {B. B \<subseteq> A}"
 
 lemma Pow_iff [iff]: "A \<in> Pow B \<longleftrightarrow> A \<subseteq> B"
   by (simp add: Pow_def)
 
 lemma PowI: "A \<subseteq> B \<Longrightarrow> A \<in> Pow B"
   by (simp add: Pow_def)
 
 lemma PowD: "A \<in> Pow B \<Longrightarrow> A \<subseteq> B"
   by (simp add: Pow_def)
 
 lemma Pow_bottom: "{} \<in> Pow B"
   by simp
 
 lemma Pow_top: "A \<in> Pow A"
   by simp
 
 lemma Pow_not_empty: "Pow A \<noteq> {}"
   using Pow_top by blast
 
 
 subsubsection \<open>Set complement\<close>
 
 lemma Compl_iff [simp]: "c \<in> - A \<longleftrightarrow> c \<notin> A"
   by (simp add: fun_Compl_def uminus_set_def)
 
 lemma ComplI [intro!]: "(c \<in> A \<Longrightarrow> False) \<Longrightarrow> c \<in> - A"
   by (simp add: fun_Compl_def uminus_set_def) blast
 
 text \<open>
   \<^medskip>
   This form, with negated conclusion, works well with the Classical prover.
   Negated assumptions behave like formulae on the right side of the
   notional turnstile \dots
 \<close>
 
 lemma ComplD [dest!]: "c \<in> - A \<Longrightarrow> c \<notin> A"
   by simp
 
 lemmas ComplE = ComplD [elim_format]
 
 lemma Compl_eq: "- A = {x. \<not> x \<in> A}"
   by blast
 
 
 subsubsection \<open>Binary intersection\<close>
 
 abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<inter>" 70)
   where "(\<inter>) \<equiv> inf"
 
 notation (ASCII)
   inter  (infixl "Int" 70)
 
 lemma Int_def: "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   by (simp add: inf_set_def inf_fun_def)
 
 lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> c \<in> A \<and> c \<in> B"
   unfolding Int_def by blast
 
 lemma IntI [intro!]: "c \<in> A \<Longrightarrow> c \<in> B \<Longrightarrow> c \<in> A \<inter> B"
   by simp
 
 lemma IntD1: "c \<in> A \<inter> B \<Longrightarrow> c \<in> A"
   by simp
 
 lemma IntD2: "c \<in> A \<inter> B \<Longrightarrow> c \<in> B"
   by simp
 
 lemma IntE [elim!]: "c \<in> A \<inter> B \<Longrightarrow> (c \<in> A \<Longrightarrow> c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   by (fact mono_inf)
 
 
 subsubsection \<open>Binary union\<close>
 
 abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<union>" 65)
   where "union \<equiv> sup"
 
 notation (ASCII)
   union  (infixl "Un" 65)
 
 lemma Un_def: "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   by (simp add: sup_set_def sup_fun_def)
 
 lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> c \<in> A \<or> c \<in> B"
   unfolding Un_def by blast
 
 lemma UnI1 [elim?]: "c \<in> A \<Longrightarrow> c \<in> A \<union> B"
   by simp
 
 lemma UnI2 [elim?]: "c \<in> B \<Longrightarrow> c \<in> A \<union> B"
   by simp
 
 text \<open>\<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs. \<open>B\<close>.\<close>
 lemma UnCI [intro!]: "(c \<notin> B \<Longrightarrow> c \<in> A) \<Longrightarrow> c \<in> A \<union> B"
   by auto
 
 lemma UnE [elim!]: "c \<in> A \<union> B \<Longrightarrow> (c \<in> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding Un_def by blast
 
 lemma insert_def: "insert a B = {x. x = a} \<union> B"
   by (simp add: insert_compr Un_def)
 
 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   by (fact mono_sup)
 
 
 subsubsection \<open>Set difference\<close>
 
 lemma Diff_iff [simp]: "c \<in> A - B \<longleftrightarrow> c \<in> A \<and> c \<notin> B"
   by (simp add: minus_set_def fun_diff_def)
 
 lemma DiffI [intro!]: "c \<in> A \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<in> A - B"
   by simp
 
 lemma DiffD1: "c \<in> A - B \<Longrightarrow> c \<in> A"
   by simp
 
 lemma DiffD2: "c \<in> A - B \<Longrightarrow> c \<in> B \<Longrightarrow> P"
   by simp
 
 lemma DiffE [elim!]: "c \<in> A - B \<Longrightarrow> (c \<in> A \<Longrightarrow> c \<notin> B \<Longrightarrow> P) \<Longrightarrow> P"
   by simp
 
 lemma set_diff_eq: "A - B = {x. x \<in> A \<and> x \<notin> B}"
   by blast
 
 lemma Compl_eq_Diff_UNIV: "- A = (UNIV - A)"
   by blast
 
 
 subsubsection \<open>Augmenting a set -- \<^const>\<open>insert\<close>\<close>
 
 lemma insert_iff [simp]: "a \<in> insert b A \<longleftrightarrow> a = b \<or> a \<in> A"
   unfolding insert_def by blast
 
 lemma insertI1: "a \<in> insert a B"
   by simp
 
 lemma insertI2: "a \<in> B \<Longrightarrow> a \<in> insert b B"
   by simp
 
 lemma insertE [elim!]: "a \<in> insert b A \<Longrightarrow> (a = b \<Longrightarrow> P) \<Longrightarrow> (a \<in> A \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding insert_def by blast
 
 lemma insertCI [intro!]: "(a \<notin> B \<Longrightarrow> a = b) \<Longrightarrow> a \<in> insert b B"
   \<comment> \<open>Classical introduction rule.\<close>
   by auto
 
 lemma subset_insert_iff: "A \<subseteq> insert x B \<longleftrightarrow> (if x \<in> A then A - {x} \<subseteq> B else A \<subseteq> B)"
   by auto
 
 lemma set_insert:
   assumes "x \<in> A"
   obtains B where "A = insert x B" and "x \<notin> B"
 proof
   show "A = insert x (A - {x})" using assms by blast
   show "x \<notin> A - {x}" by blast
 qed
 
 lemma insert_ident: "x \<notin> A \<Longrightarrow> x \<notin> B \<Longrightarrow> insert x A = insert x B \<longleftrightarrow> A = B"
   by auto
 
 lemma insert_eq_iff:
   assumes "a \<notin> A" "b \<notin> B"
   shows "insert a A = insert b B \<longleftrightarrow>
     (if a = b then A = B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
     (is "?L \<longleftrightarrow> ?R")
 proof
   show ?R if ?L
   proof (cases "a = b")
     case True
     with assms \<open>?L\<close> show ?R
       by (simp add: insert_ident)
   next
     case False
     let ?C = "A - {b}"
     have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
       using assms \<open>?L\<close> \<open>a \<noteq> b\<close> by auto
     then show ?R using \<open>a \<noteq> b\<close> by auto
   qed
   show ?L if ?R
     using that by (auto split: if_splits)
 qed
 
 lemma insert_UNIV: "insert x UNIV = UNIV"
   by auto
 
 
 subsubsection \<open>Singletons, using insert\<close>
 
 lemma singletonI [intro!]: "a \<in> {a}"
   \<comment> \<open>Redundant? But unlike \<open>insertCI\<close>, it proves the subgoal immediately!\<close>
   by (rule insertI1)
 
 lemma singletonD [dest!]: "b \<in> {a} \<Longrightarrow> b = a"
   by blast
 
 lemmas singletonE = singletonD [elim_format]
 
 lemma singleton_iff: "b \<in> {a} \<longleftrightarrow> b = a"
   by blast
 
 lemma singleton_inject [dest!]: "{a} = {b} \<Longrightarrow> a = b"
   by blast
 
 lemma singleton_insert_inj_eq [iff]: "{b} = insert a A \<longleftrightarrow> a = b \<and> A \<subseteq> {b}"
   by blast
 
 lemma singleton_insert_inj_eq' [iff]: "insert a A = {b} \<longleftrightarrow> a = b \<and> A \<subseteq> {b}"
   by blast
 
 lemma subset_singletonD: "A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}"
   by fast
 
 lemma subset_singleton_iff: "X \<subseteq> {a} \<longleftrightarrow> X = {} \<or> X = {a}"
   by blast
 
 lemma subset_singleton_iff_Uniq: "(\<exists>a. A \<subseteq> {a}) \<longleftrightarrow> (\<exists>\<^sub>\<le>\<^sub>1x. x \<in> A)"
   unfolding Uniq_def by blast
 
 lemma singleton_conv [simp]: "{x. x = a} = {a}"
   by blast
 
 lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
   by blast
 
 lemma Diff_single_insert: "A - {x} \<subseteq> B \<Longrightarrow> A \<subseteq> insert x B"
   by blast
 
 lemma subset_Diff_insert: "A \<subseteq> B - insert x C \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
   by blast
 
 lemma doubleton_eq_iff: "{a, b} = {c, d} \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
   by (blast elim: equalityE)
 
 lemma Un_singleton_iff: "A \<union> B = {x} \<longleftrightarrow> A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x}"
   by auto
 
 lemma singleton_Un_iff: "{x} = A \<union> B \<longleftrightarrow> A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x}"
   by auto
 
 
 subsubsection \<open>Image of a set under a function\<close>
 
 text \<open>Frequently \<open>b\<close> does not have the syntactic form of \<open>f x\<close>.\<close>
 
 definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set"    (infixr "`" 90)
   where "f ` A = {y. \<exists>x\<in>A. y = f x}"
 
 lemma image_eqI [simp, intro]: "b = f x \<Longrightarrow> x \<in> A \<Longrightarrow> b \<in> f ` A"
   unfolding image_def by blast
 
 lemma imageI: "x \<in> A \<Longrightarrow> f x \<in> f ` A"
   by (rule image_eqI) (rule refl)
 
 lemma rev_image_eqI: "x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A"
   \<comment> \<open>This version's more effective when we already have the required \<open>x\<close>.\<close>
   by (rule image_eqI)
 
 lemma imageE [elim!]:
   assumes "b \<in> (\<lambda>x. f x) ` A"  \<comment> \<open>The eta-expansion gives variable-name preservation.\<close>
   obtains x where "b = f x" and "x \<in> A"
   using assms unfolding image_def by blast
 
 lemma Compr_image_eq: "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}"
   by auto
 
 lemma image_Un: "f ` (A \<union> B) = f ` A \<union> f ` B"
   by blast
 
 lemma image_iff: "z \<in> f ` A \<longleftrightarrow> (\<exists>x\<in>A. z = f x)"
   by blast
 
 lemma image_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B"
   \<comment> \<open>Replaces the three steps \<open>subsetI\<close>, \<open>imageE\<close>,
     \<open>hypsubst\<close>, but breaks too many existing proofs.\<close>
   by blast
 
 lemma image_subset_iff: "f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
   \<comment> \<open>This rewrite rule would confuse users if made default.\<close>
   by blast
 
 lemma subset_imageE:
   assumes "B \<subseteq> f ` A"
   obtains C where "C \<subseteq> A" and "B = f ` C"
 proof -
   from assms have "B = f ` {a \<in> A. f a \<in> B}" by fast
   moreover have "{a \<in> A. f a \<in> B} \<subseteq> A" by blast
   ultimately show thesis by (blast intro: that)
 qed
 
 lemma subset_image_iff: "B \<subseteq> f ` A \<longleftrightarrow> (\<exists>AA\<subseteq>A. B = f ` AA)"
   by (blast elim: subset_imageE)
 
 lemma image_ident [simp]: "(\<lambda>x. x) ` Y = Y"
   by blast
 
 lemma image_empty [simp]: "f ` {} = {}"
   by blast
 
 lemma image_insert [simp]: "f ` insert a B = insert (f a) (f ` B)"
   by blast
 
 lemma image_constant: "x \<in> A \<Longrightarrow> (\<lambda>x. c) ` A = {c}"
   by auto
 
 lemma image_constant_conv: "(\<lambda>x. c) ` A = (if A = {} then {} else {c})"
   by auto
 
 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   by blast
 
 lemma insert_image [simp]: "x \<in> A \<Longrightarrow> insert (f x) (f ` A) = f ` A"
   by blast
 
 lemma image_is_empty [iff]: "f ` A = {} \<longleftrightarrow> A = {}"
   by blast
 
 lemma empty_is_image [iff]: "{} = f ` A \<longleftrightarrow> A = {}"
   by blast
 
 lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
   \<comment> \<open>NOT suitable as a default simp rule: the RHS isn't simpler than the LHS,
       with its implicit quantifier and conjunction.  Also image enjoys better
       equational properties than does the RHS.\<close>
   by blast
 
 lemma if_image_distrib [simp]:
   "(\<lambda>x. if P x then f x else g x) ` S = f ` (S \<inter> {x. P x}) \<union> g ` (S \<inter> {x. \<not> P x})"
   by auto
 
 lemma image_cong:
   "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N \<Longrightarrow> f x = g x"
   using that by (simp add: image_def)
 
 lemma image_cong_simp [cong]:
   "f ` M = g ` N" if "M = N" "\<And>x. x \<in> N =simp=> f x = g x"
   using that image_cong [of M N f g] by (simp add: simp_implies_def)
 
 lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
   by blast
 
 lemma image_diff_subset: "f ` A - f ` B \<subseteq> f ` (A - B)"
   by blast
 
 lemma Setcompr_eq_image: "{f x |x. x \<in> A} = f ` A"
   by blast
 
 lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}"
   by auto
 
 lemma ball_imageD: "\<forall>x\<in>f ` A. P x \<Longrightarrow> \<forall>x\<in>A. P (f x)"
   by simp
 
 lemma bex_imageD: "\<exists>x\<in>f ` A. P x \<Longrightarrow> \<exists>x\<in>A. P (f x)"
   by auto
 
 lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   by auto
 
 
 text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>
 
 abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set"  \<comment> \<open>of function\<close>
   where "range f \<equiv> f ` UNIV"
 
 lemma range_eqI: "b = f x \<Longrightarrow> b \<in> range f"
   by simp
 
 lemma rangeI: "f x \<in> range f"
   by simp
 
 lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) \<Longrightarrow> (\<And>x. b = f x \<Longrightarrow> P) \<Longrightarrow> P"
   by (rule imageE)
 
 lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
   by auto
 
 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
   by auto
 
 lemma range_constant [simp]: "range (\<lambda>_. x) = {x}"
   by (simp add: image_constant)
 
 lemma range_eq_singletonD: "range f = {a} \<Longrightarrow> f x = a"
   by auto
 
 
 subsubsection \<open>Some rules with \<open>if\<close>\<close>
 
 text \<open>Elimination of \<open>{x. \<dots> \<and> x = t \<and> \<dots>}\<close>.\<close>
 
 lemma Collect_conv_if: "{x. x = a \<and> P x} = (if P a then {a} else {})"
   by auto
 
 lemma Collect_conv_if2: "{x. a = x \<and> P x} = (if P a then {a} else {})"
   by auto
 
 text \<open>
   Rewrite rules for boolean case-splitting: faster than \<open>if_split [split]\<close>.
 \<close>
 
 lemma if_split_eq1: "(if Q then x else y) = b \<longleftrightarrow> (Q \<longrightarrow> x = b) \<and> (\<not> Q \<longrightarrow> y = b)"
   by (rule if_split)
 
 lemma if_split_eq2: "a = (if Q then x else y) \<longleftrightarrow> (Q \<longrightarrow> a = x) \<and> (\<not> Q \<longrightarrow> a = y)"
   by (rule if_split)
 
 text \<open>
   Split ifs on either side of the membership relation.
   Not for \<open>[simp]\<close> -- can cause goals to blow up!
 \<close>
 
 lemma if_split_mem1: "(if Q then x else y) \<in> b \<longleftrightarrow> (Q \<longrightarrow> x \<in> b) \<and> (\<not> Q \<longrightarrow> y \<in> b)"
   by (rule if_split)
 
 lemma if_split_mem2: "(a \<in> (if Q then x else y)) \<longleftrightarrow> (Q \<longrightarrow> a \<in> x) \<and> (\<not> Q \<longrightarrow> a \<in> y)"
   by (rule if_split [where P = "\<lambda>S. a \<in> S"])
 
 lemmas split_ifs = if_bool_eq_conj if_split_eq1 if_split_eq2 if_split_mem1 if_split_mem2
 
 (*Would like to add these, but the existing code only searches for the
   outer-level constant, which in this case is just Set.member; we instead need
   to use term-nets to associate patterns with rules.  Also, if a rule fails to
   apply, then the formula should be kept.
   [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
    ("Int", [IntD1,IntD2]),
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
 
 
 subsection \<open>Further operations and lemmas\<close>
 
 subsubsection \<open>The ``proper subset'' relation\<close>
 
 lemma psubsetI [intro!]: "A \<subseteq> B \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<subset> B"
   unfolding less_le by blast
 
 lemma psubsetE [elim!]: "A \<subset> B \<Longrightarrow> (A \<subseteq> B \<Longrightarrow> \<not> B \<subseteq> A \<Longrightarrow> R) \<Longrightarrow> R"
   unfolding less_le by blast
 
 lemma psubset_insert_iff:
   "A \<subset> insert x B \<longleftrightarrow> (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
   by (auto simp add: less_le subset_insert_iff)
 
 lemma psubset_eq: "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
   by (simp only: less_le)
 
 lemma psubset_imp_subset: "A \<subset> B \<Longrightarrow> A \<subseteq> B"
   by (simp add: psubset_eq)
 
 lemma psubset_trans: "A \<subset> B \<Longrightarrow> B \<subset> C \<Longrightarrow> A \<subset> C"
   unfolding less_le by (auto dest: subset_antisym)
 
 lemma psubsetD: "A \<subset> B \<Longrightarrow> c \<in> A \<Longrightarrow> c \<in> B"
   unfolding less_le by (auto dest: subsetD)
 
 lemma psubset_subset_trans: "A \<subset> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<subset> C"
   by (auto simp add: psubset_eq)
 
 lemma subset_psubset_trans: "A \<subseteq> B \<Longrightarrow> B \<subset> C \<Longrightarrow> A \<subset> C"
   by (auto simp add: psubset_eq)
 
 lemma psubset_imp_ex_mem: "A \<subset> B \<Longrightarrow> \<exists>b. b \<in> B - A"
   unfolding less_le by blast
 
 lemma atomize_ball: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<equiv> Trueprop (\<forall>x\<in>A. P x)"
   by (simp only: Ball_def atomize_all atomize_imp)
 
 lemmas [symmetric, rulify] = atomize_ball
   and [symmetric, defn] = atomize_ball
 
 lemma image_Pow_mono: "f ` A \<subseteq> B \<Longrightarrow> image f ` Pow A \<subseteq> Pow B"
   by blast
 
 lemma image_Pow_surj: "f ` A = B \<Longrightarrow> image f ` Pow A = Pow B"
   by (blast elim: subset_imageE)
 
 
 subsubsection \<open>Derived rules involving subsets.\<close>
 
 text \<open>\<open>insert\<close>.\<close>
 
 lemma subset_insertI: "B \<subseteq> insert a B"
   by (rule subsetI) (erule insertI2)
 
 lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
   by blast
 
 lemma subset_insert: "x \<notin> A \<Longrightarrow> A \<subseteq> insert x B \<longleftrightarrow> A \<subseteq> B"
   by blast
 
 
 text \<open>\<^medskip> Finite Union -- the least upper bound of two sets.\<close>
 
 lemma Un_upper1: "A \<subseteq> A \<union> B"
   by (fact sup_ge1)
 
 lemma Un_upper2: "B \<subseteq> A \<union> B"
   by (fact sup_ge2)
 
 lemma Un_least: "A \<subseteq> C \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<union> B \<subseteq> C"
   by (fact sup_least)
 
 
 text \<open>\<^medskip> Finite Intersection -- the greatest lower bound of two sets.\<close>
 
 lemma Int_lower1: "A \<inter> B \<subseteq> A"
   by (fact inf_le1)
 
 lemma Int_lower2: "A \<inter> B \<subseteq> B"
   by (fact inf_le2)
 
 lemma Int_greatest: "C \<subseteq> A \<Longrightarrow> C \<subseteq> B \<Longrightarrow> C \<subseteq> A \<inter> B"
   by (fact inf_greatest)
 
 
 text \<open>\<^medskip> Set difference.\<close>
 
 lemma Diff_subset[simp]: "A - B \<subseteq> A"
   by blast
 
 lemma Diff_subset_conv: "A - B \<subseteq> C \<longleftrightarrow> A \<subseteq> B \<union> C"
   by blast
 
 
 subsubsection \<open>Equalities involving union, intersection, inclusion, etc.\<close>
 
 text \<open>\<open>{}\<close>.\<close>
 
 lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
   \<comment> \<open>supersedes \<open>Collect_False_empty\<close>\<close>
   by auto
 
 lemma subset_empty [simp]: "A \<subseteq> {} \<longleftrightarrow> A = {}"
   by (fact bot_unique)
 
 lemma not_psubset_empty [iff]: "\<not> (A < {})"
   by (fact not_less_bot) (* FIXME: already simp *)
 
 lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
 
 lemma Collect_empty_eq [simp]: "Collect P = {} \<longleftrightarrow> (\<forall>x. \<not> P x)"
   by blast
 
 lemma empty_Collect_eq [simp]: "{} = Collect P \<longleftrightarrow> (\<forall>x. \<not> P x)"
   by blast
 
 lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
   by blast
 
 lemma Collect_disj_eq: "{x. P x \<or> Q x} = {x. P x} \<union> {x. Q x}"
   by blast
 
 lemma Collect_imp_eq: "{x. P x \<longrightarrow> Q x} = - {x. P x} \<union> {x. Q x}"
   by blast
 
 lemma Collect_conj_eq: "{x. P x \<and> Q x} = {x. P x} \<inter> {x. Q x}"
   by blast
 
 lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
   by blast
 
 
 text \<open>\<^medskip> \<open>insert\<close>.\<close>
 
 lemma insert_is_Un: "insert a A = {a} \<union> A"
   \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a {}\<close>\<close>
   by blast
 
 lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
   and empty_not_insert [simp]: "{} \<noteq> insert a A"
   by blast+
 
 lemma insert_absorb: "a \<in> A \<Longrightarrow> insert a A = A"
   \<comment> \<open>\<open>[simp]\<close> causes recursive calls when there are nested inserts\<close>
   \<comment> \<open>with \<^emph>\<open>quadratic\<close> running time\<close>
   by blast
 
 lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
   by blast
 
 lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
   by blast
 
 lemma insert_subset [simp]: "insert x A \<subseteq> B \<longleftrightarrow> x \<in> B \<and> A \<subseteq> B"
   by blast
 
 lemma mk_disjoint_insert: "a \<in> A \<Longrightarrow> \<exists>B. A = insert a B \<and> a \<notin> B"
   \<comment> \<open>use new \<open>B\<close> rather than \<open>A - {a}\<close> to avoid infinite unfolding\<close>
   by (rule exI [where x = "A - {a}"]) blast
 
 lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a \<longrightarrow> P u}"
   by auto
 
 lemma insert_inter_insert [simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   by blast
 
 lemma insert_disjoint [simp]:
   "insert a A \<inter> B = {} \<longleftrightarrow> a \<notin> B \<and> A \<inter> B = {}"
   "{} = insert a A \<inter> B \<longleftrightarrow> a \<notin> B \<and> {} = A \<inter> B"
   by auto
 
 lemma disjoint_insert [simp]:
   "B \<inter> insert a A = {} \<longleftrightarrow> a \<notin> B \<and> B \<inter> A = {}"
   "{} = A \<inter> insert b B \<longleftrightarrow> b \<notin> A \<and> {} = A \<inter> B"
   by auto
 
 
 text \<open>\<^medskip> \<open>Int\<close>\<close>
 
 lemma Int_absorb: "A \<inter> A = A"
   by (fact inf_idem) (* already simp *)
 
 lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
   by (fact inf_left_idem)
 
 lemma Int_commute: "A \<inter> B = B \<inter> A"
   by (fact inf_commute)
 
 lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
   by (fact inf_left_commute)
 
 lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
   by (fact inf_assoc)
 
 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
   \<comment> \<open>Intersection is an AC-operator\<close>
 
 lemma Int_absorb1: "B \<subseteq> A \<Longrightarrow> A \<inter> B = B"
   by (fact inf_absorb2)
 
 lemma Int_absorb2: "A \<subseteq> B \<Longrightarrow> A \<inter> B = A"
   by (fact inf_absorb1)
 
 lemma Int_empty_left: "{} \<inter> B = {}"
   by (fact inf_bot_left) (* already simp *)
 
 lemma Int_empty_right: "A \<inter> {} = {}"
   by (fact inf_bot_right) (* already simp *)
 
 lemma disjoint_eq_subset_Compl: "A \<inter> B = {} \<longleftrightarrow> A \<subseteq> - B"
   by blast
 
 lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x. x\<in>A \<longrightarrow> x \<notin> B)"
   by blast
 
 lemma disjoint_iff_not_equal: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
   by blast
 
 lemma Int_UNIV_left: "UNIV \<inter> B = B"
   by (fact inf_top_left) (* already simp *)
 
 lemma Int_UNIV_right: "A \<inter> UNIV = A"
   by (fact inf_top_right) (* already simp *)
 
 lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
   by (fact inf_sup_distrib1)
 
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   by (fact inf_sup_distrib2)
 
 lemma Int_UNIV [simp]: "A \<inter> B = UNIV \<longleftrightarrow> A = UNIV \<and> B = UNIV"
   by (fact inf_eq_top_iff) (* already simp *)
 
 lemma Int_subset_iff [simp]: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A \<and> C \<subseteq> B"
   by (fact le_inf_iff)
 
 lemma Int_Collect: "x \<in> A \<inter> {x. P x} \<longleftrightarrow> x \<in> A \<and> P x"
   by blast
 
 
 text \<open>\<^medskip> \<open>Un\<close>.\<close>
 
 lemma Un_absorb: "A \<union> A = A"
   by (fact sup_idem) (* already simp *)
 
 lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   by (fact sup_left_idem)
 
 lemma Un_commute: "A \<union> B = B \<union> A"
   by (fact sup_commute)
 
 lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
   by (fact sup_left_commute)
 
 lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
   by (fact sup_assoc)
 
 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   \<comment> \<open>Union is an AC-operator\<close>
 
 lemma Un_absorb1: "A \<subseteq> B \<Longrightarrow> A \<union> B = B"
   by (fact sup_absorb2)
 
 lemma Un_absorb2: "B \<subseteq> A \<Longrightarrow> A \<union> B = A"
   by (fact sup_absorb1)
 
 lemma Un_empty_left: "{} \<union> B = B"
   by (fact sup_bot_left) (* already simp *)
 
 lemma Un_empty_right: "A \<union> {} = A"
   by (fact sup_bot_right) (* already simp *)
 
 lemma Un_UNIV_left: "UNIV \<union> B = UNIV"
   by (fact sup_top_left) (* already simp *)
 
 lemma Un_UNIV_right: "A \<union> UNIV = UNIV"
   by (fact sup_top_right) (* already simp *)
 
 lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   by blast
 
 lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
   by blast
 
 lemma Int_insert_left: "(insert a B) \<inter> C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
   by auto
 
 lemma Int_insert_left_if0 [simp]: "a \<notin> C \<Longrightarrow> (insert a B) \<inter> C = B \<inter> C"
   by auto
 
 lemma Int_insert_left_if1 [simp]: "a \<in> C \<Longrightarrow> (insert a B) \<inter> C = insert a (B \<inter> C)"
   by auto
 
 lemma Int_insert_right: "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   by auto
 
 lemma Int_insert_right_if0 [simp]: "a \<notin> A \<Longrightarrow> A \<inter> (insert a B) = A \<inter> B"
   by auto
 
 lemma Int_insert_right_if1 [simp]: "a \<in> A \<Longrightarrow> A \<inter> (insert a B) = insert a (A \<inter> B)"
   by auto
 
 lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   by (fact sup_inf_distrib1)
 
 lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
   by (fact sup_inf_distrib2)
 
 lemma Un_Int_crazy: "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   by blast
 
 lemma subset_Un_eq: "A \<subseteq> B \<longleftrightarrow> A \<union> B = B"
   by (fact le_iff_sup)
 
 lemma Un_empty [iff]: "A \<union> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
   by (fact sup_eq_bot_iff) (* FIXME: already simp *)
 
 lemma Un_subset_iff [simp]: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C \<and> B \<subseteq> C"
   by (fact le_sup_iff)
 
 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   by blast
 
 lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
   by blast
 
 lemma subset_UnE: 
   assumes "C \<subseteq> A \<union> B"
   obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
 proof
   show "C \<inter> A \<subseteq> A" "C \<inter> B \<subseteq> B" "C = (C \<inter> A) \<union> (C \<inter> B)"
     using assms by blast+
 qed
 
 text \<open>\<^medskip> Set complement\<close>
 
 lemma Compl_disjoint [simp]: "A \<inter> - A = {}"
   by (fact inf_compl_bot)
 
 lemma Compl_disjoint2 [simp]: "- A \<inter> A = {}"
   by (fact compl_inf_bot)
 
 lemma Compl_partition: "A \<union> - A = UNIV"
   by (fact sup_compl_top)
 
 lemma Compl_partition2: "- A \<union> A = UNIV"
   by (fact compl_sup_top)
 
 lemma double_complement: "- (-A) = A" for A :: "'a set"
   by (fact double_compl) (* already simp *)
 
 lemma Compl_Un: "- (A \<union> B) = (- A) \<inter> (- B)"
   by (fact compl_sup) (* already simp *)
 
 lemma Compl_Int: "- (A \<inter> B) = (- A) \<union> (- B)"
   by (fact compl_inf) (* already simp *)
 
 lemma subset_Compl_self_eq: "A \<subseteq> - A \<longleftrightarrow> A = {}"
   by blast
 
 lemma Un_Int_assoc_eq: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C) \<longleftrightarrow> C \<subseteq> A"
   \<comment> \<open>Halmos, Naive Set Theory, page 16.\<close>
   by blast
 
 lemma Compl_UNIV_eq: "- UNIV = {}"
   by (fact compl_top_eq) (* already simp *)
 
 lemma Compl_empty_eq: "- {} = UNIV"
   by (fact compl_bot_eq) (* already simp *)
 
 lemma Compl_subset_Compl_iff [iff]: "- A \<subseteq> - B \<longleftrightarrow> B \<subseteq> A"
   by (fact compl_le_compl_iff) (* FIXME: already simp *)
 
 lemma Compl_eq_Compl_iff [iff]: "- A = - B \<longleftrightarrow> A = B"
   for A B :: "'a set"
   by (fact compl_eq_compl_iff) (* FIXME: already simp *)
 
 lemma Compl_insert: "- insert x A = (- A) - {x}"
   by blast
 
 text \<open>\<^medskip> Bounded quantifiers.
 
   The following are not added to the default simpset because
   (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.
 \<close>
 
 lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>B. P x)"
   by blast
 
 lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>B. P x)"
   by blast
 
 
 text \<open>\<^medskip> Set difference.\<close>
 
 lemma Diff_eq: "A - B = A \<inter> (- B)"
   by blast
 
 lemma Diff_eq_empty_iff [simp]: "A - B = {} \<longleftrightarrow> A \<subseteq> B"
   by blast
 
 lemma Diff_cancel [simp]: "A - A = {}"
   by blast
 
 lemma Diff_idemp [simp]: "(A - B) - B = A - B"
   for A B :: "'a set"
   by blast
 
 lemma Diff_triv: "A \<inter> B = {} \<Longrightarrow> A - B = A"
   by (blast elim: equalityE)
 
 lemma empty_Diff [simp]: "{} - A = {}"
   by blast
 
 lemma Diff_empty [simp]: "A - {} = A"
   by blast
 
 lemma Diff_UNIV [simp]: "A - UNIV = {}"
   by blast
 
 lemma Diff_insert0 [simp]: "x \<notin> A \<Longrightarrow> A - insert x B = A - B"
   by blast
 
 lemma Diff_insert: "A - insert a B = A - B - {a}"
   \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a 0\<close>\<close>
   by blast
 
 lemma Diff_insert2: "A - insert a B = A - {a} - B"
   \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} \<equiv> insert a 0\<close>\<close>
   by blast
 
 lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
   by auto
 
 lemma insert_Diff1 [simp]: "x \<in> B \<Longrightarrow> insert x A - B = A - B"
   by blast
 
 lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
   by blast
 
 lemma insert_Diff: "a \<in> A \<Longrightarrow> insert a (A - {a}) = A"
   by blast
 
 lemma Diff_insert_absorb: "x \<notin> A \<Longrightarrow> (insert x A) - {x} = A"
   by auto
 
 lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
   by blast
 
 lemma Diff_partition: "A \<subseteq> B \<Longrightarrow> A \<union> (B - A) = B"
   by blast
 
 lemma double_diff: "A \<subseteq> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> B - (C - A) = A"
   by blast
 
 lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
   by blast
 
 lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
   by blast
 
 lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
   by blast
 
 lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
   by blast
 
 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
   by blast
 
 lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   by blast
 
 lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
   by blast
 
 lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
   by blast
 
 lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
   by blast
 
 lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
   by auto
 
 lemma Compl_Diff_eq [simp]: "- (A - B) = - A \<union> B"
   by blast
 
 lemma subset_Compl_singleton [simp]: "A \<subseteq> - {b} \<longleftrightarrow> b \<notin> A"
   by blast
 
 text \<open>\<^medskip> Quantification over type \<^typ>\<open>bool\<close>.\<close>
 
 lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   by (cases x) auto
 
 lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"
   by (auto intro: bool_induct)
 
 lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"
   by (cases x) auto
 
 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   by (auto intro: bool_contrapos)
 
 lemma UNIV_bool: "UNIV = {False, True}"
   by (auto intro: bool_induct)
 
 text \<open>\<^medskip> \<open>Pow\<close>\<close>
 
 lemma Pow_empty [simp]: "Pow {} = {{}}"
   by (auto simp add: Pow_def)
 
 lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}"
   by blast  (* somewhat slow *)
 
 lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
   by (blast intro: image_eqI [where ?x = "u - {a}" for u])
 
 lemma Pow_Compl: "Pow (- A) = {- B | B. A \<in> Pow B}"
   by (blast intro: exI [where ?x = "- u" for u])
 
 lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
   by blast
 
 lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
   by blast
 
 lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
   by blast
 
 
 text \<open>\<^medskip> Miscellany.\<close>
 
 lemma set_eq_subset: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   by blast
 
 lemma subset_iff: "A \<subseteq> B \<longleftrightarrow> (\<forall>t. t \<in> A \<longrightarrow> t \<in> B)"
   by blast
 
 lemma subset_iff_psubset_eq: "A \<subseteq> B \<longleftrightarrow> A \<subset> B \<or> A = B"
   unfolding less_le by blast
 
 lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) \<longleftrightarrow> A = {}"
   by blast
 
 lemma ex_in_conv: "(\<exists>x. x \<in> A) \<longleftrightarrow> A \<noteq> {}"
   by blast
 
 lemma ball_simps [simp, no_atp]:
   "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
   "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
   "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
   "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
   "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
   "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
   "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
   "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
   "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
   "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
   by auto
 
 lemma bex_simps [simp, no_atp]:
   "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
   "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
   "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
   "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
   "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<or> (\<exists>x\<in>B. P x))"
   "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
   "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
   by auto
 
 lemma ex_image_cong_iff [simp, no_atp]:
   "(\<exists>x. x\<in>f`A) \<longleftrightarrow> A \<noteq> {}" "(\<exists>x. x\<in>f`A \<and> P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
   by auto
 
 subsubsection \<open>Monotonicity of various operations\<close>
 
 lemma image_mono: "A \<subseteq> B \<Longrightarrow> f ` A \<subseteq> f ` B"
   by blast
 
 lemma Pow_mono: "A \<subseteq> B \<Longrightarrow> Pow A \<subseteq> Pow B"
   by blast
 
 lemma insert_mono: "C \<subseteq> D \<Longrightarrow> insert a C \<subseteq> insert a D"
   by blast
 
 lemma Un_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A \<union> B \<subseteq> C \<union> D"
   by (fact sup_mono)
 
 lemma Int_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A \<inter> B \<subseteq> C \<inter> D"
   by (fact inf_mono)
 
 lemma Diff_mono: "A \<subseteq> C \<Longrightarrow> D \<subseteq> B \<Longrightarrow> A - B \<subseteq> C - D"
   by blast
 
 lemma Compl_anti_mono: "A \<subseteq> B \<Longrightarrow> - B \<subseteq> - A"
   by (fact compl_mono)
 
 text \<open>\<^medskip> Monotonicity of implications.\<close>
 
 lemma in_mono: "A \<subseteq> B \<Longrightarrow> x \<in> A \<longrightarrow> x \<in> B"
   by (rule impI) (erule subsetD)
 
 lemma conj_mono: "P1 \<longrightarrow> Q1 \<Longrightarrow> P2 \<longrightarrow> Q2 \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
   by iprover
 
 lemma disj_mono: "P1 \<longrightarrow> Q1 \<Longrightarrow> P2 \<longrightarrow> Q2 \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
   by iprover
 
 lemma imp_mono: "Q1 \<longrightarrow> P1 \<Longrightarrow> P2 \<longrightarrow> Q2 \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
   by iprover
 
 lemma imp_refl: "P \<longrightarrow> P" ..
 
 lemma not_mono: "Q \<longrightarrow> P \<Longrightarrow> \<not> P \<longrightarrow> \<not> Q"
   by iprover
 
 lemma ex_mono: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (\<exists>x. P x) \<longrightarrow> (\<exists>x. Q x)"
   by iprover
 
 lemma all_mono: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
   by iprover
 
 lemma Collect_mono: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> Collect P \<subseteq> Collect Q"
   by blast
 
 lemma Int_Collect_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P x \<longrightarrow> Q x) \<Longrightarrow> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
   by blast
 
 lemmas basic_monos =
   subset_refl imp_refl disj_mono conj_mono ex_mono Collect_mono in_mono
 
 lemma eq_to_mono: "a = b \<Longrightarrow> c = d \<Longrightarrow> b \<longrightarrow> d \<Longrightarrow> a \<longrightarrow> c"
   by iprover
 
 
 subsubsection \<open>Inverse image of a function\<close>
 
 definition vimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a set"  (infixr "-`" 90)
   where "f -` B \<equiv> {x. f x \<in> B}"
 
 lemma vimage_eq [simp]: "a \<in> f -` B \<longleftrightarrow> f a \<in> B"
   unfolding vimage_def by blast
 
 lemma vimage_singleton_eq: "a \<in> f -` {b} \<longleftrightarrow> f a = b"
   by simp
 
 lemma vimageI [intro]: "f a = b \<Longrightarrow> b \<in> B \<Longrightarrow> a \<in> f -` B"
   unfolding vimage_def by blast
 
 lemma vimageI2: "f a \<in> A \<Longrightarrow> a \<in> f -` A"
   unfolding vimage_def by fast
 
 lemma vimageE [elim!]: "a \<in> f -` B \<Longrightarrow> (\<And>x. f a = x \<Longrightarrow> x \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding vimage_def by blast
 
 lemma vimageD: "a \<in> f -` A \<Longrightarrow> f a \<in> A"
   unfolding vimage_def by fast
 
 lemma vimage_empty [simp]: "f -` {} = {}"
   by blast
 
 lemma vimage_Compl: "f -` (- A) = - (f -` A)"
   by blast
 
 lemma vimage_Un [simp]: "f -` (A \<union> B) = (f -` A) \<union> (f -` B)"
   by blast
 
 lemma vimage_Int [simp]: "f -` (A \<inter> B) = (f -` A) \<inter> (f -` B)"
   by fast
 
 lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
   by blast
 
 lemma vimage_Collect: "(\<And>x. P (f x) = Q x) \<Longrightarrow> f -` (Collect P) = Collect Q"
   by blast
 
 lemma vimage_insert: "f -` (insert a B) = (f -` {a}) \<union> (f -` B)"
   \<comment> \<open>NOT suitable for rewriting because of the recurrence of \<open>{a}\<close>.\<close>
   by blast
 
 lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
   by blast
 
 lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
   by blast
 
 lemma vimage_mono: "A \<subseteq> B \<Longrightarrow> f -` A \<subseteq> f -` B"
   \<comment> \<open>monotonicity\<close>
   by blast
 
 lemma vimage_image_eq: "f -` (f ` A) = {y. \<exists>x\<in>A. f x = f y}"
   by (blast intro: sym)
 
 lemma image_vimage_subset: "f ` (f -` A) \<subseteq> A"
   by blast
 
 lemma image_vimage_eq [simp]: "f ` (f -` A) = A \<inter> range f"
   by blast
 
 lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
   by blast
 
 lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
   by auto
 
 lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
    (if c \<in> A then (if d \<in> A then UNIV else B)
     else if d \<in> A then - B else {})"
   by (auto simp add: vimage_def)
 
 lemma vimage_inter_cong: "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
   by auto
 
 lemma vimage_ident [simp]: "(\<lambda>x. x) -` Y = Y"
   by blast
 
 
 subsubsection \<open>Singleton sets\<close>
 
 definition is_singleton :: "'a set \<Rightarrow> bool"
   where "is_singleton A \<longleftrightarrow> (\<exists>x. A = {x})"
 
 lemma is_singletonI [simp, intro!]: "is_singleton {x}"
   unfolding is_singleton_def by simp
 
 lemma is_singletonI': "A \<noteq> {} \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y) \<Longrightarrow> is_singleton A"
   unfolding is_singleton_def by blast
 
 lemma is_singletonE: "is_singleton A \<Longrightarrow> (\<And>x. A = {x} \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding is_singleton_def by blast
 
 
 subsubsection \<open>Getting the contents of a singleton set\<close>
 
 definition the_elem :: "'a set \<Rightarrow> 'a"
   where "the_elem X = (THE x. X = {x})"
 
 lemma the_elem_eq [simp]: "the_elem {x} = x"
   by (simp add: the_elem_def)
 
 lemma is_singleton_the_elem: "is_singleton A \<longleftrightarrow> A = {the_elem A}"
   by (auto simp: is_singleton_def)
 
 lemma the_elem_image_unique:
   assumes "A \<noteq> {}"
     and *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
   shows "the_elem (f ` A) = f x"
   unfolding the_elem_def
 proof (rule the1_equality)
   from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
   with * have "f x = f y" by simp
   with \<open>y \<in> A\<close> have "f x \<in> f ` A" by blast
   with * show "f ` A = {f x}" by auto
   then show "\<exists>!x. f ` A = {x}" by auto
 qed
 
 
 subsubsection \<open>Least value operator\<close>
 
 lemma Least_mono: "mono f \<Longrightarrow> \<exists>x\<in>S. \<forall>y\<in>S. x \<le> y \<Longrightarrow> (LEAST y. y \<in> f ` S) = f (LEAST x. x \<in> S)"
   for f :: "'a::order \<Rightarrow> 'b::order"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
   apply clarify
   apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
    apply fast
   apply (rule LeastI2_order)
     apply (auto elim: monoD intro!: order_antisym)
   done
 
 
 subsubsection \<open>Monad operation\<close>
 
 definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
   where "bind A f = {x. \<exists>B \<in> f`A. x \<in> B}"
 
 hide_const (open) bind
 
 lemma bind_bind: "Set.bind (Set.bind A B) C = Set.bind A (\<lambda>x. Set.bind (B x) C)"
   for A :: "'a set"
   by (auto simp: bind_def)
 
 lemma empty_bind [simp]: "Set.bind {} f = {}"
   by (simp add: bind_def)
 
 lemma nonempty_bind_const: "A \<noteq> {} \<Longrightarrow> Set.bind A (\<lambda>_. B) = B"
   by (auto simp: bind_def)
 
 lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
   by (auto simp: bind_def)
 
 lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
   by (auto simp: bind_def)
 
 
 subsubsection \<open>Operations for execution\<close>
 
 definition is_empty :: "'a set \<Rightarrow> bool"
   where [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
 
 hide_const (open) is_empty
 
 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where [code_abbrev]: "remove x A = A - {x}"
 
 hide_const (open) remove
 
 lemma member_remove [simp]: "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
   by (simp add: remove_def)
 
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where [code_abbrev]: "filter P A = {a \<in> A. P a}"
 
 hide_const (open) filter
 
 lemma member_filter [simp]: "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"
   by (simp add: filter_def)
 
 instantiation set :: (equal) equal
 begin
 
 definition "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
 
 instance by standard (auto simp add: equal_set_def)
 
 end
 
 
 text \<open>Misc\<close>
 
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
 lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
 by (auto simp add: pairwise_def)
 
 lemma pairwise_trivial [simp]: "pairwise (\<lambda>i j. j \<noteq> i) I"
   by (auto simp: pairwise_def)
 
 lemma pairwiseI [intro?]:
   "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   using that by (simp add: pairwise_def)
 
 lemma pairwiseD:
   "R x y" and "R y x"
   if "pairwise R S" "x \<in> S" and "y \<in> S" and "x \<noteq> y"
   using that by (simp_all add: pairwise_def)
 
 lemma pairwise_empty [simp]: "pairwise P {}"
   by (simp add: pairwise_def)
 
 lemma pairwise_singleton [simp]: "pairwise P {A}"
   by (simp add: pairwise_def)
 
 lemma pairwise_insert:
   "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
   by (force simp: pairwise_def)
 
 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
   by (force simp: pairwise_def)
 
 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y; B \<subseteq> A\<rbrakk> \<Longrightarrow> pairwise Q B"
   by (fastforce simp: pairwise_def)
 
 lemma pairwise_imageI:
   "pairwise P (f ` A)"
   if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)"
   using that by (auto intro: pairwiseI)
 
 lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
   by (force simp: pairwise_def)
 
 definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
 
 lemma disjnt_self_iff_empty [simp]: "disjnt S S \<longleftrightarrow> S = {}"
   by (auto simp: disjnt_def)
 
 lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
   by (force simp: disjnt_def)
 
 lemma disjnt_sym: "disjnt A B \<Longrightarrow> disjnt B A"
   using disjnt_iff by blast
 
 lemma disjnt_empty1 [simp]: "disjnt {} A" and disjnt_empty2 [simp]: "disjnt A {}"
   by (auto simp: disjnt_def)
 
 lemma disjnt_insert1 [simp]: "disjnt (insert a X) Y \<longleftrightarrow> a \<notin> Y \<and> disjnt X Y"
   by (simp add: disjnt_def)
 
 lemma disjnt_insert2 [simp]: "disjnt Y (insert a X) \<longleftrightarrow> a \<notin> Y \<and> disjnt Y X"
   by (simp add: disjnt_def)
 
 lemma disjnt_subset1 : "\<lbrakk>disjnt X Y; Z \<subseteq> X\<rbrakk> \<Longrightarrow> disjnt Z Y"
   by (auto simp: disjnt_def)
 
 lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
   by (auto simp: disjnt_def)
 
 lemma disjnt_Un1 [simp]: "disjnt (A \<union> B) C \<longleftrightarrow> disjnt A C \<and> disjnt B C"
   by (auto simp: disjnt_def)
 
 lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
   by (auto simp: disjnt_def)
 
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast
 
 lemma pairwise_disjnt_iff: "pairwise disjnt \<A> \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1 X. X \<in> \<A> \<and> x \<in> X)"
   by (auto simp: Uniq_def disjnt_iff pairwise_def)
 
 lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
   by blast
 
 lemma in_image_insert_iff:
   assumes "\<And>C. C \<in> B \<Longrightarrow> x \<notin> C"
   shows "A \<in> insert x ` B \<longleftrightarrow> x \<in> A \<and> A - {x} \<in> B" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P then show ?Q
     using assms by auto
 next
   assume ?Q
   then have "x \<in> A" and "A - {x} \<in> B"
     by simp_all
   from \<open>A - {x} \<in> B\<close> have "insert x (A - {x}) \<in> insert x ` B"
     by (rule imageI)
   also from \<open>x \<in> A\<close>
   have "insert x (A - {x}) = A"
     by auto
   finally show ?P .
 qed
 
 hide_const (open) member not_member
 
 lemmas equalityI = subset_antisym
 lemmas set_mp = subsetD
 lemmas set_rev_mp = rev_subsetD
 
 ML \<open>
 val Ball_def = @{thm Ball_def}
 val Bex_def = @{thm Bex_def}
 val CollectD = @{thm CollectD}
 val CollectE = @{thm CollectE}
 val CollectI = @{thm CollectI}
 val Collect_conj_eq = @{thm Collect_conj_eq}
 val Collect_mem_eq = @{thm Collect_mem_eq}
 val IntD1 = @{thm IntD1}
 val IntD2 = @{thm IntD2}
 val IntE = @{thm IntE}
 val IntI = @{thm IntI}
 val Int_Collect = @{thm Int_Collect}
 val UNIV_I = @{thm UNIV_I}
 val UNIV_witness = @{thm UNIV_witness}
 val UnE = @{thm UnE}
 val UnI1 = @{thm UnI1}
 val UnI2 = @{thm UnI2}
 val ballE = @{thm ballE}
 val ballI = @{thm ballI}
 val bexCI = @{thm bexCI}
 val bexE = @{thm bexE}
 val bexI = @{thm bexI}
 val bex_triv = @{thm bex_triv}
 val bspec = @{thm bspec}
 val contra_subsetD = @{thm contra_subsetD}
 val equalityCE = @{thm equalityCE}
 val equalityD1 = @{thm equalityD1}
 val equalityD2 = @{thm equalityD2}
 val equalityE = @{thm equalityE}
 val equalityI = @{thm equalityI}
 val imageE = @{thm imageE}
 val imageI = @{thm imageI}
 val image_Un = @{thm image_Un}
 val image_insert = @{thm image_insert}
 val insert_commute = @{thm insert_commute}
 val insert_iff = @{thm insert_iff}
 val mem_Collect_eq = @{thm mem_Collect_eq}
 val rangeE = @{thm rangeE}
 val rangeI = @{thm rangeI}
 val range_eqI = @{thm range_eqI}
 val subsetCE = @{thm subsetCE}
 val subsetD = @{thm subsetD}
 val subsetI = @{thm subsetI}
 val subset_refl = @{thm subset_refl}
 val subset_trans = @{thm subset_trans}
 val vimageD = @{thm vimageD}
 val vimageE = @{thm vimageE}
 val vimageI = @{thm vimageI}
 val vimageI2 = @{thm vimageI2}
 val vimage_Collect = @{thm vimage_Collect}
 val vimage_Int = @{thm vimage_Int}
 val vimage_Un = @{thm vimage_Un}
 \<close>
 
 end
diff --git a/src/Provers/quantifier1.ML b/src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML
+++ b/src/Provers/quantifier1.ML
@@ -1,285 +1,285 @@
 (*  Title:      Provers/quantifier1.ML
     Author:     Tobias Nipkow
     Copyright   1997  TU Munich
 
 Simplification procedures for turning
 
             ? x. ... & x = t & ...
      into   ? x. x = t & ... & ...
      where the `? x. x = t &' in the latter formula must be eliminated
            by ordinary simplification.
 
      and   ! x. (... & x = t & ...) --> P x
      into  ! x. x = t --> (... & ...) --> P x
      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 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"
 
 The above also works for !x1..xn. and ?x1..xn by moving the defined
 quantifier inside first, but not for nested bounded quantifiers.
 
 For set comprehensions the basic permutations
       ... & x = t & ...  ->  x = t & (... & ...)
       ... & t = x & ...  ->  t = x & (... & ...)
 are also exported.
 
 To avoid looping, NONE is returned if the term cannot be rearranged,
 esp if x=t/t=x sits at the front already.
 *)
 
 signature QUANTIFIER1_DATA =
 sig
   (*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
   val rearrange_All: Proof.context -> cterm -> thm option
-  val rearrange_ex: 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_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_Ex: 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 Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
 struct
 
 (* FIXME: only test! *)
 fun def xs eq =
   (case Data.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);
 
 fun extract_conj fst xs t =
   (case Data.dest_conj t of
     NONE => NONE
   | SOME (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 (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_conj_from_judgment ctxt fst xs t =
   if Object_Logic.is_judgment ctxt t
   then
     let
       val judg $ t' = t
     in
       case extract_conj fst xs t' of
           NONE => NONE
         | SOME (xs, eq, P) => SOME (xs, judg $ eq, judg $ P)
     end
   else NONE;
 
 fun extract_implies ctxt fst xs t =
   (case try Logic.dest_implies t of
     NONE => NONE
   | SOME (P, Q) =>
       if def xs P then (if fst then NONE else SOME (xs, P, Q))
       else
         (case extract_conj_from_judgment ctxt false xs P of
           SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q)
         | NONE =>
             (case extract_implies ctxt false xs Q of
               NONE => NONE
             | SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q')))));
 
 fun extract_quant ctxt 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 ctxt (null xs) xs P
   in exqu [] end;
 
 fun iff_reflection_tac ctxt =
   resolve_tac ctxt [Data.iff_reflection] 1;
 
 fun qcomm_tac ctxt qcomm qI i =
   REPEAT_DETERM (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_one_point_ex_tac ctxt =
+  fun prove_one_point_Ex_tac ctxt =
     qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
     ALLGOALS
       (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
         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 all_comm = Data.all_comm RS Data.iff_trans;
   val All_comm = @{thm swap_params [THEN transitive]};
 in
-  fun prove_one_point_all_tac ctxt =
+  fun prove_one_point_All_tac ctxt =
     EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI,
       resolve_tac ctxt [Data.iff_allI],
       resolve_tac ctxt [Data.iffI],
       tac ctxt,
       tac ctxt];
-  fun prove_one_point_All_tac ctxt =
+  fun prove_one_point_all_tac ctxt =
     EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
       resolve_tac ctxt [@{thm equal_allI}],
       resolve_tac ctxt [@{thm equal_intr_rule}],
       Object_Logic.atomize_prems_tac ctxt,
       tac ctxt,
       Object_Logic.atomize_prems_tac ctxt,
       tac ctxt];
 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'', ...} => tac ctxt'');
   in singleton (Variable.export ctxt' ctxt) thm 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 quant xs (qC $ Abs (x, T, Q)) 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 ctxt (K extract_imp) q P of
+      (case extract_quant ctxt extract_implies 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) (iff_reflection_tac THEN' prove_one_point_all_tac)) end)
+          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
+            in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
   | _ => NONE);
 
 fun rearrange_All ctxt ct =
   (case Thm.term_of ct of
     F as (all as Const (q, _)) $ Abs (x, T, P) =>
-      (case extract_quant ctxt extract_implies q P of
+      (case extract_quant ctxt (K extract_imp) q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
-          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
-            in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end)
+          let val R = quantify all x T xs (Data.imp $ eq $ Q)
+          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_All_tac)) end)
   | _ => NONE);
 
-fun rearrange_ball tac ctxt ct =
+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)) (iff_reflection_tac THEN' tac)) end)
+            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R))
+              (iff_reflection_tac THEN' tac THEN' prove_one_point_All_tac)) end)
   | _ => NONE);
 
-fun rearrange_ex ctxt ct =
+fun rearrange_Ex ctxt ct =
   (case Thm.term_of ct of
     F as (ex as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant ctxt (K 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) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end)
+          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_Ex_tac)) end)
   | _ => NONE);
 
-fun rearrange_bex tac ctxt ct =
+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)) (iff_reflection_tac THEN' tac)))
+          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))
+            (iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_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) (iff_reflection_tac THEN' tac)) end)
   | _ => NONE);
 
 end;
 
diff --git a/src/ZF/OrdQuant.thy b/src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy
+++ b/src/ZF/OrdQuant.thy
@@ -1,366 +1,362 @@
 (*  Title:      ZF/OrdQuant.thy
     Authors:    Krzysztof Grabczewski and L C Paulson
 *)
 
 section \<open>Special quantifiers\<close>
 
 theory OrdQuant imports Ordinal begin
 
 subsection \<open>Quantifiers and union operator for ordinals\<close>
 
 definition
   (* Ordinal Quantifiers *)
   oall :: "[i, i => o] => o"  where
     "oall(A, P) == \<forall>x. x<A \<longrightarrow> P(x)"
 
 definition
   oex :: "[i, i => o] => o"  where
     "oex(A, P)  == \<exists>x. x<A & P(x)"
 
 definition
   (* Ordinal Union *)
   OUnion :: "[i, i => i] => i"  where
     "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
 
 syntax
   "_oall"     :: "[idt, i, o] => o"        (\<open>(3\<forall>_<_./ _)\<close> 10)
   "_oex"      :: "[idt, i, o] => o"        (\<open>(3\<exists>_<_./ _)\<close> 10)
   "_OUNION"   :: "[idt, i, i] => i"        (\<open>(3\<Union>_<_./ _)\<close> 10)
 translations
   "\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
   "\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
   "\<Union>x<a. B" \<rightleftharpoons> "CONST OUnion(a, \<lambda>x. B)"
 
 
 subsubsection \<open>simplification of the new quantifiers\<close>
 
 
 (*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
   is proved.  Ord_atomize would convert this rule to
     x < 0 ==> P(x) == True, which causes dire effects!*)
 lemma [simp]: "(\<forall>x<0. P(x))"
 by (simp add: oall_def)
 
 lemma [simp]: "~(\<exists>x<0. P(x))"
 by (simp add: oex_def)
 
 lemma [simp]: "(\<forall>x<succ(i). P(x)) <-> (Ord(i) \<longrightarrow> P(i) & (\<forall>x<i. P(x)))"
 apply (simp add: oall_def le_iff)
 apply (blast intro: lt_Ord2)
 done
 
 lemma [simp]: "(\<exists>x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (\<exists>x<i. P(x))))"
 apply (simp add: oex_def le_iff)
 apply (blast intro: lt_Ord2)
 done
 
 subsubsection \<open>Union over ordinals\<close>
 
 lemma Ord_OUN [intro,simp]:
      "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"
 by (simp add: OUnion_def ltI Ord_UN)
 
 lemma OUN_upper_lt:
      "[| a<A;  i < b(a);  Ord(\<Union>x<A. b(x)) |] ==> i < (\<Union>x<A. b(x))"
 by (unfold OUnion_def lt_def, blast )
 
 lemma OUN_upper_le:
      "[| a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x)) |] ==> i \<le> (\<Union>x<A. b(x))"
 apply (unfold OUnion_def, auto)
 apply (rule UN_upper_le )
 apply (auto simp add: lt_def)
 done
 
 lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i"
 by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
 
 (* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
 lemma OUN_least:
      "(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C"
 by (simp add: OUnion_def UN_least ltI)
 
 lemma OUN_least_le:
      "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (\<Union>x<A. b(x)) \<le> i"
 by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
 
 lemma le_implies_OUN_le_OUN:
      "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (\<Union>x<A. c(x)) \<le> (\<Union>x<A. d(x))"
 by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)
 
 lemma OUN_UN_eq:
      "(!!x. x \<in> A ==> Ord(B(x)))
       ==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))"
 by (simp add: OUnion_def)
 
 lemma OUN_Union_eq:
      "(!!x. x \<in> X ==> Ord(x))
       ==> (\<Union>z < \<Union>(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
 by (simp add: OUnion_def)
 
 (*So that rule_format will get rid of this quantifier...*)
 lemma atomize_oall [symmetric, rulify]:
      "(!!x. x<A ==> P(x)) == Trueprop (\<forall>x<A. P(x))"
 by (simp add: oall_def atomize_all atomize_imp)
 
 subsubsection \<open>universal quantifier for ordinals\<close>
 
 lemma oallI [intro!]:
     "[| !!x. x<A ==> P(x) |] ==> \<forall>x<A. P(x)"
 by (simp add: oall_def)
 
 lemma ospec: "[| \<forall>x<A. P(x);  x<A |] ==> P(x)"
 by (simp add: oall_def)
 
 lemma oallE:
     "[| \<forall>x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
 by (simp add: oall_def, blast)
 
 lemma rev_oallE [elim]:
     "[| \<forall>x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
 by (simp add: oall_def, blast)
 
 
 (*Trival rewrite rule.  @{term"(\<forall>x<a.P)<->P"} holds only if a is not 0!*)
 lemma oall_simp [simp]: "(\<forall>x<a. True) <-> True"
 by blast
 
 (*Congruence rule for rewriting*)
 lemma oall_cong [cong]:
     "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
      ==> oall(a, %x. P(x)) <-> oall(a', %x. P'(x))"
 by (simp add: oall_def)
 
 
 subsubsection \<open>existential quantifier for ordinals\<close>
 
 lemma oexI [intro]:
     "[| P(x);  x<A |] ==> \<exists>x<A. P(x)"
 apply (simp add: oex_def, blast)
 done
 
 (*Not of the general form for such rules... *)
 lemma oexCI:
    "[| \<forall>x<A. ~P(x) ==> P(a);  a<A |] ==> \<exists>x<A. P(x)"
 apply (simp add: oex_def, blast)
 done
 
 lemma oexE [elim!]:
     "[| \<exists>x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
 apply (simp add: oex_def, blast)
 done
 
 lemma oex_cong [cong]:
     "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
      ==> oex(a, %x. P(x)) <-> oex(a', %x. P'(x))"
 apply (simp add: oex_def cong add: conj_cong)
 done
 
 
 subsubsection \<open>Rules for Ordinal-Indexed Unions\<close>
 
 lemma OUN_I [intro]: "[| a<i;  b \<in> B(a) |] ==> b: (\<Union>z<i. B(z))"
 by (unfold OUnion_def lt_def, blast)
 
 lemma OUN_E [elim!]:
     "[| b \<in> (\<Union>z<i. B(z));  !!a.[| b \<in> B(a);  a<i |] ==> R |] ==> R"
 apply (unfold OUnion_def lt_def, blast)
 done
 
 lemma OUN_iff: "b \<in> (\<Union>x<i. B(x)) <-> (\<exists>x<i. b \<in> B(x))"
 by (unfold OUnion_def oex_def lt_def, blast)
 
 lemma OUN_cong [cong]:
     "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (\<Union>x<i. C(x)) = (\<Union>x<j. D(x))"
 by (simp add: OUnion_def lt_def OUN_iff)
 
 lemma lt_induct:
     "[| i<k;  !!x.[| x<k;  \<forall>y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
 apply (simp add: lt_def oall_def)
 apply (erule conjE)
 apply (erule Ord_induct, assumption, blast)
 done
 
 
 subsection \<open>Quantification over a class\<close>
 
 definition
   "rall"     :: "[i=>o, i=>o] => o"  where
     "rall(M, P) == \<forall>x. M(x) \<longrightarrow> P(x)"
 
 definition
   "rex"      :: "[i=>o, i=>o] => o"  where
     "rex(M, P) == \<exists>x. M(x) & P(x)"
 
 syntax
   "_rall"     :: "[pttrn, i=>o, o] => o"        (\<open>(3\<forall>_[_]./ _)\<close> 10)
   "_rex"      :: "[pttrn, i=>o, o] => o"        (\<open>(3\<exists>_[_]./ _)\<close> 10)
 translations
   "\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
   "\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
 
 
 subsubsection\<open>Relativized universal quantifier\<close>
 
 lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> \<forall>x[M]. P(x)"
 by (simp add: rall_def)
 
 lemma rspec: "[| \<forall>x[M]. P(x); M(x) |] ==> P(x)"
 by (simp add: rall_def)
 
 (*Instantiates x first: better for automatic theorem proving?*)
 lemma rev_rallE [elim]:
     "[| \<forall>x[M]. P(x);  ~ M(x) ==> Q;  P(x) ==> Q |] ==> Q"
 by (simp add: rall_def, blast)
 
 lemma rallE: "[| \<forall>x[M]. P(x);  P(x) ==> Q;  ~ M(x) ==> Q |] ==> Q"
 by blast
 
 (*Trival rewrite rule;   (\<forall>x[M].P)<->P holds only if A is nonempty!*)
 lemma rall_triv [simp]: "(\<forall>x[M]. P) \<longleftrightarrow> ((\<exists>x. M(x)) \<longrightarrow> P)"
 by (simp add: rall_def)
 
 (*Congruence rule for rewriting*)
 lemma rall_cong [cong]:
     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\<forall>x[M]. P(x)) <-> (\<forall>x[M]. P'(x))"
 by (simp add: rall_def)
 
 
 subsubsection\<open>Relativized existential quantifier\<close>
 
 lemma rexI [intro]: "[| P(x); M(x) |] ==> \<exists>x[M]. P(x)"
 by (simp add: rex_def, blast)
 
 (*The best argument order when there is only one M(x)*)
 lemma rev_rexI: "[| M(x);  P(x) |] ==> \<exists>x[M]. P(x)"
 by blast
 
 (*Not of the general form for such rules... *)
 lemma rexCI: "[| \<forall>x[M]. ~P(x) ==> P(a); M(a) |] ==> \<exists>x[M]. P(x)"
 by blast
 
 lemma rexE [elim!]: "[| \<exists>x[M]. P(x);  !!x. [| M(x); P(x) |] ==> Q |] ==> Q"
 by (simp add: rex_def, blast)
 
 (*We do not even have (\<exists>x[M]. True) <-> True unless A is nonempty!!*)
 lemma rex_triv [simp]: "(\<exists>x[M]. P) \<longleftrightarrow> ((\<exists>x. M(x)) \<and> P)"
 by (simp add: rex_def)
 
 lemma rex_cong [cong]:
     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\<exists>x[M]. P(x)) <-> (\<exists>x[M]. P'(x))"
 by (simp add: rex_def cong: conj_cong)
 
 lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
 by blast
 
 lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
 by blast
 
 lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"
 by (simp add: rall_def atomize_all atomize_imp)
 
 declare atomize_rall [symmetric, rulify]
 
 lemma rall_simps1:
      "(\<forall>x[M]. P(x) & Q)   <-> (\<forall>x[M]. P(x)) & ((\<forall>x[M]. False) | Q)"
      "(\<forall>x[M]. P(x) | Q)   <-> ((\<forall>x[M]. P(x)) | Q)"
      "(\<forall>x[M]. P(x) \<longrightarrow> Q) <-> ((\<exists>x[M]. P(x)) \<longrightarrow> Q)"
      "(~(\<forall>x[M]. P(x))) <-> (\<exists>x[M]. ~P(x))"
 by blast+
 
 lemma rall_simps2:
      "(\<forall>x[M]. P & Q(x))   <-> ((\<forall>x[M]. False) | P) & (\<forall>x[M]. Q(x))"
      "(\<forall>x[M]. P | Q(x))   <-> (P | (\<forall>x[M]. Q(x)))"
      "(\<forall>x[M]. P \<longrightarrow> Q(x)) <-> (P \<longrightarrow> (\<forall>x[M]. Q(x)))"
 by blast+
 
 lemmas rall_simps [simp] = rall_simps1 rall_simps2
 
 lemma rall_conj_distrib:
     "(\<forall>x[M]. P(x) & Q(x)) <-> ((\<forall>x[M]. P(x)) & (\<forall>x[M]. Q(x)))"
 by blast
 
 lemma rex_simps1:
      "(\<exists>x[M]. P(x) & Q) <-> ((\<exists>x[M]. P(x)) & Q)"
      "(\<exists>x[M]. P(x) | Q) <-> (\<exists>x[M]. P(x)) | ((\<exists>x[M]. True) & Q)"
      "(\<exists>x[M]. P(x) \<longrightarrow> Q) <-> ((\<forall>x[M]. P(x)) \<longrightarrow> ((\<exists>x[M]. True) & Q))"
      "(~(\<exists>x[M]. P(x))) <-> (\<forall>x[M]. ~P(x))"
 by blast+
 
 lemma rex_simps2:
      "(\<exists>x[M]. P & Q(x)) <-> (P & (\<exists>x[M]. Q(x)))"
      "(\<exists>x[M]. P | Q(x)) <-> ((\<exists>x[M]. True) & P) | (\<exists>x[M]. Q(x))"
      "(\<exists>x[M]. P \<longrightarrow> Q(x)) <-> (((\<forall>x[M]. False) | P) \<longrightarrow> (\<exists>x[M]. Q(x)))"
 by blast+
 
 lemmas rex_simps [simp] = rex_simps1 rex_simps2
 
 lemma rex_disj_distrib:
     "(\<exists>x[M]. P(x) | Q(x)) <-> ((\<exists>x[M]. P(x)) | (\<exists>x[M]. Q(x)))"
 by blast
 
 
 subsubsection\<open>One-point rule for bounded quantifiers\<close>
 
 lemma rex_triv_one_point1 [simp]: "(\<exists>x[M]. x=a) <-> ( M(a))"
 by blast
 
 lemma rex_triv_one_point2 [simp]: "(\<exists>x[M]. a=x) <-> ( M(a))"
 by blast
 
 lemma rex_one_point1 [simp]: "(\<exists>x[M]. x=a & P(x)) <-> ( M(a) & P(a))"
 by blast
 
 lemma rex_one_point2 [simp]: "(\<exists>x[M]. a=x & P(x)) <-> ( M(a) & P(a))"
 by blast
 
 lemma rall_one_point1 [simp]: "(\<forall>x[M]. x=a \<longrightarrow> P(x)) <-> ( M(a) \<longrightarrow> P(a))"
 by blast
 
 lemma rall_one_point2 [simp]: "(\<forall>x[M]. a=x \<longrightarrow> P(x)) <-> ( M(a) \<longrightarrow> P(a))"
 by blast
 
 
 subsubsection\<open>Sets as Classes\<close>
 
 definition
   setclass :: "[i,i] => o"       (\<open>##_\<close> [40] 40)  where
    "setclass(A) == %x. x \<in> A"
 
 lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
 by (simp add: setclass_def)
 
 lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
 by auto
 
 lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
 by auto
 
 
 ML
 \<open>
 val Ord_atomize =
   atomize ([(\<^const_name>\<open>oall\<close>, @{thms ospec}), (\<^const_name>\<open>rall\<close>, @{thms rspec})] @
     ZF_conn_pairs, ZF_mem_pairs);
 \<close>
 declaration \<open>fn _ =>
   Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
     map mk_eq o Ord_atomize o Variable.gen_all ctxt))
 \<close>
 
 text \<open>Setting up the one-point-rule simproc\<close>
 
 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_bex
-    (fn ctxt =>
-      unfold_tac ctxt @{thms rex_def} THEN
-      Quantifier1.prove_one_point_ex_tac ctxt)
+  fn _ => Quantifier1.rearrange_Bex
+    (fn ctxt => unfold_tac ctxt @{thms rex_def})
 \<close>
 
 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_ball
-    (fn ctxt =>
-      unfold_tac ctxt @{thms rall_def} THEN
-      Quantifier1.prove_one_point_all_tac ctxt)
+  fn _ => Quantifier1.rearrange_Ball
+    (fn ctxt => unfold_tac ctxt @{thms rall_def})
 \<close>
 
 end
diff --git a/src/ZF/pair.thy b/src/ZF/pair.thy
--- a/src/ZF/pair.thy
+++ b/src/ZF/pair.thy
@@ -1,189 +1,185 @@
 (*  Title:      ZF/pair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
 
 section\<open>Ordered Pairs\<close>
 
 theory pair imports upair
 begin
 
 ML_file \<open>simpdata.ML\<close>
 
 setup \<open>
   map_theory_simpset
     (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
       #> Simplifier.add_cong @{thm if_weak_cong})
 \<close>
 
 ML \<open>val ZF_ss = simpset_of \<^context>\<close>
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_bex
-    (fn ctxt =>
-      unfold_tac ctxt @{thms Bex_def} THEN
-      Quantifier1.prove_one_point_ex_tac ctxt)
+  fn _ => Quantifier1.rearrange_Bex
+    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
 \<close>
 
 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_ball
-    (fn ctxt =>
-      unfold_tac ctxt @{thms Ball_def} THEN
-      Quantifier1.prove_one_point_all_tac ctxt)
+  fn _ => Quantifier1.rearrange_Ball
+    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
 \<close>
 
 
 (** Lemmas for showing that <a,b> uniquely determines a and b **)
 
 lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
 by (rule extension [THEN iff_trans], blast)
 
 lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
 by (rule extension [THEN iff_trans], blast)
 
 lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
 by (simp add: Pair_def doubleton_eq_iff, blast)
 
 lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
 
 lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
 lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
 
 lemma Pair_not_0: "<a,b> \<noteq> 0"
 apply (unfold Pair_def)
 apply (blast elim: equalityE)
 done
 
 lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
 
 declare sym [THEN Pair_neq_0, elim!]
 
 lemma Pair_neq_fst: "<a,b>=a ==> P"
 proof (unfold Pair_def)
   assume eq: "{{a, a}, {a, b}} = a"
   have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
   hence "{a, a} \<in> a" by (simp add: eq)
   moreover have "a \<in> {a, a}" by (rule consI1)
   ultimately show "P" by (rule mem_asym)
 qed
 
 lemma Pair_neq_snd: "<a,b>=b ==> P"
 proof (unfold Pair_def)
   assume eq: "{{a, a}, {a, b}} = b"
   have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
   hence "{a, b} \<in> b" by (simp add: eq)
   moreover have "b \<in> {a, b}" by blast
   ultimately show "P" by (rule mem_asym)
 qed
 
 
 subsection\<open>Sigma: Disjoint Union of a Family of Sets\<close>
 
 text\<open>Generalizes Cartesian product\<close>
 
 lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)"
 by (simp add: Sigma_def)
 
 lemma SigmaI [TC,intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a,b> \<in> Sigma(A,B)"
 by simp
 
 lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
 lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
 
 (*The general elimination rule*)
 lemma SigmaE [elim!]:
     "[| c \<in> Sigma(A,B);
         !!x y.[| x \<in> A;  y \<in> B(x);  c=<x,y> |] ==> P
      |] ==> P"
 by (unfold Sigma_def, blast)
 
 lemma SigmaE2 [elim!]:
     "[| <a,b> \<in> Sigma(A,B);
         [| a \<in> A;  b \<in> B(a) |] ==> P
      |] ==> P"
 by (unfold Sigma_def, blast)
 
 lemma Sigma_cong:
     "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
      Sigma(A,B) = Sigma(A',B')"
 by (simp add: Sigma_def)
 
 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
   flex-flex pairs and the "Check your prover" error.  Most
   Sigmas and Pis are abbreviated as * or -> *)
 
 lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
 by blast
 
 lemma Sigma_empty2 [simp]: "A*0 = 0"
 by blast
 
 lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
 by blast
 
 
 subsection\<open>Projections \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>\<close>
 
 lemma fst_conv [simp]: "fst(<a,b>) = a"
 by (simp add: fst_def)
 
 lemma snd_conv [simp]: "snd(<a,b>) = b"
 by (simp add: snd_def)
 
 lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A"
 by auto
 
 lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))"
 by auto
 
 lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a"
 by auto
 
 
 subsection\<open>The Eliminator, \<^term>\<open>split\<close>\<close>
 
 (*A META-equality, so that it applies to higher types as well...*)
 lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
 by (simp add: split_def)
 
 lemma split_type [TC]:
     "[|  p \<in> Sigma(A,B);
          !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x,y>)
      |] ==> split(%x y. c(x,y), p) \<in> C(p)"
 by (erule SigmaE, auto)
 
 lemma expand_split:
   "u \<in> A*B ==>
         R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
 by (auto simp add: split_def)
 
 
 subsection\<open>A version of \<^term>\<open>split\<close> for Formulae: Result Type \<^typ>\<open>o\<close>\<close>
 
 lemma splitI: "R(a,b) ==> split(R, <a,b>)"
 by (simp add: split_def)
 
 lemma splitE:
     "[| split(R,z);  z \<in> Sigma(A,B);
         !!x y. [| z = <x,y>;  R(x,y) |] ==> P
      |] ==> P"
 by (auto simp add: split_def)
 
 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
 by (simp add: split_def)
 
 text \<open>
   \bigskip Complex rules for Sigma.
 \<close>
 
 lemma split_paired_Bex_Sigma [simp]:
      "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
 by blast
 
 lemma split_paired_Ball_Sigma [simp]:
      "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
 by blast
 
 end