equal
deleted
inserted
replaced
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 |
485 |
486 val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm) |
|
487 val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt) |
|
488 |
|
489 val _ = trace_msg (K "Proving Replacement lemmas...") |
486 val _ = trace_msg (K "Proving Replacement lemmas...") |
490 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
487 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
491 |
488 |
492 val _ = trace_msg (K "Proving Equivariance lemmas...") |
489 val _ = trace_msg (K "Proving Equivariance lemmas...") |
493 val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses |
490 val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses |