40 |
40 |
41 lemma permute_bn_add: |
41 lemma permute_bn_add: |
42 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
42 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
43 oops |
43 oops |
44 |
44 |
|
45 lemma Lt_subst: |
|
46 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
|
47 sorry |
|
48 |
45 lemma |
49 lemma |
46 fixes t::trm |
50 fixes t::trm |
47 and l::lts |
51 and l::lts |
48 and c::"'a::fs" |
52 and c::"'a::fs" |
49 assumes a1: "\<And>name c. P1 c (Vr name)" |
53 assumes a1: "\<And>name c. P1 c (Vr name)" |
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)" |
54 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
51 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
55 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name 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)" |
56 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)" |
53 and a5: "\<And>c. P2 c Lnil" |
57 and a5: "\<And>c. P2 c Lnil" |
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)" |
58 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)" |
55 shows "P1 c t" and "P2 c l" |
59 shows "P1 c t" and "P2 c l" |
56 proof - |
60 proof - |
57 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
61 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
79 apply(simp add: finite_supp) |
83 apply(simp add: finite_supp) |
80 apply(simp add: finite_supp) |
84 apply(simp add: finite_supp) |
81 apply(simp add: fresh_def) |
85 apply(simp add: fresh_def) |
82 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
86 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
83 apply(simp) |
87 apply(simp) |
84 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") |
88 apply(subgoal_tac "\<exists>q. (bn (permute_bn q (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
85 apply(erule exE) |
89 apply(erule exE) |
86 (* HERE *) |
90 apply(erule conjE) |
87 apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)" |
91 apply(subst Lt_subst) |
88 and s="Lt (permute_bn q (p \<bullet> lts)) (q \<bullet> p \<bullet> trm)" in subst) |
92 apply assumption |
89 defer |
|
90 apply(rule a4) |
93 apply(rule a4) |
91 defer |
94 apply assumption |
92 apply(simp add: eqvts) |
95 apply (simp add: fresh_star_def fresh_def) |
93 apply(rotate_tac 1) |
96 apply(rotate_tac 1) |
94 apply(drule_tac x="q + p" in meta_spec) |
97 apply(drule_tac x="q + p" in meta_spec) |
95 apply(simp) |
98 apply(simp) |
|
99 (*apply(rule at_set_avoiding2) |
|
100 apply(simp add: finite_supp) |
|
101 apply(simp add: supp_Abs) |
|
102 apply(rule finite_Diff) |
|
103 apply(simp add: finite_supp) |
|
104 apply(simp add: fresh_star_def fresh_def supp_Abs)*) |
96 defer |
105 defer |
97 apply(simp add: test) |
106 apply(simp add: eqvts test) |
98 apply(rule a5) |
107 apply(rule a5) |
99 apply(simp add: test) |
108 apply(simp add: test) |
100 apply(rule a6) |
109 apply(rule a6) |
101 apply simp |
110 apply simp |
102 apply simp |
111 apply simp |
103 |
|
104 apply(rule at_set_avoiding2) |
|
105 apply(simp add: finite_supp) |
|
106 defer |
|
107 apply(simp add: finite_supp) |
|
108 apply(simp add: finite_supp) |
|
109 apply(simp add: fresh_star_def) |
|
110 apply(simp add: fresh_def) |
|
111 thm trm_lts.fv[simplified trm_lts.supp] |
|
112 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
113 apply(simp add: alpha_bn_eq_iff) |
|
114 defer |
|
115 apply(simp) |
|
116 apply(rule a5) |
|
117 apply(simp) |
|
118 apply(rule a6) |
|
119 apply(simp) |
|
120 apply(simp) |
|
121 oops |
112 oops |
122 |
113 |
123 |
114 |
124 |
115 |
125 lemma lets_bla: |
116 lemma lets_bla: |