Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy

--- a/src/HOL/Auth/Message.thy	Tue Jul 21 07:55:56 2009 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Jul 21 11:09:50 2009 +0200
@@ -856,6 +856,8 @@
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)

--- a/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 07:55:56 2009 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 11:09:50 2009 +0200
@@ -854,6 +854,8 @@
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)

--- a/src/HOL/Set.thy	Tue Jul 21 07:55:56 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 21 11:09:50 2009 +0200
@@ -80,12 +80,30 @@
 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   by simp
 
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
+
+setup {*
+let
+  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+  val defColl_regroup = Simplifier.simproc @{theory}
+    "defined Collect" ["{x. P x & Q x}"]
+    (Quantifier1.rearrange_Coll Coll_perm_tac)
+in
+  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
+end
+*}
+
 lemmas CollectE = CollectD [elim_format]
 
 text {* Set enumerations *}
 
 definition empty :: "'a set" ("{}") where
-  "empty \<equiv> {x. False}"
+  "empty = {x. False}"
 
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
@@ -311,6 +329,23 @@
   in [("Collect", setcompr_tr')] end;
 *}
 
+setup {*
+let
+  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
+  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
+  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
+  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
+  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
+  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
+  val defBEX_regroup = Simplifier.simproc @{theory}
+    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
+  val defBALL_regroup = Simplifier.simproc @{theory}
+    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
+in
+  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
+end
+*}
+
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
   by (simp add: Ball_def)
 
@@ -319,20 +354,6 @@
 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
   by (simp add: Ball_def)
 
-lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
-  by (unfold Ball_def) blast
-
-ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
-
-text {*
-  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
-  @{prop "a:A"}; creates assumption @{prop "P a"}.
-*}
-
-ML {*
-  fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
-*}
-
 text {*
   Gives better instantiation for bound:
 *}
@@ -341,6 +362,26 @@
   Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
 *}
 
+ML {*
+structure Simpdata =
+struct
+
+open Simpdata;
+
+val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
+
+end;
+
+open Simpdata;
+*}
+
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
+
+lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
+  by (unfold Ball_def) blast
+
 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   -- {* Normally the best argument order: @{prop "P x"} constrains the
     choice of @{prop "x:A"}. *}
@@ -382,24 +423,6 @@
 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   by blast
 
-ML {*
-  local
-    val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
-    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
-
-    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
-    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
-  in
-    val defBEX_regroup = Simplifier.simproc @{theory}
-      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
-    val defBALL_regroup = Simplifier.simproc @{theory}
-      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
-  end;
-
-  Addsimprocs [defBALL_regroup, defBEX_regroup];
-*}
 
 text {* Congruence rules *}
 
@@ -450,25 +473,12 @@
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
 
-ML {*
-  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
-*}
-
 lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   by (unfold mem_def) blast
 
 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
-text {*
-  \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
-  creates the assumption @{prop "c \<in> B"}.
-*}
-
-ML {*
-  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
-*}
-
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
@@ -538,7 +548,7 @@
 subsubsection {* The universal set -- UNIV *}
 
 definition UNIV :: "'a set" where
-  "UNIV \<equiv> {x. True}"
+  "UNIV = {x. True}"
 
 lemma UNIV_I [simp]: "x : UNIV"
   by (simp add: UNIV_def)
@@ -647,7 +657,7 @@
 subsubsection {* Binary union -- Un *}
 
 definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
+  "A Un B = {x. x \<in> A \<or> x \<in> B}"
 
 notation (xsymbols)
   "Un"  (infixl "\<union>" 65)
@@ -678,7 +688,7 @@
 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   by (unfold Un_def) blast
 
-lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
+lemma insert_def: "insert a B = {x. x = a} \<union> B"
   by (simp add: Collect_def mem_def insert_compr Un_def)
 
 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
@@ -690,7 +700,7 @@
 subsubsection {* Binary intersection -- Int *}
 
 definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
-  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
+  "A Int B = {x. x \<in> A \<and> x \<in> B}"
 
 notation (xsymbols)
   "Int"  (infixl "\<inter>" 70)
@@ -883,34 +893,15 @@
   by blast
 
 
-subsubsection {* Some proof tools *}
+subsubsection {* Some rules with @{text "if"} *}
 
 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
 
 lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
-by auto
+  by auto
 
 lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
-by auto
-
-text {*
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
-*}
-
-ML{*
-  local
-    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
-    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
-                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
-  in
-    val defColl_regroup = Simplifier.simproc @{theory}
-      "defined Collect" ["{x. P x & Q x}"]
-      (Quantifier1.rearrange_Coll Coll_perm_tac)
-  end;
-
-  Addsimprocs [defColl_regroup];
-*}
+  by auto
 
 text {*
   Rewrite rules for boolean case-splitting: faster than @{text
@@ -945,13 +936,6 @@
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
 
-ML {*
-  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
-*}
-declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
-*}
-
 
 subsection {* Complete lattices *}
 
@@ -1029,10 +1013,10 @@
   using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "SUPR A f == \<Squnion> (f ` A)"
+  "SUPR A f = \<Squnion> (f ` A)"
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "INFI A f == \<Sqinter> (f ` A)"
+  "INFI A f = \<Sqinter> (f ` A)"
 
 end
 
@@ -1215,12 +1199,12 @@
   by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
 
 lemma Union_def:
-  "\<Union>S \<equiv> \<Union>x\<in>S. x"
+  "\<Union>S = (\<Union>x\<in>S. x)"
   by (simp add: UNION_eq_Union_image image_def)
 
 lemma UNION_def [noatp]:
-  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
-  by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq)
+  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
+  by (auto simp add: UNION_eq_Union_image Union_eq)
   
 lemma Union_image_eq [simp]:
   "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
@@ -1325,12 +1309,12 @@
   by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
 
 lemma Inter_def:
-  "Inter S \<equiv> INTER S (\<lambda>x. x)"
+  "Inter S = INTER S (\<lambda>x. x)"
   by (simp add: INTER_eq_Inter_image image_def)
 
 lemma INTER_def:
-  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
-  by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq)
+  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
+  by (auto simp add: INTER_eq_Inter_image Inter_eq)
 
 lemma Inter_image_eq [simp]:
   "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
@@ -2476,23 +2460,24 @@
 
 text {* Rudimentary code generation *}
 
-lemma empty_code [code]: "{} x \<longleftrightarrow> False"
-  unfolding empty_def Collect_def ..
-
-lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
-  unfolding UNIV_def Collect_def ..
+lemma [code]: "{} = bot"
+  by (rule sym) (fact bot_set_eq)
+
+lemma [code]: "UNIV = top"
+  by (rule sym) (fact top_set_eq)
+
+lemma [code]: "op \<inter> = inf"
+  by (rule ext)+ (simp add: inf_set_eq)
+
+lemma [code]: "op \<union> = sup"
+  by (rule ext)+ (simp add: sup_set_eq)
 
 lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
-  unfolding insert_def Collect_def mem_def Un_def by auto
-
-lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
-  unfolding Int_def Collect_def mem_def ..
-
-lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
-  unfolding Un_def Collect_def mem_def ..
+  by (auto simp add: insert_compr Collect_def mem_def)
 
 lemma vimage_code [code]: "(f -` A) x = A (f x)"
-  unfolding vimage_def Collect_def mem_def ..
+  by (simp add: vimage_def Collect_def mem_def)
+
 
 text {* Misc theorem and ML bindings *}