# HG changeset patch # User haftmann # Date 1248167390 -7200 # Node ID 0762b9ad83df00c46c702b79e0660307ae60088f # Parent 045e7ca3ea74c7d36a028a0c45e2077d6ccdb2fd Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy diff -r 045e7ca3ea74 -r 0762b9ad83df src/HOL/Auth/Message.thy --- 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 \ parts(insert X H) and Y \ analz(insert X H) *) diff -r 045e7ca3ea74 -r 0762b9ad83df src/HOL/SET-Protocol/MessageSET.thy --- 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 \ parts(insert X H) and Y \ analz(insert X H) *) diff -r 045e7ca3ea74 -r 0762b9ad83df src/HOL/Set.thy --- 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. \ & x=t & \}"} +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 \ {x. False}" + "empty = {x. False}" definition insert :: "'a \ 'a set \ 'a set" where insert_compr: "insert a B = {x. x = a \ x \ 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 \ B"} to @{prop "x \ A ==> x \ B"}. *} -ML {* - fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) -*} - lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" -- {* Classical elimination rule. *} by (unfold mem_def) blast lemma subset_eq: "A \ B = (\x\A. x \ B)" by blast -text {* - \medskip Takes assumptions @{prop "A \ B"}; @{prop "c \ A"} and - creates the assumption @{prop "c \ B"}. -*} - -ML {* - fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i -*} - lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" by blast @@ -538,7 +548,7 @@ subsubsection {* The universal set -- UNIV *} definition UNIV :: "'a set" where - "UNIV \ {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 \ 'a set \ 'a set" (infixl "Un" 65) where - "A Un B \ {x. x \ A \ x \ B}" + "A Un B = {x. x \ A \ x \ B}" notation (xsymbols) "Un" (infixl "\" 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 \ {x. x = a} \ B" +lemma insert_def: "insert a B = {x. x = a} \ B" by (simp add: Collect_def mem_def insert_compr Un_def) lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)" @@ -690,7 +700,7 @@ subsubsection {* Binary intersection -- Int *} definition Int :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where - "A Int B \ {x. x \ A \ x \ B}" + "A Int B = {x. x \ A \ x \ B}" notation (xsymbols) "Int" (infixl "\" 70) @@ -883,34 +893,15 @@ by blast -subsubsection {* Some proof tools *} +subsubsection {* Some rules with @{text "if"} *} text{* Elimination of @{text"{x. \ & x=t & \}"}. *} 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. \ & x=t & \}"} -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 \ ('b \ 'a) \ 'a" where - "SUPR A f == \ (f ` A)" + "SUPR A f = \ (f ` A)" definition INFI :: "'b set \ ('b \ 'a) \ 'a" where - "INFI A f == \ (f ` A)" + "INFI A f = \ (f ` A)" end @@ -1215,12 +1199,12 @@ by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq) lemma Union_def: - "\S \ \x\S. x" + "\S = (\x\S. x)" by (simp add: UNION_eq_Union_image image_def) lemma UNION_def [noatp]: - "UNION A B \ {y. \x\A. y \ B x}" - by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq) + "UNION A B = {y. \x\A. y \ B x}" + by (auto simp add: UNION_eq_Union_image Union_eq) lemma Union_image_eq [simp]: "\(B`A) = (\x\A. B x)" @@ -1325,12 +1309,12 @@ by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq) lemma Inter_def: - "Inter S \ INTER S (\x. x)" + "Inter S = INTER S (\x. x)" by (simp add: INTER_eq_Inter_image image_def) lemma INTER_def: - "INTER A B \ {y. \x\A. y \ B x}" - by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq) + "INTER A B = {y. \x\A. y \ B x}" + by (auto simp add: INTER_eq_Inter_image Inter_eq) lemma Inter_image_eq [simp]: "\(B`A) = (\x\A. B x)" @@ -2476,23 +2460,24 @@ text {* Rudimentary code generation *} -lemma empty_code [code]: "{} x \ False" - unfolding empty_def Collect_def .. - -lemma UNIV_code [code]: "UNIV x \ 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 \ = inf" + by (rule ext)+ (simp add: inf_set_eq) + +lemma [code]: "op \ = sup" + by (rule ext)+ (simp add: sup_set_eq) lemma insert_code [code]: "insert y A x \ y = x \ A x" - unfolding insert_def Collect_def mem_def Un_def by auto - -lemma inter_code [code]: "(A \ B) x \ A x \ B x" - unfolding Int_def Collect_def mem_def .. - -lemma union_code [code]: "(A \ B) x \ A x \ 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 *}