# HG changeset patch # User haftmann # Date 1266908647 -3600 # Node ID 8ee07543409fb9e17479a6c9572443bcefb63057 # Parent 0e1adc24722ff841595206ce59e0b4d517a73819# Parent d28f453bf622e19828a0dcd82645056fbe14b610 merged diff -r 0e1adc24722f -r 8ee07543409f NEWS --- 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. diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Algebras.thy --- 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 \ 'a \ '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 diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Code_Evaluation.thy --- 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 *} diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Groups.thy --- 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 \ 'a \ '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 \ b \ c + a \ c + b" begin diff -r 0e1adc24722f -r 8ee07543409f src/HOL/IsaMakefile --- 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 \ diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Lattices.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 "\" 50) and diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Library/Dlist.thy --- /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 \ 'a \ bool" where + "member [] y \ False" + | "member (x#xs) y \ x = y \ member xs y" + +lemma member_set: + "member = set" +proof (rule ext)+ + fix xs :: "'a list" and x :: 'a + have "member xs x \ x \ 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 \ set xs = - set xs" + by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq) + +primrec fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ '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 (\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 "[] \ ?dlist" by simp +qed + +text {* Formal, totalized constructor for @{typ "'a dlist"}: *} + +definition Dlist :: "'a list \ '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 \ 'a dlist \ 'a dlist" where + "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))" + +definition remove :: "'a \ 'a dlist \ 'a dlist" where + "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))" + +definition map :: "('a \ 'b) \ 'a dlist \ 'b dlist" where + "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))" + +definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" where + "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))" + + +text {* Derived operations: *} + +definition null :: "'a dlist \ bool" where + "null dxs = List.null (list_of_dlist dxs)" + +definition member :: "'a dlist \ 'a \ bool" where + "member dxs = List.member (list_of_dlist dxs)" + +definition length :: "'a dlist \ nat" where + "length dxs = List.length (list_of_dlist dxs)" + +definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ '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 \ 'a fset" where + "Set dxs = Fset.Set (list_of_dlist dxs)" + +definition Coset :: "'a dlist \ '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 \ 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) \ 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 \ 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) \ list_all P (list_of_dlist xs)" + by (simp add: member_set list_all_iff) + +lemma exists_Set [code]: + "Fset.exists P (Set xs) \ 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 (\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 \ 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 diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Library/Library.thy --- 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 diff -r 0e1adc24722f -r 8ee07543409f src/HOL/List.thy --- 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 \ distinct (List.insert x xs)" + by (simp add: List.insert_def) + subsubsection {* @{text remove1} *} diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Orderings.thy --- 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? *) diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Prolog/Func.thy --- 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 diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Rings.thy --- 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 \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ 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 diff -r 0e1adc24722f -r 8ee07543409f src/HOL/Typerep.thy --- 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 *} diff -r 0e1adc24722f -r 8ee07543409f src/HOL/ex/Codegenerator_Candidates.thy --- 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 \ 'a list \ bool" where diff -r 0e1adc24722f -r 8ee07543409f src/Pure/Isar/code.ML --- 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)); diff -r 0e1adc24722f -r 8ee07543409f src/Tools/Code/code_eval.ML --- 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; diff -r 0e1adc24722f -r 8ee07543409f src/Tools/Code/code_thingol.ML --- 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