# HG changeset patch # User Cezary Kaliszyk # Date 1267536297 -3600 # Node ID c28403308b3471c6ae19d02c3eb4c440cecc88ba # Parent d3101a5b9c4d418a4df0196934cec62aa611026a More fixes for new alpha, the whole lift script should now work again. diff -r d3101a5b9c4d -r c28403308b34 Nominal/Fv.thy --- a/Nominal/Fv.thy Tue Mar 02 13:28:54 2010 +0100 +++ b/Nominal/Fv.thy Tue Mar 02 14:24:57 2010 +0100 @@ -325,7 +325,7 @@ fun symp_tac induct inj eqvt = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - (etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' + (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW (etac @{thm alpha_gen_compose_sym} THEN' @@ -367,7 +367,7 @@ (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW ( asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) - THEN_ALL_NEW (etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW + THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW diff -r d3101a5b9c4d -r c28403308b34 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue Mar 02 13:28:54 2010 +0100 +++ b/Nominal/Lift.thy Tue Mar 02 14:24:57 2010 +0100 @@ -25,7 +25,7 @@ val ntnames = [@{binding trm2}, @{binding as}] val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) -(* datatype rkind = +datatype rkind = Type | KPi "rty" "name" "rkind" and rty = @@ -41,16 +41,16 @@ val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rkind" val number = 3; -val binds = [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]]; +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"]*} *) +val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"] -datatype rtrm5 = +(*datatype rtrm5 = rVr5 "name" | rAp5 "rtrm5" "rtrm5" | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" @@ -64,18 +64,17 @@ "rbv5 rLnil = {}" | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" -ML Typedef.add_typedef - -ML {* +ML val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rtrm5" val number = 2; -val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] +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 ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*) + val descr = #descr info; val sorts = #sorts info; @@ -113,7 +112,7 @@ 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_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 @@ -126,19 +125,19 @@ 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 ( +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 lthy7 -val bvs_rsp = flat (map snd bvs_rsp') + (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 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; diff -r d3101a5b9c4d -r c28403308b34 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Tue Mar 02 13:28:54 2010 +0100 +++ b/Nominal/Rsp.thy Tue Mar 02 14:24:57 2010 +0100 @@ -78,8 +78,12 @@ ML {* fun fvbv_rsp_tac induct fvbv_simps = ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac - (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) + (TRY o rtac @{thm TrueI})) THEN_ALL_NEW + asm_full_simp_tac + (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) + THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' + asm_full_simp_tac + (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) *} ML {* @@ -158,7 +162,7 @@ ( (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) - THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN' + THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW