131 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
131 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
132 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
132 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
133 |
133 |
134 ML {* add_lower_defs @{context} @{thms perm_lam_def} *} |
134 ML {* add_lower_defs @{context} @{thms perm_lam_def} *} |
135 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *} |
135 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *} |
136 lemma prod_fun_id: "prod_fun id id = id" |
136 |
137 apply (simp add: prod_fun_def) |
|
138 done |
|
139 lemma map_id: "map id x = x" |
|
140 apply (induct x) |
|
141 apply (simp_all add: map.simps) |
|
142 done |
|
143 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
137 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
144 ML {* |
138 ML {* |
145 fun lift_thm_lam lthy t = |
139 fun lift_thm_lam lthy t = |
146 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
140 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
147 *} |
141 *} |
148 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_var_com}) *} |
142 |
149 ML {* val t2 = eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
143 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
150 ML {* ObjectLogic.rulify t2 *} |
144 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
151 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_app_com}) *} |
145 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
152 ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
146 |
153 ML {* ObjectLogic.rulify t2 *} |
147 fun |
154 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_lam_com}) *} |
148 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
155 ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
149 where |
156 ML {* ObjectLogic.rulify t2 *} |
150 "option_map f (nSome x) = nSome (f x)" |
157 |
151 | "option_map f nNone = nNone" |
|
152 |
|
153 fun |
|
154 option_rel |
|
155 where |
|
156 "option_rel r (nSome x) (nSome y) = r x y" |
|
157 | "option_rel r _ _ = False" |
|
158 |
|
159 declare [[map noption = (option_map, option_rel)]] |
|
160 |
|
161 lemma OPT_QUOTIENT: |
|
162 assumes q: "QUOTIENT R Abs Rep" |
|
163 shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)" |
|
164 apply (unfold QUOTIENT_def) |
|
165 apply (auto) |
|
166 using q |
|
167 apply (unfold QUOTIENT_def) |
|
168 apply (case_tac "a :: 'b noption") |
|
169 apply (simp) |
|
170 apply (simp) |
|
171 apply (case_tac "a :: 'b noption") |
|
172 apply (simp only: option_map.simps) |
|
173 apply (subst option_rel.simps) |
|
174 (* Simp starts hanging so don't know how to continue *) |
|
175 sorry |
|
176 |
|
177 (* Christian: Does it make sense? *) |
|
178 lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun" |
|
179 sorry |
|
180 |
|
181 (* Should not be needed *) |
|
182 lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op =" |
|
183 apply auto |
|
184 apply (rule ext) |
|
185 apply auto |
|
186 apply (rule ext) |
|
187 apply auto |
|
188 done |
|
189 |
|
190 (* Should not be needed *) |
|
191 lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \<bullet> op \<bullet>" |
|
192 apply auto |
|
193 thm arg_cong2 |
|
194 apply (rule_tac f="perm x" in arg_cong2) |
|
195 apply (auto) |
|
196 apply (rule ext) |
|
197 apply (auto) |
|
198 done |
|
199 |
|
200 (* Should not be needed *) |
|
201 lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh" |
|
202 apply (simp add: FUN_REL.simps) |
|
203 apply (metis ext) |
|
204 done |
|
205 |
|
206 (* It is just a test, it doesn't seem true... *) |
|
207 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
|
208 sorry |
|
209 |
|
210 |
|
211 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
|
212 ML {* |
|
213 fun lift_thm_lam lthy t = |
|
214 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
215 *} |
|
216 |
|
217 thm a3 |
|
218 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
|
219 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
|
220 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} |
|
221 |
|
222 ML t_u |
|
223 ML {* val t_a = atomize_thm t_u *} |
|
224 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
|
225 ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) (cprop_of t_u) *} |
|
226 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
|
227 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
|
228 ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *} |
|
229 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
|
230 ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *} |
|
231 ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) t *} |
|
232 ML {* term_of t *} |
|
233 term "[b].(s::rlam)" |
|
234 thm abs_fun_def |
|
235 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
236 |