nominal2: Nominal/Lift.thy@1c9931e5039a (annotated)

1274 d867021d8ac1 Preparing the generalized lifting procedure Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Lift
1494 923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
1274 d867021d8ac1 Preparing the generalized lifting procedure Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
d867021d8ac1 Preparing the generalized lifting procedure Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
1316 0577afdb1732 Porting from Lift to Parser; until defining the Quotient type. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1309 diff changeset	5	ML {*
1494 923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	6	fun lift_thm ctxt thm =
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	7	let
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	8	fun un_raw name = unprefix "_raw" name handle Fail _ => name
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	9	fun add_under names = hd names :: (map (prefix "_") (tl names))
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	10	fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	11	val un_raw_names = rename_vars un_raws
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	12	in
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	13	un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	14	end
1276 3365fce80f0f To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1274 diff changeset	15	*}
1274 d867021d8ac1 Preparing the generalized lifting procedure Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16
1494 923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	17	ML {*
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	18	fun quotient_lift_consts_export spec ctxt =
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	19	let
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	20	val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	21	val (ts_loc, defs_loc) = split_list result;
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	22	val morphism = ProofContext.export_morphism ctxt' ctxt;
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	23	val ts = map (Morphism.term morphism) ts_loc
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	24	val defs = Morphism.fact morphism defs_loc
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	25	in
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	26	(ts, defs, ctxt')
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	27	end
923413256cbb Clean 'Lift', start working only on exported things in Parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1342 diff changeset	28	*}
1342 2b98012307f7 Lift distinct. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1316 diff changeset	29
1497 1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	30	ML {*
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	31	fun define_fv_alpha_export dt binds bns ctxt =
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	32	let
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	33	val (((fv_ts_loc, fv_def_loc), alpha), ctxt') =
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	34	define_fv_alpha dt binds bns ctxt;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	35	val alpha_ts_loc = #preds alpha
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	36	val alpha_induct_loc = #induct alpha
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	37	val alpha_intros_loc = #intrs alpha;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	38	val alpha_cases_loc = #elims alpha
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	39	val morphism = ProofContext.export_morphism ctxt' ctxt;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	40	val fv_ts = map (Morphism.term morphism) fv_ts_loc;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	41	val fv_def = Morphism.fact morphism fv_def_loc;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	42	val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	43	val alpha_induct = Morphism.thm morphism alpha_induct_loc;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	44	val alpha_intros = Morphism.fact morphism alpha_intros_loc
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	45	val alpha_cases = Morphism.fact morphism alpha_cases_loc
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	46	in
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	47	(((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt')
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	48	end;
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	49	*}
1c9931e5039a Move most of the exporting out of the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1494 diff changeset	50
1280 1f057f8da8aa Progress with general lifting procedure. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1277 diff changeset	51	end
1274 d867021d8ac1 Preparing the generalized lifting procedure Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Thu, 18 Mar 2010 08:03:42 +0100
changeset 1497	1c9931e5039a
parent 1494	923413256cbb
child 1498	2ff84b1f551f
permissions	-rw-r--r--