# HG changeset patch
# User haftmann
# Date 1196449983 -3600
# Node ID 38c15efe603bb98e6a84e08295f7100fc831b4ae
# Parent  e537c91b043d99928c4ae0f00d18960ae378253e
adjustions to due to instance target

diff -r e537c91b043d -r 38c15efe603b NEWS
--- a/NEWS	Fri Nov 30 16:23:52 2007 +0100
+++ b/NEWS	Fri Nov 30 20:13:03 2007 +0100
@@ -16,7 +16,13 @@
 
 * Library/Multiset: {#a, b, c#} is new short syntax for {#a#} + {#b#} + {#c#}.
 
-* Constant "card" now with authentic syntax.
+* Constants "card", "internal_split",  "option_map" now with authentic syntax.
+
+* Definitions subset_def, psubset_def, set_diff_def, Compl_def, le_bool_def,
+less_bool_def, le_fun_def, less_fun_def, inf_bool_def, sup_bool_def,
+Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, Inf_fun_def, Sup_fun_def,
+inf_set_def, sup_set_def, Inf_set_def, Sup_set_def, le_def, less_def,
+option_map_def now with object equality.
 
 
 
diff -r e537c91b043d -r 38c15efe603b src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Inductive.thy	Fri Nov 30 20:13:03 2007 +0100
@@ -290,8 +290,10 @@
 val def_gfp_unfold = @{thm def_gfp_unfold}
 val def_lfp_induct = @{thm def_lfp_induct}
 val def_coinduct = @{thm def_coinduct}
-val inf_bool_eq = @{thm inf_bool_eq}
-val inf_fun_eq = @{thm inf_fun_eq}
+val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
+val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
+val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
+val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
 val le_boolI = @{thm le_boolI}
 val le_boolI' = @{thm le_boolI'}
 val le_funI = @{thm le_funI}
@@ -299,8 +301,8 @@
 val le_funE = @{thm le_funE}
 val le_boolD = @{thm le_boolD}
 val le_funD = @{thm le_funD}
-val le_bool_def = @{thm le_bool_def}
-val le_fun_def = @{thm le_fun_def}
+val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
+val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
 *}
 
 use "Tools/inductive_package.ML"
diff -r e537c91b043d -r 38c15efe603b src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Lattices.thy	Fri Nov 30 20:13:03 2007 +0100
@@ -479,16 +479,34 @@
 
 subsection {* Bool as lattice *}
 
-instance bool :: distrib_lattice
-  inf_bool_eq: "P \<sqinter> Q \<equiv> P \<and> Q"
-  sup_bool_eq: "P \<squnion> Q \<equiv> P \<or> Q"
+instantiation bool :: distrib_lattice
+begin
+
+definition
+  inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
+
+definition
+  sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
+
+instance
   by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
 
-instance bool :: complete_lattice
-  Inf_bool_def: "\<Sqinter>A \<equiv> \<forall>x\<in>A. x"
-  Sup_bool_def: "\<Squnion>A \<equiv> \<exists>x\<in>A. x"
+end
+
+instantiation bool :: complete_lattice
+begin
+
+definition
+  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+
+definition
+  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+
+instance
   by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
 
+end
+
 lemma Inf_empty_bool [simp]:
   "\<Sqinter>{}"
   unfolding Inf_bool_def by auto
@@ -506,12 +524,19 @@
 
 subsection {* Set as lattice *}
 
-instance set :: (type) distrib_lattice
-  inf_set_eq: "A \<sqinter> B \<equiv> A \<inter> B"
-  sup_set_eq: "A \<squnion> B \<equiv> A \<union> B"
+instantiation set :: (type) distrib_lattice
+begin
+
+definition
+  inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B"
+
+definition
+  sup_set_eq [code func del]: "A \<squnion> B = A \<union> B"
+
+instance
   by intro_classes (auto simp add: inf_set_eq sup_set_eq)
 
-lemmas [code func del] = inf_set_eq sup_set_eq
+end
 
 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   apply (fold inf_set_eq sup_set_eq)
@@ -523,12 +548,19 @@
   apply (erule mono_sup)
   done
 
-instance set :: (type) complete_lattice
-  Inf_set_def: "\<Sqinter>S \<equiv> \<Inter>S"
-  Sup_set_def: "\<Squnion>S \<equiv> \<Union>S"
+instantiation set :: (type) complete_lattice
+begin
+
+definition
+  Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S"
+
+definition
+  Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S"
+
+instance
   by intro_classes (auto simp add: Inf_set_def Sup_set_def)
 
-lemmas [code func del] = Inf_set_def Sup_set_def
+end
 
 lemma top_set_eq: "top = UNIV"
   by (iprover intro!: subset_antisym subset_UNIV top_greatest)
@@ -539,9 +571,16 @@
 
 subsection {* Fun as lattice *}
 
