182 |
181 |
183 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
182 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
184 import (export : thm -> thm) sum_psimp_eq = |
183 import (export : thm -> thm) sum_psimp_eq = |
185 let |
184 let |
186 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
185 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
187 |
186 |
188 val psimp = import sum_psimp_eq |
187 val psimp = import sum_psimp_eq |
189 val (simp, restore_cond) = |
188 val (simp, restore_cond) = |
190 case cprems_of psimp of |
189 case cprems_of psimp of |
191 [] => (psimp, I) |
190 [] => (psimp, I) |
192 | [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) |
193 | _ => raise General.Fail "Too many conditions" |
192 | _ => raise General.Fail "Too many conditions" |
194 |
|
195 in |
193 in |
196 Goal.prove ctxt [] [] |
194 Goal.prove ctxt [] [] |
197 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
195 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
198 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
196 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
199 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
197 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
200 THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) |
198 THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) |
201 |> restore_cond |
199 |> restore_cond |
202 |> export |
200 |> export |
203 end |
201 end |
204 |
202 |
|
203 fun mk_meqvts ctxt eqvt_thm f_defs = |
|
204 let |
|
205 val ctrm1 = eqvt_thm |
|
206 |> cprop_of |
|
207 |> snd o Thm.dest_implies |
|
208 |> Thm.dest_arg |
|
209 |> Thm.dest_arg1 |
|
210 |> Thm.dest_arg |
|
211 |
|
212 fun resolve f_def = |
|
213 let |
|
214 val ctrm2 = f_def |
|
215 |> cprop_of |
|
216 |> Thm.dest_equals_lhs |
|
217 in |
|
218 eqvt_thm |
|
219 |> Thm.instantiate (Thm.match (ctrm1, ctrm2)) |
|
220 |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps})) |
|
221 |> Local_Defs.unfold ctxt [f_def] |
|
222 end |
|
223 in |
|
224 map resolve f_defs |
|
225 end |
|
226 |
|
227 |
205 fun mk_applied_form ctxt caTs thm = |
228 fun mk_applied_form ctxt caTs thm = |
206 let |
229 let |
207 val thy = ProofContext.theory_of ctxt |
230 val thy = ProofContext.theory_of ctxt |
208 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
231 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
209 in |
232 in |
254 |
277 |
255 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
278 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
256 let |
279 let |
257 val result = inner_cont proof |
280 val result = inner_cont proof |
258 val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
281 val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
259 termination, domintros, eqvts,...} = result |
282 termination, domintros, eqvts=[eqvt],...} = result |
260 |
|
261 (* |
|
262 val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct) |
|
263 val _ = tracing ("premutual termination:\n" ^ @{make_string} termination) |
|
264 val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps)) |
|
265 val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) |
|
266 *) |
|
267 |
283 |
268 val (all_f_defs, fs) = |
284 val (all_f_defs, fs) = |
269 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
285 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
270 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
286 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
271 parts |
287 parts |
280 val rew_ss = HOL_basic_ss addsimps all_f_defs |
296 val rew_ss = HOL_basic_ss addsimps all_f_defs |
281 val mpsimps = map2 mk_mpsimp fqgars psimps |
297 val mpsimps = map2 mk_mpsimp fqgars psimps |
282 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
298 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
283 val mtermination = full_simplify rew_ss termination |
299 val mtermination = full_simplify rew_ss termination |
284 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
300 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
285 |
301 val meqvts = mk_meqvts lthy eqvt all_f_defs |
286 (* |
302 in |
287 val _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps)) |
|
288 val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts)) |
|
289 val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination) |
|
290 *) |
|
291 in |
|
292 NominalFunctionResult { fs=fs, G=G, R=R, |
303 NominalFunctionResult { fs=fs, G=G, R=R, |
293 psimps=mpsimps, simple_pinducts=minducts, |
304 psimps=mpsimps, simple_pinducts=minducts, |
294 cases=cases, termination=mtermination, |
305 cases=cases, termination=mtermination, |
295 domintros=mdomintros, eqvts=eqvts } |
306 domintros=mdomintros, eqvts=meqvts } |
296 end |
307 end |
297 |
308 |
298 (* nominal *) |
309 (* nominal *) |
299 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
310 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
300 let |
311 let |