# HG changeset patch # User haftmann # Date 1277996084 -7200 # Node ID 0040bafffdef09e97a47986f5b912da10fb4314e # Parent c5a8b612e5710c0c31670e380890bb4f2f1bea7e "prod" and "sum" replace "*" and "+" respectively diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Bali/Decl.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Bali/DeclConcepts.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Bali/WellForm.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Extraction/Greatest_Common_Divisor.thy --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Thu Jul 01 16:54:44 2010 +0200 @@ -69,7 +69,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Thu Jul 01 16:54:44 2010 +0200 @@ -227,7 +227,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Finite_Set.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jul 01 16:54:44 2010 +0200 @@ -123,7 +123,7 @@ import_theory pair; type_maps - prod > "Product_Type.*"; + prod > Product_Type.prod; const_maps "," > Pair diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Import/HOL/pair.imp --- a/src/HOL/Import/HOL/pair.imp Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Import/HOL/pair.imp Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Thu Jul 01 16:54:44 2010 +0200 @@ -349,7 +349,7 @@ end -instantiation * :: (default, default) default +instantiation prod :: (default, default) default begin definition "default = (default, default)" diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Lattice/Lattice.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Countable.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Enum.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Product_Vector.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Product_ord.thy --- a/src/HOL/Library/Product_ord.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Product_ord.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Product_plus.thy --- a/src/HOL/Library/Product_plus.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Product_plus.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Product_Type.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Sum_Type.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/TLA/Action.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Function/sum_tree.ML --- a/src/HOL/Tools/Function/sum_tree.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Function/sum_tree.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Function/termination.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/IOA/meta_theory/automaton.ML --- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/Library/Sum_Cpo.thy --- a/src/HOLCF/Library/Sum_Cpo.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/Library/Sum_Cpo.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/Product_Cpo.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Thu Jul 01 16:54:42 2010 +0200 +++ b/src/HOLCF/Representable.thy Thu Jul 01 16:54:44 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 c5a8b612e571 -r 0040bafffdef src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:42 2010 +0200 +++ b/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:44 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