tuning
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 550664e5ddf3162ac
parent 55065 6d0af3c10864
child 55067 a452de24a877
tuning
src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/BNF/Examples/Stream_Processor.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF_Comp.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Util.thy
src/HOL/Cardinals/Cardinal_Arithmetic.thy
src/HOL/Cardinals/Constructions_on_Wellorders.thy
src/HOL/Cardinals/Fun_More.thy
src/HOL/Cardinals/Order_Relation_More.thy
src/HOL/Cardinals/Wellfounded_More.thy
src/HOL/Cardinals/Wellorder_Embedding.thy
src/HOL/Fun.thy
src/HOL/Main.thy
src/HOL/Record.thy
     1.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -24,11 +24,11 @@
     1.4  definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
     1.5  
     1.6  lemma finite_cont[simp]: "finite (cont tr)"
     1.7 -  unfolding cont_def o_apply by (cases tr, clarsimp)
     1.8 +  unfolding cont_def comp_apply by (cases tr, clarsimp)
     1.9  
    1.10  lemma Node_root_cont[simp]:
    1.11    "Node (root tr) (cont tr) = tr"
    1.12 -  unfolding Node_def cont_def o_apply
    1.13 +  unfolding Node_def cont_def comp_apply
    1.14    apply (rule trans[OF _ dtree.collapse])
    1.15    apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
    1.16    apply (simp_all add: fset_inject)
     2.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -480,7 +480,7 @@
     2.4  proof-
     2.5    {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
     2.6     apply(induct rule: wf_raw_coind) apply safe
     2.7 -   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
     2.8 +   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp
     2.9     root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
    2.10     unfolding inj_on_def by auto
    2.11    }
    2.12 @@ -517,7 +517,7 @@
    2.13  lemma cont_hsubst_eq[simp]:
    2.14  assumes "root tr = root tr0"
    2.15  shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
    2.16 -apply(subst id_o[symmetric, of id]) unfolding id_o
    2.17 +apply(subst id_comp[symmetric, of id]) unfolding id_comp
    2.18  using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
    2.19  unfolding hsubst_def hsubst_c_def using assms by simp
    2.20  
    2.21 @@ -529,7 +529,7 @@
    2.22  lemma cont_hsubst_neq[simp]:
    2.23  assumes "root tr \<noteq> root tr0"
    2.24  shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
    2.25 -apply(subst id_o[symmetric, of id]) unfolding id_o
    2.26 +apply(subst id_comp[symmetric, of id]) unfolding id_comp
    2.27  using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
    2.28  unfolding hsubst_def hsubst_c_def using assms by simp
    2.29  
    2.30 @@ -960,7 +960,7 @@
    2.31  
    2.32  lemma cont_H[simp]:
    2.33  "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
    2.34 -apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
    2.35 +apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric]
    2.36  unfolding image_compose unfolding H_c_def[symmetric]
    2.37  using unfold(2)[of H_c n H_r, OF finite_H_c]
    2.38  unfolding H_def ..
    2.39 @@ -989,7 +989,7 @@
    2.40         obtain tr2' where tr2: "tr2 = H (root tr2')"
    2.41         and tr2': "Inr tr2' \<in> cont (pick n1)"
    2.42         using tr2 Inr_cont_H[of n1]
    2.43 -       unfolding tr1 image_def o_def using vimage_eq by auto
    2.44 +       unfolding tr1 image_def comp_def using vimage_eq by auto
    2.45         have "inItr UNIV tr0 (root tr2')"
    2.46         using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
    2.47         thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
    2.48 @@ -1005,7 +1005,7 @@
    2.49  using assms apply(cases t_tr)
    2.50    apply (metis (lifting) sum_map.simps(1))
    2.51    using pick H_def H_r_def unfold(1)
    2.52 -      inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
    2.53 +      inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2)
    2.54    by (metis UNIV_I)
    2.55  
    2.56  lemma H_P:
    2.57 @@ -1013,7 +1013,7 @@
    2.58  shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
    2.59  proof-
    2.60    have "?L = (n, (id \<oplus> root) ` cont (pick n))"
    2.61 -  unfolding cont_H image_compose[symmetric] sum_map.comp id_o o_assoc
    2.62 +  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc
    2.63    unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
    2.64    by(rule root_H_root[OF n])
    2.65    moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
     3.1 --- a/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -62,7 +62,7 @@
     3.4    "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')"
     3.5  
     3.6  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'"
     3.7 -proof (rule ext, unfold o_apply)
     3.8 +proof (rule ext, unfold comp_apply)
     3.9    fix s
    3.10    show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
    3.11    proof (coinduction arbitrary: sp sp' s)
    3.12 @@ -95,7 +95,7 @@
    3.13    "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')"
    3.14  
    3.15  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'"
    3.16 -proof (rule ext, unfold o_apply)
    3.17 +proof (rule ext, unfold comp_apply)
    3.18    fix s
    3.19    show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
    3.20    proof (coinduction arbitrary: sp sp' s)
    3.21 @@ -157,16 +157,16 @@
    3.22  
    3.23  (* The strength laws for \<theta>: *)
    3.24  lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
    3.25 -  unfolding \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
    3.26 +  unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
    3.27  
    3.28  definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
    3.29    "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
    3.30  
    3.31  lemma \<theta>_rid: "F id fst o \<theta> = fst"
    3.32 -  unfolding \<theta>_def F.map_comp F.map_id o_def id_apply convol_def fst_conv sym[OF id_def] ..
    3.33 +  unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
    3.34  
    3.35  lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
    3.36 -  unfolding assl_def \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
    3.37 +  unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
    3.38  
    3.39  datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
    3.40  codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
     4.1 --- a/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -17,6 +17,16 @@
     4.4    "~~/src/HOL/Library/Multiset"
     4.5  begin
     4.6  
     4.7 +notation
     4.8 +  ordLeq2 (infix "<=o" 50) and
     4.9 +  ordLeq3 (infix "\<le>o" 50) and
    4.10 +  ordLess2 (infix "<o" 50) and
    4.11 +  ordIso2 (infix "=o" 50) and
    4.12 +  csum (infixr "+c" 65) and
    4.13 +  cprod (infixr "*c" 80) and
    4.14 +  cexp (infixr "^c" 90) and
    4.15 +  convol ("<_ , _>")
    4.16 +
    4.17  lemma option_rec_conv_option_case: "option_rec = option_case"
    4.18  by (simp add: fun_eq_iff split: option.split)
    4.19  
    4.20 @@ -84,7 +94,7 @@
    4.21    thus "map f x = map g x" by simp
    4.22  next
    4.23    fix f
    4.24 -  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
    4.25 +  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
    4.26  next
    4.27    show "card_order natLeq" by (rule natLeq_card_order)
    4.28  next
    4.29 @@ -237,7 +247,7 @@
    4.30    also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
    4.31    finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
    4.32    thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
    4.33 -    by transfer (unfold o_apply, blast)
    4.34 +    by transfer (unfold comp_apply, blast)
    4.35  qed
    4.36  
    4.37  lemma mmap_cong:
    4.38 @@ -255,7 +265,7 @@
    4.39  end
    4.40  
    4.41  lemma set_of_mmap: "set_of o mmap h = image h o set_of"
    4.42 -proof (rule ext, unfold o_apply)
    4.43 +proof (rule ext, unfold comp_apply)
    4.44    fix M show "set_of (mmap h M) = h ` set_of M"
    4.45      by transfer (auto simp add: multiset_def setsum_gt_0_iff)
    4.46  qed
    4.47 @@ -687,7 +697,7 @@
    4.48          case True
    4.49          def c \<equiv> "f1 b1"
    4.50          have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
    4.51 -          unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
    4.52 +          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
    4.53          with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
    4.54            by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
    4.55          also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
    4.56 @@ -723,7 +733,7 @@
    4.57          case True
    4.58          def c \<equiv> "f2 b2"
    4.59          have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
    4.60 -          unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
    4.61 +          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
    4.62          with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
    4.63            by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
    4.64          also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
    4.65 @@ -738,7 +748,7 @@
    4.66            apply(rule setsum_reindex)
    4.67            using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
    4.68          also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
    4.69 -        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
    4.70 +        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
    4.71            apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
    4.72            using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
    4.73          finally show ?thesis .
    4.74 @@ -762,7 +772,7 @@
    4.75      by (blast dest: wppull_thePull)
    4.76    then show ?thesis
    4.77      by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
    4.78 -      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
    4.79 +      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
    4.80          intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
    4.81  qed
    4.82  
    4.83 @@ -774,7 +784,7 @@
    4.84  by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
    4.85    Grp_def relcompp.simps intro: mmap_cong)
    4.86    (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
    4.87 -    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
    4.88 +    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
    4.89  
    4.90  inductive rel_multiset' where
    4.91    Zero[intro]: "rel_multiset' R {#} {#}"
     5.1 --- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -15,10 +15,10 @@
     5.4  by (rule ext) simp
     5.5  
     5.6  lemma Union_natural: "Union o image (image f) = image f o Union"
     5.7 -by (rule ext) (auto simp only: o_apply)
     5.8 +by (rule ext) (auto simp only: comp_apply)
     5.9  
    5.10  lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    5.11 -by (unfold o_assoc)
    5.12 +by (unfold comp_assoc)
    5.13  
    5.14  lemma comp_single_set_bd:
    5.15    assumes fbd_Card_order: "Card_order fbd" and
    5.16 @@ -58,7 +58,7 @@
    5.17  by blast
    5.18  
    5.19  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"
    5.20 -by (unfold o_apply collect_def SUP_def)
    5.21 +by (unfold comp_apply collect_def SUP_def)
    5.22  
    5.23  lemma wpull_cong:
    5.24  "\<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"
     6.1 --- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -16,8 +16,8 @@
     6.4    "bnf" :: thy_goal
     6.5  begin
     6.6  
     6.7 -lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
     6.8 -  by (rule ext) (auto simp only: o_apply collect_def)
     6.9 +lemma collect_comp: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
    6.10 +  by (rule ext) (auto simp only: comp_apply collect_def)
    6.11  
    6.12  definition convol ("<_ , _>") where
    6.13  "<f , g> \<equiv> %a. (f a, g a)"
    6.14 @@ -67,10 +67,10 @@
    6.15  unfolding Grp_def by auto
    6.16  
    6.17  lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    6.18 -unfolding Grp_def o_def by auto
    6.19 +unfolding Grp_def comp_def by auto
    6.20  
    6.21  lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
    6.22 -unfolding Grp_def o_def by auto
    6.23 +unfolding Grp_def comp_def by auto
    6.24  
    6.25  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    6.26  
    6.27 @@ -153,10 +153,6 @@
    6.28  lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
    6.29    unfolding vimage2p_def Grp_def by auto
    6.30  
    6.31 -(*FIXME: duplicates lemma from Record.thy*)
    6.32 -lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
    6.33 -  by clarsimp
    6.34 -
    6.35  ML_file "Tools/BNF/bnf_def_tactics.ML"
    6.36  ML_file "Tools/BNF/bnf_def.ML"
    6.37  
     7.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -35,7 +35,7 @@
     7.4  by auto
     7.5  
     7.6  lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
     7.7 -unfolding o_def fun_eq_iff by simp
     7.8 +unfolding comp_def fun_eq_iff by simp
     7.9  
    7.10  lemma o_bij:
    7.11    assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
    7.12 @@ -113,16 +113,16 @@
    7.13  by blast
    7.14  
    7.15  lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
    7.16 -  unfolding o_def fun_eq_iff by auto
    7.17 +  unfolding comp_def fun_eq_iff by auto
    7.18  
    7.19  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"
    7.20 -  unfolding o_def fun_eq_iff by auto
    7.21 +  unfolding comp_def fun_eq_iff by auto
    7.22  
    7.23  lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
    7.24 -  unfolding o_def fun_eq_iff by auto
    7.25 +  unfolding comp_def fun_eq_iff by auto
    7.26  
    7.27  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"
    7.28 -  unfolding o_def fun_eq_iff by auto
    7.29 +  unfolding comp_def fun_eq_iff by auto
    7.30  
    7.31  lemma convol_o: "<f, g> o h = <f o h, g o h>"
    7.32    unfolding convol_def by auto
    7.33 @@ -131,16 +131,16 @@
    7.34    unfolding convol_def by auto
    7.35  
    7.36  lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    7.37 -  unfolding map_pair_o_convol id_o o_id ..
    7.38 +  unfolding map_pair_o_convol id_comp comp_id ..
    7.39  
    7.40  lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
    7.41 -  unfolding o_def by (auto split: sum.splits)
    7.42 +  unfolding comp_def by (auto split: sum.splits)
    7.43  
    7.44  lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
    7.45 -  unfolding o_def by (auto split: sum.splits)
    7.46 +  unfolding comp_def by (auto split: sum.splits)
    7.47  
    7.48  lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
    7.49 -  unfolding sum_case_o_sum_map id_o o_id ..
    7.50 +  unfolding sum_case_o_sum_map id_comp comp_id ..
    7.51  
    7.52  lemma fun_rel_def_butlast:
    7.53    "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
     8.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -225,10 +225,10 @@
     8.4  by (rule `(\<And>x y. PROP P x y)`)
     8.5  
     8.6  lemma nchotomy_relcomppE:
     8.7 -  "\<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"
     8.8 +  "\<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"
     8.9    by (metis relcompp.cases)
    8.10  
    8.11 -lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
    8.12 +lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
    8.13    unfolding fun_rel_def vimage2p_def by auto
    8.14  
    8.15  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
     9.1 --- a/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     9.2 +++ b/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     9.3 @@ -22,7 +22,7 @@
     9.4  lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
     9.5  by simp
     9.6  
     9.7 -lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
     9.8 +lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
     9.9  unfolding bij_def inj_on_def by auto blast
    9.10  
    9.11  (* Operator: *)
    10.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
    10.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
    10.3 @@ -11,10 +11,7 @@
    10.4  imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
    10.5  begin
    10.6  
    10.7 -notation ordLeq2 (infix "<=o" 50) and
    10.8 -  ordLeq3 (infix "\<le>o" 50) and
    10.9 -  ordLess2 (infix "<o" 50) and
   10.10 -  ordIso2 (infix "=o" 50) and
   10.11 +notation
   10.12    csum (infixr "+c" 65) and
   10.13    cprod (infixr "*c" 80) and
   10.14    cexp (infixr "^c" 90)
    11.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
    11.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
    11.3 @@ -11,7 +11,8 @@
    11.4  imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
    11.5  begin
    11.6  
    11.7 -notation ordLeq2 (infix "<=o" 50) and
    11.8 +notation
    11.9 +  ordLeq2 (infix "<=o" 50) and
   11.10    ordLeq3 (infix "\<le>o" 50) and
   11.11    ordLess2 (infix "<o" 50) and
   11.12    ordIso2 (infix "=o" 50)
    12.1 --- a/src/HOL/Cardinals/Fun_More.thy	Mon Jan 20 18:24:56 2014 +0100
    12.2 +++ b/src/HOL/Cardinals/Fun_More.thy	Mon Jan 20 18:24:56 2014 +0100
    12.3 @@ -11,7 +11,6 @@
    12.4  imports Main
    12.5  begin
    12.6  
    12.7 -
    12.8  subsection {* Purely functional properties  *}
    12.9  
   12.10  (* unused *)
    13.1 --- a/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
    13.2 +++ b/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
    13.3 @@ -11,7 +11,6 @@
    13.4  imports Main
    13.5  begin
    13.6  
    13.7 -
    13.8  subsection {* The upper and lower bounds operators  *}
    13.9  
   13.10  lemma aboveS_subset_above: "aboveS r a \<le> above r a"
    14.1 --- a/src/HOL/Cardinals/Wellfounded_More.thy	Mon Jan 20 18:24:56 2014 +0100
    14.2 +++ b/src/HOL/Cardinals/Wellfounded_More.thy	Mon Jan 20 18:24:56 2014 +0100
    14.3 @@ -11,7 +11,6 @@
    14.4  imports Wellfounded Order_Relation_More
    14.5  begin
    14.6  
    14.7 -
    14.8  subsection {* Well-founded recursion via genuine fixpoints *}
    14.9  
   14.10  (*2*)lemma adm_wf_unique_fixpoint:
    15.1 --- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
    15.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
    15.3 @@ -11,7 +11,6 @@
    15.4  imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
    15.5  begin
    15.6  
    15.7 -
    15.8  subsection {* Auxiliaries *}
    15.9  
   15.10  lemma UNION_bij_betw_ofilter:
    16.1 --- a/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
    16.2 +++ b/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
    16.3 @@ -65,6 +65,12 @@
    16.4    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    16.5    by (simp add: fun_eq_iff) 
    16.6  
    16.7 +lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
    16.8 +  by clarsimp
    16.9 +
   16.10 +lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
   16.11 +  by clarsimp
   16.12 +
   16.13  lemma image_comp:
   16.14    "(f o g) ` r = f ` (g ` r)"
   16.15    by auto
   16.16 @@ -915,6 +921,8 @@
   16.17  lemmas o_id = comp_id
   16.18  lemmas o_eq_dest = comp_eq_dest
   16.19  lemmas o_eq_elim = comp_eq_elim
   16.20 +lemmas o_eq_dest_lhs = comp_eq_dest_lhs
   16.21 +lemmas o_eq_id_dest = comp_eq_id_dest
   16.22  lemmas image_compose = image_comp
   16.23  lemmas vimage_compose = vimage_comp
   16.24  
    17.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
    17.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
    17.3 @@ -24,7 +24,8 @@
    17.4    ordIso2 (infix "=o" 50) and
    17.5    csum (infixr "+c" 65) and
    17.6    cprod (infixr "*c" 80) and
    17.7 -  cexp (infixr "^c" 90)
    17.8 +  cexp (infixr "^c" 90) and
    17.9 +  convol ("<_ , _>")
   17.10  
   17.11  no_syntax (xsymbols)
   17.12    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    18.1 --- a/src/HOL/Record.thy	Mon Jan 20 18:24:56 2014 +0100
    18.2 +++ b/src/HOL/Record.thy	Mon Jan 20 18:24:56 2014 +0100
    18.3 @@ -411,12 +411,6 @@
    18.4  lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
    18.5    by (simp add: comp_def)
    18.6  
    18.7 -lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
    18.8 -  by clarsimp
    18.9 -
   18.10 -lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
   18.11 -  by clarsimp
   18.12 -
   18.13  
   18.14  subsection {* Concrete record syntax *}
   18.15