equal
deleted
inserted
replaced
93 (@{typ "('a list) list"}, |
93 (@{typ "('a list) list"}, |
94 @{typ "('a fset) fset"}) |
94 @{typ "('a fset) fset"}) |
95 *} |
95 *} |
96 |
96 |
97 |
97 |
|
98 ML {* |
|
99 test_funs absF @{context} |
|
100 (@{typ "((nat * nat) list) list"}, |
|
101 @{typ "((myint) fset) fset"}) |
|
102 *} |
98 |
103 |
99 ML {* |
104 ML {* |
100 test_funs absF @{context} |
105 test_funs absF @{context} |
101 (@{typ "(('a * 'a) list) list"}, |
106 (@{typ "(('a * 'a) list) list"}, |
102 @{typ "(('a * 'a) fset) fset"}) |
107 @{typ "(('a * 'a) fset) fset"}) |
131 done |
136 done |
132 |
137 |
133 lemma bla: |
138 lemma bla: |
134 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
139 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
135 and a2: "Quotient r2 abs2 rep2" |
140 and a2: "Quotient r2 abs2 rep2" |
136 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
141 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
|
142 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
137 unfolding Quotient_def comp_def |
143 unfolding Quotient_def comp_def |
138 apply (rule)+ |
144 apply (rule)+ |
139 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
145 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
140 apply (rule) |
146 apply (rule) |
141 apply (rule) |
147 apply (rule) |