primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
authorhaftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 410754bed56dc95fb
parent 41074 286255f131bf
child 41076 a7fba340058c
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
src/HOL/Lattices.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/List.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Tools/inductive.ML
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 08 13:34:50 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 08 13:34:50 2010 +0100
     1.3 @@ -593,28 +593,28 @@
     1.4    bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
     1.5  
     1.6  definition
     1.7 -  inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
     1.8 +  inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
     1.9  
    1.10  definition
    1.11 -  sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    1.12 +  sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    1.13  
    1.14  instance proof
    1.15 -qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def
    1.16 -  bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto)
    1.17 +qed (simp_all add: inf_bool_def sup_bool_def le_bool_def
    1.18 +  bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto)
    1.19  
    1.20  end
    1.21  
    1.22  lemma sup_boolI1:
    1.23    "P \<Longrightarrow> P \<squnion> Q"
    1.24 -  by (simp add: sup_bool_eq)
    1.25 +  by (simp add: sup_bool_def)
    1.26  
    1.27  lemma sup_boolI2:
    1.28    "Q \<Longrightarrow> P \<squnion> Q"
    1.29 -  by (simp add: sup_bool_eq)
    1.30 +  by (simp add: sup_bool_def)
    1.31  
    1.32  lemma sup_boolE:
    1.33    "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.34 -  by (auto simp add: sup_bool_eq)
    1.35 +  by (auto simp add: sup_bool_def)
    1.36  
    1.37  
    1.38  subsection {* Fun as lattice *}
    1.39 @@ -623,19 +623,19 @@
    1.40  begin
    1.41  
    1.42  definition
    1.43 -  inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.44 +  inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.45  
    1.46  definition
    1.47 -  sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.48 +  sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.49  
    1.50  instance proof
    1.51 -qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
    1.52 +qed (simp_all add: le_fun_def inf_fun_def sup_fun_def)
    1.53  
    1.54  end
    1.55  
    1.56  instance "fun" :: (type, distrib_lattice) distrib_lattice
    1.57  proof
    1.58 -qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
    1.59 +qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1)
    1.60  
    1.61  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
    1.62  
    1.63 @@ -661,7 +661,7 @@
    1.64  
    1.65  instance "fun" :: (type, boolean_algebra) boolean_algebra
    1.66  proof
    1.67 -qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def
    1.68 +qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def
    1.69    inf_compl_bot sup_compl_top diff_eq)
    1.70  
    1.71  
     2.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Dec 08 13:34:50 2010 +0100
     2.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Dec 08 13:34:50 2010 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  declare HOL.if_bool_eq_disj[code_pred_inline]
     2.5  
     2.6  declare bool_diff_def[code_pred_inline]
     2.7 -declare inf_bool_eq_raw[code_pred_inline]
     2.8 +declare inf_bool_def_raw[code_pred_inline]
     2.9  declare less_bool_def_raw[code_pred_inline]
    2.10  declare le_bool_def_raw[code_pred_inline]
    2.11  
     3.1 --- a/src/HOL/List.thy	Wed Dec 08 13:34:50 2010 +0100
     3.2 +++ b/src/HOL/List.thy	Wed Dec 08 13:34:50 2010 +0100
     3.3 @@ -4217,7 +4217,7 @@
     3.4    show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
     3.5  qed
     3.6  
     3.7 -lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
     3.8 +lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
     3.9  
    3.10  lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
    3.11  
     4.1 --- a/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
     4.3 @@ -1214,13 +1214,13 @@
     4.4    less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
     4.5  
     4.6  definition
     4.7 -  top_bool_eq: "top = True"
     4.8 +  top_bool_def: "top = True"
     4.9  
    4.10  definition
    4.11 -  bot_bool_eq: "bot = False"
    4.12 +  bot_bool_def: "bot = False"
    4.13  
    4.14  instance proof
    4.15 -qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def)
    4.16 +qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
    4.17  
    4.18  end
    4.19  
    4.20 @@ -1237,10 +1237,10 @@
    4.21    by (simp add: le_bool_def)
    4.22  
    4.23  lemma bot_boolE: "bot \<Longrightarrow> P"
    4.24 -  by (simp add: bot_bool_eq)
    4.25 +  by (simp add: bot_bool_def)
    4.26  
    4.27  lemma top_boolI: top
    4.28 -  by (simp add: top_bool_eq)
    4.29 +  by (simp add: top_bool_def)
    4.30  
    4.31  lemma [code]:
    4.32    "False \<le> b \<longleftrightarrow> True"
    4.33 @@ -1276,11 +1276,11 @@
    4.34  begin
    4.35  
    4.36  definition
    4.37 -  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
    4.38 -declare top_fun_eq_raw [no_atp]
    4.39 +  top_fun_def [no_atp]: "top = (\<lambda>x. top)"
    4.40 +declare top_fun_def_raw [no_atp]
    4.41  
    4.42  instance proof
    4.43 -qed (simp add: top_fun_eq le_fun_def)
    4.44 +qed (simp add: top_fun_def le_fun_def)
    4.45  
    4.46  end
    4.47  
    4.48 @@ -1288,10 +1288,10 @@
    4.49  begin
    4.50  
    4.51  definition
    4.52 -  bot_fun_eq: "bot = (\<lambda>x. bot)"
    4.53 +  bot_fun_def: "bot = (\<lambda>x. bot)"
    4.54  
    4.55  instance proof
    4.56 -qed (simp add: bot_fun_eq le_fun_def)
    4.57 +qed (simp add: bot_fun_def le_fun_def)
    4.58  
    4.59  end
    4.60  
     5.1 --- a/src/HOL/Predicate.thy	Wed Dec 08 13:34:50 2010 +0100
     5.2 +++ b/src/HOL/Predicate.thy	Wed Dec 08 13:34:50 2010 +0100
     5.3 @@ -87,16 +87,16 @@
     5.4  subsubsection {* Top and bottom elements *}
     5.5  
     5.6  lemma top1I [intro!]: "top x"
     5.7 -  by (simp add: top_fun_eq top_bool_eq)
     5.8 +  by (simp add: top_fun_def top_bool_def)
     5.9  
    5.10  lemma top2I [intro!]: "top x y"
    5.11 -  by (simp add: top_fun_eq top_bool_eq)
    5.12 +  by (simp add: top_fun_def top_bool_def)
    5.13  
    5.14  lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
    5.15 -  by (simp add: bot_fun_eq bot_bool_eq)
    5.16 +  by (simp add: bot_fun_def bot_bool_def)
    5.17  
    5.18  lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    5.19 -  by (simp add: bot_fun_eq bot_bool_eq)
    5.20 +  by (simp add: bot_fun_def bot_bool_def)
    5.21  
    5.22  lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
    5.23    by (auto simp add: fun_eq_iff)
    5.24 @@ -108,22 +108,22 @@
    5.25  subsubsection {* Binary union *}
    5.26  
    5.27  lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
    5.28 -  by (simp add: sup_fun_eq sup_bool_eq)
    5.29 +  by (simp add: sup_fun_def sup_bool_def)
    5.30  
    5.31  lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
    5.32 -  by (simp add: sup_fun_eq sup_bool_eq)
    5.33 +  by (simp add: sup_fun_def sup_bool_def)
    5.34  
    5.35  lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
    5.36 -  by (simp add: sup_fun_eq sup_bool_eq)
    5.37 +  by (simp add: sup_fun_def sup_bool_def)
    5.38  
    5.39  lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
    5.40 -  by (simp add: sup_fun_eq sup_bool_eq)
    5.41 +  by (simp add: sup_fun_def sup_bool_def)
    5.42  
    5.43  lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    5.44 -  by (simp add: sup_fun_eq sup_bool_eq) iprover
    5.45 +  by (simp add: sup_fun_def sup_bool_def) iprover
    5.46  
    5.47  lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    5.48 -  by (simp add: sup_fun_eq sup_bool_eq) iprover
    5.49 +  by (simp add: sup_fun_def sup_bool_def) iprover
    5.50  
    5.51  text {*
    5.52    \medskip Classical introduction rule: no commitment to @{text A} vs
    5.53 @@ -131,49 +131,49 @@
    5.54  *}
    5.55  
    5.56  lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
    5.57 -  by (auto simp add: sup_fun_eq sup_bool_eq)
    5.58 +  by (auto simp add: sup_fun_def sup_bool_def)
    5.59  
    5.60  lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
    5.61 -  by (auto simp add: sup_fun_eq sup_bool_eq)
    5.62 +  by (auto simp add: sup_fun_def sup_bool_def)
    5.63  
    5.64  lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    5.65 -  by (simp add: sup_fun_eq sup_bool_eq mem_def)
    5.66 +  by (simp add: sup_fun_def sup_bool_def mem_def)
    5.67  
    5.68  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)"
    5.69 -  by (simp add: sup_fun_eq sup_bool_eq mem_def)
    5.70 +  by (simp add: sup_fun_def sup_bool_def mem_def)
    5.71  
    5.72  
    5.73  subsubsection {* Binary intersection *}
    5.74  
    5.75  lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
    5.76 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.77 +  by (simp add: inf_fun_def inf_bool_def)
    5.78  
    5.79  lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
    5.80 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.81 +  by (simp add: inf_fun_def inf_bool_def)
    5.82  
    5.83  lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
    5.84 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.85 +  by (simp add: inf_fun_def inf_bool_def)
    5.86  
    5.87  lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
    5.88 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.89 +  by (simp add: inf_fun_def inf_bool_def)
    5.90  
    5.91  lemma inf1D1: "inf A B x ==> A x"
    5.92 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.93 +  by (simp add: inf_fun_def inf_bool_def)
    5.94  
    5.95  lemma inf2D1: "inf A B x y ==> A x y"
    5.96 -  by (simp add: inf_fun_eq inf_bool_eq)
    5.97 +  by (simp add: inf_fun_def inf_bool_def)
    5.98  
    5.99  lemma inf1D2: "inf A B x ==> B x"
   5.100 -  by (simp add: inf_fun_eq inf_bool_eq)
   5.101 +  by (simp add: inf_fun_def inf_bool_def)
   5.102  
   5.103  lemma inf2D2: "inf A B x y ==> B x y"
   5.104 -  by (simp add: inf_fun_eq inf_bool_eq)
   5.105 +  by (simp add: inf_fun_def inf_bool_def)
   5.106  
   5.107  lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   5.108 -  by (simp add: inf_fun_eq inf_bool_eq mem_def)
   5.109 +  by (simp add: inf_fun_def inf_bool_def mem_def)
   5.110  
   5.111  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)"
   5.112 -  by (simp add: inf_fun_eq inf_bool_eq mem_def)
   5.113 +  by (simp add: inf_fun_def inf_bool_def mem_def)
   5.114  
   5.115  
   5.116  subsubsection {* Unions of families *}
   5.117 @@ -286,11 +286,11 @@
   5.118      elim: pred_compE dest: conversepD)
   5.119  
   5.120  lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
   5.121 -  by (simp add: inf_fun_eq inf_bool_eq)
   5.122 +  by (simp add: inf_fun_def inf_bool_def)
   5.123      (iprover intro: conversepI ext dest: conversepD)
   5.124  
   5.125  lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
   5.126 -  by (simp add: sup_fun_eq sup_bool_eq)
   5.127 +  by (simp add: sup_fun_def sup_bool_def)
   5.128      (iprover intro: conversepI ext dest: conversepD)
   5.129  
   5.130  lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
     6.1 --- a/src/HOL/Tools/inductive.ML	Wed Dec 08 13:34:50 2010 +0100
     6.2 +++ b/src/HOL/Tools/inductive.ML	Wed Dec 08 13:34:50 2010 +0100
     6.3 @@ -110,10 +110,10 @@
     6.4        "(P & True) = P" "(True & P) = P"
     6.5      by (fact simp_thms)+};
     6.6  
     6.7 -val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
     6.8 +val simp_thms'' = map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms';
     6.9  
    6.10  val simp_thms''' = map mk_meta_eq
    6.11 -  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
    6.12 +  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
    6.13  
    6.14  
    6.15  (** context data **)
     7.1 --- a/src/HOL/Wellfounded.thy	Wed Dec 08 13:34:50 2010 +0100
     7.2 +++ b/src/HOL/Wellfounded.thy	Wed Dec 08 13:34:50 2010 +0100
     7.3 @@ -190,7 +190,7 @@
     7.4    "wfP (\<lambda>x y. False)"
     7.5  proof -
     7.6    have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
     7.7 -  then show ?thesis by (simp add: bot_fun_eq bot_bool_eq)
     7.8 +  then show ?thesis by (simp add: bot_fun_def bot_bool_def)
     7.9  qed
    7.10  
    7.11  lemma wf_Int1: "wf r ==> wf (r Int r')"