51 local_setup {* |
51 local_setup {* |
52 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
52 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
53 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
53 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
54 print_theorems |
54 print_theorems |
55 |
55 |
|
56 lemma alpha5_reflp: |
|
57 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)" |
|
58 apply (rule rtrm5_rlts.induct) |
|
59 apply (simp_all add: alpha5_inj) |
|
60 apply (rule_tac x="0::perm" in exI) |
|
61 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
|
62 done |
|
63 |
|
64 lemma alpha5_symp: |
|
65 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
|
66 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
|
67 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
|
68 sorry |
|
69 |
|
70 lemma alpha5_transp: |
|
71 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
|
72 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
|
73 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
|
74 sorry |
|
75 |
56 lemma alpha5_equivp: |
76 lemma alpha5_equivp: |
57 "equivp alpha_rtrm5" |
77 "equivp alpha_rtrm5" |
58 "equivp alpha_rlts" |
78 "equivp alpha_rlts" |
59 sorry |
79 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
|
80 apply (simp_all only: alpha5_reflp) |
|
81 apply (meson alpha5_symp alpha5_transp) |
|
82 apply (meson alpha5_symp alpha5_transp) |
|
83 done |
60 |
84 |
61 quotient_type |
85 quotient_type |
62 trm5 = rtrm5 / alpha_rtrm5 |
86 trm5 = rtrm5 / alpha_rtrm5 |
63 and |
87 and |
64 lts = rlts / alpha_rlts |
88 lts = rlts / alpha_rlts |
94 apply(simp_all) |
118 apply(simp_all) |
95 apply(clarify) |
119 apply(clarify) |
96 apply simp |
120 apply simp |
97 done |
121 done |
98 |
122 |
99 lemma alpha_rbv5_rsp: "xa \<approx>l y \<Longrightarrow> xb \<approx>l ya \<Longrightarrow> alpha_rbv5 xa xb = alpha_rbv5 y ya" |
123 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} |
|
124 print_theorems |
|
125 |
|
126 lemma alpha_rbv_rsp_pre: |
|
127 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z" |
100 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
128 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
101 apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
129 apply (simp_all add: alpha_dis alpha5_inj) |
102 apply (simp_all) |
130 apply clarify |
103 defer defer (* should follow from distinctness *) |
131 apply (case_tac [!] z) |
104 apply clarify |
132 apply (simp_all add: alpha_dis alpha5_inj) |
105 apply (simp add: alpha5_inj) |
133 apply clarify |
106 sorry (* should be true? *) |
134 apply auto |
|
135 apply (meson alpha5_symp alpha5_transp) |
|
136 apply (meson alpha5_symp alpha5_transp) |
|
137 done |
|
138 |
|
139 lemma alpha_rbv_rsp_pre2: |
|
140 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y" |
|
141 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
142 apply (simp_all add: alpha_dis alpha5_inj) |
|
143 apply clarify |
|
144 apply (case_tac [!] z) |
|
145 apply (simp_all add: alpha_dis alpha5_inj) |
|
146 apply clarify |
|
147 apply auto |
|
148 apply (meson alpha5_symp alpha5_transp) |
|
149 apply (meson alpha5_symp alpha5_transp) |
|
150 done |
107 |
151 |
108 lemma [quot_respect]: |
152 lemma [quot_respect]: |
109 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
153 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
110 "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" |
154 "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" |
111 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
155 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
115 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
159 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
116 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
160 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
117 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
161 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
118 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
162 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
119 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
163 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
120 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv5_rsp) |
164 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp) |
121 apply (clarify) |
165 apply (clarify) |
122 apply (rule conjI) |
|
123 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
124 apply (simp_all add: alpha5_inj) |
|
125 apply clarify |
|
126 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
166 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
127 done |
167 done |
128 |
168 |
129 lemma |
169 lemma |
130 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
170 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
166 lemma lets_ok: |
206 lemma lets_ok: |
167 "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
207 "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
168 apply (simp add: alpha5_INJ) |
208 apply (simp add: alpha5_INJ) |
169 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
209 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
170 apply (simp_all add: alpha_gen) |
210 apply (simp_all add: alpha_gen) |
171 apply (simp add: permute_trm5_lts fresh_star_def) |
211 apply (simp add: permute_trm5_lts fresh_star_def eqvts) |
172 done |
212 done |
173 |
213 |
174 lemma lets_ok3: |
214 lemma lets_ok3: |
175 "x \<noteq> y \<Longrightarrow> |
215 "x \<noteq> y \<Longrightarrow> |
176 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
216 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
183 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
223 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
184 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
224 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
185 apply (simp add: alpha5_INJ alpha_gen) |
225 apply (simp add: alpha5_INJ alpha_gen) |
186 apply (rule_tac x="0::perm" in exI) |
226 apply (rule_tac x="0::perm" in exI) |
187 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
227 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
|
228 apply blast |
188 done |
229 done |
189 |
230 |
190 lemma distinct_helper: |
231 lemma distinct_helper: |
191 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
232 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
192 apply auto |
233 apply auto |