--- a/Nominal/Terms.thy Thu Feb 25 12:15:11 2010 +0100
+++ b/Nominal/Terms.thy Thu Feb 25 12:30:50 2010 +0100
@@ -46,43 +46,6 @@
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
thm alpha1_inj
-lemma alpha_bp_refl: "alpha_bp a a"
-apply induct
-apply (simp_all add: alpha1_inj)
-done
-
-lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
-apply rule
-apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
-apply (simp_all add: alpha_bp_refl)
-done
-
-lemma alpha_bp_eq: "alpha_bp = (op =)"
-apply (rule ext)+
-apply (rule alpha_bp_eq_eq)
-done
-
-ML {*
-fun build_eqvts bind funs perms simps induct ctxt =
-let
- val pi = Free ("p", @{typ perm});
- val types = map (domain_type o fastype_of) funs;
- val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
- val args = map Free (indnames ~~ types);
- val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
- fun eqvtc (fnctn, (arg, perm)) =
- HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
- fun tac _ = (indtac induct indnames THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps
- (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
- val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
- val thms = HOLogic.conj_elims thm
-in
- Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
-end
-*}
-
local_setup {*
snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
*}
@@ -91,32 +54,6 @@
snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
*}
-ML {*
-fun build_alpha_eqvts funs perms simps induct ctxt =
-let
- val pi = Free ("p", @{typ perm});
- val types = map (domain_type o fastype_of) funs;
- val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
- val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
- val args = map Free (indnames ~~ types);
- val args2 = map Free (indnames2 ~~ types);
- fun eqvtc ((alpha, perm), (arg, arg2)) =
- HOLogic.mk_imp (alpha $ arg $ arg2,
- (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
- fun tac _ = (rtac induct THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps
- (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
- THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps
- (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
- val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
-in
- map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
-end
-*}
local_setup {*
(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
@@ -222,6 +159,17 @@
apply auto
done
+lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
+apply rule
+apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
+apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)])
+done
+
+lemma alpha_bp_eq: "alpha_bp = (op =)"
+apply (rule ext)+
+apply (rule alpha_bp_eq_eq)
+done
+
lemma supp_fv:
"supp t = fv_trm1 t"
"supp b = fv_bp b"
@@ -670,9 +618,18 @@
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *}
thm alpha6_inj
-lemma alpha6_eqvt:
- "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"
-sorry
+local_setup {*
+snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct})
+*}
+
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}
+*}
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
+ build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
+*}
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
(build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}