equal
deleted
inserted
replaced
4 |
4 |
5 A reasoning infrastructure for the type of finite sets. |
5 A reasoning infrastructure for the type of finite sets. |
6 *) |
6 *) |
7 |
7 |
8 theory FSet |
8 theory FSet |
9 imports Quotient_List |
9 imports Quotient_List Quotient_Product |
10 begin |
10 begin |
11 |
11 |
12 text {* Definiton of List relation and the quotient type *} |
12 text {* Definiton of List relation and the quotient type *} |
13 |
13 |
14 fun |
14 fun |
1624 |
1624 |
1625 |
1625 |
1626 *} |
1626 *} |
1627 |
1627 |
1628 ML {* |
1628 ML {* |
|
1629 let |
|
1630 val parser = Args.context -- Scan.lift Args.name_source |
|
1631 fun typ_pat (ctxt, str) = |
|
1632 str |> Syntax.parse_typ ctxt |
|
1633 |> ML_Syntax.print_typ |
|
1634 |> ML_Syntax.atomic |
|
1635 in |
|
1636 ML_Antiquote.inline "typ_pat" (parser >> typ_pat) |
|
1637 end |
|
1638 *} |
|
1639 |
|
1640 ML {* |
|
1641 mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"} |
|
1642 |> Syntax.check_term @{context} |
|
1643 |> fastype_of |
|
1644 |> Syntax.string_of_typ @{context} |
|
1645 |> warning |
|
1646 *} |
|
1647 |
|
1648 ML {* |
|
1649 mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"} |
|
1650 |> Syntax.check_term @{context} |
|
1651 |> Syntax.string_of_term @{context} |
|
1652 |> warning |
|
1653 *} |
|
1654 |
|
1655 ML {* |
1629 absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
1656 absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
1630 |> Syntax.string_of_term @{context} |
1657 |> Syntax.string_of_term @{context} |
1631 |> writeln |
1658 |> writeln |
1632 *} |
1659 *} |
1633 |
1660 |