diff -r 52f68b524fd2 -r 923413256cbb Nominal/Lift.thy --- a/Nominal/Lift.thy Thu Mar 18 00:17:21 2010 +0100 +++ b/Nominal/Lift.thy Thu Mar 18 07:26:36 2010 +0100 @@ -1,156 +1,31 @@ theory Lift -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" begin -atom_decl name -atom_decl ident - -(* datatype rtrm2 = - rVr2 "name" -| 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} - -val ntnames = [@{binding trm2}, @{binding as}] -val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) - -(*datatype rkind = - Type - | KPi "rty" "name" "rkind" -and rty = - TConst "ident" - | TApp "rty" "rtrm" - | TPi "rty" "name" "rty" -and rtrm = - Const "ident" - | Var "name" - | App "rtrm" "rtrm" - | Lam "rty" "name" "rtrm" -ML {* -val thy1 = @{theory}; -val info = Datatype.the_info @{theory} "Lift.rkind" -val number = 3; -val binds = [[ [], [(NONE, 1, 2)]], - [ [], [], [(NONE, 1, 2)] ], - [ [], [], [], [(NONE, 1, 2)]]]; -val bvs = [] -val bv_simps = [] - -val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] -val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*}*) - -datatype rtrm5 = - rVr5 "name" -| rAp5 "rtrm5" "rtrm5" -| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" -and rlts = - rLnil -| rLcons "name" "rtrm5" "rlts" - -primrec - rbv5 -where - "rbv5 rLnil = {}" -| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" - - - ML {* -val thy1 = @{theory}; -val info = Datatype.the_info @{theory} "Lift.rtrm5" -val number = 2; -val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ] -val bvs = [(@{term rbv5}, 1)] -val bv_simps = @{thms rbv5.simps} - -val ntnames = [@{binding trm5}, @{binding lts}] -val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"] - - -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 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_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_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 -val fv_ts = map (Morphism.term morphism) fv_ts_loc -val alpha_ts = map (Morphism.term morphism) alpha_ts_loc -val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts) 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_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)) - (ALLGOALS (resolve_tac alpha_equivp)) lthy4; -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 (bvs_rsp', lthy7) = 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 lthy6; -val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts - (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) 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 thy3 = Local_Theory.exit_global lthy10; -(* TODO: fix this hack... *) -(*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*) -(*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \ rtrm1 \ rtrm1"})] - @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) -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)))) - +fun lift_thm ctxt thm = +let + fun un_raw name = unprefix "_raw" name handle Fail _ => name + fun add_under names = hd names :: (map (prefix "_") (tl names)) + fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) + val un_raw_names = rename_vars un_raws +in + un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) +end *} -setup {* fn _ => Local_Theory.exit_global lthy12 *} -thm lift_induct - +ML {* +fun quotient_lift_consts_export spec ctxt = +let + val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt; + val (ts_loc, defs_loc) = split_list result; + val morphism = ProofContext.export_morphism ctxt' ctxt; + val ts = map (Morphism.term morphism) ts_loc + val defs = Morphism.fact morphism defs_loc +in + (ts, defs, ctxt') +end +*} end