--- 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;
--- 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 \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
+ unfolding equivp_reflp_symp_transp symp_def transp_def
+ by blast
+
+lemma equivp_rspr:
+ "equivp r \<Longrightarrow> r a b \<Longrightarrow> 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 \<and>"]}) 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
--- 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 \<approx>l y \<Longrightarrow> \<forall>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 \<approx>l y \<Longrightarrow> \<forall>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
--- 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 \<approx>l y \<Longrightarrow> \<forall>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 \<approx>l y \<Longrightarrow> \<forall>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
--- 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