equal
deleted
inserted
replaced
112 test_funs absF @{context} |
112 test_funs absF @{context} |
113 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
113 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
114 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
114 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
115 *} |
115 *} |
116 |
116 |
|
117 thm pred_compI |
117 |
118 |
|
119 lemma |
|
120 assumes sr: "symp r" |
|
121 and ss: "symp s" |
|
122 shows "(r OO s) x y = (s OO r) y x" |
|
123 using sr ss |
|
124 unfolding symp_def |
|
125 apply (metis pred_comp.intros pred_compE ss symp_def) |
|
126 |
|
127 thm rep_abs_rsp |
|
128 sorry |
|
129 |
|
130 term "r^--1" |
|
131 |
|
132 lemma bla: |
|
133 assumes a1: "Quotient r1 abs1 rep1" |
|
134 and a2: "Quotient r2 abs2 rep2" |
|
135 shows "Quotient (r2) (abs1 \<circ> abs2) (rep2 \<circ> rep1)" |
|
136 |
|
137 sorry |
|
138 |
|
139 thm bla[OF Quotient_fset list_quotient] |
|
140 |
|
141 unfolding Quotient_def |
|
142 apply auto |
|
143 term rep_fset |
|
144 |
|
145 lemma |
|
146 assumes sr: "equivp r" |
|
147 and ss: "equivp s" |
|
148 shows "r OO s = s OO r" |
|
149 apply(rule ext) |
|
150 apply(rule ext) |
|
151 using sr ss |
|
152 nitpick |
|
153 |
|
154 apply(auto) |
|
155 apply(rule pred_compI) |
|
156 |
|
157 definition |
|
158 relation_compose |
|
159 where |
|
160 "relation_compose R1 R2 = \<lambda>x y. \<exists> z. (R1 x z \<and> R2 z y)" |
118 |
161 |
119 |
162 |
120 |
163 |
121 end |
164 end |