equal
deleted
inserted
replaced
306 let |
306 let |
307 val T = the (AList.lookup (op =) preds pred) |
307 val T = the (AList.lookup (op =) preds pred) |
308 val nargs = length (binder_types T) |
308 val nargs = length (binder_types T) |
309 val pred_case_rule = the_elim_of ctxt pred |
309 val pred_case_rule = the_elim_of ctxt pred |
310 in |
310 in |
311 REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) |
311 REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})) |
312 THEN print_tac options "before applying elim rule" |
312 THEN print_tac options "before applying elim rule" |
313 THEN etac (predfun_elim_of ctxt pred mode) 1 |
313 THEN etac (predfun_elim_of ctxt pred mode) 1 |
314 THEN etac pred_case_rule 1 |
314 THEN etac pred_case_rule 1 |
315 THEN print_tac options "after applying elim rule" |
315 THEN print_tac options "after applying elim rule" |
316 THEN (EVERY (map |
316 THEN (EVERY (map |
383 val mode = head_mode_of deriv |
383 val mode = head_mode_of deriv |
384 val param_derivations = param_derivations_of deriv |
384 val param_derivations = param_derivations_of deriv |
385 val ho_args = ho_args_of mode args |
385 val ho_args = ho_args_of mode args |
386 in |
386 in |
387 etac @{thm bindE} 1 |
387 etac @{thm bindE} 1 |
388 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) |
388 THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))) |
389 THEN print_tac options "prove_expr2-before" |
389 THEN print_tac options "prove_expr2-before" |
390 THEN etac (predfun_elim_of ctxt name mode) 1 |
390 THEN etac (predfun_elim_of ctxt name mode) 1 |
391 THEN print_tac options "prove_expr2" |
391 THEN print_tac options "prove_expr2" |
392 THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) |
392 THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) |
393 THEN print_tac options "finished prove_expr2" |
393 THEN print_tac options "finished prove_expr2" |
494 fun prove_clause clause i = |
494 fun prove_clause clause i = |
495 (if i < length moded_clauses then etac @{thm supE} 1 else all_tac) |
495 (if i < length moded_clauses then etac @{thm supE} 1 else all_tac) |
496 THEN (prove_clause2 options ctxt pred mode clause i) |
496 THEN (prove_clause2 options ctxt pred mode clause i) |
497 in |
497 in |
498 (DETERM (TRY (rtac @{thm unit.induct} 1))) |
498 (DETERM (TRY (rtac @{thm unit.induct} 1))) |
499 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all}))) |
499 THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))) |
500 THEN (rtac (predfun_intro_of ctxt pred mode) 1) |
500 THEN (rtac (predfun_intro_of ctxt pred mode) 1) |
501 THEN (REPEAT_DETERM (rtac @{thm refl} 2)) |
501 THEN (REPEAT_DETERM (rtac @{thm refl} 2)) |
502 THEN (if null moded_clauses then |
502 THEN (if null moded_clauses then |
503 etac @{thm botE} 1 |
503 etac @{thm botE} 1 |
504 else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) |
504 else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) |