-instance "fun" :: (type, lattice) lattice
-  inf_fun_eq: "f \<sqinter> g \<equiv> (\<lambda>x. f x \<sqinter> g x)"
-  sup_fun_eq: "f \<squnion> g \<equiv> (\<lambda>x. f x \<squnion> g x)"
+instantiation "fun" :: (type, lattice) lattice
+begin
+
+definition
+  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+
+definition
+  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+
+instance
 apply intro_classes
 unfolding inf_fun_eq sup_fun_eq
 apply (auto intro: le_funI)
@@ -551,19 +590,26 @@
 apply (auto dest: le_funD)
 done
 
-lemmas [code func del] = inf_fun_eq sup_fun_eq
+end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice
   by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
-instance "fun" :: (type, complete_lattice) complete_lattice
-  Inf_fun_def: "\<Sqinter>A \<equiv> (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
-  Sup_fun_def: "\<Squnion>A \<equiv> (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+instantiation "fun" :: (type, complete_lattice) complete_lattice
+begin
+
+definition
+  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+
+definition
+  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+
+instance
   by intro_classes
     (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
       intro: Inf_lower Sup_upper Inf_greatest Sup_least)
 
-lemmas [code func del] = Inf_fun_def Sup_fun_def
+end
 
 lemma Inf_empty_fun:
   "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
diff -r e537c91b043d -r 38c15efe603b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Nat.thy	Fri Nov 30 20:13:03 2007 +0100
@@ -54,9 +54,15 @@
 
 local
 
-instance nat :: zero
-  Zero_nat_def: "0 == Abs_Nat Zero_Rep" ..
-lemmas [code func del] = Zero_nat_def
+instantiation nat :: zero
+begin
+
+definition Zero_nat_def [code func del]:
+  "0 = Abs_Nat Zero_Rep"
+
+instance ..
+
+end
 
 defs
   Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
@@ -155,11 +161,18 @@
   pred_nat :: "(nat * nat) set" where
   "pred_nat = {(m, n). n = Suc m}"
 
-instance nat :: ord
-  less_def: "m < n == (m, n) : pred_nat^+"
-  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
+instantiation nat :: ord
+begin
+
+definition
+  less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+"
 
-lemmas [code func del] = less_def le_def
+definition
+  le_def [code func del]:   "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m"
+
+instance ..
+
+end
 
 lemma wf_pred_nat: "wf pred_nat"
   apply (unfold wf_def pred_nat_def, clarify)
@@ -1488,8 +1501,8 @@
 text {* the lattice order on @{typ nat} *}
 
 instance nat :: distrib_lattice
-  "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
-  "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
+  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
+  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
   by intro_classes
     (simp_all add: inf_nat_def sup_nat_def)
 
diff -r e537c91b043d -r 38c15efe603b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Orderings.thy	Fri Nov 30 20:13:03 2007 +0100
@@ -928,11 +928,19 @@
 
 subsection {* Order on bool *}
 
-instance bool :: order 
-  le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
-  less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
+instantiation bool :: order 
+begin
+
+definition
+  le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+
+definition
+  less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
+
+instance
   by intro_classes (auto simp add: le_bool_def less_bool_def)
-lemmas [code func del] = le_bool_def less_bool_def
+
+end
 
 lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
 by (simp add: le_bool_def)
@@ -966,11 +974,18 @@
 
 subsection {* Order on functions *}
 
-instance "fun" :: (type, ord) ord
-  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
-  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+instantiation "fun" :: (type, ord) ord
+begin
+
+definition
+  le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
 
-lemmas [code func del] = le_fun_def less_fun_def
+definition
+  less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
+
+instance ..
+
+end
 
 instance "fun" :: (type, order) order
   by default
diff -r e537c91b043d -r 38c15efe603b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Set.thy	Fri Nov 30 20:13:03 2007 +0100
@@ -143,10 +143,18 @@
   union/intersection symbol because this leads to problems with nested
   subscripts in Proof General. *}
 
-instance set :: (type) ord
-  subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
-  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
-lemmas [code func del] = subset_def psubset_def
+instantiation set :: (type) ord
+begin
+
+definition
+  subset_def [code func del]: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
+
+definition
+  psubset_def [code func del]: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B"
+
+instance ..
+
+end
 
 abbreviation
   subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -340,11 +348,18 @@
   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
 
-instance set :: (type) minus
-  Compl_def:    "- A            == {x. ~x:A}"
-  set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
-
-lemmas [code func del] = Compl_def set_diff_def
+instantiation set :: (type) minus
+begin
+
+definition
+  Compl_def [code func del]:    "- A   = {x. ~x:A}"
+
+definition
+  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
+
+instance ..
+
+end
 
 defs
   Un_def:       "A Un B         == {x. x:A | x:B}"
diff -r e537c91b043d -r 38c15efe603b src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 30 20:13:03 2007 +0100
@@ -746,7 +746,7 @@
          singleton (ProofContext.export
            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
            (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic
-             (rewrite_tac [le_fun_def, le_bool_def, @{thm sup_fun_eq}, @{thm sup_bool_eq}] THEN
+             (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
                fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
        else
          prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def