1452 

  1452 (* rep-abs injection *)

  1453 

  1454 ML {*

  1455 (* FIXME: is this the right get_fun function for rep-abs injection *)

  1456 fun mk_repabs lthy (T, T') trm = 

  1457   Quotient_Def.get_fun repF lthy (T, T') 

  1458   $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)

  1459 *}

  1460 

  1461 ML {*

  1462 (* replaces a term for the bound variable, *)

  1463 (* possible capture                        *)

  1464 fun replace_bnd0 (trm, Abs (x, T, t)) =

  1465   Abs (x, T, subst_bound (trm, t))

  1466 *}

  1467 

  1468 

  1469 ML {*

  1470 (* bound variables need to be treated properly,  *)

  1471 (* as the type of subterms need to be calculated *)

  1472 

  1473 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)

  1474 

  1475 fun inj_REPABS lthy (rtrm, qtrm) =

  1476 let

  1477   val rty = fastype_of rtrm

  1478   val qty = fastype_of qtrm

  1479 in

  1480   case (rtrm, qtrm) of

  1481     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>

  1482        Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))

  1483   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>

  1484        Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))

  1485   | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>

  1486        Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))

  1487   | (Abs (x, T, t), Abs (x', T', t')) =>

  1488       let

  1489         val (y, s) = Term.dest_abs (x, T, t)

  1490         val (_, s') = Term.dest_abs (x', T', t')

  1491         val yvar = Free (y, T)

  1492         val res = lambda yvar (inj_REPABS lthy (s, s'))

  1493       in

  1494         if rty = qty

  1495         then res

  1496         else if T = T'

  1497              then mk_repabs lthy (rty, qty) res

  1498              else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))

  1499       end

  1500   | _ =>

  1501       let

  1502         val (rhead, rargs) = strip_comb rtrm

  1503         val (qhead, qargs) = strip_comb qtrm

  1504         (* TODO:  val rhead' = inj_REPABS lthy (rhead, qhead) *)

  1505         val rhead' = rhead;

  1506         val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);

  1507         val result = list_comb (rhead', rargs');

  1508       in

  1509         if rty = qty then result else

  1510         if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else

  1511         if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else

  1512         if rargs' = [] then rhead' else result

  1513       end

  1454 

  1515 *}

  1516 

  1517 ML {*

  1518 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =

  1519   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))

  1520 *}

  1521 

  1522 

  1523 end

  1524