--- 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.
--- 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"
--- 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>{})"
--- 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)
--- 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
--- 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}"
--- 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