1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:21:41 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:25:31 2012 +0100
     1.3 @@ -20,6 +20,9 @@
     1.4    val equiv_relation: Proof.context -> typ * typ -> term
     1.5    val equiv_relation_chk: Proof.context -> typ * typ -> term
     1.6  
     1.7 +  val get_rel_from_quot_thm: thm -> term
     1.8 +  val prove_quot_theorem: Proof.context -> typ * typ -> thm
     1.9 +
    1.10    val regularize_trm: Proof.context -> term * term -> term
    1.11    val regularize_trm_chk: Proof.context -> term * term -> term
    1.12  
    1.13 @@ -331,6 +334,78 @@
    1.14    equiv_relation ctxt (rty, qty)
    1.15    |> Syntax.check_term ctxt
    1.16  
    1.17 +(* generation of the Quotient theorem  *)
    1.18 +
    1.19 +fun get_quot_thm ctxt s =
    1.20 +  let
    1.21 +    val thy = Proof_Context.theory_of ctxt
    1.22 +  in
    1.23 +    (case Quotient_Info.lookup_quotients_global thy s of
    1.24 +      SOME qdata => #quot_thm qdata
    1.25 +    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
    1.26 +  end
    1.27 +
    1.28 +fun get_rel_quot_thm thy s =
    1.29 +  (case Quotient_Info.lookup_quotmaps thy s of
    1.30 +    SOME map_data => #quot_thm map_data
    1.31 +  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
    1.32 +
    1.33 +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    1.34 +
    1.35 +infix 0 MRSL
    1.36 +
    1.37 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    1.38 +
    1.39 +exception NOT_IMPL of string
    1.40 +
    1.41 +fun get_rel_from_quot_thm quot_thm = 
    1.42 +  let
    1.43 +    val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    1.44 +  in
    1.45 +    rel
    1.46 +  end
    1.47 +
    1.48 +fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = 
    1.49 +  let
    1.50 +    val quot_thm_rel = get_rel_from_quot_thm quot_thm
    1.51 +  in
    1.52 +    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
    1.53 +    else raise NOT_IMPL "nested quotients: not implemented yet"
    1.54 +  end
    1.55 +
    1.56 +fun prove_quot_theorem ctxt (rty, qty) =
    1.57 +  if rty = qty
    1.58 +  then @{thm identity_quotient}
    1.59 +  else
    1.60 +    case (rty, qty) of
    1.61 +      (Type (s, tys), Type (s', tys')) =>
    1.62 +        if s = s'
    1.63 +        then
    1.64 +          let
    1.65 +            val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
    1.66 +          in
    1.67 +            args MRSL (get_rel_quot_thm ctxt s)
    1.68 +          end
    1.69 +        else
    1.70 +          let
    1.71 +            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
    1.72 +            val qtyenv = match ctxt equiv_match_err qty_pat qty
    1.73 +            val rtys' = map (Envir.subst_type qtyenv) rtys
    1.74 +            val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
    1.75 +            val quot_thm = get_quot_thm ctxt s'
    1.76 +          in
    1.77 +            if forall is_id_quot args
    1.78 +            then
    1.79 +              quot_thm
    1.80 +            else
    1.81 +              let
    1.82 +                val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
    1.83 +              in
    1.84 +                mk_quot_thm_compose (rel_quot_thm, quot_thm)
    1.85 +             end
    1.86 +          end
    1.87 +    | _ => @{thm identity_quotient}
    1.88 +
    1.89  
    1.90  
    1.91  (*** Regularization ***)