src/HOL/Tools/Quotient/quotient_term.ML
changeset 45796 b2205eb270e3
parent 45795 2d8949268303
child 45797 977cf00fb8d3
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:03:17 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:12:02 2011 +0100
     1.3 @@ -62,16 +62,16 @@
     1.4      AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
     1.5    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     1.6  
     1.7 -fun get_mapfun_data thy s =
     1.8 -  (case Symtab.lookup (Enriched_Type.entries (Proof_Context.init_global thy)) s of
     1.9 +fun get_mapfun_data ctxt s =
    1.10 +  (case Symtab.lookup (Enriched_Type.entries ctxt) s of
    1.11      SOME [map_data] => (case try dest_Const (#mapper map_data) of
    1.12        SOME (c, _) => (Const (c, dummyT), #variances map_data)
    1.13      | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
    1.14    | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
    1.15    | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) 
    1.16  
    1.17 -fun defined_mapfun_data thy s =
    1.18 -  Symtab.defined (Enriched_Type.entries (Proof_Context.init_global thy)) s
    1.19 +fun defined_mapfun_data ctxt s =
    1.20 +  Symtab.defined (Enriched_Type.entries ctxt) s
    1.21    
    1.22  (* makes a Free out of a TVar *)
    1.23  fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    1.24 @@ -79,10 +79,14 @@
    1.25  (* looks up the (varified) rty and qty for
    1.26     a quotient definition
    1.27  *)
    1.28 -fun get_rty_qty thy s =
    1.29 -  (case Quotient_Info.lookup_quotients_global thy s of
    1.30 -    SOME qdata => (#rtyp qdata, #qtyp qdata)
    1.31 -  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
    1.32 +fun get_rty_qty ctxt s =
    1.33 +  let
    1.34 +    val thy = Proof_Context.theory_of ctxt
    1.35 +  in
    1.36 +    (case Quotient_Info.lookup_quotients_global thy s of
    1.37 +      SOME qdata => (#rtyp qdata, #qtyp qdata)
    1.38 +    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
    1.39 +  end
    1.40  
    1.41  (* matches a type pattern with a type *)
    1.42  fun match ctxt err ty_pat ty =
    1.43 @@ -168,7 +172,6 @@
    1.44  
    1.45  fun absrep_fun flag ctxt (rty, qty) =
    1.46    let
    1.47 -    val thy = Proof_Context.theory_of ctxt
    1.48      fun absrep_args tys tys' variances =
    1.49        let
    1.50          fun absrep_arg (types, (_, variant)) =
    1.51 @@ -199,18 +202,18 @@
    1.52            if s = s'
    1.53            then
    1.54              let
    1.55 -              val (map_fun, variances) = get_mapfun_data thy s
    1.56 +              val (map_fun, variances) = get_mapfun_data ctxt s
    1.57                val args = absrep_args tys tys' variances
    1.58              in
    1.59                list_comb (map_fun, args)
    1.60              end
    1.61            else
    1.62              let
    1.63 -              val (Type (_, rtys), qty_pat) = get_rty_qty thy s'
    1.64 +              val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
    1.65                val qtyenv = match ctxt absrep_match_err qty_pat qty
    1.66                val rtys' = map (Envir.subst_type qtyenv) rtys
    1.67              in
    1.68 -              if not (defined_mapfun_data thy s)
    1.69 +              if not (defined_mapfun_data ctxt s)
    1.70                then
    1.71                  (*
    1.72                      If we don't know a map function for the raw type,
    1.73 @@ -221,7 +224,7 @@
    1.74                  test_identities tys rtys' s s'
    1.75                else
    1.76                  let
    1.77 -                  val (map_fun, variances) = get_mapfun_data thy s
    1.78 +                  val (map_fun, variances) = get_mapfun_data ctxt s
    1.79                    val args = absrep_args tys rtys' variances
    1.80                  in
    1.81                    if forall is_identity args
    1.82 @@ -320,43 +323,40 @@
    1.83     that will be the argument of Respects
    1.84  *)
    1.85  fun equiv_relation ctxt (rty, qty) =
    1.86 -  let
    1.87 -    val thy = Proof_Context.theory_of ctxt
    1.88 -  in
    1.89 -    if rty = qty
    1.90 -    then HOLogic.eq_const rty
    1.91 -    else
    1.92 -      case (rty, qty) of
    1.93 -        (Type (s, tys), Type (s', tys')) =>
    1.94 -          if s = s'
    1.95 -          then
    1.96 -            let
    1.97 -              val args = map (equiv_relation ctxt) (tys ~~ tys')
    1.98 -            in
    1.99 -              list_comb (get_relmap ctxt s, args)
   1.100 -            end
   1.101 -          else
   1.102 -            let
   1.103 -              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s'
   1.104 -              val rtyenv = match ctxt equiv_match_err rty_pat rty
   1.105 -              val qtyenv = match ctxt equiv_match_err qty_pat qty
   1.106 -              val args_aux = map (double_lookup rtyenv qtyenv) vs
   1.107 -              val args = map (equiv_relation ctxt) args_aux
   1.108 -              val eqv_rel = get_equiv_rel ctxt s'
   1.109 -              val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   1.110 -            in
   1.111 -              if forall is_eq args
   1.112 -              then eqv_rel'
   1.113 -              else
   1.114 -                let
   1.115 -                  val rel_map = mk_relmap ctxt vs rty_pat
   1.116 -                  val result = list_comb (rel_map, args)
   1.117 -                in
   1.118 -                  mk_rel_compose (result, eqv_rel')
   1.119 -                end
   1.120 -            end
   1.121 -      | _ => HOLogic.eq_const rty
   1.122 -  end
   1.123 +  if rty = qty
   1.124 +  then HOLogic.eq_const rty
   1.125 +  else
   1.126 +    case (rty, qty) of
   1.127 +      (Type (s, tys), Type (s', tys')) =>
   1.128 +        if s = s'
   1.129 +        then
   1.130 +          let
   1.131 +            val args = map (equiv_relation ctxt) (tys ~~ tys')
   1.132 +          in
   1.133 +            list_comb (get_relmap ctxt s, args)
   1.134 +          end
   1.135 +        else
   1.136 +          let
   1.137 +            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   1.138 +            val rtyenv = match ctxt equiv_match_err rty_pat rty
   1.139 +            val qtyenv = match ctxt equiv_match_err qty_pat qty
   1.140 +            val args_aux = map (double_lookup rtyenv qtyenv) vs
   1.141 +            val args = map (equiv_relation ctxt) args_aux
   1.142 +            val eqv_rel = get_equiv_rel ctxt s'
   1.143 +            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   1.144 +          in
   1.145 +            if forall is_eq args
   1.146 +            then eqv_rel'
   1.147 +            else
   1.148 +              let
   1.149 +                val rel_map = mk_relmap ctxt vs rty_pat
   1.150 +                val result = list_comb (rel_map, args)
   1.151 +              in
   1.152 +                mk_rel_compose (result, eqv_rel')
   1.153 +              end
   1.154 +          end
   1.155 +    | _ => HOLogic.eq_const rty
   1.156 +
   1.157  
   1.158  fun equiv_relation_chk ctxt (rty, qty) =
   1.159    equiv_relation ctxt (rty, qty)