191 | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
191 | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
192 | _ => raise General.Fail "Too many conditions" |
192 | _ => raise General.Fail "Too many conditions" |
193 in |
193 in |
194 Goal.prove ctxt [] [] |
194 Goal.prove ctxt [] [] |
195 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
195 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
196 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
196 (fn _ => print_tac "start" |
|
197 THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
|
198 THEN (print_tac "second") |
197 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
199 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
198 THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) |
200 THEN (print_tac "third") |
|
201 THEN (simp_tac (simpset_of ctxt)) 1 |
|
202 THEN (print_tac "fourth") |
|
203 ) (* FIXME: global simpset?!! *) |
|
204 |> restore_cond |
|
205 |> export |
|
206 end |
|
207 |
|
208 val test1 = @{lemma "x = Inl y ==> permute p (Sum_Type.Projl x) = Sum_Type.Projl (permute p x)" by simp} |
|
209 val test2 = @{lemma "x = Inr y ==> permute p (Sum_Type.Projr x) = Sum_Type.Projr (permute p x)" by simp} |
|
210 |
|
211 fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
|
212 import (export : thm -> thm) sum_psimp_eq = |
|
213 let |
|
214 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
|
215 |
|
216 val psimp = import sum_psimp_eq |
|
217 val (simp, restore_cond) = |
|
218 case cprems_of psimp of |
|
219 [] => (psimp, I) |
|
220 | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
|
221 | _ => raise General.Fail "Too many conditions" |
|
222 |
|
223 val eqvt_thm' = import eqvt_thm |
|
224 val (simp', restore_cond') = |
|
225 case cprems_of eqvt_thm' of |
|
226 [] => (eqvt_thm, I) |
|
227 | [cond] => (Thm.implies_elim eqvt_thm' (Thm.assume cond), Thm.implies_intr cond) |
|
228 | _ => raise General.Fail "Too many conditions" |
|
229 |
|
230 val _ = tracing ("sum_psimp:\n" ^ @{make_string} sum_psimp_eq) |
|
231 val _ = tracing ("psimp:\n" ^ @{make_string} psimp) |
|
232 val _ = tracing ("simp:\n" ^ @{make_string} simp) |
|
233 val _ = tracing ("eqvt:\n" ^ @{make_string} eqvt_thm) |
|
234 |
|
235 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
236 val p = Free (p, @{typ perm}) |
|
237 val ss = HOL_basic_ss addsimps [simp RS test1, simp'] |
|
238 in |
|
239 Goal.prove ctxt' [] [] |
|
240 (HOLogic.Trueprop $ |
|
241 HOLogic.mk_eq (mk_perm p (list_comb (f, args)), list_comb (f, map (mk_perm p) args))) |
|
242 (fn _ => print_tac "eqvt start" |
|
243 THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
|
244 THEN (asm_full_simp_tac ss 1) |
|
245 THEN all_tac) |
199 |> restore_cond |
246 |> restore_cond |
200 |> export |
247 |> export |
201 end |
248 end |
202 |
249 |
203 fun mk_meqvts ctxt eqvt_thm f_defs = |
250 fun mk_meqvts ctxt eqvt_thm f_defs = |
293 map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts |
340 map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts |
294 |
341 |
295 fun mk_mpsimp fqgar sum_psimp = |
342 fun mk_mpsimp fqgar sum_psimp = |
296 in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
343 in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
297 |
344 |
|
345 fun mk_meqvts fqgar sum_psimp = |
|
346 in_context lthy fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp |
|
347 |
298 val rew_ss = HOL_basic_ss addsimps all_f_defs |
348 val rew_ss = HOL_basic_ss addsimps all_f_defs |
299 val mpsimps = map2 mk_mpsimp fqgars psimps |
349 val mpsimps = map2 mk_mpsimp fqgars psimps |
300 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
350 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
301 val mtermination = full_simplify rew_ss termination |
351 val mtermination = full_simplify rew_ss termination |
302 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
352 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
303 val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*) |
353 val meqvts = map2 mk_meqvts fqgars psimps |
304 in |
354 in |
305 NominalFunctionResult { fs=fs, G=G, R=R, |
355 NominalFunctionResult { fs=fs, G=G, R=R, |
306 psimps=mpsimps, simple_pinducts=minducts, |
356 psimps=mpsimps, simple_pinducts=minducts, |
307 cases=cases, termination=mtermination, |
357 cases=cases, termination=mtermination, |
308 domintros=mdomintros, eqvts=meqvts } |
358 domintros=mdomintros, eqvts=meqvts } |