--- a/Nominal/Abs.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Abs.thy Tue Mar 02 15:07:27 2010 +0100
@@ -75,12 +75,11 @@
done
lemma alpha_gen_compose_sym:
- assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ fixes pi
+ assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+ shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
using b apply -
- apply(erule exE)
- apply(rule_tac x="- pi" in exI)
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
apply(rule conjI)
@@ -92,16 +91,14 @@
done
lemma alpha_gen_compose_trans:
- assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
- and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)"
+ fixes pi pia
+ assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+ and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)"
+ shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
using b c apply -
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
- apply(erule exE)+
- apply(erule conjE)+
- apply(rule_tac x="pia + pi" in exI)
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa" in spec)
apply(drule mp)
@@ -114,14 +111,13 @@
done
lemma alpha_gen_compose_eqvt:
- assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+ fixes pia
+ assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
- shows "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)"
+ shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
using b
apply -
- apply(erule exE)
- apply(rule_tac x="pi \<bullet> pia" in exI)
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
apply(rule conjI)
@@ -351,6 +347,8 @@
notation
alpha1 ("_ \<approx>abs1 _")
+thm swap_set_not_in
+
lemma qq:
fixes S::"atom set"
assumes a: "supp p \<inter> S = {}"
@@ -417,6 +415,7 @@
apply(simp add: supp_swap)
done
+(*
thm supp_perm
lemma perm_induct_test:
@@ -500,15 +499,6 @@
apply(simp)
oops
-fun
- distinct_perms
-where
- "distinct_perms [] = True"
-| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
-
-
-
-
-
+*)
end
--- a/Nominal/Fv.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Fv.thy Tue Mar 02 15:07:27 2010 +0100
@@ -54,6 +54,13 @@
in the database.
*)
+ML {*
+fun map2i _ [] [] = []
+ | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
+ | map2i f (x :: xs) [] = f x [] :: map2i f xs []
+ | map2i _ _ _ = raise UnequalLengths;
+*}
+
(* TODO: should be const_name union *)
ML {*
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
@@ -185,8 +192,8 @@
in
(fv_eq, alpha_eq)
end;
- fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
- val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+ fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
+ val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall))
val add_binds = map (fn x => (Attrib.empty_binding, x))
val (fvs, lthy') = (Primrec.add_primrec
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
@@ -303,18 +310,26 @@
fun reflp_tac induct inj =
rtac induct THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
- TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+(* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*)
(rtac @{thm exI[of _ "0 :: perm"]} THEN'
asm_full_simp_tac (HOL_ss addsimps
@{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
*}
+lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+by auto
+
ML {*
fun symp_tac induct inj eqvt =
- ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+ (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
- TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
+ (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'
+ (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))))
*}
ML {*
@@ -340,14 +355,23 @@
)
*}
+
+lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+apply (erule exE)+
+apply (rule_tac x="pia + pi" in exI)
+by auto
+
ML {*
fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
(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'
- TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])
+ asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct)
+ 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
+ (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))
)
*}
--- a/Nominal/LFex.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/LFex.thy Tue Mar 02 15:07:27 2010 +0100
@@ -24,9 +24,9 @@
local_setup {*
snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
- [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
- [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
- [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ [[ [], [(NONE, 1, 2)]],
+ [ [], [], [(NONE, 1, 2)] ],
+ [ [], [], [], [(NONE, 1, 2)]]] *}
notation
alpha_rkind ("_ \<approx>ki _" [100, 100] 100)
and alpha_rty ("_ \<approx>ty _" [100, 100] 100)
--- a/Nominal/Lift.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Lift.thy Tue Mar 02 15:07:27 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} \<union> (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 \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
@{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)
val lthy11 = Theory_Target.init NONE thy3;
--- a/Nominal/Rsp.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Rsp.thy Tue Mar 02 15:07:27 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 {*
@@ -136,6 +140,10 @@
end
*}
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
ML {*
fun build_alpha_eqvts funs perms simps induct ctxt =
@@ -151,18 +159,20 @@
(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 impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps
+ (
+ (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
+ 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
+ (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
(asm_full_simp_tac (HOL_ss addsimps
- (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
+ (@{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
*}
-
end
--- a/Nominal/Term1.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Term1.thy Tue Mar 02 15:07:27 2010 +0100
@@ -52,99 +52,10 @@
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 ["p"] (Datatype_Prop.make_tnames (map body_type types));
- val indnames2 = Name.variant_list ("p" :: 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 impI THEN' etac induct) ORELSE' 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
-
-in
- gl
-end
-*}ye
-
-lemma alpha_gen_compose_eqvt:
- assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
- and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
- and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
- shows "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s) \<and> P g pi d e t s R f pia"
- using b
- apply -
-sorry
-
-lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (p \<bullet> pi)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="pia \<bullet> pi" in exI)
-by auto
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
+build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *}
-prove {*
- build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context}
-*}
-apply(rule alpha_rtrm1_alpha_bp.induct)
-apply(simp_all add: atom_eqvt alpha1_inj)
-apply(erule exi)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(rule conjI)
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
-apply(subst empty_eqvt[symmetric])
-apply(subst insert_eqvt[symmetric])
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply simp
-apply(rule conjI)
-apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-thm eqvts
-apply(simp add:eqvts)
-
-thm insert_eqvt
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric])
-
-apply(rule conjI)
-thm atom_eqvt
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply simp
-apply(rule conjI)
-apply(subst permute_eqvt[symmetric])
-apply simp
-apply(rule conjI)
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply simp
-apply(subst permute_eqvt[symmetric])
-apply simp
-apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
-apply(simp)
-thm permute_eq_iff[THEN iffD1]
-apply(clarify)
-apply(rule conjI)
-
-apply(erule alpha_gen_compose_eqvt)
-
-prefer 2
-apply(erule conj_forward)
-apply (simp add: eqvts)
-apply(erule alpha_gen_compose_eqvt)
lemma alpha1_eqvt_proper[eqvt]:
"pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
"pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"
--- a/Nominal/Term4.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Term4.thy Tue Mar 02 15:07:27 2010 +0100
@@ -30,7 +30,7 @@
thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
+ [[[], [], [(NONE, 0,1)]], [[], []] ] *}
print_theorems
notation
--- a/Nominal/Term6.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Term6.thy Tue Mar 02 15:07:27 2010 +0100
@@ -22,7 +22,7 @@
print_theorems
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+ [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *}
notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
thm alpha_rtrm6.intros
@@ -41,7 +41,7 @@
(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))
*}
-
+thm alpha6_eqvt
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)) *}
thm alpha6_equivp
--- a/Nominal/Test.thy Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Test.thy Tue Mar 02 15:07:27 2010 +0100
@@ -68,22 +68,20 @@
text {* example type schemes *}
-(* does not work yet
-nominal_datatype t =
- Var "name"
+(* does not work yet
+nominal_datatype t =
+ Var "name"
| Fun "t" "t"
-nominal_datatype tyS =
+nominal_datatype tyS =
All xs::"name list" ty::"t_raw" bind xs in ty
*)
-(* also does not work
nominal_datatype t =
Var "name"
| Fun "t" "t"
and tyS =
- All xs::"name list" ty::"t" bind xs in ty
-*)
+ All xs::"name set" ty::"t" bind xs in ty
(* example 1 from Terms.thy *)
@@ -137,12 +135,12 @@
(* example 4 from Terms.thy *)
-(* does not work yet
+
nominal_datatype trm4 =
Vr4 "name"
| Ap4 "trm4" "trm4 list"
| Lm4 x::"name" t::"trm4" bind x in t
-*)
+
(* example 5 from Terms.thy *)