# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267176844 -3600
# Node ID 3365fce80f0f379e499603943781e6f755e49615
# Parent  3effd5446226c3c370eb77d1ecada0bbb7464c8a
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.

diff -r 3effd5446226 -r 3365fce80f0f Nominal/Lift.thy
--- a/Nominal/Lift.thy	Thu Feb 25 15:41:23 2010 +0100
+++ b/Nominal/Lift.thy	Fri Feb 26 10:34:04 2010 +0100
@@ -40,6 +40,7 @@
 val thy1 = @{theory};
 val tnames = ["rtrm2", "ras"];
 val ftname = "Lift.rtrm2"
+val ntnames = [(@{binding trm2}, @{typ rtrm2}), (@{binding as}, @{typ ras})]
 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], 
              [[[], []]]  (*, [[], [[], []]] *) ];
 val bv_simps = @{thms rbv2.simps}
@@ -55,7 +56,7 @@
 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1;
 val lthy1 = Theory_Target.init NONE thy2
 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha ftname binds lthy1;
-val alpha_ts = #preds alpha
+val alpha_ts_loc = #preds alpha
 val alpha_intros = #intrs alpha
 val alpha_cases = #elims alpha
 val alpha_induct = #induct alpha
@@ -63,26 +64,35 @@
 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
 val morphism = ProofContext.export_morphism lthy2 lthy1
 val fv_ts = map (Morphism.term morphism) fv_ts_loc
+val alpha_ts = map (Morphism.term morphism) alpha_ts_loc
 val (bv_eqvts, lthy3) = build_eqvts @{binding bv_eqvts} [@{term rbv2}] [hd (tl perms)] 
   (bv_simps @ raw_perm_def) @{thm rtrm2_ras.inducts(2)} lthy2;
 val (fv_eqvts, lthy4) = build_eqvts @{binding fv_eqvts} fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
-val alpha_eqvt = build_alpha_eqvts alpha_ts perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;
-val alpha_equivp = build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4
+val alpha_eqvt = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj) alpha_induct lthy4;
+val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct inject alpha_inj distinct alpha_cases alpha_eqvt lthy4;
+val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
+val lthy5 = define_quotient_type
+  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
+  (ALLGOALS (resolve_tac alpha_equivp)) lthy4;
+val ((c, def), lthy6) = Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}) lthy5
+*}
 
+ML {*
+val thyf = Local_Theory.exit_global lthy6;
 *}
+setup {* fn _ => thyf *}
+print_theorems
+
 
 
 
 ML {*
-  val thyf = Local_Theory.exit_global lthy4
+val lthy5 = define_quotient_type
+  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
+  (ALLGOALS (resolve_tac alpha_equivp)) lthy4
 *}
-setup {* fn _ => thyf *}
-print_theorems
 
 ML {*
-(*val thyn = @{theory}
-val lthy3 = Theory_Target.init NONE thyn;*)
-build_equivps alpha_ts induct alpha_induct inject alpha_inj distinct alpha_cases @{thms alpha2_eqvt} lthy2
 
 *}