1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 05 22:00:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 05 23:22:54 2012 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  
     1.5  signature LIFTING_DEF =
     1.6  sig
     1.7 +  exception FORCE_RTY of typ * term
     1.8 +
     1.9    val add_lift_def:
    1.10      (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
    1.11  
    1.12 @@ -26,6 +28,8 @@
    1.13  
    1.14  fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    1.15  
    1.16 +exception FORCE_RTY of typ * term
    1.17 +
    1.18  fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
    1.19    | get_body_types (U, V)  = (U, V)
    1.20  
    1.21 @@ -38,6 +42,7 @@
    1.22      val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
    1.23      val rty_schematic = fastype_of rhs_schematic
    1.24      val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
    1.25 +      handle Type.TYPE_MATCH => raise FORCE_RTY (rty, rhs)
    1.26    in
    1.27      Envir.subst_term_types match rhs_schematic
    1.28    end
    1.29 @@ -283,6 +288,46 @@
    1.30        | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
    1.31    end
    1.32  
    1.33 +fun quot_thm_err ctxt (rty, qty) pretty_msg =
    1.34 +  let
    1.35 +    val error_msg = cat_lines
    1.36 +       ["Lifting failed for the following types:",
    1.37 +        Pretty.string_of (Pretty.block
    1.38 +         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
    1.39 +        Pretty.string_of (Pretty.block
    1.40 +         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
    1.41 +        "",
    1.42 +        (Pretty.string_of (Pretty.block
    1.43 +         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
    1.44 +  in
    1.45 +    error error_msg
    1.46 +  end
    1.47 +
    1.48 +fun force_rty_err ctxt rty rhs =
    1.49 +  let
    1.50 +    val error_msg = cat_lines
    1.51 +       ["Lifting failed for the following term:",
    1.52 +        Pretty.string_of (Pretty.block
    1.53 +         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
    1.54 +        Pretty.string_of (Pretty.block
    1.55 +         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt (fastype_of rhs)]),
    1.56 +        "",
    1.57 +        (Pretty.string_of (Pretty.block
    1.58 +         [Pretty.str "Reason:", 
    1.59 +          Pretty.brk 2, 
    1.60 +          Pretty.str "The type of the term cannot be instancied to",
    1.61 +          Pretty.brk 1,
    1.62 +          Pretty.quote (Syntax.pretty_typ ctxt rty),
    1.63 +          Pretty.str "."]))]
    1.64 +    in
    1.65 +      error error_msg
    1.66 +    end
    1.67 +
    1.68 +fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
    1.69 +  (lift_def_cmd (raw_var, rhs_raw) lthy
    1.70 +    handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
    1.71 +    handle FORCE_RTY (rty, rhs) => force_rty_err lthy rty rhs
    1.72 +
    1.73  (* parser and command *)
    1.74  val liftdef_parser =
    1.75    ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
    1.76 @@ -291,7 +336,7 @@
    1.77  val _ =
    1.78    Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
    1.79      "definition for constants over the quotient type"
    1.80 -      (liftdef_parser >> lift_def_cmd)
    1.81 +      (liftdef_parser >> lift_def_cmd_with_err_handling)
    1.82  
    1.83  
    1.84  end; (* structure *)

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 05 22:00:27 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 05 23:22:54 2012 +0200
     2.3 @@ -50,8 +50,35 @@
     2.4    else
     2.5      lthy
     2.6  
     2.7 +fun quot_thm_sanity_check ctxt quot_thm =
     2.8 +  let
     2.9 +    val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
    2.10 +    val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
    2.11 +    val rty_tfreesT = Term.add_tfree_namesT rty []
    2.12 +    val qty_tfreesT = Term.add_tfree_namesT qty []
    2.13 +    val extra_rty_tfrees =
    2.14 +      (case subtract (op =) qty_tfreesT rty_tfreesT of
    2.15 +        [] => []
    2.16 +      | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
    2.17 +                                 Pretty.brk 1] @ 
    2.18 +                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
    2.19 +                                 [Pretty.str "."])])
    2.20 +    val not_type_constr = 
    2.21 +      (case qty of
    2.22 +         Type _ => []
    2.23 +         | _ => [Pretty.block [Pretty.str "The quotient type ",
    2.24 +                                Pretty.quote (Syntax.pretty_typ ctxt' qty),
    2.25 +                                Pretty.brk 1,
    2.26 +                                Pretty.str "is not a type constructor."]])
    2.27 +    val errs = extra_rty_tfrees @ not_type_constr
    2.28 +  in
    2.29 +    if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
    2.30 +                                                @ (map Pretty.string_of errs)))
    2.31 +  end
    2.32 +
    2.33  fun setup_lifting_infr quot_thm equiv_thm lthy =
    2.34    let
    2.35 +    val _ = quot_thm_sanity_check lthy quot_thm
    2.36      val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.37      val qty_full_name = (fst o dest_Type) qtyp
    2.38      val quotients = { quot_thm = quot_thm }

     3.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 05 22:00:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 05 23:22:54 2012 +0200
     3.3 @@ -6,6 +6,8 @@
     3.4  
     3.5  signature LIFTING_TERM =
     3.6  sig
     3.7 +  exception QUOT_THM of typ * typ * Pretty.T
     3.8 +
     3.9    val prove_quot_theorem: Proof.context -> typ * typ -> thm
    3.10  
    3.11    val absrep_fun: Proof.context -> typ * typ -> term
    3.12 @@ -24,7 +26,10 @@
    3.13  structure Lifting_Term: LIFTING_TERM =
    3.14  struct
    3.15  
    3.16 -exception LIFT_MATCH of string
    3.17 +(* generation of the Quotient theorem  *)
    3.18 +
    3.19 +exception QUOT_THM_INTERNAL of Pretty.T
    3.20 +exception QUOT_THM of typ * typ * Pretty.T
    3.21  
    3.22  (* matches a type pattern with a type *)
    3.23  fun match ctxt err ty_pat ty =
    3.24 @@ -40,21 +45,24 @@
    3.25      val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
    3.26      val ty_str = Syntax.string_of_typ ctxt ty
    3.27    in
    3.28 -    raise LIFT_MATCH (space_implode " "
    3.29 -      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
    3.30 +    raise QUOT_THM_INTERNAL (Pretty.block
    3.31 +      [Pretty.str ("The quotient type " ^ quote ty_str),
    3.32 +       Pretty.brk 1,
    3.33 +       Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str),
    3.34 +       Pretty.brk 1,
    3.35 +       Pretty.str "don't match."])
    3.36    end
    3.37  
    3.38 -(* generation of the Quotient theorem  *)
    3.39 -
    3.40 -exception QUOT_THM of string
    3.41 -
    3.42  fun get_quot_thm ctxt s =
    3.43    let
    3.44      val thy = Proof_Context.theory_of ctxt
    3.45    in
    3.46      (case Lifting_Info.lookup_quotients ctxt s of
    3.47        SOME qdata => Thm.transfer thy (#quot_thm qdata)
    3.48 -    | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found."))
    3.49 +    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    3.50 +      [Pretty.str ("No quotient type " ^ quote s), 
    3.51 +       Pretty.brk 1, 
    3.52 +       Pretty.str "found."]))
    3.53    end
    3.54  
    3.55  fun get_rel_quot_thm ctxt s =
    3.56 @@ -63,7 +71,10 @@
    3.57    in
    3.58      (case Lifting_Info.lookup_quotmaps ctxt s of
    3.59        SOME map_data => Thm.transfer thy (#quot_thm map_data)
    3.60 -    | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    3.61 +    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    3.62 +      [Pretty.str ("No relator for the type " ^ quote s), 
    3.63 +       Pretty.brk 1,
    3.64 +       Pretty.str "found."]))
    3.65    end
    3.66  
    3.67  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    3.68 @@ -106,8 +117,19 @@
    3.69      (domain_type abs_type, range_type abs_type)
    3.70    end
    3.71  
    3.72 +fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
    3.73 +  if provided_rty_name <> rty_of_qty_name then
    3.74 +    raise QUOT_THM_INTERNAL (Pretty.block 
    3.75 +        [Pretty.str ("The type " ^ quote provided_rty_name),
    3.76 +         Pretty.brk 1,
    3.77 +         Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
    3.78 +         Pretty.brk 1,
    3.79 +         Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")])
    3.80 +  else
    3.81 +    ()
    3.82 +
    3.83  fun prove_quot_theorem' ctxt (rty, qty) =
    3.84 -  case (rty, qty) of
    3.85 +  (case (rty, qty) of
    3.86      (Type (s, tys), Type (s', tys')) =>
    3.87        if s = s'
    3.88        then
    3.89 @@ -123,7 +145,8 @@
    3.90        else
    3.91          let
    3.92            val quot_thm = get_quot_thm ctxt s'
    3.93 -          val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
    3.94 +          val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
    3.95 +          val _ = check_raw_types (s, rs) s'
    3.96            val qtyenv = match ctxt equiv_match_err qty_pat qty
    3.97            val rtys' = map (Envir.subst_type qtyenv) rtys
    3.98            val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
    3.99 @@ -138,7 +161,8 @@
   3.100                [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
   3.101             end
   3.102          end
   3.103 -  | _ => @{thm identity_quotient}
   3.104 +  | _ => @{thm identity_quotient})
   3.105 +    handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
   3.106  
   3.107  fun force_qty_type thy qty quot_thm =
   3.108    let