--- 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
--- 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
--- 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]
--- 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)"
--- 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)"
--- 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)
--- 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 ..
--- 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
--- 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
--- 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"
--- 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"
--- 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)"
--- 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 \<times> 'b::lattice"
from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
--- 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 \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> 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 \<times> 'b::quasi_order"
show "p \<sqsubseteq> 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 \<times> 'b::partial_order"
assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
--- 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 "\<lambda>(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 "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
(simp split: sum.split_asm)
--- 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
--- 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 \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>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:
--- 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\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> 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
--- 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 (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
--- 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 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-declare [[map * = (prod_fun, prod_rel)]]
+declare [[map prod = (prod_fun, prod_rel)]]
lemma prod_equivp[quot_equiv]:
--- 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} *}
--- 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 \<times> '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 \<Rightarrow> 'a \<times> 'b"
fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> '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 \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"
--- 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 \<Rightarrow> 'a * 'b"
assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
--- 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)
--- 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
--- 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 *)
--- 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 \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
"Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
-typedef (prod) ('a, 'b) "*" (infixr "*" 20)
+typedef ('a, 'b) prod (infixr "*" 20)
= "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
proof
fix a b show "Pair_Rep a b \<in> ?prod"
@@ -137,14 +137,14 @@
qed
type_notation (xsymbols)
- "*" ("(_ \<times>/ _)" [21, 20] 20)
+ "prod" ("(_ \<times>/ _)" [21, 20] 20)
type_notation (HTML output)
- "*" ("(_ \<times>/ _)" [21, 20] 20)
+ "prod" ("(_ \<times>/ _)" [21, 20] 20)
definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
"Pair a b = Abs_prod (Pair_Rep a b)"
-rep_datatype (prod) Pair proof -
+rep_datatype Pair proof -
fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
assume "\<And>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 \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
"f o\<rightarrow> g = (\<lambda>x. split g (f x))"
+lemma scomp_unfold: "scomp = (\<lambda>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\<rightarrow> g) x = split g (f x)"
- by (simp add: scomp_def)
+ by (simp add: scomp_unfold split_def)
lemma Pair_scomp: "Pair x o\<rightarrow> 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\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
- by (simp add: expand_fun_eq split_twice scomp_def)
+ by (simp add: expand_fun_eq scomp_unfold)
lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>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\<rightarrow> h = f o> (g o\<rightarrow> 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 "#->")
--- 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 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
"Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
-typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
+typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
by auto
lemma Inl_RepI: "Inl_Rep a \<in> 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"
--- 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 **)
--- 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;
--- 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
--- 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
--- 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)
--- 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
--- 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)
--- 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
--- 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])
--- 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)),
--- 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
--- 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)
--- 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
--- 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)))
--- 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);
--- 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"
--- 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
--- 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"),
--- 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 =
--- 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";
--- 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);
--- 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
--- 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\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
--- 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
--- 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 **)
--- 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 \<sqsubseteq> 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 "\<Squnion>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
--- 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 \<times> 'b"
show "x \<sqsubseteq> x"
@@ -148,7 +148,7 @@
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
by (rule lub_cprod [THEN thelubI])
-instance "*" :: (cpo, cpo) cpo
+instance prod :: (cpo, cpo) cpo
proof
fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
assume "chain S"
@@ -157,9 +157,9 @@
thus "\<exists>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 \<times> 'b"
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
@@ -172,7 +172,7 @@
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> 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: "\<bottom> = (\<bottom>, \<bottom>)"
@@ -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 "\<Squnion>i. Y i", simp)
--- 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\<cdot>emb\<cdot>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},
--- 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