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 |
|
118 |
|
119 lemma |
117 lemma |
120 assumes sr: "symp r" |
118 assumes sr: "symp r" |
121 and ss: "symp s" |
119 and ss: "symp s" |
122 shows "(r OO s) x y = (s OO r) y x" |
120 shows "(r OO s) x y = (s OO r) y x" |
123 using sr ss |
121 using sr ss |
124 unfolding symp_def |
122 unfolding symp_def |
125 apply (metis pred_comp.intros pred_compE ss symp_def) |
123 apply (metis pred_comp.intros pred_compE ss symp_def) |
|
124 done |
126 |
125 |
127 thm rep_abs_rsp |
126 lemma bla: |
|
127 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
|
128 and a2: "Quotient r2 abs2 rep2" |
|
129 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
|
130 using a1 |
|
131 apply - |
128 sorry |
132 sorry |
129 |
133 |
130 term "r^--1" |
134 lemma bla2: |
|
135 assumes a2: "Quotient r1 abs1 rep_fset" |
|
136 and "Quotient r2 abs2 rep2" |
|
137 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
|
138 sorry |
|
139 |
|
140 thm bla [OF Quotient_fset] |
|
141 thm bla2[OF Quotient_fset] |
|
142 |
|
143 thm bla [OF Quotient_fset Quotient_fset] |
|
144 thm bla2[OF Quotient_fset Quotient_fset] |
131 |
145 |
132 lemma bla: |
146 lemma bla: |
133 assumes a1: "Quotient r1 abs1 rep1" |
147 assumes a1: "Quotient r1 abs1 rep1" |
134 and a2: "Quotient r2 abs2 rep2" |
148 and a2: "Quotient r2 abs2 rep2" |
135 shows "Quotient (r2) (abs1 \<circ> abs2) (rep2 \<circ> rep1)" |
149 shows "Quotient r2 (abs1 \<circ> abs2) (rep2 \<circ> rep1)" |
136 |
|
137 sorry |
150 sorry |
138 |
151 |
139 thm bla[OF Quotient_fset list_quotient] |
|
140 |
152 |
141 unfolding Quotient_def |
153 unfolding Quotient_def |
142 apply auto |
154 apply auto |
143 term rep_fset |
155 term rep_fset |
144 |
156 |