equal
deleted
inserted
replaced
480 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
480 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
481 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
481 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
482 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
482 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
483 |> instantiate' [] [NONE, SOME (cterm_of thy h)] |
483 |> instantiate' [] [NONE, SOME (cterm_of thy h)] |
484 val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) |
484 val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) |
|
485 |
|
486 val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm) |
|
487 val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt) |
485 |
488 |
486 val _ = trace_msg (K "Proving Replacement lemmas...") |
489 val _ = trace_msg (K "Proving Replacement lemmas...") |
487 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
490 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
488 |
491 |
489 val _ = trace_msg (K "Proving Equivariance lemmas...") |
492 val _ = trace_msg (K "Proving Equivariance lemmas...") |