nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:b82e765ca464
+:df225aa45770
 section {* type definition for the quotient type *}
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
-ML {*
-fun error_msg pre post msg =
-msg |> quote
-|> enclose (pre ^ " ") (" " ^ post)
-|> error
-*}
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, FUN_REL)]]
 *}
 section {* lifting of constants *}
 ML {*
-fun lookup_snd _ [] _ = NONE
-| lookup_snd eq ((value, key)::xs) key' =
-if eq (key', key) then SOME value
-else lookup_snd eq xs key';
 fun lookup_qenv qenv qty =
-(case (AList.lookup (op =) qenv qty) of
+(case (AList.lookup (op=) qenv qty) of
 SOME rty => SOME (qty, rty)
 | NONE => NONE)
 *}
 ML {*
 val nty = Type (s, ntys)
 val ftys = map (op -->) tys
 in
 (case (maps_lookup (ProofContext.theory_of lthy) s) of
 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
-| NONE      => raise ERROR ("no map association for type " ^ s))
+| NONE      => error ("no map association for type " ^ s))
 end
 fun get_fun_fun fs_tys =
 let
 val (fs, tys) = split_list fs_tys
 end
 fun mk_identity ty = Abs ("", ty, Bound 0)
 in
-if (AList.defined (op =) qenv ty)
+if (AList.defined (op=) qenv ty)
 then (get_const flag (the (lookup_qenv qenv ty)))
 else (case ty of
 TFree _ => (mk_identity ty, (ty, ty))
 | Type (_, []) => (mk_identity ty, (ty, ty))
 | Type ("fun" , [ty1, ty2]) =>
 | _ => raise ERROR ("no type variables")
 )
 end
 *}
-text {* produces the definition for a lifted constant *}
+ML {*
+fun make_def nconst_bname rhs qty mx qenv lthy =
-ML {*
-fun get_const_def nconst otrm qenv lthy =
 let
-val ty = fastype_of nconst
+val (arg_tys, res_ty) = strip_type qty
-val (arg_tys, res_ty) = strip_type ty
 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
-fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
+fun mk_fun_map t s =
+Const (@{const_name "fun_map"}, dummyT) $ t $ s
-val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)
-|> Syntax.check_term lthy
+val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
+|> Syntax.check_term lthy
 in
-fns $ otrm
+define (nconst_bname, mx, absrep_fn $ rhs) lthy
 end
 *}
+ML {*
-ML {*
+(* returns all subterms where two types differ *)
-fun exchange_ty qenv ty =
-case (lookup_snd (op =) qenv ty) of
-SOME qty => qty
-| NONE =>
-(case ty of
-Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
-| _ => ty
-)
-*}
-ML {*
-fun ppair lthy (ty1, ty2) =
-"(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
-*}
-ML {*
-fun print_env qenv lthy =
-map (ppair lthy) qenv
-|> commas
-|> tracing
-*}
-ML {*
-fun make_const_def nconst_bname otrm mx qenv lthy =
-let
-val otrm_ty = fastype_of otrm
-val nconst_ty = exchange_ty qenv otrm_ty
-val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
-val def_trm = get_const_def nconst otrm qenv lthy
-in
-define (nconst_bname, mx, def_trm) lthy
-end
-*}
-ML {*
-(* difference of two types *)
 fun diff (T, S) Ds =
 case (T, S) of
 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
 | (Type (a, Ts), Type (b, Us)) =>
 | diffs ([], []) Ds = Ds
 | diffs _ _ = error "Unequal length of type arguments"
 *}
 ML {*
-fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy =
+fun error_msg lthy (qty, rty) =
 let
-val (_, rhs) = Logic.dest_equals prop
+val qtystr = quote (Syntax.string_of_typ lthy qty)
+val rtystr = quote (Syntax.string_of_typ lthy rty)
+in
+error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
+end
+fun sanity_chk lthy qenv =
+let
+val 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 chk_inst (qty, rty) =
+if exists (is_inst thy (qty, rty)) qenv' then true
+else error_msg lthy (qty, rty)
+in
+forall chk_inst qenv
+end
+*}
+ML {*
+fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
+let
+val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
+val (_, rhs) = PrimitiveDefs.abs_def prop'
 val rty = fastype_of rhs
 val qenv = distinct (op=) (diff (qty, rty) [])
 in
-make_const_def bind rhs mx qenv lthy
+sanity_chk lthy qenv;
-end
+make_def bind rhs qty mx qenv lthy
-*}
+end
+*}
-ML {*
-val constdecl =
+ML {*
-OuterParse.binding --
+val quotdef_parser =
-(OuterParse.$$$ "::" |-- OuterParse.!!!
+(OuterParse.binding --
-(OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_))
+(OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
->> OuterParse.triple2;
+OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
-*}
+(SpecParse.opt_thm_name ":" -- OuterParse.prop)
+*}
-ML {*
-val quotdef_parser =
+ML {*
-(constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
+fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
-*}
-ML {*
-fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy =
 let
 val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
 val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
 in
-quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd
+quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 *}
 ML {*
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-OuterKeyword.thy_decl (quotdef_parser >> quotdef)
+OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 *}
 section {* ATOMIZE *}
 text {*
 ML {*
 fun old_get_fun flag rty qty lthy ty =
 get_fun flag [(qty, rty)] lthy ty
 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
-make_const_def nconst_bname otrm mx [(qty, rty)] lthy
+make_def nconst_bname otrm qty mx [(qty, rty)] lthy
 *}
 text {* Does the same as 'subst' in a given prop or theorem *}
 ML {*
 fun eqsubst_prop ctxt thms t =

changeset 274	df225aa45770
parent 273	b82e765ca464
child 275	34ad627ac5d5