--- a/NEWS Mon Feb 22 21:48:20 2010 -0800
+++ b/NEWS Tue Feb 23 08:04:07 2010 +0100
@@ -122,9 +122,6 @@
INCOMPATIBILITY.
-* New theory Algebras contains generic algebraic structures and
-generic algebraic operations.
-
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
--- a/src/HOL/Algebras.thy Mon Feb 22 21:48:20 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(* Title: HOL/Algebras.thy
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Generic algebraic structures and operations *}
-
-theory Algebras
-imports HOL
-begin
-
-text {*
- These locales provide basic structures for interpretation into
- bigger structures; extensions require careful thinking, otherwise
- undesired effects may occur due to interpretation.
-*}
-
-ML {*
-structure Ac_Simps = Named_Thms(
- val name = "ac_simps"
- val description = "associativity and commutativity simplification rules"
-)
-*}
-
-setup Ac_Simps.setup
-
-locale semigroup =
- fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
- assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
-
-locale abel_semigroup = semigroup +
- assumes commute [ac_simps]: "a * b = b * a"
-begin
-
-lemma left_commute [ac_simps]:
- "b * (a * c) = a * (b * c)"
-proof -
- have "(b * a) * c = (a * b) * c"
- by (simp only: commute)
- then show ?thesis
- by (simp only: assoc)
-qed
-
-end
-
-locale semilattice = abel_semigroup +
- assumes idem [simp]: "a * a = a"
-begin
-
-lemma left_idem [simp]:
- "a * (a * b) = a * b"
- by (simp add: assoc [symmetric])
-
-end
-
-end
\ No newline at end of file
--- a/src/HOL/Code_Evaluation.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Code_Evaluation.thy Tue Feb 23 08:04:07 2010 +0100
@@ -76,7 +76,8 @@
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
in if need_inst then add_term_of tyco raw_vs thy else thy end;
in
- Code.type_interpretation ensure_term_of
+ Code.datatype_interpretation ensure_term_of
+ #> Code.abstype_interpretation ensure_term_of
end
*}
@@ -114,7 +115,7 @@
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
in
- Code.type_interpretation ensure_term_of_code
+ Code.datatype_interpretation ensure_term_of_code
end
*}
--- a/src/HOL/Groups.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Groups.thy Tue Feb 23 08:04:07 2010 +0100
@@ -9,6 +9,65 @@
uses ("~~/src/Provers/Arith/abel_cancel.ML")
begin
+subsection {* Fact collections *}
+
+ML {*
+structure Algebra_Simps = Named_Thms(
+ val name = "algebra_simps"
+ val description = "algebra simplification rules"
+)
+*}
+
+setup Algebra_Simps.setup
+
+text{* The rewrites accumulated in @{text algebra_simps} deal with the
+classical algebraic structures of groups, rings and family. They simplify
+terms by multiplying everything out (in case of a ring) and bringing sums and
+products into a canonical form (by ordered rewriting). As a result it decides
+group and ring equalities but also helps with inequalities.
+
+Of course it also works for fields, but it knows nothing about multiplicative
+inverses or division. This is catered for by @{text field_simps}. *}
+
+
+ML {*
+structure Ac_Simps = Named_Thms(
+ val name = "ac_simps"
+ val description = "associativity and commutativity simplification rules"
+)
+*}
+
+setup Ac_Simps.setup
+
+
+subsection {* Abstract structures *}
+
+text {*
+ These locales provide basic structures for interpretation into
+ bigger structures; extensions require careful thinking, otherwise
+ undesired effects may occur due to interpretation.
+*}
+
+locale semigroup =
+ fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+ assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
+
+locale abel_semigroup = semigroup +
+ assumes commute [ac_simps]: "a * b = b * a"
+begin
+
+lemma left_commute [ac_simps]:
+ "b * (a * c) = a * (b * c)"
+proof -
+ have "(b * a) * c = (a * b) * c"
+ by (simp only: commute)
+ then show ?thesis
+ by (simp only: assoc)
+qed
+
+end
+
+
subsection {* Generic operations *}
class zero =
@@ -64,37 +123,6 @@
use "~~/src/Provers/Arith/abel_cancel.ML"
-text {*
- The theory of partially ordered groups is taken from the books:
- \begin{itemize}
- \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
- \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
- \end{itemize}
- Most of the used notions can also be looked up in
- \begin{itemize}
- \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
- \item \emph{Algebra I} by van der Waerden, Springer.
- \end{itemize}
-*}
-
-ML {*
-structure Algebra_Simps = Named_Thms(
- val name = "algebra_simps"
- val description = "algebra simplification rules"
-)
-*}
-
-setup Algebra_Simps.setup
-
-text{* The rewrites accumulated in @{text algebra_simps} deal with the
-classical algebraic structures of groups, rings and family. They simplify
-terms by multiplying everything out (in case of a ring) and bringing sums and
-products into a canonical form (by ordered rewriting). As a result it decides
-group and ring equalities but also helps with inequalities.
-
-Of course it also works for fields, but it knows nothing about multiplicative
-inverses or division. This is catered for by @{text field_simps}. *}
-
subsection {* Semigroups and Monoids *}
@@ -144,19 +172,6 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-class ab_semigroup_idem_mult = ab_semigroup_mult +
- assumes mult_idem: "x * x = x"
-
-sublocale ab_semigroup_idem_mult < times!: semilattice times proof
-qed (fact mult_idem)
-
-context ab_semigroup_idem_mult
-begin
-
-lemmas mult_left_idem = times.left_idem
-
-end
-
class monoid_add = zero + semigroup_add +
assumes add_0_left [simp]: "0 + a = a"
and add_0_right [simp]: "a + 0 = a"
@@ -411,6 +426,19 @@
subsection {* (Partially) Ordered Groups *}
+text {*
+ The theory of partially ordered groups is taken from the books:
+ \begin{itemize}
+ \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
+ \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
+ \end{itemize}
+ Most of the used notions can also be looked up in
+ \begin{itemize}
+ \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+ \item \emph{Algebra I} by van der Waerden, Springer.
+ \end{itemize}
+*}
+
class ordered_ab_semigroup_add = order + ab_semigroup_add +
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
begin
--- a/src/HOL/IsaMakefile Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/IsaMakefile Tue Feb 23 08:04:07 2010 +0100
@@ -142,7 +142,6 @@
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
- Algebras.thy \
Complete_Lattice.thy \
Datatype.thy \
Extraction.thy \
@@ -385,7 +384,7 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \
Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy \
Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy \
- Library/Sum_Of_Squares/sos_wrapper.ML \
+ Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy \
Library/Infinite_Set.thy Library/FuncSet.thy \
--- a/src/HOL/Lattices.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Lattices.thy Tue Feb 23 08:04:07 2010 +0100
@@ -8,7 +8,42 @@
imports Orderings Groups
begin
-subsection {* Lattices *}
+subsection {* Abstract semilattice *}
+
+text {*
+ This locales provide a basic structure for interpretation into
+ bigger structures; extensions require careful thinking, otherwise
+ undesired effects may occur due to interpretation.
+*}
+
+locale semilattice = abel_semigroup +
+ assumes idem [simp]: "f a a = a"
+begin
+
+lemma left_idem [simp]:
+ "f a (f a b) = f a b"
+ by (simp add: assoc [symmetric])
+
+end
+
+
+subsection {* Idempotent semigroup *}
+
+class ab_semigroup_idem_mult = ab_semigroup_mult +
+ assumes mult_idem: "x * x = x"
+
+sublocale ab_semigroup_idem_mult < times!: semilattice times proof
+qed (fact mult_idem)
+
+context ab_semigroup_idem_mult
+begin
+
+lemmas mult_left_idem = times.left_idem
+
+end
+
+
+subsection {* Conrete lattices *}
notation
less_eq (infix "\<sqsubseteq>" 50) and
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Dlist.thy Tue Feb 23 08:04:07 2010 +0100
@@ -0,0 +1,256 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Lists with elements distinct as canonical example for datatype invariants *}
+
+theory Dlist
+imports Main Fset
+begin
+
+section {* Prelude *}
+
+text {* Without canonical argument order, higher-order things tend to get confusing quite fast: *}
+
+setup {* Sign.map_naming (Name_Space.add_path "List") *}
+
+primrec member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+ "member [] y \<longleftrightarrow> False"
+ | "member (x#xs) y \<longleftrightarrow> x = y \<or> member xs y"
+
+lemma member_set:
+ "member = set"
+proof (rule ext)+
+ fix xs :: "'a list" and x :: 'a
+ have "member xs x \<longleftrightarrow> x \<in> set xs" by (induct xs) auto
+ then show "member xs x = set xs x" by (simp add: mem_def)
+qed
+
+lemma not_set_compl:
+ "Not \<circ> set xs = - set xs"
+ by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
+
+primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "fold f [] s = s"
+ | "fold f (x#xs) s = fold f xs (f x s)"
+
+lemma foldl_fold:
+ "foldl f s xs = List.fold (\<lambda>x s. f s x) xs s"
+ by (induct xs arbitrary: s) simp_all
+
+setup {* Sign.map_naming Name_Space.parent_path *}
+
+
+section {* The type of distinct lists *}
+
+typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+ morphisms list_of_dlist Abs_dlist
+proof
+ show "[] \<in> ?dlist" by simp
+qed
+
+text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
+
+definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
+ [code del]: "Dlist xs = Abs_dlist (remdups xs)"
+
+lemma distinct_list_of_dlist [simp]:
+ "distinct (list_of_dlist dxs)"
+ using list_of_dlist [of dxs] by simp
+
+lemma list_of_dlist_Dlist [simp]:
+ "list_of_dlist (Dlist xs) = remdups xs"
+ by (simp add: Dlist_def Abs_dlist_inverse)
+
+lemma Dlist_list_of_dlist [simp]:
+ "Dlist (list_of_dlist dxs) = dxs"
+ by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
+
+
+text {* Fundamental operations: *}
+
+definition empty :: "'a dlist" where
+ "empty = Dlist []"
+
+definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+ "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
+
+definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+ "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
+ "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
+
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+ "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
+
+
+text {* Derived operations: *}
+
+definition null :: "'a dlist \<Rightarrow> bool" where
+ "null dxs = List.null (list_of_dlist dxs)"
+
+definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
+ "member dxs = List.member (list_of_dlist dxs)"
+
+definition length :: "'a dlist \<Rightarrow> nat" where
+ "length dxs = List.length (list_of_dlist dxs)"
+
+definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "fold f dxs = List.fold f (list_of_dlist dxs)"
+
+
+section {* Executable version obeying invariant *}
+
+code_abstype Dlist list_of_dlist
+ by simp
+
+lemma list_of_dlist_empty [simp, code abstract]:
+ "list_of_dlist empty = []"
+ by (simp add: empty_def)
+
+lemma list_of_dlist_insert [simp, code abstract]:
+ "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
+ by (simp add: insert_def)
+
+lemma list_of_dlist_remove [simp, code abstract]:
+ "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
+ by (simp add: remove_def)
+
+lemma list_of_dlist_map [simp, code abstract]:
+ "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+ by (simp add: map_def)
+
+lemma list_of_dlist_filter [simp, code abstract]:
+ "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
+ by (simp add: filter_def)
+
+declare null_def [code] member_def [code] length_def [code] fold_def [code] -- {* explicit is better than implicit *}
+
+
+section {* Implementation of sets by distinct lists -- canonical! *}
+
+definition Set :: "'a dlist \<Rightarrow> 'a fset" where
+ "Set dxs = Fset.Set (list_of_dlist dxs)"
+
+definition Coset :: "'a dlist \<Rightarrow> 'a fset" where
+ "Coset dxs = Fset.Coset (list_of_dlist dxs)"
+
+code_datatype Set Coset
+
+declare member_code [code del]
+declare is_empty_Set [code del]
+declare empty_Set [code del]
+declare UNIV_Set [code del]
+declare insert_Set [code del]
+declare remove_Set [code del]
+declare map_Set [code del]
+declare filter_Set [code del]
+declare forall_Set [code del]
+declare exists_Set [code del]
+declare card_Set [code del]
+declare subfset_eq_forall [code del]
+declare subfset_subfset_eq [code del]
+declare eq_fset_subfset_eq [code del]
+declare inter_project [code del]
+declare subtract_remove [code del]
+declare union_insert [code del]
+declare Infimum_inf [code del]
+declare Supremum_sup [code del]
+
+lemma Set_Dlist [simp]:
+ "Set (Dlist xs) = Fset (set xs)"
+ by (simp add: Set_def Fset.Set_def)
+
+lemma Coset_Dlist [simp]:
+ "Coset (Dlist xs) = Fset (- set xs)"
+ by (simp add: Coset_def Fset.Coset_def)
+
+lemma member_Set [simp]:
+ "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
+ by (simp add: Set_def member_set)
+
+lemma member_Coset [simp]:
+ "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
+ by (simp add: Coset_def member_set not_set_compl)
+
+lemma is_empty_Set [code]:
+ "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
+ by (simp add: null_def null_empty member_set)
+
+lemma bot_code [code]:
+ "bot = Set empty"
+ by (simp add: empty_def)
+
+lemma top_code [code]:
+ "top = Coset empty"
+ by (simp add: empty_def)
+
+lemma insert_code [code]:
+ "Fset.insert x (Set dxs) = Set (insert x dxs)"
+ "Fset.insert x (Coset dxs) = Coset (remove x dxs)"
+ by (simp_all add: insert_def remove_def member_set not_set_compl)
+
+lemma remove_code [code]:
+ "Fset.remove x (Set dxs) = Set (remove x dxs)"
+ "Fset.remove x (Coset dxs) = Coset (insert x dxs)"
+ by (auto simp add: insert_def remove_def member_set not_set_compl)
+
+lemma member_code [code]:
+ "Fset.member (Set dxs) = member dxs"
+ "Fset.member (Coset dxs) = Not \<circ> member dxs"
+ by (simp_all add: member_def)
+
+lemma map_code [code]:
+ "Fset.map f (Set dxs) = Set (map f dxs)"
+ by (simp add: member_set)
+
+lemma filter_code [code]:
+ "Fset.filter f (Set dxs) = Set (filter f dxs)"
+ by (simp add: member_set)
+
+lemma forall_Set [code]:
+ "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
+ by (simp add: member_set list_all_iff)
+
+lemma exists_Set [code]:
+ "Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
+ by (simp add: member_set list_ex_iff)
+
+lemma card_code [code]:
+ "Fset.card (Set dxs) = length dxs"
+ by (simp add: length_def member_set distinct_card)
+
+lemma foldl_list_of_dlist:
+ "foldl f s (list_of_dlist dxs) = fold (\<lambda>x s. f s x) dxs s"
+ by (simp add: foldl_fold fold_def)
+
+lemma inter_code [code]:
+ "inf A (Set xs) = Set (filter (Fset.member A) xs)"
+ "inf A (Coset xs) = fold Fset.remove xs A"
+ by (simp_all only: Set_def Coset_def foldl_list_of_dlist inter_project list_of_dlist_filter)
+
+lemma subtract_code [code]:
+ "A - Set xs = fold Fset.remove xs A"
+ "A - Coset xs = Set (filter (Fset.member A) xs)"
+ by (simp_all only: Set_def Coset_def foldl_list_of_dlist subtract_remove list_of_dlist_filter)
+
+lemma union_code [code]:
+ "sup (Set xs) A = fold Fset.insert xs A"
+ "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
+ by (simp_all only: Set_def Coset_def foldl_list_of_dlist union_insert list_of_dlist_filter)
+
+context complete_lattice
+begin
+
+lemma Infimum_code [code]:
+ "Infimum (Set As) = fold inf As top"
+ by (simp only: Set_def Infimum_inf foldl_list_of_dlist inf.commute)
+
+lemma Supremum_code [code]:
+ "Supremum (Set As) = fold sup As bot"
+ by (simp only: Set_def Supremum_sup foldl_list_of_dlist sup.commute)
+
+end
+
+hide (open) const member fold empty insert remove map filter null member length fold
+
+end
--- a/src/HOL/Library/Library.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Library/Library.thy Tue Feb 23 08:04:07 2010 +0100
@@ -15,6 +15,7 @@
ContNotDenum
Countable
Diagonalize
+ Dlist
Efficient_Nat
Enum
Eval_Witness
--- a/src/HOL/List.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/List.thy Tue Feb 23 08:04:07 2010 +0100
@@ -250,7 +250,7 @@
@{lemma "distinct [2,0,1::nat]" by simp}\\
@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
-@{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\
+@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@@ -2900,10 +2900,14 @@
"List.insert x [] = [x]"
by simp
-lemma set_insert:
+lemma set_insert [simp]:
"set (List.insert x xs) = insert x (set xs)"
by (auto simp add: List.insert_def)
+lemma distinct_insert [simp]:
+ "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
+ by (simp add: List.insert_def)
+
subsubsection {* @{text remove1} *}
--- a/src/HOL/Orderings.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Orderings.thy Tue Feb 23 08:04:07 2010 +0100
@@ -5,7 +5,7 @@
header {* Abstract orderings *}
theory Orderings
-imports Algebras
+imports HOL
uses
"~~/src/Provers/order.ML"
"~~/src/Provers/quasi.ML" (* FIXME unused? *)
--- a/src/HOL/Prolog/Func.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Prolog/Func.thy Tue Feb 23 08:04:07 2010 +0100
@@ -5,7 +5,7 @@
header {* Untyped functional language, with call by value semantics *}
theory Func
-imports HOHH Algebras
+imports HOHH
begin
typedecl tm
--- a/src/HOL/Rings.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Rings.thy Tue Feb 23 08:04:07 2010 +0100
@@ -13,19 +13,6 @@
imports Groups
begin
-text {*
- The theory of partially ordered rings is taken from the books:
- \begin{itemize}
- \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
- \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
- \end{itemize}
- Most of the used notions can also be looked up in
- \begin{itemize}
- \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
- \item \emph{Algebra I} by van der Waerden, Springer.
- \end{itemize}
-*}
-
class semiring = ab_semigroup_add + semigroup_mult +
assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"
assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"
@@ -506,6 +493,19 @@
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
+text {*
+ The theory of partially ordered rings is taken from the books:
+ \begin{itemize}
+ \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
+ \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
+ \end{itemize}
+ Most of the used notions can also be looked up in
+ \begin{itemize}
+ \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+ \item \emph{Algebra I} by van der Waerden, Springer.
+ \end{itemize}
+*}
+
class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add
begin
--- a/src/HOL/Typerep.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Typerep.thy Tue Feb 23 08:04:07 2010 +0100
@@ -70,7 +70,8 @@
add_typerep @{type_name fun}
#> Typedef.interpretation ensure_typerep
-#> Code.type_interpretation (ensure_typerep o fst)
+#> Code.datatype_interpretation (ensure_typerep o fst)
+#> Code.abstype_interpretation (ensure_typerep o fst)
end
*}
--- a/src/HOL/ex/Codegenerator_Candidates.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Tue Feb 23 08:04:07 2010 +0100
@@ -8,6 +8,8 @@
Complex_Main
AssocList
Binomial
+ "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
+ Dlist
Fset
Enum
List_Prefix
@@ -17,12 +19,11 @@
Permutation
"~~/src/HOL/Number_Theory/Primes"
Product_ord
+ "~~/src/HOL/ex/Records"
SetsAndFunctions
Tree
While_Combinator
Word
- "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
- "~~/src/HOL/ex/Records"
begin
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
--- a/src/Pure/Isar/code.ML Mon Feb 22 21:48:20 2010 -0800
+++ b/src/Pure/Isar/code.ML Tue Feb 23 08:04:07 2010 +0100
@@ -49,10 +49,13 @@
val add_signature_cmd: string * string -> theory -> theory
val add_datatype: (string * typ) list -> theory -> theory
val add_datatype_cmd: string list -> theory -> theory
+ val datatype_interpretation:
+ (string * ((string * sort) list * (string * typ list) list)
+ -> theory -> theory) -> theory -> theory
val add_abstype: string * typ -> string * typ -> theory -> Proof.state
val add_abstype_cmd: string -> string -> theory -> Proof.state
- val type_interpretation:
- (string * ((string * sort) list * (string * typ list) list)
+ val abstype_interpretation:
+ (string * ((string * sort) list * ((string * typ) * (string * thm)))
-> theory -> theory) -> theory -> theory
val add_eqn: thm -> theory -> theory
val add_nbe_eqn: thm -> theory -> theory
@@ -63,8 +66,8 @@
val del_eqns: string -> theory -> theory
val add_case: thm -> theory -> theory
val add_undefined: string -> theory -> theory
- val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
- val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option
+ val get_type: theory -> string -> ((string * sort) list * (string * typ list) list)
+ val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
val is_constr: theory -> string -> bool
val is_abstr: theory -> string -> bool
val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
@@ -163,21 +166,21 @@
signatures: int Symtab.table * typ Symtab.table,
functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
(*with explicit history*),
- datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
+ types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
(*with explicit history*),
cases: (int * (int * string list)) Symtab.table * unit Symtab.table
};
-fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) =
+fun make_spec (history_concluded, ((signatures, functions), (types, cases))) =
Spec { history_concluded = history_concluded,
- signatures = signatures, functions = functions, datatypes = datatypes, cases = cases };
+ signatures = signatures, functions = functions, types = types, cases = cases };
fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
- functions = functions, datatypes = datatypes, cases = cases }) =
- make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases))));
+ functions = functions, types = types, cases = cases }) =
+ make_spec (f (history_concluded, ((signatures, functions), (types, cases))));
fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1,
- datatypes = datatypes1, cases = (cases1, undefs1) },
+ types = types1, cases = (cases1, undefs1) },
Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2,
- datatypes = datatypes2, cases = (cases2, undefs2) }) =
+ types = types2, cases = (cases2, undefs2) }) =
let
val signatures = (Symtab.merge (op =) (tycos1, tycos2),
Symtab.merge typ_equiv (sigs1, sigs2));
@@ -190,15 +193,15 @@
then raw_history else filtered_history;
in ((false, (snd o hd) history), history) end;
val functions = Symtab.join (K merge_functions) (functions1, functions2);
- val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2);
+ val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
val cases = (Symtab.merge (K true) (cases1, cases2),
Symtab.merge (K true) (undefs1, undefs2));
- in make_spec (false, ((signatures, functions), (datatypes, cases))) end;
+ in make_spec (false, ((signatures, functions), (types, cases))) end;
fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
fun the_signatures (Spec { signatures, ... }) = signatures;
fun the_functions (Spec { functions, ... }) = functions;
-fun the_datatypes (Spec { datatypes, ... }) = datatypes;
+fun the_types (Spec { types, ... }) = types;
fun the_cases (Spec { cases, ... }) = cases;
val map_history_concluded = map_spec o apfst;
val map_signatures = map_spec o apsnd o apfst o apfst;
@@ -423,11 +426,11 @@
$ Free ("x", ty_abs)), Free ("x", ty_abs));
in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;
-fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
+fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
of (_, entry) :: _ => SOME entry
| _ => NONE;
-fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco
+fun get_type_spec thy tyco = case get_type_entry thy tyco
of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
| NONE => arity_number thy tyco
|> Name.invents Name.context Name.aT
@@ -435,23 +438,23 @@
|> rpair []
|> rpair false;
-fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco
+fun get_abstype_spec thy tyco = case get_type_entry thy tyco
of SOME (vs, Abstractor spec) => (vs, spec)
| NONE => error ("Not an abstract type: " ^ tyco);
-fun get_datatype thy = fst o get_datatype_spec thy;
+fun get_type thy = fst o get_type_spec thy;
-fun get_datatype_of_constr_or_abstr thy c =
+fun get_type_of_constr_or_abstr thy c =
case (snd o strip_type o const_typ thy) c
- of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco
+ of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
| _ => NONE;
-fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c
+fun is_constr thy c = case get_type_of_constr_or_abstr thy c
of SOME (_, false) => true
| _ => false;
-fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c
+fun is_abstr thy c = case get_type_of_constr_or_abstr thy c
of SOME (_, true) => true
| _ => false;
@@ -952,7 +955,7 @@
|> Symtab.dest
|> (map o apsnd) (snd o fst)
|> sort (string_ord o pairself fst);
- val datatypes = the_datatypes exec
+ val datatypes = the_types exec
|> Symtab.dest
|> map (fn (tyco, (_, (vs, spec)) :: _) =>
((tyco, vs), constructors_of spec))
@@ -1088,24 +1091,21 @@
(map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
-(* datatypes *)
+(* types *)
-structure Type_Interpretation =
- Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
-
-fun register_datatype (tyco, vs_spec) thy =
+fun register_type (tyco, vs_spec) thy =
let
val (old_constrs, some_old_proj) =
- case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
+ case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
| (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
| [] => ([], NONE)
val outdated_funs = case some_old_proj
- of NONE => []
+ of NONE => old_constrs
| SOME old_proj => Symtab.fold
(fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
then insert (op =) c else I)
- ((the_functions o the_exec) thy) [old_proj];
+ ((the_functions o the_exec) thy) (old_proj :: old_constrs);
fun drop_outdated_cases cases = fold Symtab.delete_safe
(Symtab.fold (fn (c, (_, (_, cos))) =>
if exists (member (op =) old_constrs) cos
@@ -1116,13 +1116,15 @@
|> map_exec_purge
((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
#> (map_cases o apfst) drop_outdated_cases)
- |> Type_Interpretation.data (tyco, serial ())
end;
-fun type_interpretation f = Type_Interpretation.interpretation
- (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
+fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
-fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
+structure Datatype_Interpretation =
+ Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+
+fun datatype_interpretation f = Datatype_Interpretation.interpretation
+ (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy);
fun add_datatype proto_constrs thy =
let
@@ -1131,20 +1133,29 @@
in
thy
|> fold (del_eqns o fst) constrs
- |> register_datatype (tyco, (vs, Constructors cos))
+ |> register_type (tyco, (vs, Constructors cos))
+ |> Datatype_Interpretation.data (tyco, serial ())
end;
fun add_datatype_cmd raw_constrs thy =
add_datatype (map (read_bare_const thy) raw_constrs) thy;
+structure Abstype_Interpretation =
+ Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+
+fun abstype_interpretation f = Abstype_Interpretation.interpretation
+ (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
+
fun add_abstype proto_abs proto_rep thy =
let
val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
fun after_qed [[cert]] = ProofContext.theory
- (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
+ (del_eqns abs
+ #> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
#> change_fun_spec false rep ((K o Proj)
- (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)));
+ (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))
+ #> Abstype_Interpretation.data (tyco, serial ()));
in
thy
|> ProofContext.init
@@ -1188,7 +1199,7 @@
(mk_attribute o code_target_attr))
|| Scan.succeed (mk_attribute add_warning_eqn);
in
- Type_Interpretation.init
+ Datatype_Interpretation.init
#> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
"declare theorems for code generation"
end));
--- a/src/Tools/Code/code_eval.ML Mon Feb 22 21:48:20 2010 -0800
+++ b/src/Tools/Code/code_eval.ML Tue Feb 23 08:04:07 2010 +0100
@@ -130,7 +130,7 @@
val thy = ProofContext.theory_of background;
val tyco = Sign.intern_type thy raw_tyco;
val constrs = map (Code.check_const thy) raw_constrs;
- val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
+ val constrs' = (map fst o snd o Code.get_type thy) tyco;
val _ = if eq_set (op =) (constrs, constrs') then ()
else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
val is_first = is_first_occ background;
--- a/src/Tools/Code/code_thingol.ML Mon Feb 22 21:48:20 2010 -0800
+++ b/src/Tools/Code/code_thingol.ML Tue Feb 23 08:04:07 2010 +0100
@@ -256,7 +256,7 @@
| thyname :: _ => thyname;
fun thyname_of_const thy c = case AxClass.class_of_param thy c
of SOME class => thyname_of_class thy class
- | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
+ | NONE => (case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
| NONE => Codegen.thyname_of_const thy c);
fun purify_base "==>" = "follows"
@@ -543,7 +543,7 @@
let
val stmt_datatype =
let
- val (vs, cos) = Code.get_datatype thy tyco;
+ val (vs, cos) = Code.get_type thy tyco;
in
fold_map (translate_tyvar_sort thy algbr eqngr) vs
##>> fold_map (fn (c, tys) =>
@@ -569,7 +569,7 @@
##>> fold_map (translate_eqn thy algbr eqngr) eqns
#>> (fn info => Fun (c, info))
end;
- val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
+ val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
| NONE => (case AxClass.class_of_param thy c
of SOME class => stmt_classparam class