1412 

  1413 

  1414 ML {*

  1415 fun dest_fsetT (Type (@{type_name fset}, [T])) = T

  1416   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);

  1417 *}

  1418 

  1419 ML {*

  1420 open Quotient_Info;

  1421 

  1422 exception LIFT_MATCH of string

  1423 

  1424 

  1425 

  1426 (*** Aggregate Rep/Abs Function ***)

  1427 

  1428 

  1429 (* The flag RepF is for types in negative position; AbsF is for types

  1430    in positive position. Because of this, function types need to be

  1431    treated specially, since there the polarity changes.

  1432 *)

  1433 

  1434 datatype flag = AbsF | RepF

  1435 

  1436 fun negF AbsF = RepF

  1437   | negF RepF = AbsF

  1438 

  1439 fun is_identity (Const (@{const_name "id"}, _)) = true

  1440   | is_identity _ = false

  1441 

  1442 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)

  1443 

  1444 fun mk_fun_compose flag (trm1, trm2) =

  1445   case flag of

  1446     AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2

  1447   | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1

  1448 

  1449 fun get_mapfun ctxt s =

  1450 let

  1451   val thy = ProofContext.theory_of ctxt

  1452   val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")

  1453   val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn

  1454 in

  1455   Const (mapfun, dummyT)

  1456 end

  1457 

  1458 (* makes a Free out of a TVar *)

  1459 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)

  1460 

  1461 (* produces an aggregate map function for the

  1462    rty-part of a quotient definition; abstracts

  1463    over all variables listed in vs (these variables

  1464    correspond to the type variables in rty)

  1465 

  1466    for example for: (?'a list * ?'b)

  1467    it produces:     %a b. prod_map (map a) b

  1468 *)

  1469 fun mk_mapfun ctxt vs rty =

  1470 let

  1471   val vs' = map (mk_Free) vs

  1472 

  1473   fun mk_mapfun_aux rty =

  1474     case rty of

  1475       TVar _ => mk_Free rty

  1476     | Type (_, []) => mk_identity rty

  1477     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)

  1478     | _ => raise LIFT_MATCH "mk_mapfun (default)"

  1479 in

  1480   fold_rev Term.lambda vs' (mk_mapfun_aux rty)

  1481 end

  1482 

  1483 (* looks up the (varified) rty and qty for

  1484    a quotient definition

  1485 *)

  1486 fun get_rty_qty ctxt s =

  1487 let

  1488   val thy = ProofContext.theory_of ctxt

  1489   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")

  1490   val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn

  1491 in

  1492   (#rtyp qdata, #qtyp qdata)

  1493 end

  1494 

  1495 (* takes two type-environments and looks

  1496    up in both of them the variable v, which

  1497    must be listed in the environment

  1498 *)

  1499 fun double_lookup rtyenv qtyenv v =

  1500 let

  1501   val v' = fst (dest_TVar v)

  1502 in

  1503   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))

  1504 end

  1505 

  1506 (* matches a type pattern with a type *)

  1507 fun match ctxt err ty_pat ty =

  1508 let

  1509   val thy = ProofContext.theory_of ctxt

  1510 in

  1511   Sign.typ_match thy (ty_pat, ty) Vartab.empty

  1512   handle MATCH_TYPE => err ctxt ty_pat ty

  1513 end

  1514 

  1515 (* produces the rep or abs constant for a qty *)

  1516 fun absrep_const flag ctxt qty_str =

  1517 let

  1518   val qty_name = Long_Name.base_name qty_str

  1519   val qualifier = Long_Name.qualifier qty_str

  1520 in

  1521   case flag of

  1522     AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)

  1523   | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)

  1524 end

  1525 

  1526 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)

  1527 fun absrep_const_chk flag ctxt qty_str =

  1528   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)

  1529 

  1530 fun absrep_match_err ctxt ty_pat ty =

  1531 let

  1532   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat

  1533   val ty_str = Syntax.string_of_typ ctxt ty

  1534 in

  1535   raise LIFT_MATCH (space_implode " "

  1536     ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])

  1537 end

  1538 

  1539 

  1540 (** generation of an aggregate absrep function **)

  1541 

  1542 (* - In case of equal types we just return the identity.

  1543 

  1544    - In case of TFrees we also return the identity.

  1545 

  1546    - In case of function types we recurse taking

  1547      the polarity change into account.

  1548 

  1549    - If the type constructors are equal, we recurse for the

  1550      arguments and build the appropriate map function.

  1551 

  1552    - If the type constructors are unequal, there must be an

  1553      instance of quotient types:

  1554 

  1555        - we first look up the corresponding rty_pat and qty_pat

  1556          from the quotient definition; the arguments of qty_pat

  1557          must be some distinct TVars

  1558        - we then match the rty_pat with rty and qty_pat with qty;

  1559          if matching fails the types do not correspond -> error

  1560        - the matching produces two environments; we look up the

  1561          assignments for the qty_pat variables and recurse on the

  1562          assignments

  1563        - we prefix the aggregate map function for the rty_pat,

  1564          which is an abstraction over all type variables

  1565        - finally we compose the result with the appropriate

  1566          absrep function in case at least one argument produced

  1567          a non-identity function /

  1568          otherwise we just return the appropriate absrep

  1569          function

  1570 

  1571      The composition is necessary for types like

  1572 

  1573         ('a list) list / ('a foo) foo

  1574 

  1575      The matching is necessary for types like

  1576 

  1577         ('a * 'a) list / 'a bar

  1578 

  1579      The test is necessary in order to eliminate superfluous

  1580      identity maps.

  1581 *)

  1582 

  1583 fun absrep_fun flag ctxt (rty, qty) =

  1584   if rty = qty

  1585   then mk_identity rty

  1586   else

  1587     case (rty, qty) of

  1588       (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>

  1589         let

  1590           val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')

  1591           val arg2 = absrep_fun flag ctxt (ty2, ty2')

  1592         in

  1593           list_comb (get_mapfun ctxt "fun", [arg1, arg2])

  1594         end

  1595     | (Type (s, tys), Type (s', tys')) =>

  1596         if s = s'

  1597         then

  1598            let

  1599              val args = map (absrep_fun flag ctxt) (tys ~~ tys')

  1600            in

  1601              list_comb (get_mapfun ctxt s, args)

  1602            end

  1603         else

  1604            let

  1605              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'

  1606              val rtyenv = match ctxt absrep_match_err rty_pat rty

  1607              val qtyenv = match ctxt absrep_match_err qty_pat qty

  1608              val args_aux = map (double_lookup rtyenv qtyenv) vs

  1609              val args = map (absrep_fun flag ctxt) args_aux

  1610              val map_fun = mk_mapfun ctxt vs rty_pat

  1611              val result = list_comb (map_fun, args)

  1612            in

  1613              (*if forall is_identity args

  1614              then absrep_const flag ctxt s'

  1615              else*) mk_fun_compose flag (absrep_const flag ctxt s', result)

  1616            end

  1617     | (TFree x, TFree x') =>

  1618         if x = x'

  1619         then mk_identity rty

  1620         else raise (LIFT_MATCH "absrep_fun (frees)")

  1621     | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")

  1622     | _ => raise (LIFT_MATCH "absrep_fun (default)")

  1623 

  1624 

  1625 *}

  1626 

  1627 ML {*

  1628 let

  1629 val parser = Args.context -- Scan.lift Args.name_source

  1630 fun typ_pat (ctxt, str) =

  1631 str |> Syntax.parse_typ ctxt

  1632 |> ML_Syntax.print_typ

  1633 |> ML_Syntax.atomic

  1634 in

  1635 ML_Antiquote.inline "typ_pat" (parser >> typ_pat)

  1636 end

  1637 *}

  1638 

  1639 ML {*

  1640   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1641   |> Syntax.check_term @{context}

  1642   |> fastype_of

  1643   |> Syntax.string_of_typ @{context}

  1644   |> tracing

  1645 *}

  1646 

  1647 ML {*

  1648   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1649   |> Syntax.check_term @{context}

  1650   |> Syntax.string_of_term @{context}

  1651   |> warning

  1652 *}

  1653 

  1654 ML {*

  1655   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1656   |> Syntax.check_term @{context}

  1657 *}

  1658 

  1659 term prod_fun

  1660 term map

  1661 term fun_map

  1662 term "op o"

  1663 

  1664 ML {*

  1665   absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})

  1666   |> Syntax.string_of_term @{context}

  1667   |> writeln

  1668 *}

  1669 

  1670 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"

  1671 apply(auto simp add: mem_def)

  1672 done