# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267725443 -3600
# Node ID 2b98012307f7cdad8a4a001adcd41a18d2ebea8a
# Parent  c25f797c7e6ec9db7ed98729256bf900514db490
Lift distinct.

diff -r c25f797c7e6e -r 2b98012307f7 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Lift.thy	Thu Mar 04 18:57:23 2010 +0100
@@ -64,6 +64,8 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
+
+
 ML {*
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm5"
@@ -85,21 +87,24 @@
 val induct = #induct info;
 val inducts = #inducts info;
 val infos = map (Datatype.the_info thy1) all_full_tnames;
+val rel_infos = List.take (infos, number);
 val inject = flat (map #inject infos);
 val distinct = flat (map #distinct infos);
+val rel_distinct = map #distinct rel_infos;
 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1;
 val lthy1 = Theory_Target.init NONE thy2
 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;
 val alpha_ts_loc = #preds alpha
 val alpha_intros = #intrs alpha
-val alpha_cases = #elims alpha
+val alpha_cases_loc = #elims alpha
 val alpha_induct_loc = #induct alpha
+val alpha_cases = ProofContext.export lthy2 lthy1 alpha_cases_loc
 val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc]
 (* TODO replace when inducts is provided by the 2 lines below: *)
 val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct
 (*val alpha_inducts_loc = #inducts alpha
 val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)
-val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
+val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy2
 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc
 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
 val morphism = ProofContext.export_morphism lthy2 lthy1
@@ -109,7 +114,7 @@
 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;
 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;
-val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4;
+val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc 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 ~~ typs) ~~ alpha_ts))
@@ -139,10 +144,13 @@
 val lthy11 = Theory_Target.init NONE thy3;
 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct));
 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
+val rel_dists = flat (map (distinct_rel lthy12 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, number))))
+
 *}
 
 setup {* fn _ => Local_Theory.exit_global lthy12 *}
 thm lift_induct
 
+
 end
 
diff -r c25f797c7e6e -r 2b98012307f7 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 18:57:23 2010 +0100
@@ -240,8 +240,10 @@
   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
+  val rel_dtinfos = List.take (dtinfos, (length dts));
   val inject = flat (map #inject dtinfos);
   val distinct = flat (map #distinct dtinfos);
+  val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
@@ -261,8 +263,9 @@
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
   val alpha_intros = #intrs alpha;
-  val alpha_cases = #elims alpha
-  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4
+  val alpha_cases_loc = #elims alpha
+  val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
+  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 (*  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
@@ -272,7 +275,7 @@
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
+    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -318,7 +321,11 @@
   val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
   val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
   val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
-  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*)
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
+  val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
+    (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
+  val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+  val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;*)
 in
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 end
diff -r c25f797c7e6e -r 2b98012307f7 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Perm.thy	Thu Mar 04 18:57:23 2010 +0100
@@ -134,6 +134,37 @@
 end
 *}
 
+ML {*
+fun neq_to_rel r neq =
+let
+  val neq = HOLogic.dest_Trueprop (prop_of neq)
+  val eq = HOLogic.dest_not neq
+  val (lhs, rhs) = HOLogic.dest_eq eq
+  val rel = r $ lhs $ rhs
+  val nrel = HOLogic.mk_not rel
+in
+  HOLogic.mk_Trueprop nrel
+end
+*}
+
+ML {*
+fun neq_to_rel_tac cases distinct =
+  rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
+*}
+
+ML {*
+fun distinct_rel ctxt cases (dists, rel) =
+let
+  val ((_, thms), ctxt') = Variable.import false dists ctxt
+  val terms = map (neq_to_rel rel) thms
+  val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
+in
+  Variable.export ctxt' ctxt nrels
+end
+*}
+
+
+
 (* Test
 atom_decl name
 
diff -r c25f797c7e6e -r 2b98012307f7 Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 18:57:23 2010 +0100
@@ -148,7 +148,8 @@
 thm lam_bp_perm
 thm lam_bp_fv
 thm lam_bp_bn
-thm lam_bp_inject*)
+thm lam_bp_inject
+thm lam_bp_distinct*)
 
 text {* example 2 *}