20 |
20 |
21 |
21 |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
23 print_theorems |
23 print_theorems |
24 |
24 |
|
25 |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ |
26 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ |
26 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
27 [ [], |
|
28 [], |
|
29 [(SOME @{term rbv5}, 0, 1)] ], |
|
30 [ [], |
|
31 []] ] *} |
27 print_theorems |
32 print_theorems |
28 |
33 |
29 (* Alternate version with additional binding of name in rlts in rLcons *) |
34 (* Alternate version with additional binding of name in rlts in rLcons *) |
30 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
35 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
31 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
36 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
55 lemma alpha5_eqvt: |
60 lemma alpha5_eqvt: |
56 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
61 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
57 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
62 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
58 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
63 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
59 apply (simp_all add: alpha5_inj) |
64 apply (simp_all add: alpha5_inj) |
60 apply (tactic {* |
65 sorry |
61 ALLGOALS ( |
|
62 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
63 (etac @{thm alpha_gen_compose_eqvt}) |
|
64 ) *}) |
|
65 apply (simp_all only: eqvts atom_eqvt) |
|
66 done |
|
67 |
66 |
68 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
67 lemma alpha5_equivp: |
69 (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} |
68 "equivp alpha_rtrm5" |
70 thm alpha5_equivp |
69 "equivp alpha_rlts" |
|
70 sorry |
71 |
71 |
72 quotient_type |
72 quotient_type |
73 trm5 = rtrm5 / alpha_rtrm5 |
73 trm5 = rtrm5 / alpha_rtrm5 |
74 and |
74 and |
75 lts = rlts / alpha_rlts |
75 lts = rlts / alpha_rlts |
90 |
90 |
91 lemma alpha5_rfv: |
91 lemma alpha5_rfv: |
92 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
92 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
93 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
93 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
94 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
94 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
95 apply(simp_all add: alpha_gen) |
95 apply(simp_all) |
|
96 apply(simp add: alpha_gen) |
|
97 apply(erule conjE)+ |
|
98 apply(erule exE) |
|
99 apply(erule conjE)+ |
|
100 apply(simp_all) |
96 done |
101 done |
97 |
102 |
98 lemma bv_list_rsp: |
103 lemma bv_list_rsp: |
99 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
104 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
100 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
105 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
101 apply(simp_all) |
106 apply(simp_all) |
|
107 apply(clarify) |
|
108 apply simp |
102 done |
109 done |
103 |
110 |
104 lemma [quot_respect]: |
111 lemma [quot_respect]: |
105 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
112 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
106 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
113 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
110 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
117 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
111 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
118 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
112 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
119 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
113 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
120 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
114 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
121 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
115 apply (clarify) apply (rule conjI) |
122 apply (clarify) |
116 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
117 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
123 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
118 done |
124 done |
119 |
125 |
120 lemma |
126 lemma |
121 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
127 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
147 and bv5[simp] = rbv5.simps[quot_lifted] |
153 and bv5[simp] = rbv5.simps[quot_lifted] |
148 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
154 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
149 |
155 |
150 lemma lets_ok: |
156 lemma lets_ok: |
151 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
157 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
152 apply (subst alpha5_INJ) |
158 apply (simp add: alpha5_INJ) |
153 apply (rule conjI) |
|
154 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
159 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
155 apply (simp only: alpha_gen) |
160 apply (simp_all add: alpha_gen) |
156 apply (simp add: permute_trm5_lts fresh_star_def) |
|
157 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
158 apply (simp only: alpha_gen) |
|
159 apply (simp add: permute_trm5_lts fresh_star_def) |
|
160 done |
|
161 |
|
162 lemma lets_ok2: |
|
163 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
164 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
165 apply (subst alpha5_INJ) |
|
166 apply (rule conjI) |
|
167 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
168 apply (simp only: alpha_gen) |
|
169 apply (simp add: permute_trm5_lts fresh_star_def) |
|
170 apply (rule_tac x="0 :: perm" in exI) |
|
171 apply (simp only: alpha_gen) |
|
172 apply (simp add: permute_trm5_lts fresh_star_def) |
161 apply (simp add: permute_trm5_lts fresh_star_def) |
173 done |
162 done |
174 |
163 |
175 lemma lets_ok3: |
164 lemma lets_ok3: |
176 assumes a: "distinct [x, y]" |
165 "x \<noteq> y \<Longrightarrow> |
177 shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
166 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
178 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
167 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
179 apply (subst alpha5_INJ) |
168 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
180 apply (rule conjI) |
|
181 apply (simp add: alpha_gen) |
|
182 apply (simp add: permute_trm5_lts fresh_star_def) |
|
183 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
184 apply (simp only: alpha_gen) |
|
185 apply (simp add: permute_trm5_lts fresh_star_def) |
|
186 apply (rule_tac x="0 :: perm" in exI) |
|
187 apply (simp only: alpha_gen) |
|
188 apply (simp add: permute_trm5_lts fresh_star_def) |
|
189 done |
169 done |
|
170 |
190 |
171 |
191 lemma lets_not_ok1: |
172 lemma lets_not_ok1: |
192 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
173 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
193 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
174 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
194 apply (simp add: alpha5_INJ(3) alpha_gen) |
175 apply (simp add: alpha5_INJ alpha_gen) |
195 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
176 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
196 done |
177 done |
197 |
178 |
198 lemma distinct_helper: |
179 lemma distinct_helper: |
199 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
180 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |