nominal2: Nominal/nominal_dt_quot.ML@c6d30d5f5ba1 (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
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	10	val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list ->
2337 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
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	13	val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory ->
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	Quotient_Info.qconsts_info list * local_theory
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	15
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	16	val define_qperms: typ list -> string list -> (string * term * mixfix) list ->
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	17	thm list -> theory -> theory
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	18
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	19	val define_qsizes: typ list -> string list -> (string * term * mixfix) list ->
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	20	theory -> theory
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	struct
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	(* defines the quotient types *)
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	27	fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	let
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	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	30	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	31	in
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	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	33	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
2338 e1764a73c292 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2337 diff changeset	35
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	(* defines quotient constants *)
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	37	fun define_qconsts qtys consts_specs lthy =
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	let
2338 e1764a73c292 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2337 diff changeset	39	val (qconst_infos, lthy') =
e1764a73c292 slight cleaning Christian Urban <urbanc@in.tum.de> parents: 2337 diff changeset	40	fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	val phi = ProofContext.export_morphism lthy' lthy
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	in
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	(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	44	end
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	46
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	47	(* defines the quotient permutations and proves pt-class *)
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	48	fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy =
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	49	let
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	50	val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	51
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	52	val (_, lthy') = define_qconsts qtys perm_specs lthy
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	53
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	54	val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	55
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	56	fun tac _ =
4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	57	Class.intro_classes_tac [] THEN
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	58	(ALLGOALS (resolve_tac lifted_perm_laws))
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	59	in
2398 1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	60	lthy'
1e6160690546 improved code Christian Urban <urbanc@in.tum.de> parents: 2396 diff changeset	61	\|> Class.prove_instantiation_exit tac
2346 4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	62	end
4c5881455923 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2338 diff changeset	63
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	64
2400 c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	65	(* defines the size functions and proves size-class *)
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	66	fun define_qsizes qtys qfull_ty_names size_specs thy =
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	67	let
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	68	val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	69
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	70	val (_, lthy') = define_qconsts qtys size_specs lthy
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	71
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	72	fun tac _ = Class.intro_classes_tac []
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	73	in
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	74	lthy'
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	75	\|> Class.prove_instantiation_exit tac
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	76	end
c6d30d5f5ba1 defined qperms and qsizes Christian Urban <urbanc@in.tum.de> parents: 2398 diff changeset	77
2337 b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	end (* structure *)
b151399bd2c3 fixed according to changes in quotient Christian Urban <urbanc@in.tum.de> parents: diff changeset	79

author	Christian Urban <urbanc@in.tum.de>
	Sun, 15 Aug 2010 14:00:28 +0800
changeset 2400	c6d30d5f5ba1
parent 2398	1e6160690546
child 2401	7645e18e8b19
permissions	-rw-r--r--