equal
deleted
inserted
replaced
1280 apply (simp only: FUN_REL.simps) |
1280 apply (simp only: FUN_REL.simps) |
1281 prefer 4 |
1281 prefer 4 |
1282 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1282 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1283 prefer 2 |
1283 prefer 2 |
1284 (* APPLY_RSP *) |
1284 (* APPLY_RSP *) |
1285 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset" ] |
|
1286 |
|
1287 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] ) |
1285 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] ) |
1288 prefer 3 |
1286 prefer 3 |
1289 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1287 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1290 (* 3: CONS respects *) |
1288 (* 3: CONS respects *) |
1291 prefer 3 |
1289 prefer 3 |
1300 thm cons_preserves |
1298 thm cons_preserves |
1301 apply (rule cons_preserves) |
1299 apply (rule cons_preserves) |
1302 apply (assumption) |
1300 apply (assumption) |
1303 prefer 3 |
1301 prefer 3 |
1304 apply (simp) |
1302 apply (simp) |
|
1303 (* Mine *) |
|
1304 apply (simp only: id_def) |
|
1305 apply (rule IDENTITY_QUOTIENT) |
|
1306 prefer 2 |
|
1307 apply (rule QUOTIENT_fset) |
|
1308 prefer 2 |
|
1309 apply (rule QUOTIENT_fset) |
|
1310 prefer 3 |
|
1311 apply (rule QUOTIENT_fset) |
1305 sorry |
1312 sorry |
1306 |
1313 |
1307 thm list.recs(2) |
1314 thm list.recs(2) |
1308 |
1315 |
1309 |
1316 |