equal
deleted
inserted
replaced
8 |
8 |
9 theory Order_Union |
9 theory Order_Union |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where |
13 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix \<open>Osum\<close> 60) where |
14 "r Osum r' = r \<union> r' \<union> {(a, a'). a \<in> Field r \<and> a' \<in> Field r'}" |
14 "r Osum r' = r \<union> r' \<union> {(a, a'). a \<in> Field r \<and> a' \<in> Field r'}" |
15 |
15 |
16 notation Osum (infix "\<union>o" 60) |
16 notation Osum (infix \<open>\<union>o\<close> 60) |
17 |
17 |
18 lemma Field_Osum: "Field (r \<union>o r') = Field r \<union> Field r'" |
18 lemma Field_Osum: "Field (r \<union>o r') = Field r \<union> Field r'" |
19 unfolding Osum_def Field_def by blast |
19 unfolding Osum_def Field_def by blast |
20 |
20 |
21 lemma Osum_wf: |
21 lemma Osum_wf: |