# HG changeset patch # User haftmann # Date 1278060325 -7200 # Node ID e893e45219c31c37418a549d0c89f4dd0cc33a18 # Parent 40424fc83cc1dfa5922bced3785a91bb40b2db9d# Parent 03217132b79254ac751bc7c9dcb6e20a1e2d4983 merged diff -r 40424fc83cc1 -r e893e45219c3 NEWS --- a/NEWS Thu Jul 01 15:40:58 2010 -0700 +++ b/NEWS Fri Jul 02 10:45:25 2010 +0200 @@ -17,6 +17,9 @@ *** HOL *** +* Abolished symbol type names: "prod" and "sum" replace "*" and "+" +respectively. INCOMPATBILITY. + * Constant "split" has been merged with constant "prod_case"; names of ML functions, facts etc. involving split have been retained so far, though. INCOMPATIBILITY. @@ -41,8 +44,6 @@ types nat ~> Nat.nat - * ~> Product_Type.* - + ~> Sum_Type.+ constants Ball ~> Set.Ball @@ -51,8 +52,9 @@ Pair ~> Product_Type.Pair fst ~> Product_Type.fst snd ~> Product_Type.snd - split ~> Product_Type.split curry ~> Product_Type.curry + op : ~> Set.member + Collect ~> Set.Collect INCOMPATIBILITY. diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Bali/Decl.thy Fri Jul 02 10:45:25 2010 +0200 @@ -257,7 +257,7 @@ lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)" by (cases m) (simp add: memberdecl_memberid_def) -instantiation * :: (type, has_memberid) has_memberid +instantiation prod :: (type, has_memberid) has_memberid begin definition diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Bali/DeclConcepts.thy Fri Jul 02 10:45:25 2010 +0200 @@ -109,7 +109,7 @@ lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d" by (simp add: decl_acc_modi_def) -instantiation * :: (type, has_accmodi) has_accmodi +instantiation prod :: (type, has_accmodi) has_accmodi begin definition @@ -165,7 +165,7 @@ lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" by (simp add: qtname_declclass_def) -instantiation * :: (has_declclass, type) has_declclass +instantiation prod :: (has_declclass, type) has_declclass begin definition @@ -204,7 +204,7 @@ lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" by (simp add: static_field_type_is_static_def) -instantiation * :: (type, has_static) has_static +instantiation prod :: (type, has_static) has_static begin definition @@ -472,7 +472,7 @@ lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" by (simp add: mhead_def mhead_resTy_simp) -instantiation * :: ("type","has_resTy") has_resTy +instantiation prod :: ("type","has_resTy") has_resTy begin definition diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Bali/WellForm.thy Fri Jul 02 10:45:25 2010 +0200 @@ -2168,7 +2168,7 @@ by (force dest!: ws_dynmethd accmethd_SomeD) with dynlookup eq_mheads show ?thesis - by (cases emh type: *) (auto) + by (cases emh type: prod) (auto) next case Iface_methd fix I im @@ -2191,7 +2191,7 @@ by (force dest: implmt_methd) with dynlookup eq_mheads show ?thesis - by (cases emh type: *) (auto) + by (cases emh type: prod) (auto) next case Iface_Object_methd fix I sm @@ -2217,7 +2217,7 @@ intro: class_Object [OF wf] intro: that) with dynlookup eq_mheads show ?thesis - by (cases emh type: *) (auto) + by (cases emh type: prod) (auto) next case False with statI @@ -2243,7 +2243,7 @@ by (auto dest: implmt_methd) with wf eq_stat resProp dynlookup eq_mheads show ?thesis - by (cases emh type: *) (auto intro: widen_trans) + by (cases emh type: prod) (auto intro: widen_trans) qed next case Array_Object_methd @@ -2256,7 +2256,7 @@ by (auto simp add: dynlookup_def dynmethd_C_C) with sm eq_mheads sm show ?thesis - by (cases emh type: *) (auto dest: accmethd_SomeD) + by (cases emh type: prod) (auto dest: accmethd_SomeD) qed qed declare split_paired_All [simp] split_paired_Ex [simp] diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Jul 02 10:45:25 2010 +0200 @@ -3302,7 +3302,7 @@ fun reorder_bounds_tac prems i = let fun variable_of_bound (Const ("Trueprop", _) $ - (Const (@{const_name "op :"}, _) $ + (Const (@{const_name Set.member}, _) $ Free (name, _) $ _)) = name | variable_of_bound (Const ("Trueprop", _) $ (Const ("op =", _) $ diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Extraction/Greatest_Common_Divisor.thy --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Fri Jul 02 10:45:25 2010 +0200 @@ -69,7 +69,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Extraction/Pigeonhole.thy Fri Jul 02 10:45:25 2010 +0200 @@ -227,7 +227,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Finite_Set.thy Fri Jul 02 10:45:25 2010 +0200 @@ -530,7 +530,7 @@ instance bool :: finite proof qed (simp add: UNIV_bool) -instance * :: (finite, finite) finite proof +instance prod :: (finite, finite) finite proof qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) lemma finite_option_UNIV [simp]: @@ -557,7 +557,7 @@ qed qed -instance "+" :: (finite, finite) finite proof +instance sum :: (finite, finite) finite proof qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Hoare/hoare_tac.ML Fri Jul 02 10:45:25 2010 +0200 @@ -21,7 +21,7 @@ | abs2list _ = []; (** maps {(x1,...,xn). t} to [x1,...,xn] **) -fun mk_vars (Const ("Collect",_) $ T) = abs2list T +fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T | mk_vars _ = []; (** abstraction of body over a tuple formed from a list of free variables. diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Imperative_HOL/Heap.thy Fri Jul 02 10:45:25 2010 +0200 @@ -18,9 +18,9 @@ instance nat :: heap .. -instance "*" :: (heap, heap) heap .. +instance prod :: (heap, heap) heap .. -instance "+" :: (heap, heap) heap .. +instance sum :: (heap, heap) heap .. instance list :: (heap) heap .. diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Jul 02 10:45:25 2010 +0200 @@ -123,7 +123,7 @@ import_theory pair; type_maps - prod > "Product_Type.*"; + prod > Product_Type.prod; const_maps "," > Pair diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Jul 02 10:45:25 2010 +0200 @@ -38,9 +38,9 @@ bool > bool fun > fun N_1 > Product_Type.unit - prod > "Product_Type.*" + prod > Product_Type.prod num > Nat.nat - sum > "Sum_Type.+" + sum > Sum_Type.sum (* option > Datatype.option*); const_renames diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Import/HOL/pair.imp --- a/src/HOL/Import/HOL/pair.imp Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Import/HOL/pair.imp Fri Jul 02 10:45:25 2010 +0200 @@ -7,7 +7,7 @@ "LEX" > "LEX_def" type_maps - "prod" > "Product_Type.*" + "prod" > "Product_Type.prod" const_maps "pair_case" > "Product_Type.prod_case" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Import/HOLLight/hollight.imp Fri Jul 02 10:45:25 2010 +0200 @@ -6,7 +6,7 @@ "sum" > "+" "recspace" > "HOLLight.hollight.recspace" "real" > "HOLLight.hollight.real" - "prod" > "Product_Type.*" + "prod" > "Product_Type.prod" "option" > "HOLLight.hollight.option" "num" > "Nat.nat" "nadd" > "HOLLight.hollight.nadd" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Import/proof_kernel.ML Fri Jul 02 10:45:25 2010 +0200 @@ -2088,7 +2088,7 @@ val (HOLThm(rens,td_th)) = norm_hthm thy hth val th2 = beta_eta_thm (td_th RS ex_imp_nonempty) val c = case concl_of th2 of - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c + _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c | _ => raise ERR "new_type_definition" "Bad type definition theorem" val tfrees = OldTerm.term_tfrees c val tnames = map fst tfrees @@ -2118,7 +2118,7 @@ let val PT = domain_type exT in - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P + Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P end | _ => error "Internal error in ProofKernel.new_typedefinition" val tnames_string = if null tnames @@ -2164,7 +2164,7 @@ SOME (cterm_of thy t)] light_nonempty val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty')) val c = case concl_of th2 of - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c + _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c | _ => raise ERR "type_introduction" "Bad type definition theorem" val tfrees = OldTerm.term_tfrees c val tnames = sort_strings (map fst tfrees) @@ -2202,7 +2202,7 @@ let val PT = type_of P' in - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P' + Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P' end val tnames_string = if null tnames diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Lambda/WeakNorm.thy Fri Jul 02 10:45:25 2010 +0200 @@ -349,7 +349,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Lattice/Lattice.thy Fri Jul 02 10:45:25 2010 +0200 @@ -453,7 +453,7 @@ qed qed -instance * :: (lattice, lattice) lattice +instance prod :: (lattice, lattice) lattice proof fix p q :: "'a::lattice \ 'b::lattice" from is_inf_prod show "\inf. is_inf p q inf" .. diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Lattice/Orders.thy Fri Jul 02 10:45:25 2010 +0200 @@ -196,7 +196,7 @@ \emph{not} be linear in general. *} -instantiation * :: (leq, leq) leq +instantiation prod :: (leq, leq) leq begin definition @@ -214,7 +214,7 @@ "p \ q \ (fst p \ fst q \ snd p \ snd q \ C) \ C" by (unfold leq_prod_def) blast -instance * :: (quasi_order, quasi_order) quasi_order +instance prod :: (quasi_order, quasi_order) quasi_order proof fix p q r :: "'a::quasi_order \ 'b::quasi_order" show "p \ p" @@ -234,7 +234,7 @@ qed qed -instance * :: (partial_order, partial_order) partial_order +instance prod :: (partial_order, partial_order) partial_order proof fix p q :: "'a::partial_order \ 'b::partial_order" assume pq: "p \ q" and qp: "q \ p" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Countable.thy Fri Jul 02 10:45:25 2010 +0200 @@ -63,14 +63,14 @@ text {* Pairs *} -instance "*" :: (countable, countable) countable +instance prod :: (countable, countable) countable by (rule countable_classI [of "\(x, y). prod_encode (to_nat x, to_nat y)"]) (auto simp add: prod_encode_eq) text {* Sums *} -instance "+" :: (countable, countable) countable +instance sum :: (countable, countable) countable by (rule countable_classI [of "(\x. case x of Inl a \ to_nat (False, to_nat a) | Inr b \ to_nat (True, to_nat b))"]) (simp split: sum.split_asm) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Enum.thy Fri Jul 02 10:45:25 2010 +0200 @@ -209,7 +209,7 @@ using assms by (induct xs) (auto intro: inj_onI simp add: product_list_set distinct_map) -instantiation * :: (enum, enum) enum +instantiation prod :: (enum, enum) enum begin definition @@ -220,7 +220,7 @@ end -instantiation "+" :: (enum, enum) enum +instantiation sum :: (enum, enum) enum begin definition diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Product_Vector.thy Fri Jul 02 10:45:25 2010 +0200 @@ -10,7 +10,7 @@ subsection {* Product is a real vector space *} -instantiation "*" :: (real_vector, real_vector) real_vector +instantiation prod :: (real_vector, real_vector) real_vector begin definition scaleR_prod_def: @@ -41,8 +41,7 @@ subsection {* Product is a topological space *} -instantiation - "*" :: (topological_space, topological_space) topological_space +instantiation prod :: (topological_space, topological_space) topological_space begin definition open_prod_def: @@ -157,8 +156,7 @@ subsection {* Product is a metric space *} -instantiation - "*" :: (metric_space, metric_space) metric_space +instantiation prod :: (metric_space, metric_space) metric_space begin definition dist_prod_def: @@ -340,7 +338,7 @@ subsection {* Product is a complete metric space *} -instance "*" :: (complete_space, complete_space) complete_space +instance prod :: (complete_space, complete_space) complete_space proof fix X :: "nat \ 'a \ 'b" assume "Cauchy X" have 1: "(\n. fst (X n)) ----> lim (\n. fst (X n))" @@ -357,8 +355,7 @@ subsection {* Product is a normed vector space *} -instantiation - "*" :: (real_normed_vector, real_normed_vector) real_normed_vector +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector begin definition norm_prod_def: @@ -397,11 +394,11 @@ end -instance "*" :: (banach, banach) banach .. +instance prod :: (banach, banach) banach .. subsection {* Product is an inner product space *} -instantiation "*" :: (real_inner, real_inner) real_inner +instantiation prod :: (real_inner, real_inner) real_inner begin definition inner_prod_def: diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Product_ord.thy --- a/src/HOL/Library/Product_ord.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Product_ord.thy Fri Jul 02 10:45:25 2010 +0200 @@ -8,7 +8,7 @@ imports Main begin -instantiation "*" :: (ord, ord) ord +instantiation prod :: (ord, ord) ord begin definition @@ -26,16 +26,16 @@ "(x1\'a\{ord, eq}, y1) < (x2, y2) \ x1 < x2 \ x1 \ x2 \ y1 < y2" unfolding prod_le_def prod_less_def by simp_all -instance * :: (preorder, preorder) preorder proof +instance prod :: (preorder, preorder) preorder proof qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans) -instance * :: (order, order) order proof +instance prod :: (order, order) order proof qed (auto simp add: prod_le_def) -instance * :: (linorder, linorder) linorder proof +instance prod :: (linorder, linorder) linorder proof qed (auto simp: prod_le_def) -instantiation * :: (linorder, linorder) distrib_lattice +instantiation prod :: (linorder, linorder) distrib_lattice begin definition @@ -49,7 +49,7 @@ end -instantiation * :: (bot, bot) bot +instantiation prod :: (bot, bot) bot begin definition @@ -60,7 +60,7 @@ end -instantiation * :: (top, top) top +instantiation prod :: (top, top) top begin definition diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Product_plus.thy --- a/src/HOL/Library/Product_plus.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Product_plus.thy Fri Jul 02 10:45:25 2010 +0200 @@ -10,7 +10,7 @@ subsection {* Operations *} -instantiation "*" :: (zero, zero) zero +instantiation prod :: (zero, zero) zero begin definition zero_prod_def: "0 = (0, 0)" @@ -18,7 +18,7 @@ instance .. end -instantiation "*" :: (plus, plus) plus +instantiation prod :: (plus, plus) plus begin definition plus_prod_def: @@ -27,7 +27,7 @@ instance .. end -instantiation "*" :: (minus, minus) minus +instantiation prod :: (minus, minus) minus begin definition minus_prod_def: @@ -36,7 +36,7 @@ instance .. end -instantiation "*" :: (uminus, uminus) uminus +instantiation prod :: (uminus, uminus) uminus begin definition uminus_prod_def: @@ -83,33 +83,33 @@ subsection {* Class instances *} -instance "*" :: (semigroup_add, semigroup_add) semigroup_add +instance prod :: (semigroup_add, semigroup_add) semigroup_add by default (simp add: expand_prod_eq add_assoc) -instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add +instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add by default (simp add: expand_prod_eq add_commute) -instance "*" :: (monoid_add, monoid_add) monoid_add +instance prod :: (monoid_add, monoid_add) monoid_add by default (simp_all add: expand_prod_eq) -instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add +instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add by default (simp add: expand_prod_eq) -instance "*" :: +instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add by default (simp_all add: expand_prod_eq) -instance "*" :: +instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add by default (simp add: expand_prod_eq) -instance "*" :: +instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add .. -instance "*" :: (group_add, group_add) group_add +instance prod :: (group_add, group_add) group_add by default (simp_all add: expand_prod_eq diff_minus) -instance "*" :: (ab_group_add, ab_group_add) ab_group_add +instance prod :: (ab_group_add, ab_group_add) ab_group_add by default (simp_all add: expand_prod_eq) lemma fst_setsum: "fst (\x\A. f x) = (\x\A. fst (f x))" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Quotient_Product.thy Fri Jul 02 10:45:25 2010 +0200 @@ -13,7 +13,7 @@ where "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" -declare [[map * = (prod_fun, prod_rel)]] +declare [[map prod = (prod_fun, prod_rel)]] lemma prod_equivp[quot_equiv]: diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Jul 02 10:45:25 2010 +0200 @@ -22,7 +22,7 @@ "sum_map f1 f2 (Inl a) = Inl (f1 a)" | "sum_map f1 f2 (Inr a) = Inr (f2 a)" -declare [[map "+" = (sum_map, sum_rel)]] +declare [[map sum = (sum_map, sum_rel)]] text {* should probably be in @{theory Sum_Type} *} diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Jul 02 10:45:25 2010 +0200 @@ -5,7 +5,7 @@ imports Finite_Cartesian_Product Integration begin -instantiation * :: (real_basis, real_basis) real_basis +instantiation prod :: (real_basis, real_basis) real_basis begin definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))" @@ -131,7 +131,7 @@ lemma DIM_prod[simp]: "DIM('a \ 'b) = DIM('b::real_basis) + DIM('a::real_basis)" by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff) -instance * :: (euclidean_space, euclidean_space) euclidean_space +instance prod :: (euclidean_space, euclidean_space) euclidean_space proof (default, safe) let ?b = "basis :: nat \ 'a \ 'b" fix i j assume "i < DIM('a \ 'b)" "j < DIM('a \ 'b)" @@ -139,7 +139,7 @@ unfolding basis_prod_def by (auto simp: dot_basis) qed -instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space +instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space begin definition "x \ (y::('a\'b)) \ (\i'b). x $$ i \ y $$ i)" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jul 02 10:45:25 2010 +0200 @@ -2422,7 +2422,7 @@ apply (erule order_trans [OF real_sqrt_sum_squares_ge2]) done -instance "*" :: (heine_borel, heine_borel) heine_borel +instance prod :: (heine_borel, heine_borel) heine_borel proof fix s :: "('a * 'b) set" and f :: "nat \ 'a * 'b" assume s: "bounded s" and f: "\n. f n \ s" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Nominal/nominal_atoms.ML Fri Jul 02 10:45:25 2010 +0200 @@ -543,7 +543,7 @@ |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) - |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) + |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod) |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) @@ -604,7 +604,7 @@ in thy |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) - |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) + |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) @@ -686,7 +686,7 @@ in thy' |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) - |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) + |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Jul 02 10:45:25 2010 +0200 @@ -121,7 +121,7 @@ val dj_cp = thm "dj_cp"; -fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]), +fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]), Type ("fun", [_, U])])) = (T, U); fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u @@ -617,7 +617,7 @@ |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy => Typedef.add_typedef_global false (SOME (Binding.name name')) (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) - (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ + (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Jul 02 10:45:25 2010 +0200 @@ -103,7 +103,7 @@ case redex of (* case pi o (f x) == (pi o f) (pi o x) *) (Const("Nominal.perm", - Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => + Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => (if (applicable_app f) then let val name = Long_Name.base_name n @@ -190,8 +190,8 @@ fun perm_compose_simproc' sg ss redex = (case redex of (Const ("Nominal.perm", Type ("fun", [Type ("List.list", - [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", - Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $ + [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", + Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ pi2 $ t)) => let val tname' = Long_Name.base_name tname diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Jul 02 10:45:25 2010 +0200 @@ -103,7 +103,7 @@ let fun get_pi_aux s = (case s of (Const (@{const_name "perm"} ,typrm) $ - (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $ + (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $ (Var (n,ty))) => let (* FIXME: this should be an operation the library *) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Product_Type.thy Fri Jul 02 10:45:25 2010 +0200 @@ -129,7 +129,7 @@ definition Pair_Rep :: "'a \ 'b \ 'a \ 'b \ bool" where "Pair_Rep a b = (\x y. x = a \ y = b)" -typedef (prod) ('a, 'b) "*" (infixr "*" 20) +typedef ('a, 'b) prod (infixr "*" 20) = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" proof fix a b show "Pair_Rep a b \ ?prod" @@ -137,14 +137,14 @@ qed type_notation (xsymbols) - "*" ("(_ \/ _)" [21, 20] 20) + "prod" ("(_ \/ _)" [21, 20] 20) type_notation (HTML output) - "*" ("(_ \/ _)" [21, 20] 20) + "prod" ("(_ \/ _)" [21, 20] 20) definition Pair :: "'a \ 'b \ 'a \ 'b" where "Pair a b = Abs_prod (Pair_Rep a b)" -rep_datatype (prod) Pair proof - +rep_datatype Pair proof - fix P :: "'a \ 'b \ bool" and p assume "\a b. P (Pair a b)" then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) @@ -263,7 +263,7 @@ subsubsection {* Code generator setup *} -code_type * +code_type prod (SML infix 2 "*") (OCaml infix 2 "*") (Haskell "!((_),/ (_))") @@ -275,19 +275,19 @@ (Haskell "!((_),/ (_))") (Scala "!((_),/ (_))") -code_instance * :: eq +code_instance prod :: eq (Haskell -) code_const "eq_class.eq \ 'a\eq \ 'b\eq \ 'a \ 'b \ bool" (Haskell infixl 4 "==") types_code - "*" ("(_ */ _)") + "prod" ("(_ */ _)") attach (term_of) {* -fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; +fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; *} attach (test) {* -fun gen_id_42 aG aT bG bT i = +fun term_of_prod aG aT bG bT i = let val (x, t) = aG i; val (y, u) = bG i @@ -438,7 +438,7 @@ lemma split_weak_cong: "p = q \ split c p = split c q" -- {* Prevents simplification of @{term c}: much faster *} - by (erule arg_cong) + by (fact weak_case_cong) lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" by (simp add: split_eta) @@ -689,19 +689,18 @@ lemmas prod_caseI = prod.cases [THEN iffD2, standard] lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" - by auto + by (fact splitI2) lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" - by (auto simp: split_tupled_all) + by (fact splitI2') lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" - by (induct p) auto + by (fact splitE) lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" - by (induct p) auto + by (fact splitE') -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] -declare prod_caseE' [elim!] prod_caseE [elim!] +declare prod_caseI [intro!] lemma prod_case_beta: "prod_case f p = f (fst p) (snd p)" @@ -795,8 +794,11 @@ definition scomp :: "('a \ 'b \ 'c) \ ('b \ 'c \ 'd) \ 'a \ 'd" (infixl "o\" 60) where "f o\ g = (\x. split g (f x))" +lemma scomp_unfold: "scomp = (\f g x. g (fst (f x)) (snd (f x)))" + by (simp add: expand_fun_eq scomp_def split_def) + lemma scomp_apply: "(f o\ g) x = split g (f x)" - by (simp add: scomp_def) + by (simp add: scomp_unfold split_def) lemma Pair_scomp: "Pair x o\ f = f x" by (simp add: expand_fun_eq scomp_apply) @@ -805,13 +807,13 @@ by (simp add: expand_fun_eq scomp_apply) lemma scomp_scomp: "(f o\ g) o\ h = f o\ (\x. g x o\ h)" - by (simp add: expand_fun_eq split_twice scomp_def) + by (simp add: expand_fun_eq scomp_unfold) lemma scomp_fcomp: "(f o\ g) o> h = f o\ (\x. g x o> h)" - by (simp add: expand_fun_eq scomp_apply fcomp_def split_def) + by (simp add: expand_fun_eq scomp_unfold fcomp_def) lemma fcomp_scomp: "(f o> g) o\ h = f o> (g o\ h)" - by (simp add: expand_fun_eq scomp_apply fcomp_apply) + by (simp add: expand_fun_eq scomp_unfold fcomp_apply) code_const scomp (Eval infixl 3 "#->") diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Set.thy Fri Jul 02 10:45:25 2010 +0200 @@ -8,42 +8,36 @@ subsection {* Sets as predicates *} -global - -types 'a set = "'a => bool" +types 'a set = "'a \ bool" -consts - Collect :: "('a => bool) => 'a set" -- "comprehension" - "op :" :: "'a => 'a set => bool" -- "membership" +definition Collect :: "('a \ bool) \ 'a set" where -- "comprehension" + "Collect P = P" -local +definition member :: "'a \ 'a set \ bool" where -- "membership" + mem_def: "member x A = A x" notation - "op :" ("op :") and - "op :" ("(_/ : _)" [50, 51] 50) + member ("op :") and + member ("(_/ : _)" [50, 51] 50) -defs - mem_def [code]: "x : S == S x" - Collect_def [code]: "Collect P == P" - -abbreviation - "not_mem x A == ~ (x : A)" -- "non-membership" +abbreviation not_member where + "not_member x A \ ~ (x : A)" -- "non-membership" notation - not_mem ("op ~:") and - not_mem ("(_/ ~: _)" [50, 51] 50) + not_member ("op ~:") and + not_member ("(_/ ~: _)" [50, 51] 50) notation (xsymbols) - "op :" ("op \") and - "op :" ("(_/ \ _)" [50, 51] 50) and - not_mem ("op \") and - not_mem ("(_/ \ _)" [50, 51] 50) + member ("op \") and + member ("(_/ \ _)" [50, 51] 50) and + not_member ("op \") and + not_member ("(_/ \ _)" [50, 51] 50) notation (HTML output) - "op :" ("op \") and - "op :" ("(_/ \ _)" [50, 51] 50) and - not_mem ("op \") and - not_mem ("(_/ \ _)" [50, 51] 50) + member ("op \") and + member ("(_/ \ _)" [50, 51] 50) and + not_member ("op \") and + not_member ("(_/ \ _)" [50, 51] 50) text {* Set comprehensions *} @@ -312,7 +306,7 @@ in case t of Const (@{const_syntax "op &"}, _) $ - (Const (@{const_syntax "op :"}, _) $ + (Const (@{const_syntax Set.member}, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P => if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M | _ => M @@ -922,7 +916,7 @@ lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 (*Would like to add these, but the existing code only searches for the - outer-level constant, which in this case is just "op :"; we instead need + outer-level constant, which in this case is just Set.member; we instead need to use term-nets to associate patterns with rules. Also, if a rule fails to apply, then the formula should be kept. [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]), @@ -1691,6 +1685,7 @@ lemma vimage_code [code]: "(f -` A) x = A (f x)" by (simp add: vimage_def Collect_def mem_def) +hide_const (open) member text {* Misc theorem and ML bindings *} diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Sum_Type.thy Fri Jul 02 10:45:25 2010 +0200 @@ -17,7 +17,7 @@ definition Inr_Rep :: "'b \ 'a \ 'b \ bool \ bool" where "Inr_Rep b x y p \ y = b \ \ p" -typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" +typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" by auto lemma Inl_RepI: "Inl_Rep a \ sum" @@ -83,7 +83,7 @@ with assms show P by (auto simp add: sum_def Inl_def Inr_def) qed -rep_datatype (sum) Inl Inr +rep_datatype Inl Inr proof - fix P fix s :: "'a + 'b" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/TLA/Action.thy Fri Jul 02 10:45:25 2010 +0200 @@ -16,8 +16,7 @@ 'a trfun = "(state * state) => 'a" action = "bool trfun" -arities - "*" :: (world, world) world +arities prod :: (world, world) world consts (** abstract syntax **) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Jul 02 10:45:25 2010 +0200 @@ -75,7 +75,7 @@ val leafTs' = get_nonrec_types descr' sorts; val branchTs = get_branching_types descr' sorts; val branchT = if null branchTs then HOLogic.unitT - else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs; + else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs; val arities = remove (op =) 0 (get_arities descr'); val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars); @@ -83,7 +83,7 @@ val recTs = get_rec_types descr' sorts; val (newTs, oldTs) = chop (length (hd descr)) recTs; val sumT = if null leafTs then HOLogic.unitT - else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs; + else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs; val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); val UnivT = HOLogic.mk_setT Univ_elT; val UnivT' = Univ_elT --> HOLogic.boolT; diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Function/induction_schema.ML Fri Jul 02 10:45:25 2010 +0200 @@ -220,7 +220,7 @@ val ihyp = Term.all T $ Abs ("z", T, Logic.mk_implies (HOLogic.mk_Trueprop ( - Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) + Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) $ (HOLogic.pair_const T T $ Bound 0 $ x) $ R), HOLogic.mk_Trueprop (P_comp $ Bound 0))) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Function/measure_functions.ML Fri Jul 02 10:45:25 2010 +0200 @@ -39,17 +39,17 @@ fun constant_0 T = Abs ("x", T, HOLogic.zero) fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) -fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) = +fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) = map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) | mk_funorder_funs T = [ constant_1 T ] -fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) = +fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) = map_product (SumTree.mk_sumcase fT sT HOLogic.natT) (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) | mk_ext_base_funs ctxt T = find_measures ctxt T -fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) = +fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) = mk_ext_base_funs ctxt T @ mk_funorder_funs T | mk_all_measure_funs ctxt T = find_measures ctxt T diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Function/sum_tree.ML --- a/src/HOL/Tools/Function/sum_tree.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Function/sum_tree.ML Fri Jul 02 10:45:25 2010 +0200 @@ -17,7 +17,7 @@ {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init (* Sum types *) -fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT]) +fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT]) fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r @@ -27,18 +27,18 @@ fun mk_inj ST n i = access_top_down { init = (ST, I : term -> term), - left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) => + left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))), - right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) => + right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i |> snd fun mk_proj ST n i = access_top_down { init = (ST, I : term -> term), - left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) => + left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) => (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)), - right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) => + right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) => (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i |> snd diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Function/termination.ML Fri Jul 02 10:45:25 2010 +0200 @@ -106,7 +106,7 @@ end (* compute list of types for nodes *) -fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd +fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd (* find index and raw term *) fun dest_inj (SLeaf i) trm = (i, trm) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Jul 02 10:45:25 2010 +0200 @@ -37,7 +37,7 @@ fun check_type ctxt (Type (@{type_name fun}, Ts)) = List.app (check_type ctxt) Ts - | check_type ctxt (Type (@{type_name "*"}, Ts)) = + | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) = List.app (check_type ctxt) Ts | check_type _ @{typ bool} = () | check_type _ (TFree (_, @{sort "{}"})) = () @@ -51,7 +51,7 @@ atom_schema_of SRep card T1 | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) = atom_schema_of SRep card T1 @ atom_schema_of RRep card T2 - | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) = + | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) = maps (atom_schema_of SRep card) Ts | atom_schema_of _ card T = [card T] val arity_of = length ooo atom_schema_of @@ -290,7 +290,7 @@ val thy = ProofContext.theory_of ctxt fun card (Type (@{type_name fun}, [T1, T2])) = reasonable_power (card T2) (card T1) - | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2 + | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2 | card @{typ bool} = 2 | card T = Int.max (1, raw_card T) val neg_t = @{const Not} $ Object_Logic.atomize_term thy t diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Jul 02 10:45:25 2010 +0200 @@ -454,7 +454,7 @@ | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = - Type (@{type_name "*"}, map unarize_unbox_etc_type Ts) + Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts) | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = @@ -509,7 +509,7 @@ | is_fun_type _ = false fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true | is_set_type _ = false -fun is_pair_type (Type (@{type_name "*"}, _)) = true +fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true | is_pair_type _ = false fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s | is_lfp_iterator_type _ = false @@ -546,7 +546,7 @@ | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) val nth_range_type = snd oo strip_n_binders -fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) = +fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) = fold (Integer.add o num_factors_in_type) [T1, T2] 0 | num_factors_in_type _ = 1 fun num_binder_types (Type (@{type_name fun}, [_, T2])) = @@ -557,7 +557,7 @@ (if is_pair_type (body_type T) then binder_types else curried_binder_types) T fun mk_flat_tuple _ [t] = t - | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) = + | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) = HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) fun dest_n_tuple 1 t = [t] @@ -595,7 +595,7 @@ (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", e.g., by adding a field to "Datatype_Aux.info". *) fun is_basic_datatype thy stds s = - member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit}, + member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit}, @{type_name int}, "Code_Numeral.code_numeral"] s orelse (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) @@ -792,7 +792,7 @@ Type (@{type_name fun}, _) => (boxy = InPair orelse boxy = InFunLHS) andalso not (is_boolean_type (body_type T)) - | Type (@{type_name "*"}, Ts) => + | Type (@{type_name Product_Type.prod}, Ts) => boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse ((boxy = InExpr orelse boxy = InFunLHS) andalso exists (is_boxing_worth_it hol_ctxt InPair) @@ -812,12 +812,12 @@ else box_type hol_ctxt (in_fun_lhs_for boxy) T1 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2 - | Type (z as (@{type_name "*"}, Ts)) => + | Type (z as (@{type_name Product_Type.prod}, Ts)) => if boxy <> InConstr andalso boxy <> InSel andalso should_box_type hol_ctxt boxy z then Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) else - Type (@{type_name "*"}, + Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt (if boxy = InConstr orelse boxy = InSel then boxy else InPair)) Ts) @@ -979,7 +979,7 @@ Const (nth_sel_for_constr x n) else let - fun aux m (Type (@{type_name "*"}, [T1, T2])) = + fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) = let val (m, t1) = aux m T1 val (m, t2) = aux m T2 @@ -1069,7 +1069,7 @@ | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse - old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then + old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then case constr_expand hol_ctxt old_T t of Const (old_s, _) $ t1 => if new_s = @{type_name fun} then @@ -1081,7 +1081,7 @@ (Type (@{type_name fun}, old_Ts)) t1] | Const _ $ t1 $ t2 => construct_value ctxt stds - (if new_s = @{type_name "*"} then @{const_name Pair} + (if new_s = @{type_name Product_Type.prod} then @{const_name Pair} else @{const_name PairBox}, new_Ts ---> new_T) (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] [t1, t2]) @@ -1092,7 +1092,7 @@ fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) - | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) = + | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) = card_of_type assigns T1 * card_of_type assigns T2 | card_of_type _ (Type (@{type_name itself}, _)) = 1 | card_of_type _ @{typ prop} = 2 @@ -1113,7 +1113,7 @@ else Int.min (max, reasonable_power k2 k1) end | bounded_card_of_type max default_card assigns - (Type (@{type_name "*"}, [T1, T2])) = + (Type (@{type_name Product_Type.prod}, [T1, T2])) = let val k1 = bounded_card_of_type max default_card assigns T1 val k2 = bounded_card_of_type max default_card assigns T2 @@ -1143,7 +1143,7 @@ else if k1 >= max orelse k2 >= max then max else Int.min (max, reasonable_power k2 k1) end - | Type (@{type_name "*"}, [T1, T2]) => + | Type (@{type_name Product_Type.prod}, [T1, T2]) => let val k1 = aux avoid T1 val k2 = aux avoid T2 @@ -1196,7 +1196,7 @@ fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) fun is_funky_typedef_name thy s = - member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, + member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum}, @{type_name int}] s orelse is_frac_type thy (Type (s, [])) fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s @@ -2066,7 +2066,7 @@ val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts val set_T = tuple_T --> bool_T val curried_T = tuple_T --> set_T - val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T + val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T) val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs) @@ -2185,7 +2185,7 @@ fun aux T accum = case T of Type (@{type_name fun}, Ts) => fold aux Ts accum - | Type (@{type_name "*"}, Ts) => fold aux Ts accum + | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum | Type (@{type_name itself}, [T1]) => aux T1 accum | Type (_, Ts) => if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Jul 02 10:45:25 2010 +0200 @@ -170,7 +170,7 @@ Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])])) $ t1 $ t2) = let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in - Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts)) + Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts)) $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 end | unarize_unbox_etc_term (Const (s, T)) = @@ -185,27 +185,27 @@ | unarize_unbox_etc_term (Abs (s, T, t')) = Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t') -fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12])) - (T2 as Type (@{type_name "*"}, [T21, T22])) = +fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12])) + (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) = let val (n1, n2) = pairself num_factors_in_type (T11, T21) in if n1 = n2 then let val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 in - ((Type (@{type_name "*"}, [T11, T11']), opt_T12'), - (Type (@{type_name "*"}, [T21, T21']), opt_T22')) + ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'), + (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22')) end else if n1 < n2 then case factor_out_types T1 T21 of (p1, (T21', NONE)) => (p1, (T21', SOME T22)) | (p1, (T21', SOME T22')) => - (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22])))) + (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22])))) else swap (factor_out_types T2 T1) end - | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 = + | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE)) - | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) = + | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) = ((T1, NONE), (T21, SOME T22)) | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) @@ -239,7 +239,7 @@ val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end -fun pair_up (Type (@{type_name "*"}, [T1', T2'])) +fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2'])) (t1 as Const (@{const_name Pair}, Type (@{type_name fun}, [_, Type (@{type_name fun}, [_, T1])])) @@ -287,8 +287,8 @@ and do_term (Type (@{type_name fun}, [T1', T2'])) (Type (@{type_name fun}, [T1, T2])) t = do_fun T1' T2' T1 T2 t - | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2'])) - (Type (@{type_name "*"}, [T1, T2])) + | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2'])) + (Type (@{type_name Product_Type.prod}, [T1, T2])) (Const (@{const_name Pair}, _) $ t1 $ t2) = Const (@{const_name Pair}, Ts' ---> T') $ do_term T1' T1 t1 $ do_term T2' T2 t2 @@ -303,7 +303,7 @@ | truth_const_sort_key @{const False} = "2" | truth_const_sort_key _ = "1" -fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts = +fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts = HOLogic.mk_prod (mk_tuple T1 ts, mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) | mk_tuple _ (t :: _) = t @@ -463,7 +463,7 @@ signed_string_of_int j ^ " for " ^ string_for_rep (Vect (k1, Atom (k2, 0)))) end - | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k = + | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k = let val k1 = card_of_type card_assigns T1 val k2 = k div k1 @@ -592,7 +592,7 @@ | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] = if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) - | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _ + | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ (Struct [R1, R2]) [js] = let val arity1 = arity_of_rep R1 diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Jul 02 10:45:25 2010 +0200 @@ -254,7 +254,7 @@ else case T of Type (@{type_name fun}, [T1, T2]) => MFun (fresh_mfun_for_fun_type mdata false T1 T2) - | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2)) + | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) | Type (z as (s, _)) => if could_exist_alpha_sub_mtype ctxt alpha_T T then case AList.lookup (op =) (!datatype_mcache) z of @@ -1035,8 +1035,8 @@ | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => Type (if should_finitize T a then @{type_name fin_fun} else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) - | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) => - Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2]) + | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) => + Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2]) | (MType _, _) => T | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", [M], [T]) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Jul 02 10:45:25 2010 +0200 @@ -427,7 +427,7 @@ let val res_T = snd (HOLogic.dest_prodT T) in (res_T, Const (@{const_name snd}, T --> res_T) $ t) end -fun factorize (z as (Type (@{type_name "*"}, _), _)) = +fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) = maps factorize [mk_fst z, mk_snd z] | factorize z = [z] @@ -1199,7 +1199,7 @@ val w = constr (j, type_of v, rep_of v) in (w :: ws, pool, NameTable.update (v, w) table) end -fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2]) +fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2]) us = let val arity1 = arity_of_rep R1 in Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Jul 02 10:45:25 2010 +0200 @@ -132,8 +132,8 @@ let fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = Type (@{type_name fun}, map box_relational_operator_type Ts) - | box_relational_operator_type (Type (@{type_name "*"}, Ts)) = - Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts) + | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) = + Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts) | box_relational_operator_type T = T fun add_boxed_types_for_var (z as (_, T)) (T', t') = case t' of @@ -953,7 +953,7 @@ and add_axioms_for_type depth T = case T of Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts - | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts + | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts | @{typ prop} => I | @{typ bool} => I | @{typ unit} => I diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Jul 02 10:45:25 2010 +0200 @@ -249,7 +249,7 @@ (case best_one_rep_for_type scope T2 of Unit => Unit | R2 => Vect (card_of_type card_assigns T1, R2)) - | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) = + | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) = (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of (Unit, Unit) => Unit | (R1, R2) => Struct [R1, R2]) @@ -302,7 +302,7 @@ fun type_schema_of_rep _ (Formula _) = [] | type_schema_of_rep _ Unit = [] | type_schema_of_rep T (Atom _) = [T] - | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) = + | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) = type_schema_of_reps [T1, T2] [R1, R2] | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) = replicate_list k (type_schema_of_rep T2 R) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Jul 02 10:45:25 2010 +0200 @@ -107,7 +107,7 @@ is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) = is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2 - | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) = + | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = forall (is_complete_type dtypes facto) Ts | is_complete_type dtypes facto T = not (is_integer_like_type T) andalso not (is_bit_type T) andalso @@ -117,7 +117,7 @@ is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) = is_concrete_type dtypes facto T2 - | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) = + | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = forall (is_concrete_type dtypes facto) Ts | is_concrete_type dtypes facto T = fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Jul 02 10:45:25 2010 +0200 @@ -210,7 +210,7 @@ else [Input, Output] end - | all_modes_of_typ' (Type (@{type_name "*"}, [T1, T2])) = + | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) = map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) | all_modes_of_typ' _ = [Input, Output] @@ -230,7 +230,7 @@ fun all_smodes_of_typ (T as Type ("fun", _)) = let val (S, U) = strip_type T - fun all_smodes (Type (@{type_name "*"}, [T1, T2])) = + fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) = map_product (curry Pair) (all_smodes T1) (all_smodes T2) | all_smodes _ = [Input, Output] in @@ -280,7 +280,7 @@ fun ho_argsT_of mode Ts = let fun ho_arg (Fun _) T = [T] - | ho_arg (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2 + | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2 | ho_arg _ _ = [] in flat (map2 ho_arg (strip_fun_mode mode) Ts) @@ -309,7 +309,7 @@ fun split_map_modeT f mode Ts = let fun split_arg_mode' (m as Fun _) T = f m T - | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = + | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = let val (i1, o1) = split_arg_mode' m1 T1 val (i2, o2) = split_arg_mode' m2 T2 @@ -325,7 +325,7 @@ fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts -fun fold_map_aterms_prodT comb f (Type (@{type_name "*"}, [T1, T2])) s = +fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s = let val (x1, s') = fold_map_aterms_prodT comb f T1 s val (x2, s'') = fold_map_aterms_prodT comb f T2 s' @@ -343,7 +343,7 @@ fun split_modeT' mode Ts = let fun split_arg_mode' (Fun _) T = ([], []) - | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = + | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = let val (i1, o1) = split_arg_mode' m1 T1 val (i2, o2) = split_arg_mode' m2 T2 @@ -756,9 +756,9 @@ (case HOLogic.strip_tupleT (fastype_of arg) of (Ts as _ :: _ :: _) => let - fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2])) + fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2])) (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) - | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) = + | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) = let val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Fri Jul 02 10:45:25 2010 +0200 @@ -70,7 +70,7 @@ fun mk_randompredT T = @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed}) -fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"}, +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod}, [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); @@ -278,7 +278,7 @@ fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ Random.seed}, - Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T + Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T); diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jul 02 10:45:25 2010 +0200 @@ -117,7 +117,7 @@ end; fun dest_randomT (Type ("fun", [@{typ Random.seed}, - Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T + Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T | dest_randomT T = raise TYPE ("dest_randomT", [T], []) fun mk_tracing s t = @@ -467,7 +467,7 @@ (* generation of case rules from user-given introduction rules *) -fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st = +fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st = let val (t1, st') = mk_args2 T1 st val (t2, st'') = mk_args2 T2 st' @@ -1099,7 +1099,7 @@ fun all_input_of T = let val (Ts, U) = strip_type T - fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2) + fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2) | input_of _ = Input in if U = HOLogic.boolT then @@ -2019,7 +2019,7 @@ | strip_split_abs (Abs (_, _, t)) = strip_split_abs t | strip_split_abs t = t -fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names = +fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names = if eq_mode (m, Input) orelse eq_mode (m, Output) then let val x = Name.variant names "x" diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Jul 02 10:45:25 2010 +0200 @@ -54,15 +54,15 @@ fun negF AbsF = RepF | negF RepF = AbsF -fun is_identity (Const (@{const_name "id"}, _)) = true +fun is_identity (Const (@{const_name id}, _)) = true | is_identity _ = false -fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) +fun mk_identity ty = Const (@{const_name id}, ty --> ty) fun mk_fun_compose flag (trm1, trm2) = case flag of - AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 - | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 + | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 fun get_mapfun ctxt s = let @@ -450,7 +450,7 @@ if ty = ty' then subtrm else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm end - | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => + | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => let val subtrm = regularize_trm ctxt (t, t') val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') @@ -460,26 +460,26 @@ else mk_babs $ resrel $ subtrm end - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => + | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') in - if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm + if ty = ty' then Const (@{const_name All}, ty) $ subtrm else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => + | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => let val subtrm = apply_subt (regularize_trm ctxt) (t, t') in - if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm + if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm end - | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, - (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ - (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), - Const (@{const_name "Ex1"}, ty') $ t') => + | (Const (@{const_name Ex1}, ty) $ (Abs (_, _, + (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $ + (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), + Const (@{const_name Ex1}, ty') $ t') => let val t_ = incr_boundvars (~1) t val subtrm = apply_subt (regularize_trm ctxt) (t_, t') diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Jul 02 10:45:25 2010 +0200 @@ -36,7 +36,7 @@ val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] -val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false) +val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false) val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type) val add_pair_rules = exists_pair_type ?? append pair_rules diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Jul 02 10:45:25 2010 +0200 @@ -96,13 +96,13 @@ (* Readable names for the more common symbolic functions. Do not mess with the last nine entries of the table unless you know what you are doing. *) val const_trans_table = - Symtab.make [(@{type_name "*"}, "prod"), - (@{type_name "+"}, "sum"), + Symtab.make [(@{type_name Product_Type.prod}, "prod"), + (@{type_name Sum_Type.sum}, "sum"), (@{const_name "op ="}, "equal"), (@{const_name "op &"}, "and"), (@{const_name "op |"}, "or"), (@{const_name "op -->"}, "implies"), - (@{const_name "op :"}, "in"), + (@{const_name Set.member}, "in"), (@{const_name fequal}, "fequal"), (@{const_name COMBI}, "COMBI"), (@{const_name COMBK}, "COMBK"), diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/TFL/rules.ML Fri Jul 02 10:45:25 2010 +0200 @@ -591,10 +591,10 @@ local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end fun mk_fst tm = - let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm + let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm in Const ("Product_Type.fst", ty --> fty) $ tm end fun mk_snd tm = - let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm + let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm in Const ("Product_Type.snd", ty --> sty) $ tm end in fun XFILL tych x vstruct = diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/TFL/usyntax.ML Fri Jul 02 10:45:25 2010 +0200 @@ -372,7 +372,7 @@ (* Miscellaneous *) fun mk_vstruct ty V = - let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs = + let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs = let val (ltm,vs1) = follow_prod_type ty1 vs val (rtm,vs2) = follow_prod_type ty2 vs1 in (mk_pair{fst=ltm, snd=rtm}, vs2) end @@ -393,7 +393,7 @@ fun dest_relation tm = if (type_of tm = HOLogic.boolT) - then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm + then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm in (R,y,x) end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" else raise USYN_ERR "dest_relation" "not a boolean term"; diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/hologic.ML Fri Jul 02 10:45:25 2010 +0200 @@ -167,15 +167,15 @@ | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u | dest_set t = raise TERM ("dest_set", [t]); -fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T); +fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T); fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t); fun mk_mem (x, A) = let val setT = fastype_of A in - Const ("op :", dest_setT setT --> setT --> boolT) $ x $ A + Const ("Set.member", dest_setT setT --> setT --> boolT) $ x $ A end; -fun dest_mem (Const ("op :", _) $ x $ A) = (x, A) +fun dest_mem (Const ("Set.member", _) $ x $ A) = (x, A) | dest_mem t = raise TERM ("dest_mem", [t]); @@ -289,9 +289,9 @@ (* prod *) -fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]); +fun mk_prodT (T1, T2) = Type ("Product_Type.prod", [T1, T2]); -fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2) +fun dest_prodT (Type ("Product_Type.prod", [T1, T2])) = (T1, T2) | dest_prodT T = raise TYPE ("dest_prodT", [T], []); fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2)); @@ -324,7 +324,7 @@ | _ => raise TERM ("mk_split: bad body type", [t])); (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) -fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 +fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 | flatten_tupleT T = [T]; @@ -334,7 +334,7 @@ | mk_tupleT Ts = foldr1 mk_prodT Ts; fun strip_tupleT (Type ("Product_Type.unit", [])) = [] - | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2 + | strip_tupleT (Type ("Product_Type.prod", [T1, T2])) = T1 :: strip_tupleT T2 | strip_tupleT T = [T]; fun mk_tuple [] = unit @@ -367,14 +367,14 @@ fun strip_ptupleT ps = let fun factors p T = if member (op =) ps p then (case T of - Type ("Product_Type.*", [T1, T2]) => + Type ("Product_Type.prod", [T1, T2]) => factors (1::p) T1 @ factors (2::p) T2 | _ => ptuple_err "strip_ptupleT") else [T] in factors [] end; val flat_tupleT_paths = let - fun factors p (Type ("Product_Type.*", [T1, T2])) = + fun factors p (Type ("Product_Type.prod", [T1, T2])) = p :: factors (1::p) T1 @ factors (2::p) T2 | factors p _ = [] in factors [] end; @@ -383,7 +383,7 @@ let fun mk p T ts = if member (op =) ps p then (case T of - Type ("Product_Type.*", [T1, T2]) => + Type ("Product_Type.prod", [T1, T2]) => let val (t, ts') = mk (1::p) T1 ts; val (u, ts'') = mk (2::p) T2 ts' @@ -414,7 +414,7 @@ let fun ap ((p, T) :: pTs) = if member (op =) ps p then (case T of - Type ("Product_Type.*", [T1, T2]) => + Type ("Product_Type.prod", [T1, T2]) => split_const (T1, T2, map snd pTs ---> T3) $ ap ((1::p, T1) :: (2::p, T2) :: pTs) | _ => ptuple_err "mk_psplits") diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 02 10:45:25 2010 +0200 @@ -579,7 +579,7 @@ fun get_nparms s = if member (op =) names s then SOME nparms else Option.map #3 (get_clauses thy s); - fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) = + fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true) | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) = Prem ([t, u], eq, false) diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 02 10:45:25 2010 +0200 @@ -173,7 +173,7 @@ (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems' end else (case strip_type T of - (Ts, Type (@{type_name "*"}, [T1, T2])) => + (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) => let val fx = Free (x, Ts ---> T1); val fr = Free (r, Ts ---> T2); diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/inductive_set.ML Fri Jul 02 10:45:25 2010 +0200 @@ -36,7 +36,7 @@ fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t => let val (u, _, ps) = HOLogic.strip_psplits t in case u of - (c as Const (@{const_name "op :"}, _)) $ q $ S' => + (c as Const (@{const_name Set.member}, _)) $ q $ S' => (case try (HOLogic.strip_ptuple ps) q of NONE => NONE | SOME ts => @@ -84,10 +84,10 @@ in HOLogic.Collect_const U $ HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t end; - fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"}, + fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member}, Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = mkop s T (m, p, S, mk_collect p T (head_of u)) - | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"}, + | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member}, Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = mkop s T (m, p, mk_collect p T (head_of u), S) | decomp _ = NONE; @@ -271,7 +271,7 @@ let val thy = Context.theory_of ctxt; fun factors_of t fs = case strip_abs_body t of - Const (@{const_name "op :"}, _) $ u $ S => + Const (@{const_name Set.member}, _) $ u $ S => if is_Free S orelse is_Var S then let val ps = HOLogic.flat_tuple_paths u in (SOME ps, (S, ps) :: fs) end @@ -281,7 +281,7 @@ val (pfs, fs) = fold_map factors_of ts []; val ((h', ts'), fs') = (case rhs of Abs _ => (case strip_abs_body rhs of - Const (@{const_name "op :"}, _) $ u $ S => + Const (@{const_name Set.member}, _) $ u $ S => (strip_comb S, SOME (HOLogic.flat_tuple_paths u)) | _ => error "member symbol on right-hand side expected") | _ => (strip_comb rhs, NONE)) @@ -414,7 +414,7 @@ val {set_arities, pred_arities, to_pred_simps, ...} = PredSetConvData.get (Context.Proof lthy); fun infer (Abs (_, _, t)) = infer t - | infer (Const (@{const_name "op :"}, _) $ t $ u) = + | infer (Const (@{const_name Set.member}, _) $ t $ u) = infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u) | infer (t $ u) = infer t #> infer u | infer _ = I; diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/refute.ML Fri Jul 02 10:45:25 2010 +0200 @@ -653,7 +653,7 @@ | Const (@{const_name "op -->"}, _) => t (* sets *) | Const (@{const_name Collect}, _) => t - | Const (@{const_name "op :"}, _) => t + | Const (@{const_name Set.member}, _) => t (* other optimizations *) | Const (@{const_name Finite_Set.card}, _) => t | Const (@{const_name Finite_Set.finite}, _) => t @@ -829,7 +829,7 @@ | Const (@{const_name "op -->"}, _) => axs (* sets *) | Const (@{const_name Collect}, T) => collect_type_axioms T axs - | Const (@{const_name "op :"}, T) => collect_type_axioms T axs + | Const (@{const_name Set.member}, T) => collect_type_axioms T axs (* other optimizations *) | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs | Const (@{const_name Finite_Set.finite}, T) => @@ -2634,11 +2634,11 @@ | Const (@{const_name Collect}, _) => SOME (interpret thy model args (eta_expand t 1)) (* 'op :' == application *) - | Const (@{const_name "op :"}, _) $ t1 $ t2 => + | Const (@{const_name Set.member}, _) $ t1 $ t2 => SOME (interpret thy model args (t2 $ t1)) - | Const (@{const_name "op :"}, _) $ t1 => + | Const (@{const_name Set.member}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const (@{const_name "op :"}, _) => + | Const (@{const_name Set.member}, _) => SOME (interpret thy model args (eta_expand t 2)) | _ => NONE) end; @@ -3050,7 +3050,7 @@ fun Product_Type_fst_interpreter thy model args t = case t of - Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) => + Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let val constants_T = make_constants thy model T val size_U = size_of_type thy model U @@ -3069,7 +3069,7 @@ fun Product_Type_snd_interpreter thy model args t = case t of - Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) => + Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let val size_T = size_of_type thy model T val constants_U = make_constants thy model U diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Tools/split_rule.ML Fri Jul 02 10:45:25 2010 +0200 @@ -31,7 +31,7 @@ (*In ap_split S T u, term u expects separate arguments for the factors of S, with result type T. The call creates a new term expecting one argument of type S.*) -fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u = +fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u = internal_split_const (T1, T2, T3) $ Abs ("v", T1, ap_split T2 T3 diff -r 40424fc83cc1 -r e893e45219c3 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOL/Transitive_Closure.thy Fri Jul 02 10:45:25 2010 +0200 @@ -858,7 +858,7 @@ val rtrancl_trans = @{thm rtrancl_trans}; fun decomp (@{const Trueprop} $ t) = - let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) = + let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) = let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") | decr r = (r,"r"); diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/Bifinite.thy Fri Jul 02 10:45:25 2010 +0200 @@ -161,7 +161,7 @@ by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed -instantiation "*" :: (profinite, profinite) profinite +instantiation prod :: (profinite, profinite) profinite begin definition @@ -187,7 +187,7 @@ end -instance "*" :: (bifinite, bifinite) bifinite .. +instance prod :: (bifinite, bifinite) bifinite .. lemma approx_Pair [simp]: "approx i\(x, y) = (approx i\x, approx i\y)" diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Fri Jul 02 10:45:25 2010 +0200 @@ -34,9 +34,9 @@ exception malformed; -fun fst_type (Type(@{type_name "*"},[a,_])) = a | +fun fst_type (Type(@{type_name prod},[a,_])) = a | fst_type _ = raise malformed; -fun snd_type (Type(@{type_name "*"},[_,a])) = a | +fun snd_type (Type(@{type_name prod},[_,a])) = a | snd_type _ = raise malformed; fun element_type (Type("set",[a])) = a | @@ -121,10 +121,10 @@ fun delete_ul_string s = implode(delete_ul (explode s)); -fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) | +fun type_list_of sign (Type(@{type_name prod},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) | type_list_of sign a = [(Syntax.string_of_typ_global sign a)]; -fun structured_tuple l (Type(@{type_name "*"},s::t::_)) = +fun structured_tuple l (Type(@{type_name prod},s::t::_)) = let val (r,str) = structured_tuple l s; in diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/IOA/meta_theory/automaton.ML --- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML Fri Jul 02 10:45:25 2010 +0200 @@ -298,7 +298,7 @@ (string_of_typ thy t)); fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | -comp_st_type_of thy (a::r) = Type(@{type_name "*"},[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | +comp_st_type_of thy (a::r) = HOLogic.mk_prodT (st_type_of thy (aut_type_of thy a), comp_st_type_of thy r) | comp_st_type_of _ _ = error "empty automaton list"; (* checking consistency of action types (for composition) *) @@ -378,25 +378,22 @@ end) fun add_composition automaton_name aut_list thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val acttyp = check_ac thy aut_list; -val st_typ = comp_st_type_of thy aut_list; -val comp_list = clist aut_list; -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, -Type(@{type_name "*"}, -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]), - Type(@{type_name "*"},[Type("set",[st_typ]), - Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]), - Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) -,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == " ^ comp_list)] -end) + let + val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...") + val acttyp = check_ac thy aut_list; + val st_typ = comp_st_type_of thy aut_list; + val comp_list = clist aut_list; + in + thy + |> Sign.add_consts_i + [(Binding.name automaton_name, HOLogic.mk_prodT (HOLogic.mk_prodT + (HOLogic.mk_setT acttyp, HOLogic.mk_prodT (HOLogic.mk_setT acttyp, HOLogic.mk_setT acttyp)), + HOLogic.mk_prodT (HOLogic.mk_setT st_typ, HOLogic.mk_prodT (HOLogic.mk_setT + (HOLogic.mk_prodT (st_typ, HOLogic.mk_prodT (acttyp, st_typ))), + HOLogic.mk_prodT (HOLogic.mk_setT (HOLogic.mk_setT acttyp), HOLogic.mk_setT (HOLogic.mk_setT acttyp))))), + NoSyn)] + |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)] + end fun add_restriction automaton_name aut_source actlist thy = (writeln("Constructing automaton " ^ automaton_name ^ " ..."); @@ -433,25 +430,23 @@ | _ => error "could not extract argument type of renaming function term"); fun add_rename automaton_name aut_source fun_name thy = -(writeln("Constructing automaton " ^ automaton_name ^ " ..."); -let -val auttyp = aut_type_of thy aut_source; -val st_typ = st_type_of thy auttyp; -val acttyp = ren_act_type_of thy fun_name -in -thy -|> Sign.add_consts_i -[(Binding.name automaton_name, -Type(@{type_name "*"}, -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]), - Type(@{type_name "*"},[Type("set",[st_typ]), - Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]), - Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) -,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] -end) + let + val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...") + val auttyp = aut_type_of thy aut_source; + val st_typ = st_type_of thy auttyp; + val acttyp = ren_act_type_of thy fun_name + in + thy + |> Sign.add_consts_i + [(Binding.name automaton_name, + Type(@{type_name prod}, + [Type(@{type_name prod},[HOLogic.mk_setT acttyp,Type(@{type_name prod},[HOLogic.mk_setT acttyp,HOLogic.mk_setT acttyp])]), + Type(@{type_name prod},[HOLogic.mk_setT st_typ, + Type(@{type_name prod},[HOLogic.mk_setT (Type(@{type_name prod},[st_typ,Type(@{type_name prod},[acttyp,st_typ])])), + Type(@{type_name prod},[HOLogic.mk_setT (HOLogic.mk_setT acttyp),HOLogic.mk_setT (HOLogic.mk_setT acttyp)])])])]) + ,NoSyn)] + |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] + end (** outer syntax **) diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/Library/Sum_Cpo.thy --- a/src/HOLCF/Library/Sum_Cpo.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/Library/Sum_Cpo.thy Fri Jul 02 10:45:25 2010 +0200 @@ -10,7 +10,7 @@ subsection {* Ordering on sum type *} -instantiation "+" :: (below, below) below +instantiation sum :: (below, below) below begin definition below_sum_def: @@ -56,7 +56,7 @@ subsection {* Sum type is a complete partial order *} -instance "+" :: (po, po) po +instance sum :: (po, po) po proof fix x :: "'a + 'b" show "x \ x" @@ -117,7 +117,7 @@ apply (drule ub_rangeD, simp) done -instance "+" :: (cpo, cpo) cpo +instance sum :: (cpo, cpo) cpo apply intro_classes apply (erule sum_chain_cases, safe) apply (rule exI) @@ -217,20 +217,20 @@ lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a" by (safe elim!: compact_Inr compact_Inr_rev) -instance "+" :: (chfin, chfin) chfin +instance sum :: (chfin, chfin) chfin apply intro_classes apply (erule compact_imp_max_in_chain) apply (case_tac "\i. Y i", simp_all) done -instance "+" :: (finite_po, finite_po) finite_po .. +instance sum :: (finite_po, finite_po) finite_po .. -instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo +instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo by intro_classes (simp add: below_sum_def split: sum.split) subsection {* Sum type is a bifinite domain *} -instantiation "+" :: (profinite, profinite) profinite +instantiation sum :: (profinite, profinite) profinite begin definition diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/Product_Cpo.thy Fri Jul 02 10:45:25 2010 +0200 @@ -32,7 +32,7 @@ subsection {* Product type is a partial order *} -instantiation "*" :: (below, below) below +instantiation prod :: (below, below) below begin definition @@ -41,7 +41,7 @@ instance .. end -instance "*" :: (po, po) po +instance prod :: (po, po) po proof fix x :: "'a \ 'b" show "x \ x" @@ -148,7 +148,7 @@ \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" by (rule lub_cprod [THEN thelubI]) -instance "*" :: (cpo, cpo) cpo +instance prod :: (cpo, cpo) cpo proof fix S :: "nat \ ('a \ 'b)" assume "chain S" @@ -157,9 +157,9 @@ thus "\x. range S <<| x" .. qed -instance "*" :: (finite_po, finite_po) finite_po .. +instance prod :: (finite_po, finite_po) finite_po .. -instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo +instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo proof fix x y :: "'a \ 'b" show "x \ y \ x = y" @@ -172,7 +172,7 @@ lemma minimal_cprod: "(\, \) \ p" by (simp add: below_prod_def) -instance "*" :: (pcpo, pcpo) pcpo +instance prod :: (pcpo, pcpo) pcpo by intro_classes (fast intro: minimal_cprod) lemma inst_cprod_pcpo: "\ = (\, \)" @@ -297,7 +297,7 @@ apply (drule compact_snd, simp) done -instance "*" :: (chfin, chfin) chfin +instance prod :: (chfin, chfin) chfin apply intro_classes apply (erule compact_imp_max_in_chain) apply (case_tac "\i. Y i", simp) diff -r 40424fc83cc1 -r e893e45219c3 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Thu Jul 01 15:40:58 2010 -0700 +++ b/src/HOLCF/Representable.thy Fri Jul 02 10:45:25 2010 +0200 @@ -447,7 +447,7 @@ text "Cartesian products of representable types are representable." -instantiation "*" :: (rep, rep) rep +instantiation prod :: (rep, rep) rep begin definition emb_cprod_def: "emb = udom_emb oo cprod_map\emb\emb" @@ -763,7 +763,7 @@ (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), - (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, + (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up}, diff -r 40424fc83cc1 -r e893e45219c3 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Thu Jul 01 15:40:58 2010 -0700 +++ b/src/Pure/Isar/class_target.ML Fri Jul 02 10:45:25 2010 +0200 @@ -450,7 +450,7 @@ (* target *) -val sanitize_name = (*FIXME*) +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) let fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'" orelse s = "_"; @@ -465,9 +465,7 @@ explode #> scan_valids #> implode end; -fun type_name "Product_Type.*" = "prod" - | type_name "Sum_Type.+" = "sum" - | type_name s = sanitize_name (Long_Name.base_name s); +val type_name = sanitize_name o Long_Name.base_name; fun resort_terms pp algebra consts constraints ts = let