# HG changeset patch # User Cezary Kaliszyk # Date 1268893596 -3600 # Node ID 923413256cbb6a9de49f7969e91343eb30c79ebd # Parent 52f68b524fd28d8bfa27539646f4c3e238d57e12 Clean 'Lift', start working only on exported things in Parser. 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 diff -r 52f68b524fd2 -r 923413256cbb Nominal/Parser.thy --- a/Nominal/Parser.thy Thu Mar 18 00:17:21 2010 +0100 +++ b/Nominal/Parser.thy Thu Mar 18 07:26:36 2010 +0100 @@ -1,5 +1,5 @@ theory Parser -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift" begin atom_decl name @@ -253,14 +253,6 @@ end *} -ML {* -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 -fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) -*} - lemma equivp_hack: "equivp x" sorry ML {* @@ -333,10 +325,11 @@ val bn_tys = map (domain_type o fastype_of) raw_bn_funs; 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_intros_loc = #intrs alpha; val alpha_cases_loc = #elims alpha + val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc - val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 + val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc val _ = tracing "Proving equivariance"; val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; @@ -350,18 +343,16 @@ (fv_ts_loc_bn ~~ (map snd bns)) lthy6; val lthy6 = lthy6a; val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) - val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; + val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc; fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy - else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1 - val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6; - val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; + else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1 + val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; val _ = tracing "Proving equivalence"; - val alpha_equivp_loc = - if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn - else build_equivps alpha_ts_loc induct alpha_induct_loc - inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6; - val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; + val alpha_equivp = + if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn + else build_equivps alpha_ts induct alpha_induct + inject alpha_inj distincts alpha_cases alpha_eqvt lthy6; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names @@ -374,10 +365,7 @@ map (fn (cname, dts) => Const (cname, map (typ_of_dtyp descr sorts) dts ---> typ_of_dtyp descr sorts (DtRec i))) l) descr); - val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; - val (consts_loc, const_defs) = split_list consts_defs; - val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7; - val consts = map (Morphism.term morphism_8_7) consts_loc; + val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; (* Could be done nicer *) val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); val _ = tracing "Proving respects"; diff -r 52f68b524fd2 -r 923413256cbb Nominal/Rsp.thy --- a/Nominal/Rsp.thy Thu Mar 18 00:17:21 2010 +0100 +++ b/Nominal/Rsp.thy Thu Mar 18 07:26:36 2010 +0100 @@ -186,7 +186,7 @@ (split_conjs THEN_ALL_NEW TRY o resolve_tac @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) + asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) *} ML {*