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_zero: |
|
42 "permute_bn 0 a = a" |
|
43 apply(induct a rule: trm_lts.inducts(2)) |
|
44 apply(rule TrueI) |
|
45 apply(simp_all add:test eqvts) |
|
46 done |
|
47 |
41 lemma permute_bn_add: |
48 lemma permute_bn_add: |
42 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
49 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
43 oops |
50 oops |
44 |
51 |
45 lemma Lt_subst: |
52 lemma Lt_subst: |
46 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
53 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
47 sorry |
54 sorry |
|
55 |
|
56 lemma perm_bn: |
|
57 "p \<bullet> bn l = bn(permute_bn p l)" |
|
58 apply(induct l rule: trm_lts.inducts(2)) |
|
59 apply(rule TrueI) |
|
60 apply(simp_all add:test eqvts) |
|
61 done |
|
62 |
|
63 lemma fin_bn: |
|
64 "finite (bn l)" |
|
65 apply(induct l rule: trm_lts.inducts(2)) |
|
66 apply(simp_all add:test eqvts) |
|
67 done |
48 |
68 |
49 lemma |
69 lemma |
50 fixes t::trm |
70 fixes t::trm |
51 and l::lts |
71 and l::lts |
52 and c::"'a::fs" |
72 and c::"'a::fs" |
57 and a5: "\<And>c. P2 c Lnil" |
77 and a5: "\<And>c. P2 c Lnil" |
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)" |
78 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)" |
59 shows "P1 c t" and "P2 c l" |
79 shows "P1 c t" and "P2 c l" |
60 proof - |
80 proof - |
61 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
81 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
62 "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
82 b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
63 apply(induct rule: trm_lts.inducts) |
83 apply(induct rule: trm_lts.inducts) |
64 apply(simp) |
84 apply(simp) |
65 apply(rule a1) |
85 apply(rule a1) |
66 apply(simp) |
86 apply(simp) |
67 apply(rule a2) |
87 apply(rule a2) |
83 apply(simp add: finite_supp) |
103 apply(simp add: finite_supp) |
84 apply(simp add: finite_supp) |
104 apply(simp add: finite_supp) |
85 apply(simp add: fresh_def) |
105 apply(simp add: fresh_def) |
86 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
106 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
87 apply(simp) |
107 apply(simp) |
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") |
108 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") |
89 apply(erule exE) |
109 apply(erule exE) |
90 apply(erule conjE) |
110 apply(erule conjE) |
91 apply(subst Lt_subst) |
111 apply(subst Lt_subst) |
92 apply assumption |
112 apply assumption |
93 apply(rule a4) |
113 apply(rule a4) |
|
114 apply(simp add:perm_bn) |
94 apply assumption |
115 apply assumption |
95 apply (simp add: fresh_star_def fresh_def) |
116 apply (simp add: fresh_star_def fresh_def) |
96 apply(rotate_tac 1) |
117 apply(rotate_tac 1) |
97 apply(drule_tac x="q + p" in meta_spec) |
118 apply(drule_tac x="q + p" in meta_spec) |
98 apply(simp) |
119 apply(simp) |
99 (*apply(rule at_set_avoiding2) |
120 apply(rule at_set_avoiding2) |
|
121 apply(rule fin_bn) |
100 apply(simp add: finite_supp) |
122 apply(simp add: finite_supp) |
101 apply(simp add: supp_Abs) |
123 apply(simp add: supp_Abs) |
102 apply(rule finite_Diff) |
124 apply(rule finite_Diff) |
103 apply(simp add: finite_supp) |
125 apply(simp add: finite_supp) |
104 apply(simp add: fresh_star_def fresh_def supp_Abs)*) |
126 apply(simp add: fresh_star_def fresh_def supp_Abs) |
105 defer |
|
106 apply(simp add: eqvts test) |
127 apply(simp add: eqvts test) |
107 apply(rule a5) |
128 apply(rule a5) |
108 apply(simp add: test) |
129 apply(simp add: test) |
109 apply(rule a6) |
130 apply(rule a6) |
110 apply simp |
131 apply simp |
111 apply simp |
132 apply simp |
112 oops |
133 done |
113 |
134 then have a: "P1 c (0 \<bullet> t)" by blast |
|
135 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
136 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
137 qed |
|
138 |
114 |
139 |
115 |
140 |
116 lemma lets_bla: |
141 lemma lets_bla: |
117 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
142 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
118 by (simp add: trm_lts.eq_iff) |
143 by (simp add: trm_lts.eq_iff) |