1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Apr 03 16:26:48 2012 +0200
1.3 @@ -0,0 +1,173 @@
1.4 +(* Title: HOL/Tools/Lifting/lifting_term.ML
1.5 + Author: Ondrej Kuncar
1.6 +
1.7 +Proves Quotient theorem.
1.8 +*)
1.9 +
1.10 +signature LIFTING_TERM =
1.11 +sig
1.12 + val prove_quot_theorem: Proof.context -> typ * typ -> thm
1.13 +
1.14 + val absrep_fun: Proof.context -> typ * typ -> term
1.15 +
1.16 + (* Allows Nitpick to represent quotient types as single elements from raw type *)
1.17 + (* val absrep_const_chk: Proof.context -> flag -> string -> term *)
1.18 +
1.19 + val equiv_relation: Proof.context -> typ * typ -> term
1.20 +
1.21 + val quot_thm_rel: thm -> term
1.22 + val quot_thm_abs: thm -> term
1.23 + val quot_thm_rep: thm -> term
1.24 + val quot_thm_rty_qty: thm -> typ * typ
1.25 +end
1.26 +
1.27 +structure Lifting_Term: LIFTING_TERM =
1.28 +struct
1.29 +
1.30 +exception LIFT_MATCH of string
1.31 +
1.32 +(* matches a type pattern with a type *)
1.33 +fun match ctxt err ty_pat ty =
1.34 + let
1.35 + val thy = Proof_Context.theory_of ctxt
1.36 + in
1.37 + Sign.typ_match thy (ty_pat, ty) Vartab.empty
1.38 + handle Type.TYPE_MATCH => err ctxt ty_pat ty
1.39 + end
1.40 +
1.41 +fun equiv_match_err ctxt ty_pat ty =
1.42 + let
1.43 + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
1.44 + val ty_str = Syntax.string_of_typ ctxt ty
1.45 + in
1.46 + raise LIFT_MATCH (space_implode " "
1.47 + ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
1.48 + end
1.49 +
1.50 +(* generation of the Quotient theorem *)
1.51 +
1.52 +exception QUOT_THM of string
1.53 +
1.54 +fun get_quot_thm ctxt s =
1.55 + let
1.56 + val thy = Proof_Context.theory_of ctxt
1.57 + in
1.58 + (case Lifting_Info.lookup_quotients ctxt s of
1.59 + SOME qdata => Thm.transfer thy (#quot_thm qdata)
1.60 + | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found."))
1.61 + end
1.62 +
1.63 +fun get_rel_quot_thm ctxt s =
1.64 + let
1.65 + val thy = Proof_Context.theory_of ctxt
1.66 + in
1.67 + (case Lifting_Info.lookup_quotmaps ctxt s of
1.68 + SOME map_data => Thm.transfer thy (#quot_thm map_data)
1.69 + | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")"))
1.70 + end
1.71 +
1.72 +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
1.73 +
1.74 +infix 0 MRSL
1.75 +
1.76 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
1.77 +
1.78 +exception NOT_IMPL of string
1.79 +
1.80 +fun quot_thm_rel quot_thm =
1.81 + let
1.82 + val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) =
1.83 + (HOLogic.dest_Trueprop o prop_of) quot_thm
1.84 + in
1.85 + rel
1.86 + end
1.87 +
1.88 +fun quot_thm_abs quot_thm =
1.89 + let
1.90 + val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) =
1.91 + (HOLogic.dest_Trueprop o prop_of) quot_thm
1.92 + in
1.93 + abs
1.94 + end
1.95 +
1.96 +fun quot_thm_rep quot_thm =
1.97 + let
1.98 + val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) =
1.99 + (HOLogic.dest_Trueprop o prop_of) quot_thm
1.100 + in
1.101 + rep
1.102 + end
1.103 +
1.104 +fun quot_thm_rty_qty quot_thm =
1.105 + let
1.106 + val abs = quot_thm_abs quot_thm
1.107 + val abs_type = fastype_of abs
1.108 + in
1.109 + (domain_type abs_type, range_type abs_type)
1.110 + end
1.111 +
1.112 +fun prove_quot_theorem ctxt (rty, qty) =
1.113 + case (rty, qty) of
1.114 + (Type (s, tys), Type (s', tys')) =>
1.115 + if s = s'
1.116 + then
1.117 + let
1.118 + val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
1.119 + in
1.120 + if forall is_id_quot args
1.121 + then
1.122 + @{thm identity_quotient}
1.123 + else
1.124 + args MRSL (get_rel_quot_thm ctxt s)
1.125 + end
1.126 + else
1.127 + let
1.128 + val quot_thm = get_quot_thm ctxt s'
1.129 + val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
1.130 + val qtyenv = match ctxt equiv_match_err qty_pat qty
1.131 + val rtys' = map (Envir.subst_type qtyenv) rtys
1.132 + val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
1.133 + in
1.134 + if forall is_id_quot args
1.135 + then
1.136 + quot_thm
1.137 + else
1.138 + let
1.139 + val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
1.140 + in
1.141 + [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
1.142 + end
1.143 + end
1.144 + | _ => @{thm identity_quotient}
1.145 +
1.146 +fun force_qty_type thy qty quot_thm =
1.147 + let
1.148 + val abs_schematic = quot_thm_abs quot_thm
1.149 + val qty_schematic = (range_type o fastype_of) abs_schematic
1.150 + val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
1.151 + fun prep_ty thy (x, (S, ty)) =
1.152 + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
1.153 + val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
1.154 + in
1.155 + Thm.instantiate (ty_inst, []) quot_thm
1.156 + end
1.157 +
1.158 +fun absrep_fun ctxt (rty, qty) =
1.159 + let
1.160 + val thy = Proof_Context.theory_of ctxt
1.161 + val quot_thm = prove_quot_theorem ctxt (rty, qty)
1.162 + val forced_quot_thm = force_qty_type thy qty quot_thm
1.163 + in
1.164 + quot_thm_abs forced_quot_thm
1.165 + end
1.166 +
1.167 +fun equiv_relation ctxt (rty, qty) =
1.168 + let
1.169 + val thy = Proof_Context.theory_of ctxt
1.170 + val quot_thm = prove_quot_theorem ctxt (rty, qty)
1.171 + val forced_quot_thm = force_qty_type thy qty quot_thm
1.172 + in
1.173 + quot_thm_rel forced_quot_thm
1.174 + end
1.175 +
1.176 +end;