36 lemma test: |
36 lemma test: |
37 "permute_bn pi (Lnil) = Lnil" |
37 "permute_bn pi (Lnil) = Lnil" |
38 "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)" |
38 "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)" |
39 sorry |
39 sorry |
40 |
40 |
|
41 lemma permute_bn_add: |
|
42 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
|
43 oops |
|
44 |
41 lemma |
45 lemma |
42 fixes t::trm |
46 fixes t::trm |
43 and l::lts |
47 and l::lts |
44 and c::"'a::fs" |
48 and c::"'a::fs" |
45 assumes a1: "\<And>name c. P1 c (Vr name)" |
49 assumes a1: "\<And>name c. P1 c (Vr name)" |
46 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
50 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
47 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
51 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
48 and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* (c, Lt lts trm); \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
52 and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* (c, Lt lts trm); \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
49 and a5: "\<And>c. P2 c Lnil" |
53 and a5: "\<And>c. P2 c Lnil" |
50 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)" |
54 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)" |
51 shows "P1 c t" and "P2 c l" |
55 shows "P1 c t" and "P2 c l" |
52 proof - |
56 proof - |
53 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
57 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
54 "(\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> l))" |
58 "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
55 apply(induct rule: trm_lts.inducts) |
59 apply(induct rule: trm_lts.inducts) |
56 apply(simp) |
60 apply(simp) |
57 apply(rule a1) |
61 apply(rule a1) |
58 apply(simp) |
62 apply(simp) |
59 apply(rule a2) |
63 apply(rule a2) |
84 and s="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst) |
88 and s="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst) |
85 defer |
89 defer |
86 apply(rule a4) |
90 apply(rule a4) |
87 defer |
91 defer |
88 apply(simp add: eqvts) |
92 apply(simp add: eqvts) |
89 apply(simp add: fresh_star_prod) |
93 apply(rotate_tac 1) |
90 apply(simp add: fresh_star_def) |
94 apply(drule_tac x="q + p" in meta_spec) |
91 apply(simp add: fresh_def) |
95 apply(simp) |
92 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
96 defer |
93 apply(subst permute_plus[symmetric]) |
97 apply(simp add: test) |
94 apply(blast) |
98 apply(rule a5) |
95 apply(subst permute_plus[symmetric]) |
99 apply(simp add: test) |
96 apply(blast) |
100 apply(rule a6) |
|
101 apply simp |
|
102 apply simp |
|
103 |
97 apply(rule at_set_avoiding2) |
104 apply(rule at_set_avoiding2) |
98 apply(simp add: finite_supp) |
105 apply(simp add: finite_supp) |
99 defer |
106 defer |
100 apply(simp add: finite_supp) |
107 apply(simp add: finite_supp) |
101 apply(simp add: finite_supp) |
108 apply(simp add: finite_supp) |