nominal2: comparison Nominal/Test.thy

equal deleted inserted replaced

-:b52b72676e20
+:76fa21f27f22
 | Ap "lm" "lm"
 | Lm x::"name" l::"lm"  bind x in l
 lemma finite_fv:
 shows "finite (fv_lm t)"
-apply(induct t rule: lm_induct)
+apply(induct t rule: lm.induct)
 apply(simp_all)
 done
 lemma supp_fn:
 shows "supp t = fv_lm t"
-apply(induct t rule: lm_induct)
+apply(induct t rule: lm.induct)
 apply(simp_all)
 apply(simp only: supp_def)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lm_eq_iff)
+apply(simp only: lm.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 done
-lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]]
+lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]]
 lemma
 fixes c::"'a::fs"
 assumes a1: "\<And>name c. P c (Vr name)"
 and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
 and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
 shows "P c lm"
 proof -
 have "\<And>p. P c (p \<bullet> lm)"
-apply(induct lm arbitrary: c rule: lm_induct)
+apply(induct lm arbitrary: c rule: lm.induct)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
 apply(rule a1)
-apply(simp only: lm_perm)
+apply(simp only: lm.perm)
 apply(rule a2)
 apply(blast)[1]
 apply(assumption)
 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
 apply(erule exE)
 apply(rule_tac t="p \<bullet> Lm name lm" and
 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-apply(simp del: lm_perm)
+apply(simp del: lm.perm)
-apply(subst lm_perm)
+apply(subst lm.perm)
-apply(subst (2) lm_perm)
+apply(subst (2) lm.perm)
 apply(rule flip_fresh_fresh)
 apply(simp add: fresh_def)
 apply(simp only: supp_fn')
 apply(simp)
 apply(simp add: fresh_Pair)
 binder
 bi::"bp \<Rightarrow> atom set"
 where
 "bi (BP x t) = {atom x}"
-thm lam_bp_fv
+thm lam_bp.fv
-thm lam_bp_eq_iff
+thm lam_bp.eq_iff
-thm lam_bp_bn
+thm lam_bp.bn
-thm lam_bp_perm
+thm lam_bp.perm
-thm lam_bp_induct
+thm lam_bp.induct
-thm lam_bp_inducts
+thm lam_bp.inducts
-thm lam_bp_distinct
+thm lam_bp.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 term "supp (x :: lam)"
 lemma bi_eqvt:
 by (rule eqvts)
 lemma supp_fv:
 shows "supp t = fv_lam t"
 and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
-apply(induct t and bp rule: lam_bp_inducts)
+apply(induct t and bp rule: lam_bp.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
 apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(blast)
 apply(simp add: supp_Abs)
 apply(blast)
 (* BP case *)
 apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp_eq_iff)
+apply(simp only: lam_bp.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp)
 done
-thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 ML {* val _ = recursive := true *}
 nominal_datatype lam' =
 VAR' "name"
 binder
 bi'::"bp' \<Rightarrow> atom set"
 where
 "bi' (BP' x t) = {atom x}"
-thm lam'_bp'_fv
+thm lam'_bp'.fv
-thm lam'_bp'_eq_iff[no_vars]
+thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'_bn
+thm lam'_bp'.bn
-thm lam'_bp'_perm
+thm lam'_bp'.perm
-thm lam'_bp'_induct
+thm lam'_bp'.induct
-thm lam'_bp'_inducts
+thm lam'_bp'.inducts
-thm lam'_bp'_distinct
+thm lam'_bp'.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 lemma supp_fv':
 shows "supp t = fv_lam' t"
 and "supp bp = fv_bp' bp"
-apply(induct t and bp rule: lam'_bp'_inducts)
+apply(induct t and bp rule: lam'_bp'.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
 apply(rule_tac t="supp (LET' bp' lam')" and
 s="supp (Abs (bi' bp') (bp', lam'))" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen)
 apply(simp only: eqvts split_def fst_conv snd_conv)
 apply(simp only: eqvts[symmetric] supp_Pair)
 apply(simp only: eqvts Pair_eq)
 apply(simp add: supp_Abs supp_Pair)
 apply blast
 apply(simp only: supp_def)
-apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'_eq_iff)
+apply(simp only: lam'_bp'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base supp_atom)
 apply simp
 done
-thm lam'_bp'_fv[simplified supp_fv'[symmetric]]
+thm lam'_bp'.fv[simplified supp_fv'[symmetric]]
 text {* example 2 *}
 ML {* val _ = recursive := false  *}
 where
 "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
-thm trm'_pat'_fv
+thm trm'_pat'.fv
-thm trm'_pat'_eq_iff
+thm trm'_pat'.eq_iff
-thm trm'_pat'_bn
+thm trm'_pat'.bn
-thm trm'_pat'_perm
+thm trm'_pat'.perm
-thm trm'_pat'_induct
+thm trm'_pat'.induct
-thm trm'_pat'_distinct
+thm trm'_pat'.distinct
 lemma supp_fv_trm'_pat':
 shows "supp t = fv_trm' t"
 and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
-apply(induct t and bp rule: trm'_pat'_inducts)
+apply(induct t and bp rule: trm'_pat'.inducts)
 apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
 apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
 apply(rule_tac t="supp (Let pat' trm'1 trm'2)"
 and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(blast)
 apply(simp add: supp_Abs)
 apply(blast)
 (* PN case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp)
 (* PS case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp)
 (* PD case *)
 apply(simp only: supp_def)
-apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'_eq_iff)
+apply(simp only: trm'_pat'.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
 apply(simp add: supp_at_base)
 done
-thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
+thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
 nominal_datatype trm0 =
 Var0 "name"
 | App0 "trm0" "trm0"
 | Lam0 x::"name" t::"trm0"          bind x in t
 where
 "f0 PN0 = {}"
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
-thm trm0_pat0_fv
+thm trm0_pat0.fv
-thm trm0_pat0_eq_iff
+thm trm0_pat0.eq_iff
-thm trm0_pat0_bn
+thm trm0_pat0.bn
-thm trm0_pat0_perm
+thm trm0_pat0.perm
-thm trm0_pat0_induct
+thm trm0_pat0.induct
-thm trm0_pat0_distinct
+thm trm0_pat0.distinct
 text {* example type schemes *}
 nominal_datatype t =
 VarTS "name"
 | FunTS "t" "t"
 and  tyS =
 All xs::"name set" ty::"t" bind xs in ty
-thm t_tyS_fv
+thm t_tyS.fv
-thm t_tyS_eq_iff
+thm t_tyS.eq_iff
-thm t_tyS_bn
+thm t_tyS.bn
-thm t_tyS_perm
+thm t_tyS.perm
-thm t_tyS_induct
+thm t_tyS.induct
-thm t_tyS_distinct
+thm t_tyS.distinct
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 lemma supports_subset:
 lemma finite_fv_t_tyS:
 fixes T::"t"
 and   S::"tyS"
 shows "finite (fv_t T)"
 and   "finite (fv_tyS S)"
-apply(induct T and S rule: t_tyS_inducts)
+apply(induct T and S rule: t_tyS.inducts)
-apply(simp_all add: t_tyS_fv)
+apply(simp_all add: t_tyS.fv)
 done
 lemma supp_fv_t_tyS:
 shows "supp T = fv_t T"
 and   "supp S = fv_tyS S"
-apply(induct T and S rule: t_tyS_inducts)
+apply(induct T and S rule: t_tyS.inducts)
 apply(simp_all)
 (* VarTS case *)
 apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS.perm)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* FunTS case *)
 apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS.perm)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* All case *)
 apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst)
 apply(simp (no_asm) only: supp_def)
-apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS.perm)
 apply(simp only: permute_ABS)
-apply(simp only: t_tyS_eq_iff)
+apply(simp only: t_tyS.eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
 where
 "bv1 (BUnit1) = {}"
 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
-thm trm1_bp1_fv
+thm trm1_bp1.fv
-thm trm1_bp1_eq_iff
+thm trm1_bp1.eq_iff
-thm trm1_bp1_bn
+thm trm1_bp1.bn
-thm trm1_bp1_perm
+thm trm1_bp1.perm
-thm trm1_bp1_induct
+thm trm1_bp1.induct
-thm trm1_bp1_distinct
+thm trm1_bp1.distinct
 text {* example 3 from Terms.thy *}
 nominal_datatype trm3 =
 Vr3 "name"
 bv3
 where
 "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-thm trm3_rassigns3_fv
+thm trm3_rassigns3.fv
-thm trm3_rassigns3_eq_iff
+thm trm3_rassigns3.eq_iff
-thm trm3_rassigns3_bn
+thm trm3_rassigns3.bn
-thm trm3_rassigns3_perm
+thm trm3_rassigns3.perm
-thm trm3_rassigns3_induct
+thm trm3_rassigns3.induct
-thm trm3_rassigns3_distinct
+thm trm3_rassigns3.distinct
 (* example 5 from Terms.thy *)
 nominal_datatype trm5 =
 Vr5 "name"
 bv5
 where
 "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
-thm trm5_lts_fv
+thm trm5_lts.fv
-thm trm5_lts_eq_iff
+thm trm5_lts.eq_iff
-thm trm5_lts_bn
+thm trm5_lts.bn
-thm trm5_lts_perm
+thm trm5_lts.perm
-thm trm5_lts_induct
+thm trm5_lts.induct
-thm trm5_lts_distinct
+thm trm5_lts.distinct
 (* example from my PHD *)
 atom_decl coname
 |  AndL1 n::"name" t::"phd" "name"                              bind n in t
 |  AndL2 n::"name" t::"phd" "name"                              bind n in t
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
-thm phd_fv
+thm phd.fv
-thm phd_eq_iff
+thm phd.eq_iff
-thm phd_bn
+thm phd.bn
-thm phd_perm
+thm phd.perm
-thm phd_induct
+thm phd.induct
-thm phd_distinct
+thm phd.distinct
 (* example form Leroy 96 about modules; OTT *)
 nominal_datatype mexp =
 Acc "path"
 | "Cbinders (Type1 t) = {atom t}"
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_eq_iff
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
 (* example 3 from Peter Sewell's bestiary *)
 nominal_datatype exp =
 VarP "name"
 where
 "bp'' (PVar x) = {atom x}"
 | "bp'' (PUnit) = {}"
 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
-thm exp_pat3_fv
+thm exp_pat3.fv
-thm exp_pat3_eq_iff
+thm exp_pat3.eq_iff
-thm exp_pat3_bn
+thm exp_pat3.bn
-thm exp_pat3_perm
+thm exp_pat3.perm
-thm exp_pat3_induct
+thm exp_pat3.induct
-thm exp_pat3_distinct
+thm exp_pat3.distinct
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
 EVar name
 | EPair exp6 exp6
 where
 "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-thm exp6_pat6_fv
+thm exp6_pat6.fv
-thm exp6_pat6_eq_iff
+thm exp6_pat6.eq_iff
-thm exp6_pat6_bn
+thm exp6_pat6.bn
-thm exp6_pat6_perm
+thm exp6_pat6.perm
-thm exp6_pat6_induct
+thm exp6_pat6.induct
-thm exp6_pat6_distinct
+thm exp6_pat6.distinct
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 (* example 7 from Peter Sewell's bestiary *)
 (* dest_Const raised

changeset 1515	76fa21f27f22
parent 1510	be911e869fde
child 1517	62d6f7acc110