nominal2: Nominal/nominal_dt_quot.ML@b151399bd2c3 (annotated)

2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	(* Title: nominal_dt_alpha.ML
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	Author: Christian Urban
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	Author: Cezary Kaliszyk
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	Performing quotient constructions
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	*)
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	7
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	signature NOMINAL_DT_QUOT =
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	sig
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list ->
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory ->
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	Quotient_Info.qconsts_info list * local_theory
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	struct
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	(* defines the quotient types *)
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	let
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	in
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	fold_map Quotient_Type.add_quotient_type qty_args2 lthy
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	28
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	(* defines quotient constants *)
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	fun qconst_defs qtys const_spec lthy =
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	let
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	val phi = ProofContext.export_morphism lthy' lthy
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	in
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	(map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	37
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	39
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	end (* structure *)
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	41

author	Christian Urban <urbanc@in.tum.de>
	Sun, 27 Jun 2010 21:41:21 +0100
changeset 2337	b151399bd2c3
child 2338	e1764a73c292
permissions	-rw-r--r--