Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
authorhaftmann
Tue Jul 21 11:09:50 2009 +0200 (2009-07-21)
changeset 321170762b9ad83df
parent 32116 045e7ca3ea74
child 32118 1c9a3fc45141
child 32119 a853099fd9ca
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
src/HOL/Auth/Message.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Tue Jul 21 07:55:56 2009 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Jul 21 11:09:50 2009 +0200
     1.3 @@ -856,6 +856,8 @@
     1.4    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
     1.5    DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
     1.6  
     1.7 +fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
     1.8 +
     1.9  (*Apply rules to break down assumptions of the form
    1.10    Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
    1.11  *)
     2.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 07:55:56 2009 +0200
     2.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 11:09:50 2009 +0200
     2.3 @@ -854,6 +854,8 @@
     2.4    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
     2.5    DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
     2.6  
     2.7 +fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
     2.8 +
     2.9  (*Apply rules to break down assumptions of the form
    2.10    Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
    2.11  *)
     3.1 --- a/src/HOL/Set.thy	Tue Jul 21 07:55:56 2009 +0200
     3.2 +++ b/src/HOL/Set.thy	Tue Jul 21 11:09:50 2009 +0200
     3.3 @@ -80,12 +80,30 @@
     3.4  lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
     3.5    by simp
     3.6  
     3.7 +text {*
     3.8 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
     3.9 +to the front (and similarly for @{text "t=x"}):
    3.10 +*}
    3.11 +
    3.12 +setup {*
    3.13 +let
    3.14 +  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    3.15 +    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    3.16 +                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    3.17 +  val defColl_regroup = Simplifier.simproc @{theory}
    3.18 +    "defined Collect" ["{x. P x & Q x}"]
    3.19 +    (Quantifier1.rearrange_Coll Coll_perm_tac)
    3.20 +in
    3.21 +  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
    3.22 +end
    3.23 +*}
    3.24 +
    3.25  lemmas CollectE = CollectD [elim_format]
    3.26  
    3.27  text {* Set enumerations *}
    3.28  
    3.29  definition empty :: "'a set" ("{}") where
    3.30 -  "empty \<equiv> {x. False}"
    3.31 +  "empty = {x. False}"
    3.32  
    3.33  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    3.34    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    3.35 @@ -311,6 +329,23 @@
    3.36    in [("Collect", setcompr_tr')] end;
    3.37  *}
    3.38  
    3.39 +setup {*
    3.40 +let
    3.41 +  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    3.42 +  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    3.43 +  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    3.44 +  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    3.45 +  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    3.46 +  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    3.47 +  val defBEX_regroup = Simplifier.simproc @{theory}
    3.48 +    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    3.49 +  val defBALL_regroup = Simplifier.simproc @{theory}
    3.50 +    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    3.51 +in
    3.52 +  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
    3.53 +end
    3.54 +*}
    3.55 +
    3.56  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
    3.57    by (simp add: Ball_def)
    3.58  
    3.59 @@ -319,20 +354,6 @@
    3.60  lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
    3.61    by (simp add: Ball_def)
    3.62  
    3.63 -lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    3.64 -  by (unfold Ball_def) blast
    3.65 -
    3.66 -ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
    3.67 -
    3.68 -text {*
    3.69 -  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
    3.70 -  @{prop "a:A"}; creates assumption @{prop "P a"}.
    3.71 -*}
    3.72 -
    3.73 -ML {*
    3.74 -  fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
    3.75 -*}
    3.76 -
    3.77  text {*
    3.78    Gives better instantiation for bound:
    3.79  *}
    3.80 @@ -341,6 +362,26 @@
    3.81    Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
    3.82  *}
    3.83  
    3.84 +ML {*
    3.85 +structure Simpdata =
    3.86 +struct
    3.87 +
    3.88 +open Simpdata;
    3.89 +
    3.90 +val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
    3.91 +
    3.92 +end;
    3.93 +
    3.94 +open Simpdata;
    3.95 +*}
    3.96 +
    3.97 +declaration {* fn _ =>
    3.98 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
    3.99 +*}
   3.100 +
   3.101 +lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
   3.102 +  by (unfold Ball_def) blast
   3.103 +
   3.104  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   3.105    -- {* Normally the best argument order: @{prop "P x"} constrains the
   3.106      choice of @{prop "x:A"}. *}
   3.107 @@ -382,24 +423,6 @@
   3.108  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   3.109    by blast
   3.110  
   3.111 -ML {*
   3.112 -  local
   3.113 -    val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
   3.114 -    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   3.115 -    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   3.116 -
   3.117 -    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
   3.118 -    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   3.119 -    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   3.120 -  in
   3.121 -    val defBEX_regroup = Simplifier.simproc @{theory}
   3.122 -      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
   3.123 -    val defBALL_regroup = Simplifier.simproc @{theory}
   3.124 -      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   3.125 -  end;
   3.126 -
   3.127 -  Addsimprocs [defBALL_regroup, defBEX_regroup];
   3.128 -*}
   3.129  
   3.130  text {* Congruence rules *}
   3.131  
   3.132 @@ -450,25 +473,12 @@
   3.133    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
   3.134  *}
   3.135  
   3.136 -ML {*
   3.137 -  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
   3.138 -*}
   3.139 -
   3.140  lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   3.141    -- {* Classical elimination rule. *}
   3.142    by (unfold mem_def) blast
   3.143  
   3.144  lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   3.145  
   3.146 -text {*
   3.147 -  \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
   3.148 -  creates the assumption @{prop "c \<in> B"}.
   3.149 -*}
   3.150 -
   3.151 -ML {*
   3.152 -  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
   3.153 -*}
   3.154 -
   3.155  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   3.156    by blast
   3.157  
   3.158 @@ -538,7 +548,7 @@
   3.159  subsubsection {* The universal set -- UNIV *}
   3.160  
   3.161  definition UNIV :: "'a set" where
   3.162 -  "UNIV \<equiv> {x. True}"
   3.163 +  "UNIV = {x. True}"
   3.164  
   3.165  lemma UNIV_I [simp]: "x : UNIV"
   3.166    by (simp add: UNIV_def)
   3.167 @@ -647,7 +657,7 @@
   3.168  subsubsection {* Binary union -- Un *}
   3.169  
   3.170  definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   3.171 -  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
   3.172 +  "A Un B = {x. x \<in> A \<or> x \<in> B}"
   3.173  
   3.174  notation (xsymbols)
   3.175    "Un"  (infixl "\<union>" 65)
   3.176 @@ -678,7 +688,7 @@
   3.177  lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   3.178    by (unfold Un_def) blast
   3.179  
   3.180 -lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
   3.181 +lemma insert_def: "insert a B = {x. x = a} \<union> B"
   3.182    by (simp add: Collect_def mem_def insert_compr Un_def)
   3.183  
   3.184  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   3.185 @@ -690,7 +700,7 @@
   3.186  subsubsection {* Binary intersection -- Int *}
   3.187  
   3.188  definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   3.189 -  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
   3.190 +  "A Int B = {x. x \<in> A \<and> x \<in> B}"
   3.191  
   3.192  notation (xsymbols)
   3.193    "Int"  (infixl "\<inter>" 70)
   3.194 @@ -883,34 +893,15 @@
   3.195    by blast
   3.196  
   3.197  
   3.198 -subsubsection {* Some proof tools *}
   3.199 +subsubsection {* Some rules with @{text "if"} *}
   3.200  
   3.201  text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
   3.202  
   3.203  lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
   3.204 -by auto
   3.205 +  by auto
   3.206  
   3.207  lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
   3.208 -by auto
   3.209 -
   3.210 -text {*
   3.211 -Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
   3.212 -to the front (and similarly for @{text "t=x"}):
   3.213 -*}
   3.214 -
   3.215 -ML{*
   3.216 -  local
   3.217 -    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
   3.218 -    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
   3.219 -                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
   3.220 -  in
   3.221 -    val defColl_regroup = Simplifier.simproc @{theory}
   3.222 -      "defined Collect" ["{x. P x & Q x}"]
   3.223 -      (Quantifier1.rearrange_Coll Coll_perm_tac)
   3.224 -  end;
   3.225 -
   3.226 -  Addsimprocs [defColl_regroup];
   3.227 -*}
   3.228 +  by auto
   3.229  
   3.230  text {*
   3.231    Rewrite rules for boolean case-splitting: faster than @{text
   3.232 @@ -945,13 +936,6 @@
   3.233     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   3.234   *)
   3.235  
   3.236 -ML {*
   3.237 -  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
   3.238 -*}
   3.239 -declaration {* fn _ =>
   3.240 -  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
   3.241 -*}
   3.242 -
   3.243  
   3.244  subsection {* Complete lattices *}
   3.245  
   3.246 @@ -1029,10 +1013,10 @@
   3.247    using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
   3.248  
   3.249  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   3.250 -  "SUPR A f == \<Squnion> (f ` A)"
   3.251 +  "SUPR A f = \<Squnion> (f ` A)"
   3.252  
   3.253  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   3.254 -  "INFI A f == \<Sqinter> (f ` A)"
   3.255 +  "INFI A f = \<Sqinter> (f ` A)"
   3.256  
   3.257  end
   3.258  
   3.259 @@ -1215,12 +1199,12 @@
   3.260    by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
   3.261  
   3.262  lemma Union_def:
   3.263 -  "\<Union>S \<equiv> \<Union>x\<in>S. x"
   3.264 +  "\<Union>S = (\<Union>x\<in>S. x)"
   3.265    by (simp add: UNION_eq_Union_image image_def)
   3.266  
   3.267  lemma UNION_def [noatp]:
   3.268 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
   3.269 -  by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq)
   3.270 +  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
   3.271 +  by (auto simp add: UNION_eq_Union_image Union_eq)
   3.272    
   3.273  lemma Union_image_eq [simp]:
   3.274    "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   3.275 @@ -1325,12 +1309,12 @@
   3.276    by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
   3.277  
   3.278  lemma Inter_def:
   3.279 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
   3.280 +  "Inter S = INTER S (\<lambda>x. x)"
   3.281    by (simp add: INTER_eq_Inter_image image_def)
   3.282  
   3.283  lemma INTER_def:
   3.284 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
   3.285 -  by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq)
   3.286 +  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
   3.287 +  by (auto simp add: INTER_eq_Inter_image Inter_eq)
   3.288  
   3.289  lemma Inter_image_eq [simp]:
   3.290    "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   3.291 @@ -2476,23 +2460,24 @@
   3.292  
   3.293  text {* Rudimentary code generation *}
   3.294  
   3.295 -lemma empty_code [code]: "{} x \<longleftrightarrow> False"
   3.296 -  unfolding empty_def Collect_def ..
   3.297 -
   3.298 -lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
   3.299 -  unfolding UNIV_def Collect_def ..
   3.300 +lemma [code]: "{} = bot"
   3.301 +  by (rule sym) (fact bot_set_eq)
   3.302 +
   3.303 +lemma [code]: "UNIV = top"
   3.304 +  by (rule sym) (fact top_set_eq)
   3.305 +
   3.306 +lemma [code]: "op \<inter> = inf"
   3.307 +  by (rule ext)+ (simp add: inf_set_eq)
   3.308 +
   3.309 +lemma [code]: "op \<union> = sup"
   3.310 +  by (rule ext)+ (simp add: sup_set_eq)
   3.311  
   3.312  lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   3.313 -  unfolding insert_def Collect_def mem_def Un_def by auto
   3.314 -
   3.315 -lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
   3.316 -  unfolding Int_def Collect_def mem_def ..
   3.317 -
   3.318 -lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
   3.319 -  unfolding Un_def Collect_def mem_def ..
   3.320 +  by (auto simp add: insert_compr Collect_def mem_def)
   3.321  
   3.322  lemma vimage_code [code]: "(f -` A) x = A (f x)"
   3.323 -  unfolding vimage_def Collect_def mem_def ..
   3.324 +  by (simp add: vimage_def Collect_def mem_def)
   3.325 +
   3.326  
   3.327  text {* Misc theorem and ML bindings *}
   3.328