equal
deleted
inserted
replaced
13 "print_bnfs" :: diag and |
13 "print_bnfs" :: diag and |
14 "bnf" :: thy_goal |
14 "bnf" :: thy_goal |
15 begin |
15 begin |
16 |
16 |
17 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)" |
17 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)" |
18 by (rule ext) (auto simp only: o_apply collect_def) |
18 by (rule ext) (auto simp only: o_apply collect_def) |
19 |
|
20 lemma converse_shift: |
|
21 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2" |
|
22 unfolding converse_def by auto |
|
23 |
|
24 lemma conversep_shift: |
|
25 "R1 \<le> R2 ^--1 \<Longrightarrow> R1 ^--1 \<le> R2" |
|
26 unfolding conversep.simps by auto |
|
27 |
19 |
28 definition convol ("<_ , _>") where |
20 definition convol ("<_ , _>") where |
29 "<f , g> \<equiv> %a. (f a, g a)" |
21 "<f , g> \<equiv> %a. (f a, g a)" |
30 |
22 |
31 lemma fst_convol: |
23 lemma fst_convol: |