--- a/Nominal/Lift.thy	Fri Feb 26 15:42:00 2010 +0100
+++ b/Nominal/Lift.thy	Fri Feb 26 16:15:03 2010 +0100
@@ -1,5 +1,5 @@
 theory Lift
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
 begin
 
 atom_decl name
@@ -7,97 +7,93 @@
 
 datatype rtrm2 =
   rVr2 "name"
-| rAp2 "rtrm2" "rtrm2 list"
+| rAp2 "rtrm2" "rtrm2"
 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
 and ras =
   rAs "name" "rtrm2"
 
 primrec rbv2 where "rbv2 (rAs x t) = {atom x}"
 
+ML {*
+val thy1 = @{theory};
+val info = Datatype.the_info @{theory} "Lift.rtrm2"
+val number = 2; (* Number of defined types, rest are unfoldings *)
+val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]],
+             [[[], []]]  (*, [[], [[], []]] *) ];
+val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *)
+val bv_simps = @{thms rbv2.simps}
 
-ML {*
-fun build_eqvts_ funs perms simps induct ctxt =
-let
-  val pi = Free ("pi", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val fv_indnames = Datatype_Prop.make_tnames (map body_type types);
-  val args = map Free (fv_indnames ~~ types);
-  val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})
-  fun eqvtc (fv, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
-  fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
-in
-  Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac
-end
-*}
+val ntnames = [@{binding trm2}, @{binding as}]
+val ncnames = ["Vr2", "Ap2", "Lt2", "As"]
+
+
 
 
-ML {*
-print_depth 500;
-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}
-val info = Datatype.the_info @{theory} ftname;
-*}
-
-.
-{*
 val descr = #descr info;
+val sorts = #sorts info;
+val nos = map fst descr
+val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos
+val typs = List.take (all_typs, number)
 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
-val full_tnames = List.take (all_full_tnames, length tnames);
+val full_tnames = List.take (all_full_tnames, number);
 val induct = #induct info;
 val inducts = #inducts info;
-val infos = map (Datatype.the_info @{theory}) all_full_tnames;
+val infos = map (Datatype.the_info thy1) all_full_tnames;
 val inject = flat (map #inject infos);
 val distinct = flat (map #distinct infos);
-val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms tnames full_tnames thy1;
+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 ftname binds lthy1;
+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_induct = #induct alpha
-val alpha_inj = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
+val alpha_induct_loc = #induct alpha
+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 = ProofContext.export lthy2 lthy1 alpha_inj_loc
 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_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;
+fun build_bv_eqvt (t, n) =
+  build_eqvts Binding.empty [t] [nth perms n]
+    (bv_simps @ raw_perm_def) (nth inducts n)
+val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2;
+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 = ProofContext.export lthy4 lthy1 alpha_equivp_loc
 val lthy5 = define_quotient_type
-  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
+  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts))
   (ALLGOALS (resolve_tac alpha_equivp)) lthy4;
-val ((c, def), lthy6) = Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}) lthy5
+val consts =
+  flat (map (fn (i, (_, _, l)) =>
+    map (fn (cname, dts) =>
+      Const (cname, map (typ_of_dtyp descr sorts) dts --->
+        typ_of_dtyp descr sorts (DtRec i))) l) descr);
+val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5;
+val (cs, def) = split_list csdefl;
+val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts
+  (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6
+val (bvs_rsp', lthy8) = fold_map (
+  fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t]
+    (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7
+val bvs_rsp = flat (map snd bvs_rsp')
+val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+  (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8
+val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms
+  (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9;
+val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy1, induct));
+val lthy11 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy10)
 *}
 
-ML {*
-val thyf = Local_Theory.exit_global lthy6;
-*}
-setup {* fn _ => thyf *}
-print_theorems
-
-
-
+setup {* fn _ => Local_Theory.exit_global lthy11 *}
+thm lift_induct
 
-ML {*
-val lthy5 = define_quotient_type
-  (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) (ntnames ~~ alpha_ts))
-  (ALLGOALS (resolve_tac alpha_equivp)) lthy4
-*}
+end
 
-ML {*
-
-*}
-
-