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 := false *} |
9 ML {* val _ = recursive := false *} |
10 |
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 |
15 | Lt a::"lts" t::"trm" bind "bn a" in t |
15 | Lt a::"lts" t::"trm" bind "bn a" in t |
17 Lnil |
17 Lnil |
18 | Lcons "name" "trm" "lts" |
18 | Lcons "name" "trm" "lts" |
19 binder |
19 binder |
20 bn |
20 bn |
21 where |
21 where |
22 "bn Lnil = {}" |
22 "bn Lnil = []" |
23 | "bn (Lcons x t l) = {atom x} \<union> (bn l)" |
23 | "bn (Lcons x t l) = (atom x) # (bn l)" |
24 |
24 |
25 thm trm_lts.fv |
25 thm trm_lts.fv |
26 thm trm_lts.eq_iff |
26 thm trm_lts.eq_iff |
27 thm trm_lts.bn |
27 thm trm_lts.bn |
28 thm trm_lts.perm |
28 thm trm_lts.perm |
29 thm trm_lts.induct[no_vars] |
29 thm trm_lts.induct[no_vars] |
30 thm trm_lts.inducts[no_vars] |
30 thm trm_lts.inducts[no_vars] |
31 thm trm_lts.distinct |
31 thm trm_lts.distinct |
32 thm trm_lts.fv[simplified trm_lts.supp] |
32 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
33 |
33 |
34 primrec |
34 primrec |
35 permute_bn_raw |
35 permute_bn_raw |
36 where |
36 where |
37 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
37 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
78 apply(rule TrueI) |
78 apply(rule TrueI) |
79 apply(simp_all add:permute_bn eqvts) |
79 apply(simp_all add:permute_bn eqvts) |
80 done |
80 done |
81 |
81 |
82 lemma Lt_subst: |
82 lemma Lt_subst: |
83 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
83 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
84 apply (simp only: trm_lts.eq_iff) |
84 apply (simp only: trm_lts.eq_iff) |
85 apply (rule_tac x="q" in exI) |
85 apply (rule_tac x="q" in exI) |
86 apply (simp add: alphas) |
86 apply (simp add: alphas) |
87 apply (simp add: permute_bn_alpha_bn) |
87 apply (simp add: permute_bn_alpha_bn) |
88 apply (simp add: perm_bn[symmetric]) |
88 apply (simp add: perm_bn[symmetric]) |
108 and l::lts |
108 and l::lts |
109 and c::"'a::fs" |
109 and c::"'a::fs" |
110 assumes a1: "\<And>name c. P1 c (Vr name)" |
110 assumes a1: "\<And>name c. P1 c (Vr name)" |
111 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
111 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
112 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
112 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
113 and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
113 and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
114 and a5: "\<And>c. P2 c Lnil" |
114 and a5: "\<And>c. P2 c Lnil" |
115 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
115 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
116 shows "P1 c t" and "P2 c l" |
116 shows "P1 c t" and "P2 c l" |
117 proof - |
117 proof - |
118 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
118 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
140 apply(simp add: finite_supp) |
140 apply(simp add: finite_supp) |
141 apply(simp add: finite_supp) |
141 apply(simp add: finite_supp) |
142 apply(simp add: fresh_def) |
142 apply(simp add: fresh_def) |
143 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
143 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
144 apply(simp) |
144 apply(simp) |
145 apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
145 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
146 apply(erule exE) |
146 apply(erule exE) |
147 apply(erule conjE) |
147 apply(erule conjE) |
148 apply(subst Lt_subst) |
148 apply(subst Lt_subst) |
149 apply assumption |
149 apply assumption |
150 apply(rule a4) |
150 apply(rule a4) |
151 apply(simp add:perm_bn) |
151 apply(simp add:perm_bn[symmetric]) |
152 apply assumption |
152 apply(simp add: eqvts) |
153 apply (simp add: fresh_star_def fresh_def) |
153 apply (simp add: fresh_star_def fresh_def) |
154 apply(rotate_tac 1) |
154 apply(rotate_tac 1) |
155 apply(drule_tac x="q + p" in meta_spec) |
155 apply(drule_tac x="q + p" in meta_spec) |
156 apply(simp) |
156 apply(simp) |
157 apply(rule at_set_avoiding2) |
157 apply(rule at_set_avoiding2) |
158 apply(rule fin_bn) |
158 apply(rule fin_bn) |
159 apply(simp add: finite_supp) |
159 apply(simp add: finite_supp) |
160 apply(simp add: supp_abs) |
|
161 apply(rule finite_Diff) |
|
162 apply(simp add: finite_supp) |
160 apply(simp add: finite_supp) |
163 apply(simp add: fresh_star_def fresh_def supp_abs) |
161 apply(simp add: fresh_star_def fresh_def supp_abs) |
164 apply(simp add: eqvts permute_bn) |
162 apply(simp add: eqvts permute_bn) |
165 apply(rule a5) |
163 apply(rule a5) |
166 apply(simp add: permute_bn) |
164 apply(simp add: permute_bn) |
194 apply (simp add: alphas trm_lts.eq_iff) |
192 apply (simp add: alphas trm_lts.eq_iff) |
195 done |
193 done |
196 |
194 |
197 |
195 |
198 lemma lets_not_ok1: |
196 lemma lets_not_ok1: |
199 "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = |
197 "x \<noteq> y \<Longrightarrow> |
|
198 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
200 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
199 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
201 apply (simp add: alphas trm_lts.eq_iff) |
200 apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) |
202 apply (rule_tac x="0::perm" in exI) |
|
203 apply (simp add: fresh_star_def eqvts) |
|
204 apply blast |
|
205 done |
201 done |
206 |
202 |
207 lemma lets_nok: |
203 lemma lets_nok: |
208 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
204 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
209 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
205 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |