# 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 \<longleftrightarrow> A \<and> \<not> B"
 
 definition
-  inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
+  inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
 
 definition
-  sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
+  sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> 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 \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
+  by (simp add: sup_bool_def)
 
 lemma sup_boolI2:
   "Q \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
+  by (simp add: sup_bool_def)
 
 lemma sup_boolE:
   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> 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 \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+  inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
 definition
-  sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+  sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> 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) \<le> 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\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> 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 \<Longrightarrow> 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 \<le> b \<longleftrightarrow> True"
@@ -1276,11 +1276,11 @@
 begin
 
 definition
-  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
-declare top_fun_eq_raw [no_atp]
+  top_fun_def [no_atp]: "top = (\<lambda>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 = (\<lambda>x. bot)"
+  bot_fun_def: "bot = (\<lambda>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 \<Longrightarrow> 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 \<Longrightarrow> P"
-  by (simp add: bot_fun_eq bot_bool_eq)
+  by (simp add: bot_fun_def bot_bool_def)
 
 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
@@ -108,22 +108,22 @@
 subsubsection {* Binary union *}
 
 lemma sup1I1 [elim?]: "A x \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> 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 (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> 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 (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> 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 (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> 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 (\<lambda>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')"