# HG changeset patch # User Christian Urban # Date 1269271348 -3600 # Node ID 1dbc4f33549c0c0bd9102bf3cffca762b029d777 # Parent 8466fe2216da31952803d757a1ae8df117cef4fd# Parent 2c37f5a8c747e9c8213ee80c324c9e67d8ddb7f3 merged diff -r 8466fe2216da -r 1dbc4f33549c Nominal/Parser.thy --- a/Nominal/Parser.thy Mon Mar 22 16:22:07 2010 +0100 +++ b/Nominal/Parser.thy Mon Mar 22 16:22:28 2010 +0100 @@ -265,13 +265,11 @@ end *} -(* These 2 are critical, we don't know how to do it in term5 *) -ML {* val cheat_fv_rsp = Unsynchronized.ref true *} ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} - ML {* val cheat_equivp = Unsynchronized.ref true *} -(* These 2 are not needed any more *) +(* These 3 are not needed any more *) +ML {* val cheat_fv_rsp = Unsynchronized.ref false *} ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} @@ -332,7 +330,8 @@ else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; val _ = tracing "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; + val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; + val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn @@ -356,11 +355,15 @@ val _ = tracing "Proving respects"; val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] - (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; + (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy - else fvbv_rsp_tac alpha_induct fv_def 1; - val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 + else fvbv_rsp_tac alpha_induct fv_def lthy8 1; + val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; + val (fv_rsp_pre, lthy10) = fold_map + (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] + (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; + val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; diff -r 8466fe2216da -r 1dbc4f33549c Nominal/Rsp.thy --- a/Nominal/Rsp.thy Mon Mar 22 16:22:07 2010 +0100 +++ b/Nominal/Rsp.thy Mon Mar 22 16:22:28 2010 +0100 @@ -73,20 +73,21 @@ end *} - +ML {* +fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct +*} 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)) - THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' - asm_full_simp_tac - (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) +fun fvbv_rsp_tac induct fvbv_simps ctxt = + ind_tac induct THEN_ALL_NEW + (TRY o rtac @{thm TrueI}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) 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_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW + TRY o blast_tac (claset_of ctxt) *} - ML {* fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) fun all_eqvts ctxt = @@ -124,10 +125,6 @@ *) ML {* -fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct -*} - -ML {* fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 @@ -219,4 +216,90 @@ build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt *} +ML {* +fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = +let + val (fvs_alphas, ls) = split_list fv_alphas_lst; + val (fv_ts, alpha_ts) = split_list fvs_alphas; + val tys = map (domain_type o fastype_of) alpha_ts; + val names = Datatype_Prop.make_tnames tys; + val names2 = Name.variant_list names names; + val args = map Free (names ~~ tys); + val args2 = map Free (names2 ~~ tys); + fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2)); + fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) = + HOLogic.mk_imp ( + (alpha $ arg $ arg2), + (foldr1 HOLogic.mk_conj + (HOLogic.mk_eq (fv $ arg, fv $ arg2) :: + (map (mk_fv_rsp arg arg2) l)))); + val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls); + fun mk_fv_rsp_bn arg arg2 (fv, alpha) = + HOLogic.mk_imp ( + (alpha $ arg $ arg2), + HOLogic.mk_eq ((fv $ arg), (fv $ arg2))); + fun fv_rsp_arg_bn ((arg, arg2), l) = + map (mk_fv_rsp_bn arg arg2) l; + val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls)); + val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas; + val atys = map (domain_type o fastype_of) add_alphas; + val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys); + val aargs = map Free (anames ~~ atys); + val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True})) + add_alphas aargs; + val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs)); + val th = Goal.prove ctxt (names @ names2) [] eq tac; + val ths = HOLogic.conj_elims th; + val (ths_nobn, ths_bn) = chop (length ls) ths; + fun project (th, l) = + Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th)) + val ths_nobn_pr = map project (ths_nobn ~~ ls); +in + (flat ths_nobn_pr @ ths_bn) end +*} + +lemma equivp_rspl: + "equivp r \ r a b \ r a c = r b c" + unfolding equivp_reflp_symp_transp symp_def transp_def + by blast + +lemma equivp_rspr: + "equivp r \ r a b \ r c a = r c b" + unfolding equivp_reflp_symp_transp symp_def transp_def + by blast + +ML {* +fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) = +let + val alpha = nth alphas n; + val ty = domain_type (fastype_of alpha); + val names = Datatype_Prop.make_tnames [ty, ty]; + val [l, r] = map (fn x => (Free (x, ty))) names; + val g1 = + Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), + HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, + HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))) + val g2 = + Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), + HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, + HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))) + fun tac {context, ...} = ( + etac (nth inducts n) THEN_ALL_NEW + (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW + InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW + REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW + TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW + TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW + TRY o rtac refl + ) 1; + val t1 = Goal.prove ctxt names [] g1 tac; + val t2 = Goal.prove ctxt names [] g2 tac; +in + [t1, t2] +end +*} + + +end diff -r 8466fe2216da -r 1dbc4f33549c Nominal/Term5.thy --- a/Nominal/Term5.thy Mon Mar 22 16:22:07 2010 +0100 +++ b/Nominal/Term5.thy Mon Mar 22 16:22:28 2010 +0100 @@ -183,32 +183,8 @@ local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} print_theorems - -lemma alpha_rbv_rsp_pre: - "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done - -lemma alpha_rbv_rsp_pre2: - "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" @@ -221,13 +197,10 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - apply clarify - apply (simp add: alpha_rbv_rsp_pre2) - apply (simp add: alpha_rbv_rsp_pre) done lemma diff -r 8466fe2216da -r 1dbc4f33549c Nominal/Term5n.thy --- a/Nominal/Term5n.thy Mon Mar 22 16:22:07 2010 +0100 +++ b/Nominal/Term5n.thy Mon Mar 22 16:22:28 2010 +0100 @@ -123,31 +123,9 @@ local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} print_theorems -lemma alpha_rbv_rsp_pre: - "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp -lemma alpha_rbv_rsp_pre2: - "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" @@ -161,7 +139,7 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp) + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) done diff -r 8466fe2216da -r 1dbc4f33549c TODO --- a/TODO Mon Mar 22 16:22:07 2010 +0100 +++ b/TODO Mon Mar 22 16:22:28 2010 +0100 @@ -8,7 +8,7 @@ ty1_tyn.induct ty1_tyn.inducts instance ty1 and tyn :: fs - ty1_tyn.supp for too many bindings empty + ty1_tyn.supp empty when for too many bindings Smaller things: @@ -27,14 +27,17 @@ - check support equations for more bindings per constructor - automate the proofs that are currently proved with sorry: - alpha_equivp, fv_rsp, alpha_bn_rsp + alpha_equivp, alpha_bn_rsp - store information about defined nominal datatypes, so that it can be used to define new types that depend on these -- make 3 versions of Abs - - make parser aware of bn functions that call other bn functions and reflect it in the datastructure passed to Fv/Alpha generation - make parser aware of recursive and of different versions of abs + +Less important: + +- fv_rsp uses 'blast' to show goals of the type: + a u b = c u d ==> a u x u b = c u x u d