--- a/NEWS Sun Dec 27 21:46:36 2015 +0100
+++ b/NEWS Sun Dec 27 22:07:17 2015 +0100
@@ -476,6 +476,8 @@
notation iff (infixr "<->" 25)
+ notation Times (infixr "<*>" 80)
+
type_notation Map.map (infixr "~=>" 0)
notation Map.map_comp (infixl "o'_m" 55)
--- a/src/Doc/Main/Main_Doc.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/Doc/Main/Main_Doc.thy Sun Dec 27 22:07:17 2015 +0100
@@ -228,7 +228,7 @@
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
@{term"Pair a b"} & @{term[source]"Pair a b"}\\
@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
+@{term"A \<times> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"}
\end{tabular}
Pairs may be nested. Nesting to the right is printed as a tuple,
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Dec 27 22:07:17 2015 +0100
@@ -281,7 +281,7 @@
subsection \<open>Product\<close>
definition cprod (infixr "*c" 80) where
- "r1 *c r2 = |Field r1 <*> Field r2|"
+ "r1 *c r2 = |Field r1 \<times> Field r2|"
lemma card_order_cprod:
assumes "card_order r1" "card_order r2"
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sun Dec 27 22:07:17 2015 +0100
@@ -788,7 +788,7 @@
qed
lemma card_of_Times_Plus_distrib:
- "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
+ "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
proof -
let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
@@ -1038,7 +1038,7 @@
lemma card_of_Times_ordLeq_infinite_Field:
"\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
- \<Longrightarrow> |A <*> B| \<le>o r"
+ \<Longrightarrow> |A \<times> B| \<le>o r"
by(simp add: card_of_Sigma_ordLeq_infinite_Field)
lemma card_of_Times_infinite_simps:
@@ -1619,7 +1619,7 @@
subsection \<open>Others\<close>
lemma card_of_Func_Times:
-"|Func (A <*> B) C| =o |Func A (Func B C)|"
+"|Func (A \<times> B) C| =o |Func A (Func B C)|"
unfolding card_of_ordIso[symmetric]
using bij_betw_curr by blast
@@ -1661,7 +1661,7 @@
qed
lemma Func_Times_Range:
- "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
+ "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
proof -
let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
\<lambda>x. if x \<in> A then snd (fg x) else undefined)"
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Dec 27 22:07:17 2015 +0100
@@ -73,7 +73,7 @@
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
unfolding Gr_def by simp
-lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
+lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
unfolding Gr_def by auto
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
@@ -137,7 +137,7 @@
by (auto simp: proj_preserves)
lemma relImage_relInvImage:
- assumes "R \<subseteq> f ` A <*> f ` A"
+ assumes "R \<subseteq> f ` A \<times> f ` A"
shows "relImage (relInvImage A R f) f = R"
using assms unfolding relImage_def relInvImage_def by fast
--- a/src/HOL/BNF_Wellorder_Constructions.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Sun Dec 27 22:07:17 2015 +0100
@@ -1515,19 +1515,19 @@
"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
lemma curr_in:
-assumes f: "f \<in> Func (A <*> B) C"
+assumes f: "f \<in> Func (A \<times> B) C"
shows "curr A f \<in> Func A (Func B C)"
using assms unfolding curr_def Func_def by auto
lemma curr_inj:
-assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
+assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
proof safe
assume c: "curr A f1 = curr A f2"
show "f1 = f2"
proof (rule ext, clarify)
fix a b show "f1 (a, b) = f2 (a, b)"
- proof (cases "(a,b) \<in> A <*> B")
+ proof (cases "(a,b) \<in> A \<times> B")
case False
thus ?thesis using assms unfolding Func_def by auto
next
@@ -1540,7 +1540,7 @@
lemma curr_surj:
assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
+shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
proof
let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
show "curr A ?f = g"
@@ -1557,11 +1557,11 @@
thus ?thesis using True unfolding Func_def curr_def by auto
qed
qed
- show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
+ show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
qed
lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
+"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
unfolding bij_betw_def inj_on_def image_def
apply (intro impI conjI ballI)
apply (erule curr_inj[THEN iffD1], assumption+)
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Sun Dec 27 22:07:17 2015 +0100
@@ -51,8 +51,8 @@
shows "|A \<times> {x}| =o |A|"
proof -
def f \<equiv> "\<lambda>(a::'a,b::'b). (a)"
- have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff)
- hence "bij_betw f (A <*> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce
+ have "A \<subseteq> f ` (A \<times> {x})" unfolding f_def by (auto simp: image_iff)
+ hence "bij_betw f (A \<times> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce
thus ?thesis using card_of_ordIso by blast
qed
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sun Dec 27 22:07:17 2015 +0100
@@ -489,7 +489,7 @@
lemma card_of_Times_ordLeq_infinite:
"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
- \<Longrightarrow> |A <*> B| \<le>o |C|"
+ \<Longrightarrow> |A \<times> B| \<le>o |C|"
by(simp add: card_of_Sigma_ordLeq_infinite)
corollary Plus_infinite_bij_betw:
@@ -621,7 +621,7 @@
ordIso_symmetric by blast
hence "|A| <o |?C|" "|B| <o |?C|"
using LESS1 LESS2 ordLess_ordIso_trans by blast+
- hence "|A <*> B| <o |?C|" using INF
+ hence "|A \<times> B| <o |?C|" using INF
card_of_Times_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
@@ -1502,12 +1502,12 @@
lemma card_of_Pfunc_Pow_Func_option:
assumes "B \<noteq> {}"
-shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
+shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
proof-
have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
unfolding Pfunc_Func_option by(rule card_of_refl)
also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
- also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
+ also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
finally show ?thesis .
qed
--- a/src/HOL/Groups_Big.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Groups_Big.thy Sun Dec 27 22:07:17 2015 +0100
@@ -350,7 +350,7 @@
qed
lemma cartesian_product:
- "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
+ "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
apply (rule sym)
apply (cases "finite A")
apply (cases "finite B")
@@ -1032,15 +1032,15 @@
(*
lemma SigmaI_insert: "y \<notin> A ==>
- (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
+ (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
by auto
*)
-lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
+lemma card_cartesian_product: "card (A \<times> B) = card(A) * card(B)"
by (cases "finite A \<and> finite B")
(auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
-lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)"
+lemma card_cartesian_product_singleton: "card({x} \<times> A) = card(A)"
by (simp add: card_cartesian_product)
--- a/src/HOL/Induct/SList.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/SList.thy Sun Dec 27 22:07:17 2015 +0100
@@ -10,8 +10,8 @@
Definition of type 'a list (strict lists) by a least fixed point
-We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
so that list can serve as a "functor" for defining other recursive types.
--- a/src/HOL/Induct/Sexp.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/Sexp.thy Sun Dec 27 22:07:17 2015 +0100
@@ -74,7 +74,7 @@
(** Introduction rules for 'pred_sexp' **)
-lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
+lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp \<times> sexp"
by (simp add: pred_sexp_def) blast
(* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
--- a/src/HOL/Library/Formal_Power_Series.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Sun Dec 27 22:07:17 2015 +0100
@@ -3108,7 +3108,7 @@
setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r")
proof -
let ?S = "{(k::nat, m::nat). k + m \<le> n}"
- have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
+ have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (auto simp add: subset_eq)
have f: "finite {(k::nat, m::nat). k + m \<le> n}"
apply (rule finite_subset[OF s])
apply auto
--- a/src/HOL/Library/Old_Datatype.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Sun Dec 27 22:07:17 2015 +0100
@@ -495,7 +495,7 @@
(*** Bounding theorems ***)
-lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
+lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
by blast
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
@@ -505,7 +505,7 @@
"(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
by auto
-lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
+lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
by blast
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
--- a/src/HOL/MicroJava/BV/JVMType.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sun Dec 27 22:07:17 2015 +0100
@@ -62,7 +62,7 @@
lemma JVM_states_unfold:
- "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
+ "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
list maxr (err(types S))))"
apply (unfold states_def sl_def Opt.esl_def Err.sl_def
stk_esl_def reg_sl_def Product.esl_def
--- a/src/HOL/MicroJava/DFA/Product.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Sun Dec 27 22:07:17 2015 +0100
@@ -16,7 +16,7 @@
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
definition esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" where
-"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
+"esl == %(A,rA,fA) (B,rB,fB). (A \<times> B, le rA rB, sup fA fB)"
abbreviation
lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
@@ -57,7 +57,7 @@
lemma closed_lift2_sup:
"\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow>
- closed (err(A<*>B)) (lift2(sup f g))"
+ closed (err(A\<times>B)) (lift2(sup f g))"
apply (unfold closed_def plussub_def lift2_def err_def sup_def)
apply (simp split: err.split)
apply blast
--- a/src/HOL/Nominal/Examples/Class3.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy Sun Dec 27 22:07:17 2015 +0100
@@ -2265,7 +2265,7 @@
by (induct rule: SNa.induct) (blast)
lemma wf_SNa_restricted:
- shows "wf (A_Redu_set \<inter> (UNIV <*> SNa_set))"
+ shows "wf (A_Redu_set \<inter> (UNIV \<times> SNa_set))"
apply(unfold wf_def)
apply(intro strip)
apply(case_tac "SNa x")
@@ -2280,7 +2280,7 @@
done
definition SNa_Redu :: "(trm \<times> trm) set" where
- "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV <*> SNa_set)"
+ "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV \<times> SNa_set)"
lemma wf_SNa_Redu:
shows "wf SNa_Redu"
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Dec 27 22:07:17 2015 +0100
@@ -173,7 +173,7 @@
where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
definition S :: "(int * int) set"
- where "S = P_set <*> Q_set"
+ where "S = P_set \<times> Q_set"
definition S1 :: "(int * int) set"
where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
--- a/src/HOL/Product_Type.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Product_Type.thy Sun Dec 27 22:07:17 2015 +0100
@@ -1005,12 +1005,8 @@
Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
abbreviation
- Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
- (infixr "<*>" 80) where
- "A <*> B == Sigma A (%_. B)"
-
-notation (xsymbols)
- Times (infixr "\<times>" 80)
+ Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr "\<times>" 80) where
+ "A \<times> B == Sigma A (%_. B)"
hide_const (open) Times
@@ -1057,16 +1053,16 @@
lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
by blast
-lemma Sigma_empty2 [simp]: "A <*> {} = {}"
+lemma Sigma_empty2 [simp]: "A \<times> {} = {}"
by blast
-lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
+lemma UNIV_Times_UNIV [simp]: "UNIV \<times> UNIV = UNIV"
by auto
-lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
+lemma Compl_Times_UNIV1 [simp]: "- (UNIV \<times> A) = UNIV \<times> (-A)"
by auto
-lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
+lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV"
by auto
lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
@@ -1075,10 +1071,10 @@
lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
by auto
-lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
+lemma Times_subset_cancel2: "x:C ==> (A \<times> C <= B \<times> C) = (A <= B)"
by blast
-lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
+lemma Times_eq_cancel2: "x:C ==> (A \<times> C = B \<times> C) = (A = B)"
by (blast elim: equalityE)
lemma Collect_case_prod_Sigma:
--- a/src/HOL/UNITY/Comp/TimerArray.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Sun Dec 27 22:07:17 2015 +0100
@@ -42,7 +42,7 @@
lemma TimerArray_leadsTo_zero:
"finite I
==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
-apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)"
+apply (erule_tac A'1 = "%i. lift_set i ({0} \<times> UNIV)"
in finite_stable_completion [THEN leadsTo_weaken])
apply auto
(*Safety property, already reduced to the single Timer case*)
@@ -51,7 +51,7 @@
(*Progress property for the array of Timers*)
apply (rule_tac f = "sub i o fst" in lessThan_induct)
apply (case_tac "m")
-(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
+(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
apply (auto intro: subset_imp_leadsTo
simp add: insert_absorb
lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric]
--- a/src/HOL/UNITY/Extend.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Extend.thy Sun Dec 27 22:07:17 2015 +0100
@@ -14,7 +14,7 @@
definition
(*MOVE to Relation.thy?*)
Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
- where "Restrict A r = r \<inter> (A <*> UNIV)"
+ where "Restrict A r = r \<inter> (A \<times> UNIV)"
definition
good_map :: "['a*'b => 'c] => bool"
@@ -23,7 +23,7 @@
definition
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
- where "extend_set h A = h ` (A <*> UNIV)"
+ where "extend_set h A = h ` (A \<times> UNIV)"
definition
project_set :: "['a*'b => 'c, 'c set] => 'a set"
--- a/src/HOL/UNITY/Lift_prog.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Sun Dec 27 22:07:17 2015 +0100
@@ -270,13 +270,13 @@
"[| delete_map j g = delete_map j g'; i\<noteq>j |] ==> g i = g' i"
by force
-(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
+(*A set of the form (A \<times> UNIV) ignores the second (dummy) state component*)
-lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
+lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) \<times> UNIV"
by auto
lemma vimage_sub_eq_lift_set [simp]:
- "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
+ "(sub i -`A) \<times> UNIV = lift_set i (A \<times> UNIV)"
by auto
lemma mem_lift_act_iff [iff]:
@@ -288,7 +288,7 @@
lemma preserves_snd_lift_stable:
"[| F \<in> preserves snd; i\<noteq>j |]
- ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
+ ==> lift j F \<in> stable (lift_set i (A \<times> UNIV))"
apply (auto simp add: lift_def lift_set_def stable_def constrains_def
rename_def extend_def mem_rename_set_iff)
apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
@@ -298,9 +298,9 @@
(*If i\<noteq>j then lift j F does nothing to lift_set i, and the
premise ensures A \<subseteq> B.*)
lemma constrains_imp_lift_constrains:
- "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);
+ "[| F i \<in> (A \<times> UNIV) co (B \<times> UNIV);
F j \<in> preserves snd |]
- ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+ ==> lift j (F j) \<in> (lift_set i (A \<times> UNIV)) co (lift_set i (B \<times> UNIV))"
apply (cases "i=j")
apply (simp add: lift_def lift_set_def rename_constrains)
apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
@@ -310,8 +310,8 @@
(*USELESS??*)
lemma lift_map_image_Times:
- "lift_map i ` (A <*> UNIV) =
- (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
+ "lift_map i ` (A \<times> UNIV) =
+ (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) \<times> UNIV"
apply (auto intro!: bexI image_eqI simp add: lift_map_def)
apply (rule split_conv [symmetric])
done
--- a/src/HOL/UNITY/PPROD.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/PPROD.thy Sun Dec 27 22:07:17 2015 +0100
@@ -48,9 +48,9 @@
lemma PLam_constrains:
"[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
- ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
- (lift_set i (B <*> UNIV))) =
- (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
+ ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
+ (lift_set i (B \<times> UNIV))) =
+ (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
apply (simp add: PLam_def JN_constrains)
apply (subst insert_Diff [symmetric], assumption)
apply (simp add: lift_constrains)
@@ -59,8 +59,8 @@
lemma PLam_stable:
"[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
- ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
- (F i \<in> stable (A <*> UNIV))"
+ ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
+ (F i \<in> stable (A \<times> UNIV))"
by (simp add: stable_def PLam_constrains)
lemma PLam_transient:
@@ -70,9 +70,9 @@
text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
lemma PLam_ensures:
- "[| i \<in> I; F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
+ "[| i \<in> I; F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
\<forall>j. F j \<in> preserves snd |]
- ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+ ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
apply (simp add: ensures_def PLam_constrains PLam_transient
lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
@@ -82,11 +82,11 @@
lemma PLam_leadsTo_Basis:
"[| i \<in> I;
- F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
- ((A <*> UNIV) \<union> (B <*> UNIV));
- F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
+ F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
+ ((A \<times> UNIV) \<union> (B \<times> UNIV));
+ F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
\<forall>j. F j \<in> preserves snd |]
- ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+ ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
@@ -94,9 +94,9 @@
(** invariant **)
lemma invariant_imp_PLam_invariant:
- "[| F i \<in> invariant (A <*> UNIV); i \<in> I;
+ "[| F i \<in> invariant (A \<times> UNIV); i \<in> I;
\<forall>j. F j \<in> preserves snd |]
- ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
+ ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
by (auto simp add: PLam_stable invariant_def)
--- a/src/HOL/Wellfounded.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Wellfounded.thy Sun Dec 27 22:07:17 2015 +0100
@@ -32,7 +32,7 @@
text\<open>Restriction to domain @{term A} and range @{term B}. If @{term r} is
well-founded over their intersection, then @{term "wf r"}\<close>
lemma wfI:
- "[| r \<subseteq> A <*> B;
+ "[| r \<subseteq> A \<times> B;
!!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |]
==> wf r"
unfolding wf_def by blast