# HG changeset patch # User haftmann # Date 1291811690 -3600 # Node ID 4bed56dc95fb4cc88e4c47401911d38399a03483 # Parent 286255f131bf725fce4739bb66e8c144c291c208 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq` diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Lattices.thy Wed Dec 08 13:34:50 2010 +0100 @@ -593,28 +593,28 @@ bool_diff_def: "A - B \ A \ \ B" definition - inf_bool_eq: "P \ Q \ P \ Q" + inf_bool_def: "P \ Q \ P \ Q" definition - sup_bool_eq: "P \ Q \ P \ Q" + sup_bool_def: "P \ Q \ P \ Q" instance proof -qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def - bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) +qed (simp_all add: inf_bool_def sup_bool_def le_bool_def + bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto) end lemma sup_boolI1: "P \ P \ Q" - by (simp add: sup_bool_eq) + by (simp add: sup_bool_def) lemma sup_boolI2: "Q \ P \ Q" - by (simp add: sup_bool_eq) + by (simp add: sup_bool_def) lemma sup_boolE: "P \ Q \ (P \ R) \ (Q \ R) \ R" - by (auto simp add: sup_bool_eq) + by (auto simp add: sup_bool_def) subsection {* Fun as lattice *} @@ -623,19 +623,19 @@ begin definition - inf_fun_eq: "f \ g = (\x. f x \ g x)" + inf_fun_def: "f \ g = (\x. f x \ g x)" definition - sup_fun_eq: "f \ g = (\x. f x \ g x)" + sup_fun_def: "f \ g = (\x. f x \ g x)" instance proof -qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq) +qed (simp_all add: le_fun_def inf_fun_def sup_fun_def) end instance "fun" :: (type, distrib_lattice) distrib_lattice proof -qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1) +qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1) instance "fun" :: (type, bounded_lattice) bounded_lattice .. @@ -661,7 +661,7 @@ instance "fun" :: (type, boolean_algebra) boolean_algebra proof -qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def +qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def inf_compl_bot sup_compl_top diff_eq) diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Dec 08 13:34:50 2010 +0100 @@ -7,7 +7,7 @@ declare HOL.if_bool_eq_disj[code_pred_inline] declare bool_diff_def[code_pred_inline] -declare inf_bool_eq_raw[code_pred_inline] +declare inf_bool_def_raw[code_pred_inline] declare less_bool_def_raw[code_pred_inline] declare le_bool_def_raw[code_pred_inline] diff -r 286255f131bf -r 4bed56dc95fb src/HOL/List.thy --- a/src/HOL/List.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/List.thy Wed Dec 08 13:34:50 2010 +0100 @@ -4217,7 +4217,7 @@ show "inf (listsp A) (listsp B) \ listsp (inf A B)" by (blast intro!: listsp_infI predicate1I) qed -lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq] +lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def] lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq] diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Orderings.thy Wed Dec 08 13:34:50 2010 +0100 @@ -1214,13 +1214,13 @@ less_bool_def: "(P\bool) < Q \ \ P \ Q" definition - top_bool_eq: "top = True" + top_bool_def: "top = True" definition - bot_bool_eq: "bot = False" + bot_bool_def: "bot = False" instance proof -qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def) +qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def) end @@ -1237,10 +1237,10 @@ by (simp add: le_bool_def) lemma bot_boolE: "bot \ P" - by (simp add: bot_bool_eq) + by (simp add: bot_bool_def) lemma top_boolI: top - by (simp add: top_bool_eq) + by (simp add: top_bool_def) lemma [code]: "False \ b \ True" @@ -1276,11 +1276,11 @@ begin definition - top_fun_eq [no_atp]: "top = (\x. top)" -declare top_fun_eq_raw [no_atp] + top_fun_def [no_atp]: "top = (\x. top)" +declare top_fun_def_raw [no_atp] instance proof -qed (simp add: top_fun_eq le_fun_def) +qed (simp add: top_fun_def le_fun_def) end @@ -1288,10 +1288,10 @@ begin definition - bot_fun_eq: "bot = (\x. bot)" + bot_fun_def: "bot = (\x. bot)" instance proof -qed (simp add: bot_fun_eq le_fun_def) +qed (simp add: bot_fun_def le_fun_def) end diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Predicate.thy Wed Dec 08 13:34:50 2010 +0100 @@ -87,16 +87,16 @@ subsubsection {* Top and bottom elements *} lemma top1I [intro!]: "top x" - by (simp add: top_fun_eq top_bool_eq) + by (simp add: top_fun_def top_bool_def) lemma top2I [intro!]: "top x y" - by (simp add: top_fun_eq top_bool_eq) + by (simp add: top_fun_def top_bool_def) lemma bot1E [no_atp, elim!]: "bot x \ P" - by (simp add: bot_fun_eq bot_bool_eq) + by (simp add: bot_fun_def bot_bool_def) lemma bot2E [elim!]: "bot x y \ P" - by (simp add: bot_fun_eq bot_bool_eq) + by (simp add: bot_fun_def bot_bool_def) lemma bot_empty_eq: "bot = (\x. x \ {})" by (auto simp add: fun_eq_iff) @@ -108,22 +108,22 @@ subsubsection {* Binary union *} lemma sup1I1 [elim?]: "A x \ sup A B x" - by (simp add: sup_fun_eq sup_bool_eq) + by (simp add: sup_fun_def sup_bool_def) lemma sup2I1 [elim?]: "A x y \ sup A B x y" - by (simp add: sup_fun_eq sup_bool_eq) + by (simp add: sup_fun_def sup_bool_def) lemma sup1I2 [elim?]: "B x \ sup A B x" - by (simp add: sup_fun_eq sup_bool_eq) + by (simp add: sup_fun_def sup_bool_def) lemma sup2I2 [elim?]: "B x y \ sup A B x y" - by (simp add: sup_fun_eq sup_bool_eq) + by (simp add: sup_fun_def sup_bool_def) lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" - by (simp add: sup_fun_eq sup_bool_eq) iprover + by (simp add: sup_fun_def sup_bool_def) iprover lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" - by (simp add: sup_fun_eq sup_bool_eq) iprover + by (simp add: sup_fun_def sup_bool_def) iprover text {* \medskip Classical introduction rule: no commitment to @{text A} vs @@ -131,49 +131,49 @@ *} lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x" - by (auto simp add: sup_fun_eq sup_bool_eq) + by (auto simp add: sup_fun_def sup_bool_def) lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y" - by (auto simp add: sup_fun_eq sup_bool_eq) + by (auto simp add: sup_fun_def sup_bool_def) lemma sup_Un_eq: "sup (\x. x \ R) (\x. x \ S) = (\x. x \ R \ S)" - by (simp add: sup_fun_eq sup_bool_eq mem_def) + by (simp add: sup_fun_def sup_bool_def mem_def) lemma sup_Un_eq2 [pred_set_conv]: "sup (\x y. (x, y) \ R) (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" - by (simp add: sup_fun_eq sup_bool_eq mem_def) + by (simp add: sup_fun_def sup_bool_def mem_def) subsubsection {* Binary intersection *} lemma inf1I [intro!]: "A x ==> B x ==> inf A B x" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf1D1: "inf A B x ==> A x" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf2D1: "inf A B x y ==> A x y" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf1D2: "inf A B x ==> B x" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf2D2: "inf A B x y ==> B x y" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) lemma inf_Int_eq: "inf (\x. x \ R) (\x. x \ S) = (\x. x \ R \ S)" - by (simp add: inf_fun_eq inf_bool_eq mem_def) + by (simp add: inf_fun_def inf_bool_def mem_def) lemma inf_Int_eq2 [pred_set_conv]: "inf (\x y. (x, y) \ R) (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" - by (simp add: inf_fun_eq inf_bool_eq mem_def) + by (simp add: inf_fun_def inf_bool_def mem_def) subsubsection {* Unions of families *} @@ -286,11 +286,11 @@ elim: pred_compE dest: conversepD) lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1" - by (simp add: inf_fun_eq inf_bool_eq) + by (simp add: inf_fun_def inf_bool_def) (iprover intro: conversepI ext dest: conversepD) lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1" - by (simp add: sup_fun_eq sup_bool_eq) + by (simp add: sup_fun_def sup_bool_def) (iprover intro: conversepI ext dest: conversepD) lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~=" diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Dec 08 13:34:50 2010 +0100 @@ -110,10 +110,10 @@ "(P & True) = P" "(True & P) = P" by (fact simp_thms)+}; -val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms'; +val simp_thms'' = map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms'; val simp_thms''' = map mk_meta_eq - [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}]; + [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; (** context data **) diff -r 286255f131bf -r 4bed56dc95fb src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Dec 08 13:34:50 2010 +0100 +++ b/src/HOL/Wellfounded.thy Wed Dec 08 13:34:50 2010 +0100 @@ -190,7 +190,7 @@ "wfP (\x y. False)" proof - have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2]) - then show ?thesis by (simp add: bot_fun_eq bot_bool_eq) + then show ?thesis by (simp add: bot_fun_def bot_bool_def) qed lemma wf_Int1: "wf r ==> wf (r Int r')"