1429 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1427 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1430 ) |
1428 ) |
1431 ) |
1429 ) |
1432 *} |
1430 *} |
1433 |
1431 |
1434 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
|
1435 (((REP_fset ---> id) ---> id) |
|
1436 (((ABS_fset ---> id) ---> id) |
|
1437 (\<lambda>P. |
|
1438 (ABS_fset ---> id) ((REP_fset ---> id) P) |
|
1439 (REP_fset (ABS_fset [])) \<and> |
|
1440 Ball (Respects (op \<approx>)) |
|
1441 ((ABS_fset ---> id) |
|
1442 ((REP_fset ---> id) |
|
1443 (\<lambda>t. |
|
1444 ((ABS_fset ---> id) |
|
1445 ((REP_fset ---> id) P) |
|
1446 (REP_fset (ABS_fset t))) \<longrightarrow> |
|
1447 (!h. |
|
1448 (ABS_fset ---> id) |
|
1449 ((REP_fset ---> id) P) |
|
1450 (REP_fset |
|
1451 (ABS_fset |
|
1452 (h # |
|
1453 REP_fset |
|
1454 (ABS_fset t)))))))) \<longrightarrow> |
|
1455 Ball (Respects (op \<approx>)) |
|
1456 ((ABS_fset ---> id) |
|
1457 ((REP_fset ---> id) |
|
1458 (\<lambda>l. |
|
1459 (ABS_fset ---> id) |
|
1460 ((REP_fset ---> id) P) |
|
1461 (REP_fset (ABS_fset l))))))))) |
|
1462 |
|
1463 = Ball (Respects ((op \<approx>) ===> (op =))) |
|
1464 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
|
1465 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
|
1466 |
|
1467 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
|
1468 proof - |
|
1469 note APPLY_RSP_I = APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
|
1470 show ?thesis apply - |
|
1471 |
|
1472 |
|
1473 ML_prf {* |
|
1474 val gc = Subgoal.focus @{context} 1 (Isar.goal ()) |
|
1475 |> fst |
|
1476 |> #concl |
|
1477 val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP" })) |
|
1478 val (_, tc') = Thm.dest_comb tc |
|
1479 val (_, gc') = Thm.dest_comb gc |
|
1480 *} |
|
1481 |
|
1482 |
|
1483 |
|
1484 |
|
1485 ML_prf {* |
|
1486 (gc', tc') |
|
1487 *} |
|
1488 ML_prf {* Pattern.first_order_match *} |
|
1489 ML_prf {* Thm.match (@{cpat "?P::?'a"}, @{cterm "1::nat"}) *} |
|
1490 ML_prf {* Pattern.match @{theory} (term_of @{cpat "?P::nat"}, term_of @{cterm "1::nat"}) (Vartab.empty, Vartab.empty) *} |
|
1491 |
|
1492 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1493 ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *} |
|
1494 |
|
1495 ML_prf {* val mo = Thm.match (op1, op2) *} |
|
1496 ML_prf {* val t1 = Drule.instantiate mo @{thm "APPLY_RSP" } *} |
|
1497 ML_prf {* val tc = cterm_of @{theory} (concl_of t1) *} |
|
1498 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1499 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1500 ML_prf {* val (mlty, mlt) = Thm.match (l1, l2) *} |
|
1501 ML_prf {* val t2 = Drule.instantiate (mlty, []) t1 *} |
|
1502 ML_prf {* val tc = cterm_of @{theory} (concl_of t2) *} |
|
1503 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1504 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *} |
|
1505 ML_prf {* val mr = Thm.match (r1, r2) *} |
|
1506 |
|
1507 ML_prf {* val t3 = Drule.instantiate ml t2 *} |
|
1508 ML_prf {* val tc = cterm_of @{theory} (concl_of t3) *} |
|
1509 ML_prf {* val (_, tc') = Thm.dest_comb tc *} |
|
1510 |
|
1511 |
|
1512 |
|
1513 ML_prf {* mtyl; mtyr *} |
|
1514 |
|
1515 ML_prf {* val ol1 = Thm.capply op1 l1 *} |
|
1516 ML_prf {* val ol2 = Thm.capply op2 l2 *} |
|
1517 ML_prf {* (ol1, ol2); Thm.match (ol1, ol2) *} |
|
1518 ML_prf {* val w1 = Thm.capply ol1 r1 *} |
|
1519 ML_prf {* val w2 = Thm.capply ol2 r2 *} |
|
1520 |
|
1521 |
|
1522 . |
|
1523 (*ML_prf {* (w1, w2); Thm.match (w1, w2) *}*) |
|
1524 |
|
1525 |
|
1526 |
|
1527 ML_prf {* |
|
1528 (tc', gc') |
|
1529 *} |
|
1530 |
|
1531 thm APPLY_RSP |
|
1532 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)"] |
|
1533 term "(op \<approx> ===> op =) ===> op =" |
|
1534 proof - |
|
1535 note APPLY_RSP_I2 = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \<approx> ===> op =)" "Ball (Respects op \<approx> ===> op =)"] |
|
1536 show ?thesis apply - |
|
1537 |
|
1538 thm APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow> |
|
1539 (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"] |
|
1540 proof - |
|
1541 note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow> |
|
1542 (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"] |
|
1543 show ?thesis apply - |
|
1544 term "(REP_fset ---> id ---> id |
|
1545 (ABS_fset ---> id ---> id |
|
1546 (\<lambda>P\<Colon>'a list \<Rightarrow> bool. |
|
1547 ABS_fset ---> id (REP_fset ---> id P) |
|
1548 (REP_fset (ABS_fset [])) \<and> |
|
1549 Ball (Respects op \<approx>) |
|
1550 (ABS_fset ---> id |
|
1551 (REP_fset ---> id |
|
1552 (\<lambda>t\<Colon>'a list. |
|
1553 ABS_fset ---> id (REP_fset ---> id P) |
|
1554 (REP_fset (ABS_fset t)) \<longrightarrow> |
|
1555 (\<forall>h\<Colon>'a. |
|
1556 ABS_fset ---> id (REP_fset ---> id P) |
|
1557 (REP_fset |
|
1558 (ABS_fset |
|
1559 (h # REP_fset (ABS_fset t)))))))) \<longrightarrow> |
|
1560 Ball (Respects op \<approx>) |
|
1561 (ABS_fset ---> id |
|
1562 (REP_fset ---> id |
|
1563 (\<lambda>l\<Colon>'a list. |
|
1564 ABS_fset ---> id (REP_fset ---> id P) |
|
1565 (REP_fset (ABS_fset l))))))))" |
|
1566 |
|
1567 apply (rule APPLY_RSP_I3) |
|
1568 term "Ball (Respects op \<approx> ===> op =)" |
|
1569 thm APPLY_RSP_I [of _ "Ball (Respects op \<approx> ===> op =)"] |
|
1570 |
|
1571 thm APPLY_RSP |
|
1572 |
|
1573 . |
|
1574 |
|
1575 apply (tactic {* Cong_Tac.cong_tac @{thm APPLY_RSP_I} 1 *} ) |
|
1576 |
|
1577 apply (tactic {* match_tac @{thms APPLY_RSP_I} 1 *}) |
|
1578 . |
|
1579 |
|
1580 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]) |
|
1581 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
|
1582 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
|
1583 thm LAMBDA_PRS1[symmetric] |
|
1584 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
|
1585 apply (unfold Ball_def) |
|
1586 apply (simp only: IN_RESPECTS) |
|
1587 apply (simp only:list_eq_refl) |
|
1588 apply (unfold id_def) |
|
1589 (*apply (simp only: FUN_MAP_I)*) |
|
1590 apply (simp) |
|
1591 apply (simp only: QUOT_TYPE_I_fset.thm10) |
|
1592 .. |
|
1593 apply (simp add:IN_RESPECTS) |
|
1594 |
|
1595 |
|
1596 |
|
1597 |
|
1598 apply (simp add: QUOT_TYPE_I_fset.R_trans2) |
|
1599 |
|
1600 apply (rule ext) |
|
1601 apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
1602 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} ) |
|
1603 apply (simp add:cons_preserves) |
|
1604 |
|
1605 |
1432 |
1606 |
1433 |
1607 (*prove aaa: {* (Thm.term_of cgoal2) *} |
1434 (*prove aaa: {* (Thm.term_of cgoal2) *} |
1608 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1435 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1609 apply (atomize(full)) |
1436 apply (atomize(full)) |