# HG changeset patch # User Christian Urban # Date 1257425224 -3600 # Node ID a0be84b0c7073d1c0e432c3cd2f094b2a7dd02fa # Parent f1a840dd07438d541cad84bb5a24683fc5d4706e removed typing information from get_fun in quotient_def; *potentially* dangerous diff -r f1a840dd0743 -r a0be84b0c707 FSet.thy --- a/FSet.thy Thu Nov 05 10:46:54 2009 +0100 +++ b/FSet.thy Thu Nov 05 13:47:04 2009 +0100 @@ -172,6 +172,8 @@ term fmap thm fmap_def +ML {* prop_of @{thm fmap_def} *} + ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} ML {* val consts = lookup_quot_consts defs *} ML {* val defs_sym = add_lower_defs @{context} defs *} diff -r f1a840dd0743 -r a0be84b0c707 IntEx.thy --- a/IntEx.thy Thu Nov 05 10:46:54 2009 +0100 +++ b/IntEx.thy Thu Nov 05 13:47:04 2009 +0100 @@ -23,6 +23,8 @@ term ZERO thm ZERO_def +ML {* prop_of @{thm ZERO_def} *} + quotient_def ONE::"my_int" where @@ -44,6 +46,10 @@ term PLUS thm PLUS_def +ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *} + +ML {* prop_of @{thm PLUS_def} *} + fun my_neg :: "(nat \ nat) \ (nat \ nat)" where diff -r f1a840dd0743 -r a0be84b0c707 QuotTest.thy --- a/QuotTest.thy Thu Nov 05 10:46:54 2009 +0100 +++ b/QuotTest.thy Thu Nov 05 13:47:04 2009 +0100 @@ -77,27 +77,19 @@ print_quotients ML {* -Toplevel.context_of; -Toplevel.keep -*} - -ML {* get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \ qt) \ qt) \ qt) list) * nat"} - |> fst |> Syntax.string_of_term @{context} |> writeln *} ML {* get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"} - |> fst |> Syntax.string_of_term @{context} |> writeln *} ML {* get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \ qt) \ qt"} - |> fst |> Syntax.pretty_term @{context} |> Pretty.string_of |> writeln diff -r f1a840dd0743 -r a0be84b0c707 quotient.ML --- a/quotient.ML Thu Nov 05 10:46:54 2009 +0100 +++ b/quotient.ML Thu Nov 05 13:47:04 2009 +0100 @@ -1,7 +1,7 @@ signature QUOTIENT = sig - val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state - val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state + val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state + val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory val note: binding * thm -> local_theory -> thm * local_theory end; @@ -190,7 +190,7 @@ (* - the type to be quotient *) (* - the relation according to which the type is quotient *) -fun mk_quotient_type quot_list lthy = +fun quotient_type quot_list lthy = let fun mk_goal (rty, rel) = let @@ -207,7 +207,7 @@ theorem after_qed goals lthy end -fun mk_quotient_type_cmd spec lthy = +fun quotient_type_cmd spec lthy = let fun parse_spec (((qty_str, mx), rty_str), rel_str) = let @@ -218,7 +218,7 @@ ((qty_name, mx), (rty, rel)) end in - mk_quotient_type (map parse_spec spec) lthy + quotient_type (map parse_spec spec) lthy end val quotspec_parser = @@ -232,7 +232,7 @@ val _ = OuterSyntax.local_theory_to_proof "quotient" "quotient type definitions (requires equivalence proofs)" - OuterKeyword.thy_goal (quotspec_parser >> mk_quotient_type_cmd) + OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) end; (* structure *) diff -r f1a840dd0743 -r a0be84b0c707 quotient_def.ML --- a/quotient_def.ML Thu Nov 05 10:46:54 2009 +0100 +++ b/quotient_def.ML Thu Nov 05 13:47:04 2009 +0100 @@ -2,7 +2,7 @@ signature QUOTIENT_DEF = sig datatype flag = absF | repF - val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term * (typ * typ) + val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term val make_def: binding -> term -> typ -> mixfix -> Attrib.binding -> (typ * typ) list -> Proof.context -> (term * thm) * local_theory @@ -38,68 +38,54 @@ fun get_fun flag qenv lthy ty = let - fun get_fun_aux s fs_tys = - let - val (fs, tys) = split_list fs_tys - val (otys, ntys) = split_list tys - val oty = Type (s, otys) - val nty = Type (s, ntys) - val ftys = map (op -->) tys - in + fun get_fun_aux s fs = (case (maps_lookup (ProofContext.theory_of lthy) s) of - SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) + SOME info => list_comb (Const (#mapfun info, dummyT), fs) | NONE => error ("no map association for type " ^ s)) - end - fun get_fun_fun fs_tys = - let - val (fs, tys) = split_list fs_tys - val ([oty1, oty2], [nty1, nty2]) = split_list tys - val oty = nty1 --> oty2 - val nty = oty1 --> nty2 - val ftys = map (op -->) tys - in - (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) - end - - fun get_const flag (qty, rty) = + fun get_const flag qty = let val thy = ProofContext.theory_of lthy val qty_name = Long_Name.base_name (fst (dest_Type qty)) in case flag of - absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) - | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) + absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) end fun mk_identity ty = Abs ("", ty, Bound 0) in if (AList.defined (op=) qenv ty) - then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty))) + then (get_const flag ty) else (case ty of - TFree _ => (mk_identity ty, (ty, ty)) - | Type (_, []) => (mk_identity ty, (ty, ty)) + TFree _ => mk_identity ty + | Type (_, []) => mk_identity ty | Type ("fun" , [ty1, ty2]) => - get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] + let + val fs_ty1 = get_fun (negF flag) qenv lthy ty1 + val fs_ty2 = get_fun flag qenv lthy ty2 + in + get_fun_aux "fun" [fs_ty1, fs_ty2] + end | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) - | _ => raise ERROR ("no type variables")) + | _ => error ("no type variables allowed")) end fun make_def nconst_bname rhs qty mx attr qenv lthy = let val (arg_tys, res_ty) = strip_type qty - val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys - val abs_fn = (fst o get_fun absF qenv lthy) res_ty + val rep_fns = map (get_fun repF qenv lthy) arg_tys + val abs_fn = (get_fun absF qenv lthy) res_ty - fun mk_fun_map t s = + fun mk_fun_map t s = Const (@{const_name "fun_map"}, dummyT) $ t $ s - val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn - |> Syntax.check_term lthy + val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) + |> Syntax.check_term lthy in - define nconst_bname mx attr (absrep_fn $ rhs) lthy + define nconst_bname mx attr absrep_trm lthy end @@ -131,21 +117,21 @@ val global_qenv = Quotient_Info.mk_qenv lthy val thy = ProofContext.theory_of lthy - fun is_inst thy (qty, rty) (qty', rty') = - if Sign.typ_instance thy (qty, qty') - then let - val inst = Sign.typ_match thy (qty', qty) Vartab.empty - in - rty = Envir.subst_type inst rty' - end - else false + fun is_inst (qty, rty) (qty', rty') = + if Sign.typ_instance thy (qty, qty') + then let + val inst = Sign.typ_match thy (qty', qty) Vartab.empty + in + rty = Envir.subst_type inst rty' + end + else false fun chk_inst (qty, rty) = - if exists (is_inst thy (qty, rty)) global_qenv + if exists (is_inst (qty, rty)) global_qenv then true else error_msg lthy (qty, rty) in - forall chk_inst qenv + map chk_inst qenv end