--- a/NEWS Fri Aug 20 17:04:15 2010 +0200
+++ b/NEWS Fri Aug 20 20:29:50 2010 +0200
@@ -35,6 +35,10 @@
*** HOL ***
+* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
+canonical names for instance definitions for functions; various improvements.
+INCOMPATIBILITY.
+
* Records: logical foundation type for records do not carry a '_type' suffix
any longer. INCOMPATIBILITY.
--- a/src/HOL/Fun.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Fun.thy Fri Aug 20 20:29:50 2010 +0200
@@ -162,6 +162,13 @@
lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
by (force simp add: inj_on_def)
+lemma inj_comp:
+ "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
+ by (simp add: inj_on_def)
+
+lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
+ by (simp add: inj_on_def expand_fun_eq)
+
lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
by (simp add: inj_on_eq_iff)
--- a/src/HOL/IsaMakefile Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Aug 20 20:29:50 2010 +0200
@@ -408,6 +408,7 @@
Library/Executable_Set.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \
+ Library/Function_Algebras.thy \
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
Library/Indicator_Function.thy Library/Infinite_Set.thy \
Library/Inner_Product.thy Library/Kleene_Algebra.thy \
@@ -428,8 +429,8 @@
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
Library/RBT.thy Library/RBT_Impl.thy Library/README.html \
- Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
- Library/SML_Quickcheck.thy Library/SetsAndFunctions.thy \
+ Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
+ Library/Reflection.thy Library/SML_Quickcheck.thy \
Library/Sublist_Order.thy Library/Sum_Of_Squares.thy \
Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML \
--- a/src/HOL/Library/BigO.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Library/BigO.thy Fri Aug 20 20:29:50 2010 +0200
@@ -5,7 +5,7 @@
header {* Big O notation *}
theory BigO
-imports Complex_Main SetsAndFunctions
+imports Complex_Main Function_Algebras Set_Algebras
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Function_Algebras.thy Fri Aug 20 20:29:50 2010 +0200
@@ -0,0 +1,207 @@
+(* Title: HOL/Library/Function_Algebras.thy
+ Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Pointwise instantiation of functions to algebra type classes *}
+
+theory Function_Algebras
+imports Main
+begin
+
+text {* Pointwise operations *}
+
+instantiation "fun" :: (type, plus) plus
+begin
+
+definition
+ "f + g = (\<lambda>x. f x + g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, zero) zero
+begin
+
+definition
+ "0 = (\<lambda>x. 0)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, times) times
+begin
+
+definition
+ "f * g = (\<lambda>x. f x * g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, one) one
+begin
+
+definition
+ "1 = (\<lambda>x. 1)"
+
+instance ..
+
+end
+
+
+text {* Additive structures *}
+
+instance "fun" :: (type, semigroup_add) semigroup_add proof
+qed (simp add: plus_fun_def add.assoc)
+
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
+qed (simp_all add: plus_fun_def expand_fun_eq)
+
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
+qed (simp add: plus_fun_def add.commute)
+
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
+qed simp
+
+instance "fun" :: (type, monoid_add) monoid_add proof
+qed (simp_all add: plus_fun_def zero_fun_def)
+
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
+qed simp
+
+instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
+instance "fun" :: (type, group_add) group_add proof
+qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+
+instance "fun" :: (type, ab_group_add) ab_group_add proof
+qed (simp_all add: diff_minus)
+
+
+text {* Multiplicative structures *}
+
+instance "fun" :: (type, semigroup_mult) semigroup_mult proof
+qed (simp add: times_fun_def mult.assoc)
+
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
+qed (simp add: times_fun_def mult.commute)
+
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
+qed (simp add: times_fun_def)
+
+instance "fun" :: (type, monoid_mult) monoid_mult proof
+qed (simp_all add: times_fun_def one_fun_def)
+
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
+qed simp
+
+
+text {* Misc *}
+
+instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
+
+instance "fun" :: (type, mult_zero) mult_zero proof
+qed (simp_all add: zero_fun_def times_fun_def)
+
+instance "fun" :: (type, mult_mono) mult_mono proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+
+instance "fun" :: (type, mult_mono1) mult_mono1 proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
+
+instance "fun" :: (type, zero_neq_one) zero_neq_one proof
+qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
+
+
+text {* Ring structures *}
+
+instance "fun" :: (type, semiring) semiring proof
+qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, comm_semiring) comm_semiring proof
+qed (simp add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, semiring_0) semiring_0 ..
+
+instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
+
+instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
+
+instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
+
+instance "fun" :: (type, semiring_1) semiring_1 ..
+
+lemma of_nat_fun:
+ shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+proof -
+ have comp: "comp = (\<lambda>f g x. f (g x))"
+ by (rule ext)+ simp
+ have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
+ by (rule ext, rule ext) (fact plus_fun_def)
+ have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
+ by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
+ also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
+ by (simp only: comp_funpow)
+ finally show ?thesis by (simp add: of_nat_def comp)
+qed
+
+instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
+
+instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
+
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
+
+instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+ from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
+ by (rule inj_fun)
+ then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
+ by (simp add: of_nat_fun)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
+qed
+
+instance "fun" :: (type, ring) ring ..
+
+instance "fun" :: (type, comm_ring) comm_ring ..
+
+instance "fun" :: (type, ring_1) ring_1 ..
+
+instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
+
+instance "fun" :: (type, ring_char_0) ring_char_0 ..
+
+
+text {* Ordereded structures *}
+
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
+qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+
+instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
+
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
+qed (simp add: plus_fun_def le_fun_def)
+
+instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
+
+instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
+
+instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+
+instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
+
+instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
+
+instance "fun" :: (type, ordered_ring) ordered_ring ..
+
+instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
+
+
+lemmas func_plus = plus_fun_def
+lemmas func_zero = zero_fun_def
+lemmas func_times = times_fun_def
+lemmas func_one = one_fun_def
+
+end
--- a/src/HOL/Library/Library.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Library/Library.thy Fri Aug 20 20:29:50 2010 +0200
@@ -22,6 +22,7 @@
FrechetDeriv
Fset
FuncSet
+ Function_Algebras
Fundamental_Theorem_Algebra
Indicator_Function
Infinite_Set
@@ -54,6 +55,7 @@
Ramsey
Reflection
RBT
+ Set_Algebras
SML_Quickcheck
State_Monad
Sum_Of_Squares
--- a/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 20:29:50 2010 +0200
@@ -227,8 +227,10 @@
apply (simp add: plus_1_iSuc iSuc_Fin)
done
-instance inat :: semiring_char_0
- by default (simp add: of_nat_eq_Fin)
+instance inat :: semiring_char_0 proof
+ have "inj Fin" by (rule injI) simp
+ then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
+qed
subsection {* Ordering *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Set_Algebras.thy Fri Aug 20 20:29:50 2010 +0200
@@ -0,0 +1,357 @@
+(* Title: HOL/Library/Set_Algebras.thy
+ Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Algebraic operations on sets *}
+
+theory Set_Algebras
+imports Main
+begin
+
+text {*
+ This library lifts operations like addition and muliplication to
+ sets. It was designed to support asymptotic calculations. See the
+ comments at the top of theory @{text BigO}.
+*}
+
+definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<oplus>" 65) where
+ "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
+
+definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 70) where
+ "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
+
+definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "+o" 70) where
+ "a +o B = {c. \<exists>b\<in>B. c = a + b}"
+
+definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "*o" 80) where
+ "a *o B = {c. \<exists>b\<in>B. c = a * b}"
+
+abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infix "=o" 50) where
+ "x =o A \<equiv> x \<in> A"
+
+interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.assoc)
+
+interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.commute)
+
+interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp_all add: set_plus_def)
+
+interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp add: set_plus_def)
+
+definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
+ "listsum_set = monoid_add.listsum set_plus {0}"
+
+interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+ "monoid_add.listsum set_plus {0::'a} = listsum_set"
+proof -
+ show "class.monoid_add set_plus {0::'a}" proof
+ qed (simp_all add: set_add.assoc)
+ then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+ show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ by (simp only: listsum_set_def)
+qed
+
+definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+ "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
+
+interpretation set_add!:
+ comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set
+proof
+qed (fact setsum_set_def)
+
+interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+ "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+proof -
+ show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
+ qed (simp_all add: set_add.commute)
+ then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+ show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ by (simp only: listsum_set_def)
+ show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+ by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
+qed
+
+interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.assoc)
+
+interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.commute)
+
+interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp_all add: set_times_def)
+
+interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp add: set_times_def)
+
+definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
+ "power_set n A = power.power {1} set_times A n"
+
+interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+proof -
+ show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
+ qed (simp_all add: set_mult.assoc)
+ show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ by (simp add: power_set_def)
+qed
+
+definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+ "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
+
+interpretation set_mult!:
+ comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set
+proof
+qed (fact setprod_set_def)
+
+interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
+ "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+proof -
+ show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
+ qed (simp_all add: set_mult.commute)
+ then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
+ show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ by (simp add: power_set_def)
+ show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+ by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
+qed
+
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
+ by (auto simp add: set_plus_def)
+
+lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
+ (b +o D) = (a + b) +o (C \<oplus> D)"
+ apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (rule_tac x = "ba + bb" in exI)
+ apply (auto simp add: add_ac)
+ apply (rule_tac x = "aa + a" in exI)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
+ (a + b) +o C"
+ by (auto simp add: elt_set_plus_def add_assoc)
+
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
+ a +o (B \<oplus> C)"
+ apply (auto simp add: elt_set_plus_def set_plus_def)
+ apply (blast intro: add_ac)
+ apply (rule_tac x = "a + aa" in exI)
+ apply (rule conjI)
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
+ apply (rule_tac x = "ba" in bexI)
+ apply (auto simp add: add_ac)
+ done
+
+theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
+ a +o (C \<oplus> D)"
+ apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (rule_tac x = "aa + ba" in exI)
+ apply (auto simp add: add_ac)
+ done
+
+theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
+ set_plus_rearrange3 set_plus_rearrange4
+
+lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
+ C \<oplus> E <= D \<oplus> F"
+ by (auto simp add: set_plus_def)
+
+lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
+ by (auto simp add: elt_set_plus_def set_plus_def)
+
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
+ a +o D <= D \<oplus> C"
+ by (auto simp add: elt_set_plus_def set_plus_def add_ac)
+
+lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
+ apply (subgoal_tac "a +o B <= a +o D")
+ apply (erule order_trans)
+ apply (erule set_plus_mono3)
+ apply (erule set_plus_mono)
+ done
+
+lemma set_plus_mono_b: "C <= D ==> x : a +o C
+ ==> x : a +o D"
+ apply (frule set_plus_mono)
+ apply auto
+ done
+
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
+ x : D \<oplus> F"
+ apply (frule set_plus_mono2)
+ prefer 2
+ apply force
+ apply assumption
+ done
+
+lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
+ apply (frule set_plus_mono3)
+ apply auto
+ done
+
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
+ x : a +o D ==> x : D \<oplus> C"
+ apply (frule set_plus_mono4)
+ apply auto
+ done
+
+lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
+ apply (auto intro!: subsetI simp add: set_plus_def)
+ apply (rule_tac x = 0 in bexI)
+ apply (rule_tac x = x in bexI)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
+ by (auto simp add: elt_set_plus_def add_ac diff_minus)
+
+lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
+ apply (auto simp add: elt_set_plus_def add_ac diff_minus)
+ apply (subgoal_tac "a = (a + - b) + b")
+ apply (rule bexI, assumption, assumption)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
+ by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
+ assumption)
+
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
+ by (auto simp add: set_times_def)
+
+lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
+ (b *o D) = (a * b) *o (C \<otimes> D)"
+ apply (auto simp add: elt_set_times_def set_times_def)
+ apply (rule_tac x = "ba * bb" in exI)
+ apply (auto simp add: mult_ac)
+ apply (rule_tac x = "aa * a" in exI)
+ apply (auto simp add: mult_ac)
+ done
+
+lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
+ (a * b) *o C"
+ by (auto simp add: elt_set_times_def mult_assoc)
+
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
+ a *o (B \<otimes> C)"
+ apply (auto simp add: elt_set_times_def set_times_def)
+ apply (blast intro: mult_ac)
+ apply (rule_tac x = "a * aa" in exI)
+ apply (rule conjI)
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
+ apply (rule_tac x = "ba" in bexI)
+ apply (auto simp add: mult_ac)
+ done
+
+theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
+ a *o (C \<otimes> D)"
+ apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
+ mult_ac)
+ apply (rule_tac x = "aa * ba" in exI)
+ apply (auto simp add: mult_ac)
+ done
+
+theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
+ set_times_rearrange3 set_times_rearrange4
+
+lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
+ C \<otimes> E <= D \<otimes> F"
+ by (auto simp add: set_times_def)
+
+lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
+ by (auto simp add: elt_set_times_def set_times_def)
+
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
+ a *o D <= D \<otimes> C"
+ by (auto simp add: elt_set_times_def set_times_def mult_ac)
+
+lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
+ apply (subgoal_tac "a *o B <= a *o D")
+ apply (erule order_trans)
+ apply (erule set_times_mono3)
+ apply (erule set_times_mono)
+ done
+
+lemma set_times_mono_b: "C <= D ==> x : a *o C
+ ==> x : a *o D"
+ apply (frule set_times_mono)
+ apply auto
+ done
+
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
+ x : D \<otimes> F"
+ apply (frule set_times_mono2)
+ prefer 2
+ apply force
+ apply assumption
+ done
+
+lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
+ apply (frule set_times_mono3)
+ apply auto
+ done
+
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
+ x : a *o D ==> x : D \<otimes> C"
+ apply (frule set_times_mono4)
+ apply auto
+ done
+
+lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
+ (a * b) +o (a *o C)"
+ by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
+
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
+ (a *o B) \<oplus> (a *o C)"
+ apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
+ apply blast
+ apply (rule_tac x = "b + bb" in exI)
+ apply (auto simp add: ring_distribs)
+ done
+
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
+ a *o D \<oplus> C \<otimes> D"
+ apply (auto intro!: subsetI simp add:
+ elt_set_plus_def elt_set_times_def set_times_def
+ set_plus_def ring_distribs)
+ apply auto
+ done
+
+theorems set_times_plus_distribs =
+ set_times_plus_distrib
+ set_times_plus_distrib2
+
+lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
+ - a : C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
+ - a : (- 1) *o C"
+ by (auto simp add: elt_set_times_def)
+
+end
--- a/src/HOL/Library/SetsAndFunctions.thy Fri Aug 20 17:04:15 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,373 +0,0 @@
-(* Title: HOL/Library/SetsAndFunctions.thy
- Author: Jeremy Avigad and Kevin Donnelly
-*)
-
-header {* Operations on sets and functions *}
-
-theory SetsAndFunctions
-imports Main
-begin
-
-text {*
-This library lifts operations like addition and muliplication to sets and
-functions of appropriate types. It was designed to support asymptotic
-calculations. See the comments at the top of theory @{text BigO}.
-*}
-
-subsection {* Basic definitions *}
-
-definition
- set_plus :: "('a::plus) set => 'a set => 'a set" (infixl "\<oplus>" 65) where
- "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
-
-instantiation "fun" :: (type, plus) plus
-begin
-
-definition
- func_plus: "f + g == (%x. f x + g x)"
-
-instance ..
-
-end
-
-definition
- set_times :: "('a::times) set => 'a set => 'a set" (infixl "\<otimes>" 70) where
- "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
-
-instantiation "fun" :: (type, times) times
-begin
-
-definition
- func_times: "f * g == (%x. f x * g x)"
-
-instance ..
-
-end
-
-
-instantiation "fun" :: (type, zero) zero
-begin
-
-definition
- func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, one) one
-begin
-
-definition
- func_one: "1::(('a::type) => ('b::one)) == %x. 1"
-
-instance ..
-
-end
-
-definition
- elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70) where
- "a +o B = {c. EX b:B. c = a + b}"
-
-definition
- elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80) where
- "a *o B = {c. EX b:B. c = a * b}"
-
-abbreviation (input)
- elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) where
- "x =o A == x : A"
-
-instance "fun" :: (type,semigroup_add)semigroup_add
- by default (auto simp add: func_plus add_assoc)
-
-instance "fun" :: (type,comm_monoid_add)comm_monoid_add
- by default (auto simp add: func_zero func_plus add_ac)
-
-instance "fun" :: (type,ab_group_add)ab_group_add
- apply default
- apply (simp add: fun_Compl_def func_plus func_zero)
- apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
- done
-
-instance "fun" :: (type,semigroup_mult)semigroup_mult
- apply default
- apply (auto simp add: func_times mult_assoc)
- done
-
-instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
- apply default
- apply (auto simp add: func_one func_times mult_ac)
- done
-
-instance "fun" :: (type,comm_ring_1)comm_ring_1
- apply default
- apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def
- func_one func_zero algebra_simps)
- apply (drule fun_cong)
- apply simp
- done
-
-interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
- apply default
- apply (unfold set_plus_def)
- apply (force simp add: add_assoc)
- done
-
-interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
- apply default
- apply (unfold set_times_def)
- apply (force simp add: mult_assoc)
- done
-
-interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
- apply default
- apply (unfold set_plus_def)
- apply (force simp add: add_ac)
- apply force
- done
-
-interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
- apply default
- apply (unfold set_times_def)
- apply (force simp add: mult_ac)
- apply force
- done
-
-
-subsection {* Basic properties *}
-
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
- by (auto simp add: set_plus_def)
-
-lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
- (b +o D) = (a + b) +o (C \<oplus> D)"
- apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
- apply (rule_tac x = "ba + bb" in exI)
- apply (auto simp add: add_ac)
- apply (rule_tac x = "aa + a" in exI)
- apply (auto simp add: add_ac)
- done
-
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
- (a + b) +o C"
- by (auto simp add: elt_set_plus_def add_assoc)
-
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
- a +o (B \<oplus> C)"
- apply (auto simp add: elt_set_plus_def set_plus_def)
- apply (blast intro: add_ac)
- apply (rule_tac x = "a + aa" in exI)
- apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
- apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: add_ac)
- done
-
-theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
- a +o (C \<oplus> D)"
- apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
- apply (rule_tac x = "aa + ba" in exI)
- apply (auto simp add: add_ac)
- done
-
-theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
- set_plus_rearrange3 set_plus_rearrange4
-
-lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
- C \<oplus> E <= D \<oplus> F"
- by (auto simp add: set_plus_def)
-
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
- by (auto simp add: elt_set_plus_def set_plus_def)
-
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
- a +o D <= D \<oplus> C"
- by (auto simp add: elt_set_plus_def set_plus_def add_ac)
-
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
- apply (subgoal_tac "a +o B <= a +o D")
- apply (erule order_trans)
- apply (erule set_plus_mono3)
- apply (erule set_plus_mono)
- done
-
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
- ==> x : a +o D"
- apply (frule set_plus_mono)
- apply auto
- done
-
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
- x : D \<oplus> F"
- apply (frule set_plus_mono2)
- prefer 2
- apply force
- apply assumption
- done
-
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
- apply (frule set_plus_mono3)
- apply auto
- done
-
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
- x : a +o D ==> x : D \<oplus> C"
- apply (frule set_plus_mono4)
- apply auto
- done
-
-lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
- apply (auto intro!: subsetI simp add: set_plus_def)
- apply (rule_tac x = 0 in bexI)
- apply (rule_tac x = x in bexI)
- apply (auto simp add: add_ac)
- done
-
-lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
- by (auto simp add: elt_set_plus_def add_ac diff_minus)
-
-lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
- apply (auto simp add: elt_set_plus_def add_ac diff_minus)
- apply (subgoal_tac "a = (a + - b) + b")
- apply (rule bexI, assumption, assumption)
- apply (auto simp add: add_ac)
- done
-
-lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
- by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
- assumption)
-
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
- by (auto simp add: set_times_def)
-
-lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
- (b *o D) = (a * b) *o (C \<otimes> D)"
- apply (auto simp add: elt_set_times_def set_times_def)
- apply (rule_tac x = "ba * bb" in exI)
- apply (auto simp add: mult_ac)
- apply (rule_tac x = "aa * a" in exI)
- apply (auto simp add: mult_ac)
- done
-
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
- (a * b) *o C"
- by (auto simp add: elt_set_times_def mult_assoc)
-
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
- a *o (B \<otimes> C)"
- apply (auto simp add: elt_set_times_def set_times_def)
- apply (blast intro: mult_ac)
- apply (rule_tac x = "a * aa" in exI)
- apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
- apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: mult_ac)
- done
-
-theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
- a *o (C \<otimes> D)"
- apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
- mult_ac)
- apply (rule_tac x = "aa * ba" in exI)
- apply (auto simp add: mult_ac)
- done
-
-theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
- set_times_rearrange3 set_times_rearrange4
-
-lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
- C \<otimes> E <= D \<otimes> F"
- by (auto simp add: set_times_def)
-
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
- by (auto simp add: elt_set_times_def set_times_def)
-
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
- a *o D <= D \<otimes> C"
- by (auto simp add: elt_set_times_def set_times_def mult_ac)
-
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
- apply (subgoal_tac "a *o B <= a *o D")
- apply (erule order_trans)
- apply (erule set_times_mono3)
- apply (erule set_times_mono)
- done
-
-lemma set_times_mono_b: "C <= D ==> x : a *o C
- ==> x : a *o D"
- apply (frule set_times_mono)
- apply auto
- done
-
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
- x : D \<otimes> F"
- apply (frule set_times_mono2)
- prefer 2
- apply force
- apply assumption
- done
-
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
- apply (frule set_times_mono3)
- apply auto
- done
-
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
- x : a *o D ==> x : D \<otimes> C"
- apply (frule set_times_mono4)
- apply auto
- done
-
-lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
- (a * b) +o (a *o C)"
- by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
-
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
- (a *o B) \<oplus> (a *o C)"
- apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
- apply blast
- apply (rule_tac x = "b + bb" in exI)
- apply (auto simp add: ring_distribs)
- done
-
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
- a *o D \<oplus> C \<otimes> D"
- apply (auto intro!: subsetI simp add:
- elt_set_plus_def elt_set_times_def set_times_def
- set_plus_def ring_distribs)
- apply auto
- done
-
-theorems set_times_plus_distribs =
- set_times_plus_distrib
- set_times_plus_distrib2
-
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
- - a : C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
- - a : (- 1) *o C"
- by (auto simp add: elt_set_times_def)
-
-end
--- a/src/HOL/Metis_Examples/BigO.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Fri Aug 20 20:29:50 2010 +0200
@@ -7,7 +7,7 @@
header {* Big O notation *}
theory BigO
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main SetsAndFunctions
+imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
begin
subsection {* Definitions *}
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 20:29:50 2010 +0200
@@ -346,15 +346,15 @@
lemma one_index[simp]:
"(1 :: 'a::one ^'n)$i = 1" by vector
-instance cart :: (semiring_char_0,finite) semiring_char_0
-proof (intro_classes)
- fix m n ::nat
- show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
- by (simp add: Cart_eq of_nat_index)
+instance cart :: (semiring_char_0, finite) semiring_char_0
+proof
+ fix m n :: nat
+ show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
+ by (auto intro!: injI simp add: Cart_eq of_nat_index)
qed
-instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
-instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
+instance cart :: (comm_ring_1,finite) comm_ring_1 ..
+instance cart :: (ring_char_0,finite) ring_char_0 ..
instance cart :: (real_vector,finite) real_vector ..
--- a/src/HOL/NSA/StarDef.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Aug 20 20:29:50 2010 +0200
@@ -1000,8 +1000,11 @@
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
by transfer (rule refl)
-instance star :: (semiring_char_0) semiring_char_0
-by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+instance star :: (semiring_char_0) semiring_char_0 proof
+ have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
+ then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
+qed
instance star :: (ring_char_0) ring_char_0 ..
--- a/src/HOL/Nat.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Nat.thy Fri Aug 20 20:29:50 2010 +0200
@@ -1227,21 +1227,27 @@
finally show ?thesis .
qed
+lemma comp_funpow:
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "comp f ^^ n = comp (f ^^ n)"
+ by (induct n) simp_all
-subsection {* Embedding of the Naturals into any
- @{text semiring_1}: @{term of_nat} *}
+
+subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
context semiring_1
begin
-primrec
- of_nat :: "nat \<Rightarrow> 'a"
-where
- of_nat_0: "of_nat 0 = 0"
- | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+definition of_nat :: "nat \<Rightarrow> 'a" where
+ "of_nat n = (plus 1 ^^ n) 0"
+
+lemma of_nat_simps [simp]:
+ shows of_nat_0: "of_nat 0 = 0"
+ and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+ by (simp_all add: of_nat_def)
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- unfolding One_nat_def by simp
+ by (simp add: of_nat_def)
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1274,19 +1280,19 @@
Includes non-ordered rings like the complex numbers.*}
class semiring_char_0 = semiring_1 +
- assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ assumes inj_of_nat: "inj of_nat"
begin
+lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ by (auto intro: inj_of_nat injD)
+
text{*Special cases where either operand is zero*}
lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
- by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
+ by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
- by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
-
-lemma inj_of_nat: "inj of_nat"
- by (simp add: inj_on_def)
+ by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
end
@@ -1315,8 +1321,8 @@
text{*Every @{text linordered_semidom} has characteristic zero.*}
-subclass semiring_char_0
- proof qed (simp add: eq_iff order_eq_iff)
+subclass semiring_char_0 proof
+qed (auto intro!: injI simp add: eq_iff)
text{*Special cases where either operand is zero*}
--- a/src/HOL/RealVector.thy Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/RealVector.thy Fri Aug 20 20:29:50 2010 +0200
@@ -270,6 +270,10 @@
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
by (simp add: of_real_def)
+lemma inj_of_real:
+ "inj of_real"
+ by (auto intro: injI)
+
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
@@ -291,13 +295,11 @@
by (simp add: number_of_eq)
text{*Every real algebra has characteristic zero*}
+
instance real_algebra_1 < ring_char_0
proof
- fix m n :: nat
- have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
- by (simp only: of_real_eq_iff of_nat_eq_iff)
- thus "(of_nat m = (of_nat n::'a)) = (m = n)"
- by (simp only: of_real_of_nat_eq)
+ from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def)
qed
instance real_field < field_char_0 ..
--- a/src/HOL/Tools/meson.ML Fri Aug 20 17:04:15 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 20 20:29:50 2010 +0200
@@ -411,7 +411,7 @@
(fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
(*A higher-order instance of a first-order constant? Example is the definition of
- one, 1, at a function type in theory SetsAndFunctions.*)
+ one, 1, at a function type in theory Function_Algebras.*)
fun higher_inst_const thy (c,T) =
case binder_types T of
[] => false (*not a function type, OK*)
--- a/src/Pure/Isar/class.ML Fri Aug 20 17:04:15 2010 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 20 20:29:50 2010 +0200
@@ -17,9 +17,8 @@
val print_classes: theory -> unit
val init: class -> theory -> Proof.context
val begin: class list -> sort -> Proof.context -> Proof.context
- val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
- val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
- val refresh_syntax: class -> Proof.context -> Proof.context
+ val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
+ val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
val class_prefix: string -> string
val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -286,12 +285,6 @@
|> Overloading.set_primary_constraints
end;
-fun refresh_syntax class ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val base_sort = base_sort thy class;
- in synchronize_class_syntax [class] base_sort ctxt end;
-
fun redeclare_operations thy sort =
fold (redeclare_const thy o fst) (these_operations thy sort);
@@ -312,7 +305,15 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
-fun const class ((c, mx), (type_params, dict)) thy =
+fun target_extension f class lthy =
+ lthy
+ |> Local_Theory.raw_theory f
+ |> Local_Theory.target (synchronize_class_syntax [class]
+ (base_sort (ProofContext.theory_of lthy) class));
+
+local
+
+fun target_const class ((c, mx), (type_params, dict)) thy =
let
val morph = morphism thy class;
val b = Morphism.binding morph c;
@@ -334,7 +335,7 @@
|> Sign.add_const_constraint (c', SOME ty')
end;
-fun abbrev class prmode ((c, mx), rhs) thy =
+fun target_abbrev class prmode ((c, mx), rhs) thy =
let
val morph = morphism thy class;
val unchecks = these_unchecks thy [class];
@@ -352,6 +353,13 @@
|> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
end;
+in
+
+fun const class arg = target_extension (target_const class arg) class;
+fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
+
+end;
+
(* simple subclasses *)
--- a/src/Pure/Isar/named_target.ML Fri Aug 20 17:04:15 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Fri Aug 20 20:29:50 2010 +0200
@@ -88,10 +88,6 @@
fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
-fun class_target (Target {target, ...}) f =
- Local_Theory.raw_theory f #>
- Local_Theory.target (Class.refresh_syntax target);
-
(* define *)
@@ -104,7 +100,7 @@
(((b, U), mx), (b_def, rhs)) (type_params, term_params) =
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
- #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
+ #> Class.const target ((b, mx), (type_params, lhs))
#> pair (lhs, def))
fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
@@ -143,7 +139,7 @@
if is_locale
then lthy
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
- |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
+ |> is_class ? Class.abbrev target prmode ((b, mx), t')
else lthy
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);