1506 |
1509 |
1507 (* The main end product for multiset_rel: inductive characterization *) |
1510 (* The main end product for multiset_rel: inductive characterization *) |
1508 theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] = |
1511 theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] = |
1509 multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]] |
1512 multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]] |
1510 |
1513 |
|
1514 |
|
1515 |
|
1516 (* Advanced relator customization *) |
|
1517 |
|
1518 (* Set vs. sum relators: *) |
|
1519 (* FIXME: All such facts should be declared as simps: *) |
|
1520 declare sum_rel_simps[simp] |
|
1521 |
|
1522 lemma set_rel_sum_rel[simp]: |
|
1523 "set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> |
|
1524 set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)" |
|
1525 (is "?L \<longleftrightarrow> ?Rl \<and> ?Rr") |
|
1526 proof safe |
|
1527 assume L: "?L" |
|
1528 show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe |
|
1529 fix l1 assume "Inl l1 \<in> A1" |
|
1530 then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2" |
|
1531 using L unfolding set_rel_def by auto |
|
1532 then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto) |
|
1533 thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto |
|
1534 next |
|
1535 fix l2 assume "Inl l2 \<in> A2" |
|
1536 then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)" |
|
1537 using L unfolding set_rel_def by auto |
|
1538 then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto) |
|
1539 thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto |
|
1540 qed |
|
1541 show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe |
|
1542 fix r1 assume "Inr r1 \<in> A1" |
|
1543 then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2" |
|
1544 using L unfolding set_rel_def by auto |
|
1545 then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto) |
|
1546 thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto |
|
1547 next |
|
1548 fix r2 assume "Inr r2 \<in> A2" |
|
1549 then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)" |
|
1550 using L unfolding set_rel_def by auto |
|
1551 then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto) |
|
1552 thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto |
|
1553 qed |
|
1554 next |
|
1555 assume Rl: "?Rl" and Rr: "?Rr" |
|
1556 show ?L unfolding set_rel_def Bex_def vimage_eq proof safe |
|
1557 fix a1 assume a1: "a1 \<in> A1" |
|
1558 show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2" |
|
1559 proof(cases a1) |
|
1560 case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2" |
|
1561 using Rl a1 unfolding set_rel_def by blast |
|
1562 thus ?thesis unfolding Inl by auto |
|
1563 next |
|
1564 case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2" |
|
1565 using Rr a1 unfolding set_rel_def by blast |
|
1566 thus ?thesis unfolding Inr by auto |
|
1567 qed |
|
1568 next |
|
1569 fix a2 assume a2: "a2 \<in> A2" |
|
1570 show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2" |
|
1571 proof(cases a2) |
|
1572 case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2" |
|
1573 using Rl a2 unfolding set_rel_def by blast |
|
1574 thus ?thesis unfolding Inl by auto |
|
1575 next |
|
1576 case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2" |
|
1577 using Rr a2 unfolding set_rel_def by blast |
|
1578 thus ?thesis unfolding Inr by auto |
|
1579 qed |
|
1580 qed |
|
1581 qed |
|
1582 |
|
1583 |
|
1584 |
|
1585 |
1511 end |
1586 end |