equal
deleted
inserted
replaced
4 |
4 |
5 text {* example 3 or example 5 from Terms.thy *} |
5 text {* example 3 or example 5 from Terms.thy *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := true *} |
9 ML {* val _ = recursive := false *} |
10 ML {* val _ = alpha_type := AlphaLst *} |
10 ML {* val _ = alpha_type := AlphaLst *} |
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Vr "name" |
12 Vr "name" |
13 | Ap "trm" "trm" |
13 | Ap "trm" "trm" |
14 | Lm x::"name" t::"trm" bind x in t |
14 | Lm x::"name" t::"trm" bind x in t |
83 apply(induct l rule: trm_lts.inducts(2)) |
83 apply(induct l rule: trm_lts.inducts(2)) |
84 apply(rule TrueI) |
84 apply(rule TrueI) |
85 apply(simp_all add:permute_bn eqvts) |
85 apply(simp_all add:permute_bn eqvts) |
86 done |
86 done |
87 |
87 |
|
88 lemma fv_perm_bn: |
|
89 "fv_bn l = fv_bn (permute_bn p l)" |
|
90 apply(induct l rule: trm_lts.inducts(2)) |
|
91 apply(rule TrueI) |
|
92 apply(simp_all add:permute_bn eqvts) |
|
93 done |
|
94 |
88 lemma Lt_subst: |
95 lemma Lt_subst: |
89 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
96 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
90 apply (simp only: trm_lts.eq_iff) |
97 apply (simp only: trm_lts.eq_iff) |
91 apply (rule_tac x="q" in exI) |
98 apply (rule_tac x="q" in exI) |
92 apply (simp add: alphas) |
99 apply (simp add: alphas) |