1234 prefer 2 |
1234 prefer 2 |
1235 (* MINE *) |
1235 (* MINE *) |
1236 apply (simp only: FUN_REL.simps) |
1236 apply (simp only: FUN_REL.simps) |
1237 prefer 3 |
1237 prefer 3 |
1238 (* APPLY_RSP *) |
1238 (* APPLY_RSP *) |
1239 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"] |
1239 apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"]) |
1240 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1240 (* 3: ho_respects *) |
|
1241 prefer 4 |
|
1242 (* ABS_REP_RSP *) |
|
1243 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1244 prefer 2 |
|
1245 (* LAMBDA_RSP *) |
|
1246 apply (simp only: FUN_REL.simps) |
|
1247 apply (rule allI) |
|
1248 apply (rule allI) |
|
1249 apply (rule impI) |
|
1250 (* MK_COMB_TAC *) |
|
1251 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
1252 (* MK_COMB_TAC *) |
|
1253 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
1254 (* REFL_TAC *) |
|
1255 apply (simp) |
|
1256 (* APPLY_RSP *) |
|
1257 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
|
1258 prefer 3 |
|
1259 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1260 prefer 2 |
1241 (* MINE *) |
1261 (* MINE *) |
|
1262 apply (simp only: FUN_REL.simps) |
1242 prefer 4 |
1263 prefer 4 |
1243 apply (rule list_eq_refl ) |
1264 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1244 |
1265 prefer 2 |
|
1266 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
|
1267 apply (assumption) |
|
1268 prefer 5 |
|
1269 (* MK_COMB_TAC *) |
|
1270 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
1271 (* REFL_TAC *) |
|
1272 apply (simp) |
|
1273 (* W(C (curry op THEN) (G... *) |
|
1274 apply (rule ext) |
|
1275 (* APPLY_RSP *) |
|
1276 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
|
1277 prefer 3 |
|
1278 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1279 prefer 2 |
|
1280 apply (simp only: FUN_REL.simps) |
|
1281 prefer 4 |
|
1282 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
|
1283 prefer 2 |
|
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"] ) |
|
1288 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"]) |
|
1290 (* 3: CONS respects *) |
|
1291 prefer 3 |
|
1292 apply (simp only: FUN_REL.simps) |
|
1293 apply (rule allI) |
|
1294 apply (rule allI) |
|
1295 apply (rule impI) |
|
1296 apply (rule allI) |
|
1297 apply (rule allI) |
|
1298 apply (rule impI) |
|
1299 apply (simp) |
|
1300 thm cons_preserves |
|
1301 apply (rule cons_preserves) |
|
1302 apply (assumption) |
|
1303 prefer 3 |
|
1304 apply (simp) |
1245 sorry |
1305 sorry |
1246 |
1306 |
1247 thm list.recs(2) |
1307 thm list.recs(2) |
1248 |
1308 |
1249 |
1309 |