1.1 --- a/src/HOL/Bali/Decl.thy Thu Jul 01 16:54:42 2010 +0200
1.2 +++ b/src/HOL/Bali/Decl.thy Thu Jul 01 16:54:44 2010 +0200
1.3 @@ -257,7 +257,7 @@
1.4 lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
1.5 by (cases m) (simp add: memberdecl_memberid_def)
1.6
1.7 -instantiation * :: (type, has_memberid) has_memberid
1.8 +instantiation prod :: (type, has_memberid) has_memberid
1.9 begin
1.10
1.11 definition
2.1 --- a/src/HOL/Bali/DeclConcepts.thy Thu Jul 01 16:54:42 2010 +0200
2.2 +++ b/src/HOL/Bali/DeclConcepts.thy Thu Jul 01 16:54:44 2010 +0200
2.3 @@ -109,7 +109,7 @@
2.4 lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
2.5 by (simp add: decl_acc_modi_def)
2.6
2.7 -instantiation * :: (type, has_accmodi) has_accmodi
2.8 +instantiation prod :: (type, has_accmodi) has_accmodi
2.9 begin
2.10
2.11 definition
2.12 @@ -165,7 +165,7 @@
2.13 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
2.14 by (simp add: qtname_declclass_def)
2.15
2.16 -instantiation * :: (has_declclass, type) has_declclass
2.17 +instantiation prod :: (has_declclass, type) has_declclass
2.18 begin
2.19
2.20 definition
2.21 @@ -204,7 +204,7 @@
2.22 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
2.23 by (simp add: static_field_type_is_static_def)
2.24
2.25 -instantiation * :: (type, has_static) has_static
2.26 +instantiation prod :: (type, has_static) has_static
2.27 begin
2.28
2.29 definition
2.30 @@ -472,7 +472,7 @@
2.31 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
2.32 by (simp add: mhead_def mhead_resTy_simp)
2.33
2.34 -instantiation * :: ("type","has_resTy") has_resTy
2.35 +instantiation prod :: ("type","has_resTy") has_resTy
2.36 begin
2.37
2.38 definition
3.1 --- a/src/HOL/Bali/WellForm.thy Thu Jul 01 16:54:42 2010 +0200
3.2 +++ b/src/HOL/Bali/WellForm.thy Thu Jul 01 16:54:44 2010 +0200
3.3 @@ -2168,7 +2168,7 @@
3.4 by (force dest!: ws_dynmethd accmethd_SomeD)
3.5 with dynlookup eq_mheads
3.6 show ?thesis
3.7 - by (cases emh type: *) (auto)
3.8 + by (cases emh type: prod) (auto)
3.9 next
3.10 case Iface_methd
3.11 fix I im
3.12 @@ -2191,7 +2191,7 @@
3.13 by (force dest: implmt_methd)
3.14 with dynlookup eq_mheads
3.15 show ?thesis
3.16 - by (cases emh type: *) (auto)
3.17 + by (cases emh type: prod) (auto)
3.18 next
3.19 case Iface_Object_methd
3.20 fix I sm
3.21 @@ -2217,7 +2217,7 @@
3.22 intro: class_Object [OF wf] intro: that)
3.23 with dynlookup eq_mheads
3.24 show ?thesis
3.25 - by (cases emh type: *) (auto)
3.26 + by (cases emh type: prod) (auto)
3.27 next
3.28 case False
3.29 with statI
3.30 @@ -2243,7 +2243,7 @@
3.31 by (auto dest: implmt_methd)
3.32 with wf eq_stat resProp dynlookup eq_mheads
3.33 show ?thesis
3.34 - by (cases emh type: *) (auto intro: widen_trans)
3.35 + by (cases emh type: prod) (auto intro: widen_trans)
3.36 qed
3.37 next
3.38 case Array_Object_methd
3.39 @@ -2256,7 +2256,7 @@
3.40 by (auto simp add: dynlookup_def dynmethd_C_C)
3.41 with sm eq_mheads sm
3.42 show ?thesis
3.43 - by (cases emh type: *) (auto dest: accmethd_SomeD)
3.44 + by (cases emh type: prod) (auto dest: accmethd_SomeD)
3.45 qed
3.46 qed
3.47 declare split_paired_All [simp] split_paired_Ex [simp]
4.1 --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy Thu Jul 01 16:54:42 2010 +0200
4.2 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Thu Jul 01 16:54:44 2010 +0200
4.3 @@ -69,7 +69,7 @@
4.4
4.5 end
4.6
4.7 -instantiation * :: (default, default) default
4.8 +instantiation prod :: (default, default) default
4.9 begin
4.10
4.11 definition "default = (default, default)"
5.1 --- a/src/HOL/Extraction/Pigeonhole.thy Thu Jul 01 16:54:42 2010 +0200
5.2 +++ b/src/HOL/Extraction/Pigeonhole.thy Thu Jul 01 16:54:44 2010 +0200
5.3 @@ -227,7 +227,7 @@
5.4
5.5 end
5.6
5.7 -instantiation * :: (default, default) default
5.8 +instantiation prod :: (default, default) default
5.9 begin
5.10
5.11 definition "default = (default, default)"
6.1 --- a/src/HOL/Finite_Set.thy Thu Jul 01 16:54:42 2010 +0200
6.2 +++ b/src/HOL/Finite_Set.thy Thu Jul 01 16:54:44 2010 +0200
6.3 @@ -530,7 +530,7 @@
6.4 instance bool :: finite proof
6.5 qed (simp add: UNIV_bool)
6.6
6.7 -instance * :: (finite, finite) finite proof
6.8 +instance prod :: (finite, finite) finite proof
6.9 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
6.10
6.11 lemma finite_option_UNIV [simp]:
6.12 @@ -557,7 +557,7 @@
6.13 qed
6.14 qed
6.15
6.16 -instance "+" :: (finite, finite) finite proof
6.17 +instance sum :: (finite, finite) finite proof
6.18 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
6.19
6.20
7.1 --- a/src/HOL/Imperative_HOL/Heap.thy Thu Jul 01 16:54:42 2010 +0200
7.2 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Jul 01 16:54:44 2010 +0200
7.3 @@ -18,9 +18,9 @@
7.4
7.5 instance nat :: heap ..
7.6
7.7 -instance "*" :: (heap, heap) heap ..
7.8 +instance prod :: (heap, heap) heap ..
7.9
7.10 -instance "+" :: (heap, heap) heap ..
7.11 +instance sum :: (heap, heap) heap ..
7.12
7.13 instance list :: (heap) heap ..
7.14
8.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jul 01 16:54:42 2010 +0200
8.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jul 01 16:54:44 2010 +0200
8.3 @@ -123,7 +123,7 @@
8.4 import_theory pair;
8.5
8.6 type_maps
8.7 - prod > "Product_Type.*";
8.8 + prod > Product_Type.prod;
8.9
8.10 const_maps
8.11 "," > Pair
9.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jul 01 16:54:42 2010 +0200
9.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jul 01 16:54:44 2010 +0200
9.3 @@ -38,9 +38,9 @@
9.4 bool > bool
9.5 fun > fun
9.6 N_1 > Product_Type.unit
9.7 - prod > "Product_Type.*"
9.8 + prod > Product_Type.prod
9.9 num > Nat.nat
9.10 - sum > "Sum_Type.+"
9.11 + sum > Sum_Type.sum
9.12 (* option > Datatype.option*);
9.13
9.14 const_renames
10.1 --- a/src/HOL/Import/HOL/pair.imp Thu Jul 01 16:54:42 2010 +0200
10.2 +++ b/src/HOL/Import/HOL/pair.imp Thu Jul 01 16:54:44 2010 +0200
10.3 @@ -7,7 +7,7 @@
10.4 "LEX" > "LEX_def"
10.5
10.6 type_maps
10.7 - "prod" > "Product_Type.*"
10.8 + "prod" > "Product_Type.prod"
10.9
10.10 const_maps
10.11 "pair_case" > "Product_Type.prod_case"
11.1 --- a/src/HOL/Import/HOLLight/hollight.imp Thu Jul 01 16:54:42 2010 +0200
11.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jul 01 16:54:44 2010 +0200
11.3 @@ -6,7 +6,7 @@
11.4 "sum" > "+"
11.5 "recspace" > "HOLLight.hollight.recspace"
11.6 "real" > "HOLLight.hollight.real"
11.7 - "prod" > "Product_Type.*"
11.8 + "prod" > "Product_Type.prod"
11.9 "option" > "HOLLight.hollight.option"
11.10 "num" > "Nat.nat"
11.11 "nadd" > "HOLLight.hollight.nadd"
12.1 --- a/src/HOL/Lambda/WeakNorm.thy Thu Jul 01 16:54:42 2010 +0200
12.2 +++ b/src/HOL/Lambda/WeakNorm.thy Thu Jul 01 16:54:44 2010 +0200
12.3 @@ -349,7 +349,7 @@
12.4
12.5 end
12.6
12.7 -instantiation * :: (default, default) default
12.8 +instantiation prod :: (default, default) default
12.9 begin
12.10
12.11 definition "default = (default, default)"
13.1 --- a/src/HOL/Lattice/Lattice.thy Thu Jul 01 16:54:42 2010 +0200
13.2 +++ b/src/HOL/Lattice/Lattice.thy Thu Jul 01 16:54:44 2010 +0200
13.3 @@ -453,7 +453,7 @@
13.4 qed
13.5 qed
13.6
13.7 -instance * :: (lattice, lattice) lattice
13.8 +instance prod :: (lattice, lattice) lattice
13.9 proof
13.10 fix p q :: "'a::lattice \<times> 'b::lattice"
13.11 from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
14.1 --- a/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:42 2010 +0200
14.2 +++ b/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:44 2010 +0200
14.3 @@ -196,7 +196,7 @@
14.4 \emph{not} be linear in general.
14.5 *}
14.6
14.7 -instantiation * :: (leq, leq) leq
14.8 +instantiation prod :: (leq, leq) leq
14.9 begin
14.10
14.11 definition
14.12 @@ -214,7 +214,7 @@
14.13 "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
14.14 by (unfold leq_prod_def) blast
14.15
14.16 -instance * :: (quasi_order, quasi_order) quasi_order
14.17 +instance prod :: (quasi_order, quasi_order) quasi_order
14.18 proof
14.19 fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
14.20 show "p \<sqsubseteq> p"
14.21 @@ -234,7 +234,7 @@
14.22 qed
14.23 qed
14.24
14.25 -instance * :: (partial_order, partial_order) partial_order
14.26 +instance prod :: (partial_order, partial_order) partial_order
14.27 proof
14.28 fix p q :: "'a::partial_order \<times> 'b::partial_order"
14.29 assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
15.1 --- a/src/HOL/Library/Countable.thy Thu Jul 01 16:54:42 2010 +0200
15.2 +++ b/src/HOL/Library/Countable.thy Thu Jul 01 16:54:44 2010 +0200
15.3 @@ -63,14 +63,14 @@
15.4
15.5 text {* Pairs *}
15.6
15.7 -instance "*" :: (countable, countable) countable
15.8 +instance prod :: (countable, countable) countable
15.9 by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
15.10 (auto simp add: prod_encode_eq)
15.11
15.12
15.13 text {* Sums *}
15.14
15.15 -instance "+" :: (countable, countable) countable
15.16 +instance sum :: (countable, countable) countable
15.17 by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
15.18 | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
15.19 (simp split: sum.split_asm)
16.1 --- a/src/HOL/Library/Enum.thy Thu Jul 01 16:54:42 2010 +0200
16.2 +++ b/src/HOL/Library/Enum.thy Thu Jul 01 16:54:44 2010 +0200
16.3 @@ -209,7 +209,7 @@
16.4 using assms by (induct xs)
16.5 (auto intro: inj_onI simp add: product_list_set distinct_map)
16.6
16.7 -instantiation * :: (enum, enum) enum
16.8 +instantiation prod :: (enum, enum) enum
16.9 begin
16.10
16.11 definition
16.12 @@ -220,7 +220,7 @@
16.13
16.14 end
16.15
16.16 -instantiation "+" :: (enum, enum) enum
16.17 +instantiation sum :: (enum, enum) enum
16.18 begin
16.19
16.20 definition
17.1 --- a/src/HOL/Library/Product_Vector.thy Thu Jul 01 16:54:42 2010 +0200
17.2 +++ b/src/HOL/Library/Product_Vector.thy Thu Jul 01 16:54:44 2010 +0200
17.3 @@ -10,7 +10,7 @@
17.4
17.5 subsection {* Product is a real vector space *}
17.6
17.7 -instantiation "*" :: (real_vector, real_vector) real_vector
17.8 +instantiation prod :: (real_vector, real_vector) real_vector
17.9 begin
17.10
17.11 definition scaleR_prod_def:
17.12 @@ -41,8 +41,7 @@
17.13
17.14 subsection {* Product is a topological space *}
17.15
17.16 -instantiation
17.17 - "*" :: (topological_space, topological_space) topological_space
17.18 +instantiation prod :: (topological_space, topological_space) topological_space
17.19 begin
17.20
17.21 definition open_prod_def:
17.22 @@ -157,8 +156,7 @@
17.23
17.24 subsection {* Product is a metric space *}
17.25
17.26 -instantiation
17.27 - "*" :: (metric_space, metric_space) metric_space
17.28 +instantiation prod :: (metric_space, metric_space) metric_space
17.29 begin
17.30
17.31 definition dist_prod_def:
17.32 @@ -340,7 +338,7 @@
17.33
17.34 subsection {* Product is a complete metric space *}
17.35
17.36 -instance "*" :: (complete_space, complete_space) complete_space
17.37 +instance prod :: (complete_space, complete_space) complete_space
17.38 proof
17.39 fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
17.40 have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
17.41 @@ -357,8 +355,7 @@
17.42
17.43 subsection {* Product is a normed vector space *}
17.44
17.45 -instantiation
17.46 - "*" :: (real_normed_vector, real_normed_vector) real_normed_vector
17.47 +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
17.48 begin
17.49
17.50 definition norm_prod_def:
17.51 @@ -397,11 +394,11 @@
17.52
17.53 end
17.54
17.55 -instance "*" :: (banach, banach) banach ..
17.56 +instance prod :: (banach, banach) banach ..
17.57
17.58 subsection {* Product is an inner product space *}
17.59
17.60 -instantiation "*" :: (real_inner, real_inner) real_inner
17.61 +instantiation prod :: (real_inner, real_inner) real_inner
17.62 begin
17.63
17.64 definition inner_prod_def:
18.1 --- a/src/HOL/Library/Product_ord.thy Thu Jul 01 16:54:42 2010 +0200
18.2 +++ b/src/HOL/Library/Product_ord.thy Thu Jul 01 16:54:44 2010 +0200
18.3 @@ -8,7 +8,7 @@
18.4 imports Main
18.5 begin
18.6
18.7 -instantiation "*" :: (ord, ord) ord
18.8 +instantiation prod :: (ord, ord) ord
18.9 begin
18.10
18.11 definition
18.12 @@ -26,16 +26,16 @@
18.13 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
18.14 unfolding prod_le_def prod_less_def by simp_all
18.15
18.16 -instance * :: (preorder, preorder) preorder proof
18.17 +instance prod :: (preorder, preorder) preorder proof
18.18 qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
18.19
18.20 -instance * :: (order, order) order proof
18.21 +instance prod :: (order, order) order proof
18.22 qed (auto simp add: prod_le_def)
18.23
18.24 -instance * :: (linorder, linorder) linorder proof
18.25 +instance prod :: (linorder, linorder) linorder proof
18.26 qed (auto simp: prod_le_def)
18.27
18.28 -instantiation * :: (linorder, linorder) distrib_lattice
18.29 +instantiation prod :: (linorder, linorder) distrib_lattice
18.30 begin
18.31
18.32 definition
18.33 @@ -49,7 +49,7 @@
18.34
18.35 end
18.36
18.37 -instantiation * :: (bot, bot) bot
18.38 +instantiation prod :: (bot, bot) bot
18.39 begin
18.40
18.41 definition
18.42 @@ -60,7 +60,7 @@
18.43
18.44 end
18.45
18.46 -instantiation * :: (top, top) top
18.47 +instantiation prod :: (top, top) top
18.48 begin
18.49
18.50 definition
19.1 --- a/src/HOL/Library/Product_plus.thy Thu Jul 01 16:54:42 2010 +0200
19.2 +++ b/src/HOL/Library/Product_plus.thy Thu Jul 01 16:54:44 2010 +0200
19.3 @@ -10,7 +10,7 @@
19.4
19.5 subsection {* Operations *}
19.6
19.7 -instantiation "*" :: (zero, zero) zero
19.8 +instantiation prod :: (zero, zero) zero
19.9 begin
19.10
19.11 definition zero_prod_def: "0 = (0, 0)"
19.12 @@ -18,7 +18,7 @@
19.13 instance ..
19.14 end
19.15
19.16 -instantiation "*" :: (plus, plus) plus
19.17 +instantiation prod :: (plus, plus) plus
19.18 begin
19.19
19.20 definition plus_prod_def:
19.21 @@ -27,7 +27,7 @@
19.22 instance ..
19.23 end
19.24
19.25 -instantiation "*" :: (minus, minus) minus
19.26 +instantiation prod :: (minus, minus) minus
19.27 begin
19.28
19.29 definition minus_prod_def:
19.30 @@ -36,7 +36,7 @@
19.31 instance ..
19.32 end
19.33
19.34 -instantiation "*" :: (uminus, uminus) uminus
19.35 +instantiation prod :: (uminus, uminus) uminus
19.36 begin
19.37
19.38 definition uminus_prod_def:
19.39 @@ -83,33 +83,33 @@
19.40
19.41 subsection {* Class instances *}
19.42
19.43 -instance "*" :: (semigroup_add, semigroup_add) semigroup_add
19.44 +instance prod :: (semigroup_add, semigroup_add) semigroup_add
19.45 by default (simp add: expand_prod_eq add_assoc)
19.46
19.47 -instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
19.48 +instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
19.49 by default (simp add: expand_prod_eq add_commute)
19.50
19.51 -instance "*" :: (monoid_add, monoid_add) monoid_add
19.52 +instance prod :: (monoid_add, monoid_add) monoid_add
19.53 by default (simp_all add: expand_prod_eq)
19.54
19.55 -instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
19.56 +instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
19.57 by default (simp add: expand_prod_eq)
19.58
19.59 -instance "*" ::
19.60 +instance prod ::
19.61 (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
19.62 by default (simp_all add: expand_prod_eq)
19.63
19.64 -instance "*" ::
19.65 +instance prod ::
19.66 (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
19.67 by default (simp add: expand_prod_eq)
19.68
19.69 -instance "*" ::
19.70 +instance prod ::
19.71 (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
19.72
19.73 -instance "*" :: (group_add, group_add) group_add
19.74 +instance prod :: (group_add, group_add) group_add
19.75 by default (simp_all add: expand_prod_eq diff_minus)
19.76
19.77 -instance "*" :: (ab_group_add, ab_group_add) ab_group_add
19.78 +instance prod :: (ab_group_add, ab_group_add) ab_group_add
19.79 by default (simp_all add: expand_prod_eq)
19.80
19.81 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
20.1 --- a/src/HOL/Library/Quotient_Product.thy Thu Jul 01 16:54:42 2010 +0200
20.2 +++ b/src/HOL/Library/Quotient_Product.thy Thu Jul 01 16:54:44 2010 +0200
20.3 @@ -13,7 +13,7 @@
20.4 where
20.5 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
20.6
20.7 -declare [[map * = (prod_fun, prod_rel)]]
20.8 +declare [[map prod = (prod_fun, prod_rel)]]
20.9
20.10
20.11 lemma prod_equivp[quot_equiv]:
21.1 --- a/src/HOL/Library/Quotient_Sum.thy Thu Jul 01 16:54:42 2010 +0200
21.2 +++ b/src/HOL/Library/Quotient_Sum.thy Thu Jul 01 16:54:44 2010 +0200
21.3 @@ -22,7 +22,7 @@
21.4 "sum_map f1 f2 (Inl a) = Inl (f1 a)"
21.5 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
21.6
21.7 -declare [[map "+" = (sum_map, sum_rel)]]
21.8 +declare [[map sum = (sum_map, sum_rel)]]
21.9
21.10
21.11 text {* should probably be in @{theory Sum_Type} *}
22.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jul 01 16:54:42 2010 +0200
22.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jul 01 16:54:44 2010 +0200
22.3 @@ -5,7 +5,7 @@
22.4 imports Finite_Cartesian_Product Integration
22.5 begin
22.6
22.7 -instantiation * :: (real_basis, real_basis) real_basis
22.8 +instantiation prod :: (real_basis, real_basis) real_basis
22.9 begin
22.10
22.11 definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
22.12 @@ -131,7 +131,7 @@
22.13 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
22.14 by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
22.15
22.16 -instance * :: (euclidean_space, euclidean_space) euclidean_space
22.17 +instance prod :: (euclidean_space, euclidean_space) euclidean_space
22.18 proof (default, safe)
22.19 let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
22.20 fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
22.21 @@ -139,7 +139,7 @@
22.22 unfolding basis_prod_def by (auto simp: dot_basis)
22.23 qed
22.24
22.25 -instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
22.26 +instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
22.27 begin
22.28
22.29 definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"
23.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 16:54:42 2010 +0200
23.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 16:54:44 2010 +0200
23.3 @@ -2422,7 +2422,7 @@
23.4 apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
23.5 done
23.6
23.7 -instance "*" :: (heine_borel, heine_borel) heine_borel
23.8 +instance prod :: (heine_borel, heine_borel) heine_borel
23.9 proof
23.10 fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
23.11 assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
24.1 --- a/src/HOL/Nominal/nominal_atoms.ML Thu Jul 01 16:54:42 2010 +0200
24.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu Jul 01 16:54:44 2010 +0200
24.3 @@ -543,7 +543,7 @@
24.4 |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
24.5 |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
24.6 |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
24.7 - |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
24.8 + |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
24.9 |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
24.10 (pt_proof pt_thm_nprod)
24.11 |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
24.12 @@ -604,7 +604,7 @@
24.13 in
24.14 thy
24.15 |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
24.16 - |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
24.17 + |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
24.18 |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
24.19 (fs_proof fs_thm_nprod)
24.20 |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
24.21 @@ -686,7 +686,7 @@
24.22 in
24.23 thy'
24.24 |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
24.25 - |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
24.26 + |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
24.27 |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
24.28 |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
24.29 |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
25.1 --- a/src/HOL/Nominal/nominal_permeq.ML Thu Jul 01 16:54:42 2010 +0200
25.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jul 01 16:54:44 2010 +0200
25.3 @@ -103,7 +103,7 @@
25.4 case redex of
25.5 (* case pi o (f x) == (pi o f) (pi o x) *)
25.6 (Const("Nominal.perm",
25.7 - Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
25.8 + Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
25.9 (if (applicable_app f) then
25.10 let
25.11 val name = Long_Name.base_name n
25.12 @@ -190,8 +190,8 @@
25.13 fun perm_compose_simproc' sg ss redex =
25.14 (case redex of
25.15 (Const ("Nominal.perm", Type ("fun", [Type ("List.list",
25.16 - [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
25.17 - Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $
25.18 + [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
25.19 + Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
25.20 pi2 $ t)) =>
25.21 let
25.22 val tname' = Long_Name.base_name tname
26.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:42 2010 +0200
26.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Jul 01 16:54:44 2010 +0200
26.3 @@ -103,7 +103,7 @@
26.4 let fun get_pi_aux s =
26.5 (case s of
26.6 (Const (@{const_name "perm"} ,typrm) $
26.7 - (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
26.8 + (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
26.9 (Var (n,ty))) =>
26.10 let
26.11 (* FIXME: this should be an operation the library *)
27.1 --- a/src/HOL/Product_Type.thy Thu Jul 01 16:54:42 2010 +0200
27.2 +++ b/src/HOL/Product_Type.thy Thu Jul 01 16:54:44 2010 +0200
27.3 @@ -129,7 +129,7 @@
27.4 definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
27.5 "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
27.6
27.7 -typedef (prod) ('a, 'b) "*" (infixr "*" 20)
27.8 +typedef ('a, 'b) prod (infixr "*" 20)
27.9 = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
27.10 proof
27.11 fix a b show "Pair_Rep a b \<in> ?prod"
27.12 @@ -137,14 +137,14 @@
27.13 qed
27.14
27.15 type_notation (xsymbols)
27.16 - "*" ("(_ \<times>/ _)" [21, 20] 20)
27.17 + "prod" ("(_ \<times>/ _)" [21, 20] 20)
27.18 type_notation (HTML output)
27.19 - "*" ("(_ \<times>/ _)" [21, 20] 20)
27.20 + "prod" ("(_ \<times>/ _)" [21, 20] 20)
27.21
27.22 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
27.23 "Pair a b = Abs_prod (Pair_Rep a b)"
27.24
27.25 -rep_datatype (prod) Pair proof -
27.26 +rep_datatype Pair proof -
27.27 fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
27.28 assume "\<And>a b. P (Pair a b)"
27.29 then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
27.30 @@ -263,7 +263,7 @@
27.31
27.32 subsubsection {* Code generator setup *}
27.33
27.34 -code_type *
27.35 +code_type prod
27.36 (SML infix 2 "*")
27.37 (OCaml infix 2 "*")
27.38 (Haskell "!((_),/ (_))")
27.39 @@ -275,19 +275,19 @@
27.40 (Haskell "!((_),/ (_))")
27.41 (Scala "!((_),/ (_))")
27.42
27.43 -code_instance * :: eq
27.44 +code_instance prod :: eq
27.45 (Haskell -)
27.46
27.47 code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
27.48 (Haskell infixl 4 "==")
27.49
27.50 types_code
27.51 - "*" ("(_ */ _)")
27.52 + "prod" ("(_ */ _)")
27.53 attach (term_of) {*
27.54 -fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
27.55 +fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
27.56 *}
27.57 attach (test) {*
27.58 -fun gen_id_42 aG aT bG bT i =
27.59 +fun term_of_prod aG aT bG bT i =
27.60 let
27.61 val (x, t) = aG i;
27.62 val (y, u) = bG i
27.63 @@ -438,7 +438,7 @@
27.64
27.65 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
27.66 -- {* Prevents simplification of @{term c}: much faster *}
27.67 - by (erule arg_cong)
27.68 + by (fact weak_case_cong)
27.69
27.70 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
27.71 by (simp add: split_eta)
27.72 @@ -689,19 +689,18 @@
27.73 lemmas prod_caseI = prod.cases [THEN iffD2, standard]
27.74
27.75 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
27.76 - by auto
27.77 + by (fact splitI2)
27.78
27.79 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
27.80 - by (auto simp: split_tupled_all)
27.81 + by (fact splitI2')
27.82
27.83 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
27.84 - by (induct p) auto
27.85 + by (fact splitE)
27.86
27.87 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
27.88 - by (induct p) auto
27.89 + by (fact splitE')
27.90
27.91 -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
27.92 -declare prod_caseE' [elim!] prod_caseE [elim!]
27.93 +declare prod_caseI [intro!]
27.94
27.95 lemma prod_case_beta:
27.96 "prod_case f p = f (fst p) (snd p)"
27.97 @@ -795,8 +794,11 @@
27.98 definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
27.99 "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
27.100
27.101 +lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
27.102 + by (simp add: expand_fun_eq scomp_def split_def)
27.103 +
27.104 lemma scomp_apply: "(f o\<rightarrow> g) x = split g (f x)"
27.105 - by (simp add: scomp_def)
27.106 + by (simp add: scomp_unfold split_def)
27.107
27.108 lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
27.109 by (simp add: expand_fun_eq scomp_apply)
27.110 @@ -805,13 +807,13 @@
27.111 by (simp add: expand_fun_eq scomp_apply)
27.112
27.113 lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
27.114 - by (simp add: expand_fun_eq split_twice scomp_def)
27.115 + by (simp add: expand_fun_eq scomp_unfold)
27.116
27.117 lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
27.118 - by (simp add: expand_fun_eq scomp_apply fcomp_def split_def)
27.119 + by (simp add: expand_fun_eq scomp_unfold fcomp_def)
27.120
27.121 lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
27.122 - by (simp add: expand_fun_eq scomp_apply fcomp_apply)
27.123 + by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
27.124
27.125 code_const scomp
27.126 (Eval infixl 3 "#->")
28.1 --- a/src/HOL/Sum_Type.thy Thu Jul 01 16:54:42 2010 +0200
28.2 +++ b/src/HOL/Sum_Type.thy Thu Jul 01 16:54:44 2010 +0200
28.3 @@ -17,7 +17,7 @@
28.4 definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
28.5 "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
28.6
28.7 -typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
28.8 +typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
28.9 by auto
28.10
28.11 lemma Inl_RepI: "Inl_Rep a \<in> sum"
28.12 @@ -83,7 +83,7 @@
28.13 with assms show P by (auto simp add: sum_def Inl_def Inr_def)
28.14 qed
28.15
28.16 -rep_datatype (sum) Inl Inr
28.17 +rep_datatype Inl Inr
28.18 proof -
28.19 fix P
28.20 fix s :: "'a + 'b"
29.1 --- a/src/HOL/TLA/Action.thy Thu Jul 01 16:54:42 2010 +0200
29.2 +++ b/src/HOL/TLA/Action.thy Thu Jul 01 16:54:44 2010 +0200
29.3 @@ -16,8 +16,7 @@
29.4 'a trfun = "(state * state) => 'a"
29.5 action = "bool trfun"
29.6
29.7 -arities
29.8 - "*" :: (world, world) world
29.9 +arities prod :: (world, world) world
29.10
29.11 consts
29.12 (** abstract syntax **)
30.1 --- a/src/HOL/Tools/Datatype/datatype.ML Thu Jul 01 16:54:42 2010 +0200
30.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Jul 01 16:54:44 2010 +0200
30.3 @@ -75,7 +75,7 @@
30.4 val leafTs' = get_nonrec_types descr' sorts;
30.5 val branchTs = get_branching_types descr' sorts;
30.6 val branchT = if null branchTs then HOLogic.unitT
30.7 - else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs;
30.8 + else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
30.9 val arities = remove (op =) 0 (get_arities descr');
30.10 val unneeded_vars =
30.11 subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
30.12 @@ -83,7 +83,7 @@
30.13 val recTs = get_rec_types descr' sorts;
30.14 val (newTs, oldTs) = chop (length (hd descr)) recTs;
30.15 val sumT = if null leafTs then HOLogic.unitT
30.16 - else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs;
30.17 + else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
30.18 val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
30.19 val UnivT = HOLogic.mk_setT Univ_elT;
30.20 val UnivT' = Univ_elT --> HOLogic.boolT;
31.1 --- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 01 16:54:42 2010 +0200
31.2 +++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jul 01 16:54:44 2010 +0200
31.3 @@ -39,17 +39,17 @@
31.4 fun constant_0 T = Abs ("x", T, HOLogic.zero)
31.5 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
31.6
31.7 -fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
31.8 +fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
31.9 map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
31.10 @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
31.11 | mk_funorder_funs T = [ constant_1 T ]
31.12
31.13 -fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
31.14 +fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
31.15 map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
31.16 (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
31.17 | mk_ext_base_funs ctxt T = find_measures ctxt T
31.18
31.19 -fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
31.20 +fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
31.21 mk_ext_base_funs ctxt T @ mk_funorder_funs T
31.22 | mk_all_measure_funs ctxt T = find_measures ctxt T
31.23
32.1 --- a/src/HOL/Tools/Function/sum_tree.ML Thu Jul 01 16:54:42 2010 +0200
32.2 +++ b/src/HOL/Tools/Function/sum_tree.ML Thu Jul 01 16:54:44 2010 +0200
32.3 @@ -17,7 +17,7 @@
32.4 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
32.5
32.6 (* Sum types *)
32.7 -fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT])
32.8 +fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT])
32.9 fun mk_sumcase TL TR T l r =
32.10 Const (@{const_name sum.sum_case},
32.11 (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
32.12 @@ -27,18 +27,18 @@
32.13 fun mk_inj ST n i =
32.14 access_top_down
32.15 { init = (ST, I : term -> term),
32.16 - left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
32.17 + left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
32.18 (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
32.19 - right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
32.20 + right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
32.21 (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
32.22 |> snd
32.23
32.24 fun mk_proj ST n i =
32.25 access_top_down
32.26 { init = (ST, I : term -> term),
32.27 - left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
32.28 + left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
32.29 (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
32.30 - right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
32.31 + right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
32.32 (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
32.33 |> snd
32.34
33.1 --- a/src/HOL/Tools/Function/termination.ML Thu Jul 01 16:54:42 2010 +0200
33.2 +++ b/src/HOL/Tools/Function/termination.ML Thu Jul 01 16:54:44 2010 +0200
33.3 @@ -106,7 +106,7 @@
33.4 end
33.5
33.6 (* compute list of types for nodes *)
33.7 -fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
33.8 +fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd
33.9
33.10 (* find index and raw term *)
33.11 fun dest_inj (SLeaf i) trm = (i, trm)
34.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Thu Jul 01 16:54:42 2010 +0200
34.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Jul 01 16:54:44 2010 +0200
34.3 @@ -37,7 +37,7 @@
34.4
34.5 fun check_type ctxt (Type (@{type_name fun}, Ts)) =
34.6 List.app (check_type ctxt) Ts
34.7 - | check_type ctxt (Type (@{type_name "*"}, Ts)) =
34.8 + | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) =
34.9 List.app (check_type ctxt) Ts
34.10 | check_type _ @{typ bool} = ()
34.11 | check_type _ (TFree (_, @{sort "{}"})) = ()
34.12 @@ -51,7 +51,7 @@
34.13 atom_schema_of SRep card T1
34.14 | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
34.15 atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
34.16 - | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
34.17 + | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) =
34.18 maps (atom_schema_of SRep card) Ts
34.19 | atom_schema_of _ card T = [card T]
34.20 val arity_of = length ooo atom_schema_of
34.21 @@ -290,7 +290,7 @@
34.22 val thy = ProofContext.theory_of ctxt
34.23 fun card (Type (@{type_name fun}, [T1, T2])) =
34.24 reasonable_power (card T2) (card T1)
34.25 - | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
34.26 + | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2
34.27 | card @{typ bool} = 2
34.28 | card T = Int.max (1, raw_card T)
34.29 val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
35.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:42 2010 +0200
35.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 01 16:54:44 2010 +0200
35.3 @@ -454,7 +454,7 @@
35.4 | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
35.5 unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
35.6 | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
35.7 - Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
35.8 + Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts)
35.9 | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
35.10 | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
35.11 | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
35.12 @@ -509,7 +509,7 @@
35.13 | is_fun_type _ = false
35.14 fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
35.15 | is_set_type _ = false
35.16 -fun is_pair_type (Type (@{type_name "*"}, _)) = true
35.17 +fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
35.18 | is_pair_type _ = false
35.19 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
35.20 | is_lfp_iterator_type _ = false
35.21 @@ -546,7 +546,7 @@
35.22 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
35.23 val nth_range_type = snd oo strip_n_binders
35.24
35.25 -fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
35.26 +fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) =
35.27 fold (Integer.add o num_factors_in_type) [T1, T2] 0
35.28 | num_factors_in_type _ = 1
35.29 fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
35.30 @@ -557,7 +557,7 @@
35.31 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
35.32
35.33 fun mk_flat_tuple _ [t] = t
35.34 - | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
35.35 + | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) =
35.36 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
35.37 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
35.38 fun dest_n_tuple 1 t = [t]
35.39 @@ -595,7 +595,7 @@
35.40 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
35.41 e.g., by adding a field to "Datatype_Aux.info". *)
35.42 fun is_basic_datatype thy stds s =
35.43 - member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
35.44 + member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit},
35.45 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
35.46 (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
35.47
35.48 @@ -792,7 +792,7 @@
35.49 Type (@{type_name fun}, _) =>
35.50 (boxy = InPair orelse boxy = InFunLHS) andalso
35.51 not (is_boolean_type (body_type T))
35.52 - | Type (@{type_name "*"}, Ts) =>
35.53 + | Type (@{type_name Product_Type.prod}, Ts) =>
35.54 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
35.55 ((boxy = InExpr orelse boxy = InFunLHS) andalso
35.56 exists (is_boxing_worth_it hol_ctxt InPair)
35.57 @@ -812,12 +812,12 @@
35.58 else
35.59 box_type hol_ctxt (in_fun_lhs_for boxy) T1
35.60 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
35.61 - | Type (z as (@{type_name "*"}, Ts)) =>
35.62 + | Type (z as (@{type_name Product_Type.prod}, Ts)) =>
35.63 if boxy <> InConstr andalso boxy <> InSel
35.64 andalso should_box_type hol_ctxt boxy z then
35.65 Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
35.66 else
35.67 - Type (@{type_name "*"},
35.68 + Type (@{type_name Product_Type.prod},
35.69 map (box_type hol_ctxt
35.70 (if boxy = InConstr orelse boxy = InSel then boxy
35.71 else InPair)) Ts)
35.72 @@ -979,7 +979,7 @@
35.73 Const (nth_sel_for_constr x n)
35.74 else
35.75 let
35.76 - fun aux m (Type (@{type_name "*"}, [T1, T2])) =
35.77 + fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
35.78 let
35.79 val (m, t1) = aux m T1
35.80 val (m, t2) = aux m T2
35.81 @@ -1069,7 +1069,7 @@
35.82 | (Type (new_s, new_Ts as [new_T1, new_T2]),
35.83 Type (old_s, old_Ts as [old_T1, old_T2])) =>
35.84 if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
35.85 - old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
35.86 + old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
35.87 case constr_expand hol_ctxt old_T t of
35.88 Const (old_s, _) $ t1 =>
35.89 if new_s = @{type_name fun} then
35.90 @@ -1081,7 +1081,7 @@
35.91 (Type (@{type_name fun}, old_Ts)) t1]
35.92 | Const _ $ t1 $ t2 =>
35.93 construct_value ctxt stds
35.94 - (if new_s = @{type_name "*"} then @{const_name Pair}
35.95 + (if new_s = @{type_name Product_Type.prod} then @{const_name Pair}
35.96 else @{const_name PairBox}, new_Ts ---> new_T)
35.97 (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
35.98 [t1, t2])
35.99 @@ -1092,7 +1092,7 @@
35.100
35.101 fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
35.102 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
35.103 - | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
35.104 + | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) =
35.105 card_of_type assigns T1 * card_of_type assigns T2
35.106 | card_of_type _ (Type (@{type_name itself}, _)) = 1
35.107 | card_of_type _ @{typ prop} = 2
35.108 @@ -1113,7 +1113,7 @@
35.109 else Int.min (max, reasonable_power k2 k1)
35.110 end
35.111 | bounded_card_of_type max default_card assigns
35.112 - (Type (@{type_name "*"}, [T1, T2])) =
35.113 + (Type (@{type_name Product_Type.prod}, [T1, T2])) =
35.114 let
35.115 val k1 = bounded_card_of_type max default_card assigns T1
35.116 val k2 = bounded_card_of_type max default_card assigns T2
35.117 @@ -1143,7 +1143,7 @@
35.118 else if k1 >= max orelse k2 >= max then max
35.119 else Int.min (max, reasonable_power k2 k1)
35.120 end
35.121 - | Type (@{type_name "*"}, [T1, T2]) =>
35.122 + | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
35.123 let
35.124 val k1 = aux avoid T1
35.125 val k2 = aux avoid T2
35.126 @@ -1196,7 +1196,7 @@
35.127 fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
35.128
35.129 fun is_funky_typedef_name thy s =
35.130 - member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
35.131 + member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum},
35.132 @{type_name int}] s orelse
35.133 is_frac_type thy (Type (s, []))
35.134 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
35.135 @@ -2066,7 +2066,7 @@
35.136 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
35.137 val set_T = tuple_T --> bool_T
35.138 val curried_T = tuple_T --> set_T
35.139 - val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
35.140 + val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T
35.141 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
35.142 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
35.143 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
35.144 @@ -2185,7 +2185,7 @@
35.145 fun aux T accum =
35.146 case T of
35.147 Type (@{type_name fun}, Ts) => fold aux Ts accum
35.148 - | Type (@{type_name "*"}, Ts) => fold aux Ts accum
35.149 + | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum
35.150 | Type (@{type_name itself}, [T1]) => aux T1 accum
35.151 | Type (_, Ts) =>
35.152 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
36.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 01 16:54:42 2010 +0200
36.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 01 16:54:44 2010 +0200
36.3 @@ -170,7 +170,7 @@
36.4 Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
36.5 $ t1 $ t2) =
36.6 let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
36.7 - Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
36.8 + Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts))
36.9 $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
36.10 end
36.11 | unarize_unbox_etc_term (Const (s, T)) =
36.12 @@ -185,27 +185,27 @@
36.13 | unarize_unbox_etc_term (Abs (s, T, t')) =
36.14 Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
36.15
36.16 -fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
36.17 - (T2 as Type (@{type_name "*"}, [T21, T22])) =
36.18 +fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12]))
36.19 + (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) =
36.20 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
36.21 if n1 = n2 then
36.22 let
36.23 val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
36.24 in
36.25 - ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
36.26 - (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
36.27 + ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'),
36.28 + (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22'))
36.29 end
36.30 else if n1 < n2 then
36.31 case factor_out_types T1 T21 of
36.32 (p1, (T21', NONE)) => (p1, (T21', SOME T22))
36.33 | (p1, (T21', SOME T22')) =>
36.34 - (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
36.35 + (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22]))))
36.36 else
36.37 swap (factor_out_types T2 T1)
36.38 end
36.39 - | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
36.40 + | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 =
36.41 ((T11, SOME T12), (T2, NONE))
36.42 - | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
36.43 + | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) =
36.44 ((T1, NONE), (T21, SOME T22))
36.45 | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
36.46
36.47 @@ -239,7 +239,7 @@
36.48 val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
36.49 val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
36.50 in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
36.51 -fun pair_up (Type (@{type_name "*"}, [T1', T2']))
36.52 +fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2']))
36.53 (t1 as Const (@{const_name Pair},
36.54 Type (@{type_name fun},
36.55 [_, Type (@{type_name fun}, [_, T1])]))
36.56 @@ -287,8 +287,8 @@
36.57 and do_term (Type (@{type_name fun}, [T1', T2']))
36.58 (Type (@{type_name fun}, [T1, T2])) t =
36.59 do_fun T1' T2' T1 T2 t
36.60 - | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
36.61 - (Type (@{type_name "*"}, [T1, T2]))
36.62 + | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2']))
36.63 + (Type (@{type_name Product_Type.prod}, [T1, T2]))
36.64 (Const (@{const_name Pair}, _) $ t1 $ t2) =
36.65 Const (@{const_name Pair}, Ts' ---> T')
36.66 $ do_term T1' T1 t1 $ do_term T2' T2 t2
36.67 @@ -303,7 +303,7 @@
36.68 | truth_const_sort_key @{const False} = "2"
36.69 | truth_const_sort_key _ = "1"
36.70
36.71 -fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
36.72 +fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts =
36.73 HOLogic.mk_prod (mk_tuple T1 ts,
36.74 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
36.75 | mk_tuple _ (t :: _) = t
36.76 @@ -463,7 +463,7 @@
36.77 signed_string_of_int j ^ " for " ^
36.78 string_for_rep (Vect (k1, Atom (k2, 0))))
36.79 end
36.80 - | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
36.81 + | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k =
36.82 let
36.83 val k1 = card_of_type card_assigns T1
36.84 val k2 = k div k1
36.85 @@ -592,7 +592,7 @@
36.86 | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
36.87 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
36.88 else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
36.89 - | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
36.90 + | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _
36.91 (Struct [R1, R2]) [js] =
36.92 let
36.93 val arity1 = arity_of_rep R1
37.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jul 01 16:54:42 2010 +0200
37.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jul 01 16:54:44 2010 +0200
37.3 @@ -254,7 +254,7 @@
37.4 else case T of
37.5 Type (@{type_name fun}, [T1, T2]) =>
37.6 MFun (fresh_mfun_for_fun_type mdata false T1 T2)
37.7 - | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
37.8 + | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
37.9 | Type (z as (s, _)) =>
37.10 if could_exist_alpha_sub_mtype ctxt alpha_T T then
37.11 case AList.lookup (op =) (!datatype_mcache) z of
37.12 @@ -1035,8 +1035,8 @@
37.13 | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
37.14 Type (if should_finitize T a then @{type_name fin_fun}
37.15 else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
37.16 - | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
37.17 - Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
37.18 + | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
37.19 + Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
37.20 | (MType _, _) => T
37.21 | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
37.22 [M], [T])
38.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jul 01 16:54:42 2010 +0200
38.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jul 01 16:54:44 2010 +0200
38.3 @@ -427,7 +427,7 @@
38.4 let val res_T = snd (HOLogic.dest_prodT T) in
38.5 (res_T, Const (@{const_name snd}, T --> res_T) $ t)
38.6 end
38.7 -fun factorize (z as (Type (@{type_name "*"}, _), _)) =
38.8 +fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) =
38.9 maps factorize [mk_fst z, mk_snd z]
38.10 | factorize z = [z]
38.11
38.12 @@ -1199,7 +1199,7 @@
38.13 val w = constr (j, type_of v, rep_of v)
38.14 in (w :: ws, pool, NameTable.update (v, w) table) end
38.15
38.16 -fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
38.17 +fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2])
38.18 us =
38.19 let val arity1 = arity_of_rep R1 in
38.20 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
39.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 01 16:54:42 2010 +0200
39.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 01 16:54:44 2010 +0200
39.3 @@ -132,8 +132,8 @@
39.4 let
39.5 fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
39.6 Type (@{type_name fun}, map box_relational_operator_type Ts)
39.7 - | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
39.8 - Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
39.9 + | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) =
39.10 + Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts)
39.11 | box_relational_operator_type T = T
39.12 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
39.13 case t' of
39.14 @@ -953,7 +953,7 @@
39.15 and add_axioms_for_type depth T =
39.16 case T of
39.17 Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
39.18 - | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
39.19 + | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
39.20 | @{typ prop} => I
39.21 | @{typ bool} => I
39.22 | @{typ unit} => I
40.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jul 01 16:54:42 2010 +0200
40.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jul 01 16:54:44 2010 +0200
40.3 @@ -249,7 +249,7 @@
40.4 (case best_one_rep_for_type scope T2 of
40.5 Unit => Unit
40.6 | R2 => Vect (card_of_type card_assigns T1, R2))
40.7 - | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
40.8 + | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) =
40.9 (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
40.10 (Unit, Unit) => Unit
40.11 | (R1, R2) => Struct [R1, R2])
40.12 @@ -302,7 +302,7 @@
40.13 fun type_schema_of_rep _ (Formula _) = []
40.14 | type_schema_of_rep _ Unit = []
40.15 | type_schema_of_rep T (Atom _) = [T]
40.16 - | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
40.17 + | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) =
40.18 type_schema_of_reps [T1, T2] [R1, R2]
40.19 | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
40.20 replicate_list k (type_schema_of_rep T2 R)
41.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:42 2010 +0200
41.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:44 2010 +0200
41.3 @@ -107,7 +107,7 @@
41.4 is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
41.5 | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
41.6 is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
41.7 - | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
41.8 + | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
41.9 forall (is_complete_type dtypes facto) Ts
41.10 | is_complete_type dtypes facto T =
41.11 not (is_integer_like_type T) andalso not (is_bit_type T) andalso
41.12 @@ -117,7 +117,7 @@
41.13 is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
41.14 | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
41.15 is_concrete_type dtypes facto T2
41.16 - | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
41.17 + | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
41.18 forall (is_concrete_type dtypes facto) Ts
41.19 | is_concrete_type dtypes facto T =
41.20 fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
42.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jul 01 16:54:42 2010 +0200
42.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jul 01 16:54:44 2010 +0200
42.3 @@ -210,7 +210,7 @@
42.4 else
42.5 [Input, Output]
42.6 end
42.7 - | all_modes_of_typ' (Type (@{type_name "*"}, [T1, T2])) =
42.8 + | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) =
42.9 map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
42.10 | all_modes_of_typ' _ = [Input, Output]
42.11
42.12 @@ -230,7 +230,7 @@
42.13 fun all_smodes_of_typ (T as Type ("fun", _)) =
42.14 let
42.15 val (S, U) = strip_type T
42.16 - fun all_smodes (Type (@{type_name "*"}, [T1, T2])) =
42.17 + fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) =
42.18 map_product (curry Pair) (all_smodes T1) (all_smodes T2)
42.19 | all_smodes _ = [Input, Output]
42.20 in
42.21 @@ -280,7 +280,7 @@
42.22 fun ho_argsT_of mode Ts =
42.23 let
42.24 fun ho_arg (Fun _) T = [T]
42.25 - | ho_arg (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
42.26 + | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
42.27 | ho_arg _ _ = []
42.28 in
42.29 flat (map2 ho_arg (strip_fun_mode mode) Ts)
42.30 @@ -309,7 +309,7 @@
42.31 fun split_map_modeT f mode Ts =
42.32 let
42.33 fun split_arg_mode' (m as Fun _) T = f m T
42.34 - | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
42.35 + | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
42.36 let
42.37 val (i1, o1) = split_arg_mode' m1 T1
42.38 val (i2, o2) = split_arg_mode' m2 T2
42.39 @@ -325,7 +325,7 @@
42.40
42.41 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
42.42
42.43 -fun fold_map_aterms_prodT comb f (Type (@{type_name "*"}, [T1, T2])) s =
42.44 +fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s =
42.45 let
42.46 val (x1, s') = fold_map_aterms_prodT comb f T1 s
42.47 val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
42.48 @@ -343,7 +343,7 @@
42.49 fun split_modeT' mode Ts =
42.50 let
42.51 fun split_arg_mode' (Fun _) T = ([], [])
42.52 - | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
42.53 + | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
42.54 let
42.55 val (i1, o1) = split_arg_mode' m1 T1
42.56 val (i2, o2) = split_arg_mode' m2 T2
42.57 @@ -756,9 +756,9 @@
42.58 (case HOLogic.strip_tupleT (fastype_of arg) of
42.59 (Ts as _ :: _ :: _) =>
42.60 let
42.61 - fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
42.62 + fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
42.63 (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
42.64 - | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
42.65 + | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
42.66 let
42.67 val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
42.68 val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
43.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Jul 01 16:54:42 2010 +0200
43.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Jul 01 16:54:44 2010 +0200
43.3 @@ -70,7 +70,7 @@
43.4 fun mk_randompredT T =
43.5 @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
43.6
43.7 -fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
43.8 +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
43.9 [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
43.10 | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
43.11
43.12 @@ -278,7 +278,7 @@
43.13
43.14 fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
43.15 Type ("fun", [@{typ Random.seed},
43.16 - Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
43.17 + Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
43.18 | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
43.19
43.20 fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
44.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jul 01 16:54:42 2010 +0200
44.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jul 01 16:54:44 2010 +0200
44.3 @@ -117,7 +117,7 @@
44.4 end;
44.5
44.6 fun dest_randomT (Type ("fun", [@{typ Random.seed},
44.7 - Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
44.8 + Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
44.9 | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
44.10
44.11 fun mk_tracing s t =
44.12 @@ -467,7 +467,7 @@
44.13
44.14 (* generation of case rules from user-given introduction rules *)
44.15
44.16 -fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st =
44.17 +fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
44.18 let
44.19 val (t1, st') = mk_args2 T1 st
44.20 val (t2, st'') = mk_args2 T2 st'
44.21 @@ -1099,7 +1099,7 @@
44.22 fun all_input_of T =
44.23 let
44.24 val (Ts, U) = strip_type T
44.25 - fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2)
44.26 + fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2)
44.27 | input_of _ = Input
44.28 in
44.29 if U = HOLogic.boolT then
44.30 @@ -2019,7 +2019,7 @@
44.31 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
44.32 | strip_split_abs t = t
44.33
44.34 -fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names =
44.35 +fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
44.36 if eq_mode (m, Input) orelse eq_mode (m, Output) then
44.37 let
44.38 val x = Name.variant names "x"
45.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML Thu Jul 01 16:54:42 2010 +0200
45.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Thu Jul 01 16:54:44 2010 +0200
45.3 @@ -36,7 +36,7 @@
45.4
45.5 val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
45.6
45.7 -val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
45.8 +val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
45.9 val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
45.10
45.11 val add_pair_rules = exists_pair_type ?? append pair_rules
46.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 16:54:42 2010 +0200
46.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 01 16:54:44 2010 +0200
46.3 @@ -96,13 +96,13 @@
46.4 (* Readable names for the more common symbolic functions. Do not mess with the
46.5 last nine entries of the table unless you know what you are doing. *)
46.6 val const_trans_table =
46.7 - Symtab.make [(@{type_name "*"}, "prod"),
46.8 - (@{type_name "+"}, "sum"),
46.9 + Symtab.make [(@{type_name Product_Type.prod}, "prod"),
46.10 + (@{type_name Sum_Type.sum}, "sum"),
46.11 (@{const_name "op ="}, "equal"),
46.12 (@{const_name "op &"}, "and"),
46.13 (@{const_name "op |"}, "or"),
46.14 (@{const_name "op -->"}, "implies"),
46.15 - (@{const_name "op :"}, "in"),
46.16 + (@{const_name Set.member}, "in"),
46.17 (@{const_name fequal}, "fequal"),
46.18 (@{const_name COMBI}, "COMBI"),
46.19 (@{const_name COMBK}, "COMBK"),
47.1 --- a/src/HOL/Tools/TFL/rules.ML Thu Jul 01 16:54:42 2010 +0200
47.2 +++ b/src/HOL/Tools/TFL/rules.ML Thu Jul 01 16:54:44 2010 +0200
47.3 @@ -591,10 +591,10 @@
47.4
47.5 local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
47.6 fun mk_fst tm =
47.7 - let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
47.8 + let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
47.9 in Const ("Product_Type.fst", ty --> fty) $ tm end
47.10 fun mk_snd tm =
47.11 - let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
47.12 + let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
47.13 in Const ("Product_Type.snd", ty --> sty) $ tm end
47.14 in
47.15 fun XFILL tych x vstruct =
48.1 --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jul 01 16:54:42 2010 +0200
48.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jul 01 16:54:44 2010 +0200
48.3 @@ -372,7 +372,7 @@
48.4 (* Miscellaneous *)
48.5
48.6 fun mk_vstruct ty V =
48.7 - let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs =
48.8 + let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
48.9 let val (ltm,vs1) = follow_prod_type ty1 vs
48.10 val (rtm,vs2) = follow_prod_type ty2 vs1
48.11 in (mk_pair{fst=ltm, snd=rtm}, vs2) end
48.12 @@ -393,7 +393,7 @@
48.13
48.14 fun dest_relation tm =
48.15 if (type_of tm = HOLogic.boolT)
48.16 - then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
48.17 + then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
48.18 in (R,y,x)
48.19 end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
48.20 else raise USYN_ERR "dest_relation" "not a boolean term";
49.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 01 16:54:42 2010 +0200
49.2 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 01 16:54:44 2010 +0200
49.3 @@ -173,7 +173,7 @@
49.4 (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
49.5 end
49.6 else (case strip_type T of
49.7 - (Ts, Type (@{type_name "*"}, [T1, T2])) =>
49.8 + (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
49.9 let
49.10 val fx = Free (x, Ts ---> T1);
49.11 val fr = Free (r, Ts ---> T2);
50.1 --- a/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:42 2010 +0200
50.2 +++ b/src/HOL/Tools/split_rule.ML Thu Jul 01 16:54:44 2010 +0200
50.3 @@ -31,7 +31,7 @@
50.4 (*In ap_split S T u, term u expects separate arguments for the factors of S,
50.5 with result type T. The call creates a new term expecting one argument
50.6 of type S.*)
50.7 -fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
50.8 +fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
50.9 internal_split_const (T1, T2, T3) $
50.10 Abs ("v", T1,
50.11 ap_split T2 T3
51.1 --- a/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:42 2010 +0200
51.2 +++ b/src/HOLCF/Bifinite.thy Thu Jul 01 16:54:44 2010 +0200
51.3 @@ -161,7 +161,7 @@
51.4 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
51.5 qed
51.6
51.7 -instantiation "*" :: (profinite, profinite) profinite
51.8 +instantiation prod :: (profinite, profinite) profinite
51.9 begin
51.10
51.11 definition
51.12 @@ -187,7 +187,7 @@
51.13
51.14 end
51.15
51.16 -instance "*" :: (bifinite, bifinite) bifinite ..
51.17 +instance prod :: (bifinite, bifinite) bifinite ..
51.18
51.19 lemma approx_Pair [simp]:
51.20 "approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
52.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 01 16:54:42 2010 +0200
52.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 01 16:54:44 2010 +0200
52.3 @@ -34,9 +34,9 @@
52.4
52.5 exception malformed;
52.6
52.7 -fun fst_type (Type(@{type_name "*"},[a,_])) = a |
52.8 +fun fst_type (Type(@{type_name prod},[a,_])) = a |
52.9 fst_type _ = raise malformed;
52.10 -fun snd_type (Type(@{type_name "*"},[_,a])) = a |
52.11 +fun snd_type (Type(@{type_name prod},[_,a])) = a |
52.12 snd_type _ = raise malformed;
52.13
52.14 fun element_type (Type("set",[a])) = a |
52.15 @@ -121,10 +121,10 @@
52.16
52.17 fun delete_ul_string s = implode(delete_ul (explode s));
52.18
52.19 -fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
52.20 +fun type_list_of sign (Type(@{type_name prod},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
52.21 type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
52.22
52.23 -fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
52.24 +fun structured_tuple l (Type(@{type_name prod},s::t::_)) =
52.25 let
52.26 val (r,str) = structured_tuple l s;
52.27 in
53.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jul 01 16:54:42 2010 +0200
53.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jul 01 16:54:44 2010 +0200
53.3 @@ -298,7 +298,7 @@
53.4 (string_of_typ thy t));
53.5
53.6 fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
53.7 -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]) |
53.8 +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) |
53.9 comp_st_type_of _ _ = error "empty automaton list";
53.10
53.11 (* checking consistency of action types (for composition) *)
53.12 @@ -378,25 +378,22 @@
53.13 end)
53.14
53.15 fun add_composition automaton_name aut_list thy =
53.16 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
53.17 -let
53.18 -val acttyp = check_ac thy aut_list;
53.19 -val st_typ = comp_st_type_of thy aut_list;
53.20 -val comp_list = clist aut_list;
53.21 -in
53.22 -thy
53.23 -|> Sign.add_consts_i
53.24 -[(Binding.name automaton_name,
53.25 -Type(@{type_name "*"},
53.26 -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
53.27 - Type(@{type_name "*"},[Type("set",[st_typ]),
53.28 - Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
53.29 - Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
53.30 -,NoSyn)]
53.31 -|> add_defs
53.32 -[(automaton_name ^ "_def",
53.33 -automaton_name ^ " == " ^ comp_list)]
53.34 -end)
53.35 + let
53.36 + val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
53.37 + val acttyp = check_ac thy aut_list;
53.38 + val st_typ = comp_st_type_of thy aut_list;
53.39 + val comp_list = clist aut_list;
53.40 + in
53.41 + thy
53.42 + |> Sign.add_consts_i
53.43 + [(Binding.name automaton_name, HOLogic.mk_prodT (HOLogic.mk_prodT
53.44 + (HOLogic.mk_setT acttyp, HOLogic.mk_prodT (HOLogic.mk_setT acttyp, HOLogic.mk_setT acttyp)),
53.45 + HOLogic.mk_prodT (HOLogic.mk_setT st_typ, HOLogic.mk_prodT (HOLogic.mk_setT
53.46 + (HOLogic.mk_prodT (st_typ, HOLogic.mk_prodT (acttyp, st_typ))),
53.47 + HOLogic.mk_prodT (HOLogic.mk_setT (HOLogic.mk_setT acttyp), HOLogic.mk_setT (HOLogic.mk_setT acttyp))))),
53.48 + NoSyn)]
53.49 + |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)]
53.50 + end
53.51
53.52 fun add_restriction automaton_name aut_source actlist thy =
53.53 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
53.54 @@ -433,25 +430,23 @@
53.55 | _ => error "could not extract argument type of renaming function term");
53.56
53.57 fun add_rename automaton_name aut_source fun_name thy =
53.58 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
53.59 -let
53.60 -val auttyp = aut_type_of thy aut_source;
53.61 -val st_typ = st_type_of thy auttyp;
53.62 -val acttyp = ren_act_type_of thy fun_name
53.63 -in
53.64 -thy
53.65 -|> Sign.add_consts_i
53.66 -[(Binding.name automaton_name,
53.67 -Type(@{type_name "*"},
53.68 -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
53.69 - Type(@{type_name "*"},[Type("set",[st_typ]),
53.70 - Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
53.71 - Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
53.72 -,NoSyn)]
53.73 -|> add_defs
53.74 -[(automaton_name ^ "_def",
53.75 -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
53.76 -end)
53.77 + let
53.78 + val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
53.79 + val auttyp = aut_type_of thy aut_source;
53.80 + val st_typ = st_type_of thy auttyp;
53.81 + val acttyp = ren_act_type_of thy fun_name
53.82 + in
53.83 + thy
53.84 + |> Sign.add_consts_i
53.85 + [(Binding.name automaton_name,
53.86 + Type(@{type_name prod},
53.87 + [Type(@{type_name prod},[HOLogic.mk_setT acttyp,Type(@{type_name prod},[HOLogic.mk_setT acttyp,HOLogic.mk_setT acttyp])]),
53.88 + Type(@{type_name prod},[HOLogic.mk_setT st_typ,
53.89 + Type(@{type_name prod},[HOLogic.mk_setT (Type(@{type_name prod},[st_typ,Type(@{type_name prod},[acttyp,st_typ])])),
53.90 + Type(@{type_name prod},[HOLogic.mk_setT (HOLogic.mk_setT acttyp),HOLogic.mk_setT (HOLogic.mk_setT acttyp)])])])])
53.91 + ,NoSyn)]
53.92 + |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
53.93 + end
53.94
53.95
53.96 (** outer syntax **)
54.1 --- a/src/HOLCF/Library/Sum_Cpo.thy Thu Jul 01 16:54:42 2010 +0200
54.2 +++ b/src/HOLCF/Library/Sum_Cpo.thy Thu Jul 01 16:54:44 2010 +0200
54.3 @@ -10,7 +10,7 @@
54.4
54.5 subsection {* Ordering on sum type *}
54.6
54.7 -instantiation "+" :: (below, below) below
54.8 +instantiation sum :: (below, below) below
54.9 begin
54.10
54.11 definition below_sum_def:
54.12 @@ -56,7 +56,7 @@
54.13
54.14 subsection {* Sum type is a complete partial order *}
54.15
54.16 -instance "+" :: (po, po) po
54.17 +instance sum :: (po, po) po
54.18 proof
54.19 fix x :: "'a + 'b"
54.20 show "x \<sqsubseteq> x"
54.21 @@ -117,7 +117,7 @@
54.22 apply (drule ub_rangeD, simp)
54.23 done
54.24
54.25 -instance "+" :: (cpo, cpo) cpo
54.26 +instance sum :: (cpo, cpo) cpo
54.27 apply intro_classes
54.28 apply (erule sum_chain_cases, safe)
54.29 apply (rule exI)
54.30 @@ -217,20 +217,20 @@
54.31 lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
54.32 by (safe elim!: compact_Inr compact_Inr_rev)
54.33
54.34 -instance "+" :: (chfin, chfin) chfin
54.35 +instance sum :: (chfin, chfin) chfin
54.36 apply intro_classes
54.37 apply (erule compact_imp_max_in_chain)
54.38 apply (case_tac "\<Squnion>i. Y i", simp_all)
54.39 done
54.40
54.41 -instance "+" :: (finite_po, finite_po) finite_po ..
54.42 +instance sum :: (finite_po, finite_po) finite_po ..
54.43
54.44 -instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
54.45 +instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
54.46 by intro_classes (simp add: below_sum_def split: sum.split)
54.47
54.48 subsection {* Sum type is a bifinite domain *}
54.49
54.50 -instantiation "+" :: (profinite, profinite) profinite
54.51 +instantiation sum :: (profinite, profinite) profinite
54.52 begin
54.53
54.54 definition
55.1 --- a/src/HOLCF/Product_Cpo.thy Thu Jul 01 16:54:42 2010 +0200
55.2 +++ b/src/HOLCF/Product_Cpo.thy Thu Jul 01 16:54:44 2010 +0200
55.3 @@ -32,7 +32,7 @@
55.4
55.5 subsection {* Product type is a partial order *}
55.6
55.7 -instantiation "*" :: (below, below) below
55.8 +instantiation prod :: (below, below) below
55.9 begin
55.10
55.11 definition
55.12 @@ -41,7 +41,7 @@
55.13 instance ..
55.14 end
55.15
55.16 -instance "*" :: (po, po) po
55.17 +instance prod :: (po, po) po
55.18 proof
55.19 fix x :: "'a \<times> 'b"
55.20 show "x \<sqsubseteq> x"
55.21 @@ -148,7 +148,7 @@
55.22 \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
55.23 by (rule lub_cprod [THEN thelubI])
55.24
55.25 -instance "*" :: (cpo, cpo) cpo
55.26 +instance prod :: (cpo, cpo) cpo
55.27 proof
55.28 fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
55.29 assume "chain S"
55.30 @@ -157,9 +157,9 @@
55.31 thus "\<exists>x. range S <<| x" ..
55.32 qed
55.33
55.34 -instance "*" :: (finite_po, finite_po) finite_po ..
55.35 +instance prod :: (finite_po, finite_po) finite_po ..
55.36
55.37 -instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
55.38 +instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
55.39 proof
55.40 fix x y :: "'a \<times> 'b"
55.41 show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
55.42 @@ -172,7 +172,7 @@
55.43 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
55.44 by (simp add: below_prod_def)
55.45
55.46 -instance "*" :: (pcpo, pcpo) pcpo
55.47 +instance prod :: (pcpo, pcpo) pcpo
55.48 by intro_classes (fast intro: minimal_cprod)
55.49
55.50 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
55.51 @@ -297,7 +297,7 @@
55.52 apply (drule compact_snd, simp)
55.53 done
55.54
55.55 -instance "*" :: (chfin, chfin) chfin
55.56 +instance prod :: (chfin, chfin) chfin
55.57 apply intro_classes
55.58 apply (erule compact_imp_max_in_chain)
55.59 apply (case_tac "\<Squnion>i. Y i", simp)
56.1 --- a/src/HOLCF/Representable.thy Thu Jul 01 16:54:42 2010 +0200
56.2 +++ b/src/HOLCF/Representable.thy Thu Jul 01 16:54:44 2010 +0200
56.3 @@ -447,7 +447,7 @@
56.4
56.5 text "Cartesian products of representable types are representable."
56.6
56.7 -instantiation "*" :: (rep, rep) rep
56.8 +instantiation prod :: (rep, rep) rep
56.9 begin
56.10
56.11 definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
56.12 @@ -763,7 +763,7 @@
56.13 (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
56.14 @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
56.15
56.16 - (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
56.17 + (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
56.18 @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
56.19
56.20 (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},
57.1 --- a/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:42 2010 +0200
57.2 +++ b/src/Pure/Isar/class_target.ML Thu Jul 01 16:54:44 2010 +0200
57.3 @@ -450,7 +450,7 @@
57.4
57.5 (* target *)
57.6
57.7 -val sanitize_name = (*FIXME*)
57.8 +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
57.9 let
57.10 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
57.11 orelse s = "'" orelse s = "_";
57.12 @@ -465,9 +465,7 @@
57.13 explode #> scan_valids #> implode
57.14 end;
57.15
57.16 -fun type_name "Product_Type.*" = "prod"
57.17 - | type_name "Sum_Type.+" = "sum"
57.18 - | type_name s = sanitize_name (Long_Name.base_name s);
57.19 +val type_name = sanitize_name o Long_Name.base_name;
57.20
57.21 fun resort_terms pp algebra consts constraints ts =
57.22 let