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}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
27 [ [], |
|
28 [], |
|
29 [(SOME @{term rbv5}, 0, 1)] ], |
|
30 [ [], |
|
31 []] ] *} |
|
32 print_theorems |
27 print_theorems |
33 |
|
34 (* Alternate version with additional binding of name in rlts in rLcons *) |
|
35 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
|
36 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
|
37 print_theorems*) |
|
38 |
28 |
39 notation |
29 notation |
40 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
30 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
41 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
31 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
42 thm alpha_rtrm5_alpha_rlts.intros |
32 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
43 |
33 |
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} |
45 thm alpha5_inj |
35 thm alpha5_inj |
46 |
36 |
47 lemma rbv5_eqvt[eqvt]: |
37 lemma rbv5_eqvt[eqvt]: |
48 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
38 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
49 apply (induct x) |
39 apply (induct x) |
58 done |
48 done |
59 |
49 |
60 lemma alpha5_eqvt: |
50 lemma alpha5_eqvt: |
61 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
51 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
62 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
63 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
53 "alpha_rbv5 a b c \<Longrightarrow> True" |
64 apply (simp_all add: alpha5_inj) |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
|
55 apply (simp_all add: alpha5_inj) |
|
56 apply (erule exE) |
|
57 apply (rule_tac x="pi" in exI) |
|
58 apply clarify |
|
59 apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) |
|
60 apply (subst eqvts[symmetric]) |
|
61 apply (subst eqvts[symmetric]) |
65 sorry |
62 sorry |
66 |
63 |
67 lemma alpha5_equivp: |
64 lemma alpha5_equivp: |
68 "equivp alpha_rtrm5" |
65 "equivp alpha_rtrm5" |
69 "equivp alpha_rlts" |
66 "equivp alpha_rlts" |
82 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
79 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
83 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
80 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
84 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
81 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
85 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
82 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
86 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
83 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
87 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
84 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) |
|
85 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
88 *} |
86 *} |
89 print_theorems |
87 print_theorems |
90 |
88 |
91 lemma alpha5_rfv: |
89 lemma alpha5_rfv: |
92 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
90 "(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)" |
93 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
91 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
94 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
|
95 apply(simp_all) |
92 apply(simp_all) |
96 apply(simp add: alpha_gen) |
93 apply(simp add: alpha_gen) |
97 apply(erule conjE)+ |
94 apply(erule conjE)+ |
98 apply(erule exE) |
95 apply(erule exE) |
99 apply(erule conjE)+ |
96 apply(erule conjE)+ |
100 apply(simp_all) |
97 apply(simp_all) |
101 done |
98 sorry |
102 |
99 |
103 lemma bv_list_rsp: |
100 lemma bv_list_rsp: |
104 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
101 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
105 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
102 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
106 apply(simp_all) |
103 apply(simp_all) |
107 apply(clarify) |
104 apply(clarify) |
108 apply simp |
105 apply simp |
109 done |
106 done |
110 |
107 |
116 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
113 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
117 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
114 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
118 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
115 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
119 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
116 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
120 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
117 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
|
118 "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
121 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
119 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
122 apply (clarify) |
120 apply (clarify) |
123 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
121 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
124 done |
122 defer |
125 |
123 apply clarify |
|
124 apply (erule alpha_rlts.cases) |
|
125 apply (erule alpha_rlts.cases) |
|
126 apply (simp_all) |
|
127 defer |
|
128 apply (erule alpha_rlts.cases) |
|
129 apply (simp_all) |
|
130 defer |
|
131 apply clarify |
|
132 apply (simp add: alpha5_inj) |
|
133 sorry (* may be true? *) |
126 lemma |
134 lemma |
127 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
135 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
128 by (simp add: bv_list_rsp) |
136 by (simp add: bv_list_rsp) |
129 |
137 |
130 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
138 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
145 instance by default |
153 instance by default |
146 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
154 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
147 |
155 |
148 end |
156 end |
149 |
157 |
150 lemmas |
158 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
151 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
159 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
152 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
160 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
153 and bv5[simp] = rbv5.simps[quot_lifted] |
161 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
154 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
155 |
162 |
156 lemma lets_ok: |
163 lemma lets_ok: |
157 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
164 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
158 apply (simp add: alpha5_INJ) |
165 apply (simp add: alpha5_INJ) |
159 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
166 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
160 apply (simp_all add: alpha_gen) |
167 apply (simp_all add: alpha_gen) |
161 apply (simp add: permute_trm5_lts fresh_star_def) |
168 apply (simp add: permute_trm5_lts fresh_star_def) |
|
169 apply (metis flip_at_simps(1) supp_at_base supp_eqvt) |
162 done |
170 done |
163 |
171 |
164 lemma lets_ok3: |
172 lemma lets_ok3: |
165 "x \<noteq> y \<Longrightarrow> |
173 "x \<noteq> y \<Longrightarrow> |
166 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
174 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
168 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
176 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
169 done |
177 done |
170 |
178 |
171 |
179 |
172 lemma lets_not_ok1: |
180 lemma lets_not_ok1: |
173 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
181 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
174 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
182 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
175 apply (simp add: alpha5_INJ alpha_gen) |
183 apply (simp add: alpha5_INJ alpha_gen) |
176 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
184 apply (rule_tac x="0::perm" in exI) |
|
185 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
|
186 apply auto |
177 done |
187 done |
178 |
188 |
179 lemma distinct_helper: |
189 lemma distinct_helper: |
180 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
190 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
181 apply auto |
191 apply auto |
190 lemma lets_nok: |
200 lemma lets_nok: |
191 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
201 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
192 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
202 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
193 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
203 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
194 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
204 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
195 apply (simp add: distinct_helper2) |
205 apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) |
196 done |
206 done |
197 |
207 |
198 end |
208 end |