--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Mon Jan 20 18:24:56 2014 +0100
@@ -24,11 +24,11 @@
definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
lemma finite_cont[simp]: "finite (cont tr)"
- unfolding cont_def o_apply by (cases tr, clarsimp)
+ unfolding cont_def comp_apply by (cases tr, clarsimp)
lemma Node_root_cont[simp]:
"Node (root tr) (cont tr) = tr"
- unfolding Node_def cont_def o_apply
+ unfolding Node_def cont_def comp_apply
apply (rule trans[OF _ dtree.collapse])
apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
apply (simp_all add: fset_inject)
--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Mon Jan 20 18:24:56 2014 +0100
@@ -480,7 +480,7 @@
proof-
{fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
apply(induct rule: wf_raw_coind) apply safe
- unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
+ unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp
root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
unfolding inj_on_def by auto
}
@@ -517,7 +517,7 @@
lemma cont_hsubst_eq[simp]:
assumes "root tr = root tr0"
shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
+apply(subst id_comp[symmetric, of id]) unfolding id_comp
using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
unfolding hsubst_def hsubst_c_def using assms by simp
@@ -529,7 +529,7 @@
lemma cont_hsubst_neq[simp]:
assumes "root tr \<noteq> root tr0"
shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
+apply(subst id_comp[symmetric, of id]) unfolding id_comp
using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
unfolding hsubst_def hsubst_c_def using assms by simp
@@ -960,7 +960,7 @@
lemma cont_H[simp]:
"cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
-apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
+apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric]
unfolding image_compose unfolding H_c_def[symmetric]
using unfold(2)[of H_c n H_r, OF finite_H_c]
unfolding H_def ..
@@ -989,7 +989,7 @@
obtain tr2' where tr2: "tr2 = H (root tr2')"
and tr2': "Inr tr2' \<in> cont (pick n1)"
using tr2 Inr_cont_H[of n1]
- unfolding tr1 image_def o_def using vimage_eq by auto
+ unfolding tr1 image_def comp_def using vimage_eq by auto
have "inItr UNIV tr0 (root tr2')"
using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
@@ -1005,7 +1005,7 @@
using assms apply(cases t_tr)
apply (metis (lifting) sum_map.simps(1))
using pick H_def H_r_def unfold(1)
- inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
+ inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2)
by (metis UNIV_I)
lemma H_P:
@@ -1013,7 +1013,7 @@
shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
proof-
have "?L = (n, (id \<oplus> root) ` cont (pick n))"
- unfolding cont_H image_compose[symmetric] sum_map.comp id_o o_assoc
+ unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc
unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
by(rule root_H_root[OF n])
moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
--- a/src/HOL/BNF/Examples/Stream_Processor.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Stream_Processor.thy Mon Jan 20 18:24:56 2014 +0100
@@ -62,7 +62,7 @@
"out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
fix s
show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
proof (coinduction arbitrary: sp sp' s)
@@ -95,7 +95,7 @@
"out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')"
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
fix s
show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
proof (coinduction arbitrary: sp sp' s)
@@ -157,16 +157,16 @@
(* The strength laws for \<theta>: *)
lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
- unfolding \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
+ unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
"assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
lemma \<theta>_rid: "F id fst o \<theta> = fst"
- unfolding \<theta>_def F.map_comp F.map_id o_def id_apply convol_def fst_conv sym[OF id_def] ..
+ unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
- unfolding assl_def \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
+ unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
--- a/src/HOL/BNF/More_BNFs.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Mon Jan 20 18:24:56 2014 +0100
@@ -17,6 +17,16 @@
"~~/src/HOL/Library/Multiset"
begin
+notation
+ ordLeq2 (infix "<=o" 50) and
+ ordLeq3 (infix "\<le>o" 50) and
+ ordLess2 (infix "<o" 50) and
+ ordIso2 (infix "=o" 50) and
+ csum (infixr "+c" 65) and
+ cprod (infixr "*c" 80) and
+ cexp (infixr "^c" 90) and
+ convol ("<_ , _>")
+
lemma option_rec_conv_option_case: "option_rec = option_case"
by (simp add: fun_eq_iff split: option.split)
@@ -84,7 +94,7 @@
thus "map f x = map g x" by simp
next
fix f
- show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
+ show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
@@ -237,7 +247,7 @@
also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
- by transfer (unfold o_apply, blast)
+ by transfer (unfold comp_apply, blast)
qed
lemma mmap_cong:
@@ -255,7 +265,7 @@
end
lemma set_of_mmap: "set_of o mmap h = image h o set_of"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
fix M show "set_of (mmap h M) = h ` set_of M"
by transfer (auto simp add: multiset_def setsum_gt_0_iff)
qed
@@ -687,7 +697,7 @@
case True
def c \<equiv> "f1 b1"
have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
- unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+ unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
@@ -723,7 +733,7 @@
case True
def c \<equiv> "f2 b2"
have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
- unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+ unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
@@ -738,7 +748,7 @@
apply(rule setsum_reindex)
using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
- also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
+ also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
finally show ?thesis .
@@ -762,7 +772,7 @@
by (blast dest: wppull_thePull)
then show ?thesis
by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
- (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
+ (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
qed
@@ -774,7 +784,7 @@
by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
Grp_def relcompp.simps intro: mmap_cong)
(metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
- o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
+ o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
inductive rel_multiset' where
Zero[intro]: "rel_multiset' R {#} {#}"
--- a/src/HOL/BNF_Comp.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Jan 20 18:24:56 2014 +0100
@@ -15,10 +15,10 @@
by (rule ext) simp
lemma Union_natural: "Union o image (image f) = image f o Union"
-by (rule ext) (auto simp only: o_apply)
+by (rule ext) (auto simp only: comp_apply)
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
-by (unfold o_assoc)
+by (unfold comp_assoc)
lemma comp_single_set_bd:
assumes fbd_Card_order: "Card_order fbd" and
@@ -58,7 +58,7 @@
by blast
lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold o_apply collect_def SUP_def)
+by (unfold comp_apply collect_def SUP_def)
lemma wpull_cong:
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
--- a/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100
@@ -16,8 +16,8 @@
"bnf" :: thy_goal
begin
-lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
- by (rule ext) (auto simp only: o_apply collect_def)
+lemma collect_comp: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
+ by (rule ext) (auto simp only: comp_apply collect_def)
definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"
@@ -67,10 +67,10 @@
unfolding Grp_def by auto
lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
-unfolding Grp_def o_def by auto
+unfolding Grp_def comp_def by auto
lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
-unfolding Grp_def o_def by auto
+unfolding Grp_def comp_def by auto
definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
@@ -153,10 +153,6 @@
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
unfolding vimage2p_def Grp_def by auto
-(*FIXME: duplicates lemma from Record.thy*)
-lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
- by clarsimp
-
ML_file "Tools/BNF/bnf_def_tactics.ML"
ML_file "Tools/BNF/bnf_def.ML"
--- a/src/HOL/BNF_FP_Base.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Mon Jan 20 18:24:56 2014 +0100
@@ -35,7 +35,7 @@
by auto
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding o_def fun_eq_iff by simp
+unfolding comp_def fun_eq_iff by simp
lemma o_bij:
assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
@@ -113,16 +113,16 @@
by blast
lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
- unfolding o_def fun_eq_iff by auto
+ unfolding comp_def fun_eq_iff by auto
lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
- unfolding o_def fun_eq_iff by auto
+ unfolding comp_def fun_eq_iff by auto
lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
- unfolding o_def fun_eq_iff by auto
+ unfolding comp_def fun_eq_iff by auto
lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
- unfolding o_def fun_eq_iff by auto
+ unfolding comp_def fun_eq_iff by auto
lemma convol_o: "<f, g> o h = <f o h, g o h>"
unfolding convol_def by auto
@@ -131,16 +131,16 @@
unfolding convol_def by auto
lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
- unfolding map_pair_o_convol id_o o_id ..
+ unfolding map_pair_o_convol id_comp comp_id ..
lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
- unfolding o_def by (auto split: sum.splits)
+ unfolding comp_def by (auto split: sum.splits)
lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
- unfolding o_def by (auto split: sum.splits)
+ unfolding comp_def by (auto split: sum.splits)
lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
- unfolding sum_case_o_sum_map id_o o_id ..
+ unfolding sum_case_o_sum_map id_comp comp_id ..
lemma fun_rel_def_butlast:
"(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
--- a/src/HOL/BNF_LFP.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Jan 20 18:24:56 2014 +0100
@@ -225,10 +225,10 @@
by (rule `(\<And>x y. PROP P x y)`)
lemma nchotomy_relcomppE:
- "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; (\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (metis relcompp.cases)
-lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
+lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
unfolding fun_rel_def vimage2p_def by auto
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
--- a/src/HOL/BNF_Util.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Util.thy Mon Jan 20 18:24:56 2014 +0100
@@ -22,7 +22,7 @@
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
by simp
-lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
unfolding bij_def inj_on_def by auto blast
(* Operator: *)
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,10 +11,7 @@
imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
begin
-notation ordLeq2 (infix "<=o" 50) and
- ordLeq3 (infix "\<le>o" 50) and
- ordLess2 (infix "<o" 50) and
- ordIso2 (infix "=o" 50) and
+notation
csum (infixr "+c" 65) and
cprod (infixr "*c" 80) and
cexp (infixr "^c" 90)
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,8 @@
imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
begin
-notation ordLeq2 (infix "<=o" 50) and
+notation
+ ordLeq2 (infix "<=o" 50) and
ordLeq3 (infix "\<le>o" 50) and
ordLess2 (infix "<o" 50) and
ordIso2 (infix "=o" 50)
--- a/src/HOL/Cardinals/Fun_More.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
imports Main
begin
-
subsection {* Purely functional properties *}
(* unused *)
--- a/src/HOL/Cardinals/Order_Relation_More.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
imports Main
begin
-
subsection {* The upper and lower bounds operators *}
lemma aboveS_subset_above: "aboveS r a \<le> above r a"
--- a/src/HOL/Cardinals/Wellfounded_More.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
imports Wellfounded Order_Relation_More
begin
-
subsection {* Well-founded recursion via genuine fixpoints *}
(*2*)lemma adm_wf_unique_fixpoint:
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
begin
-
subsection {* Auxiliaries *}
lemma UNION_bij_betw_ofilter:
--- a/src/HOL/Fun.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Fun.thy Mon Jan 20 18:24:56 2014 +0100
@@ -65,6 +65,12 @@
"a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
by (simp add: fun_eq_iff)
+lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
+ by clarsimp
+
+lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
+ by clarsimp
+
lemma image_comp:
"(f o g) ` r = f ` (g ` r)"
by auto
@@ -915,6 +921,8 @@
lemmas o_id = comp_id
lemmas o_eq_dest = comp_eq_dest
lemmas o_eq_elim = comp_eq_elim
+lemmas o_eq_dest_lhs = comp_eq_dest_lhs
+lemmas o_eq_id_dest = comp_eq_id_dest
lemmas image_compose = image_comp
lemmas vimage_compose = vimage_comp
--- a/src/HOL/Main.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy Mon Jan 20 18:24:56 2014 +0100
@@ -24,7 +24,8 @@
ordIso2 (infix "=o" 50) and
csum (infixr "+c" 65) and
cprod (infixr "*c" 80) and
- cexp (infixr "^c" 90)
+ cexp (infixr "^c" 90) and
+ convol ("<_ , _>")
no_syntax (xsymbols)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- a/src/HOL/Record.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Record.thy Mon Jan 20 18:24:56 2014 +0100
@@ -411,12 +411,6 @@
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
by (simp add: comp_def)
-lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
- by clarsimp
-
-lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
- by clarsimp
-
subsection {* Concrete record syntax *}