equal
deleted
inserted
replaced
53 val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} |
53 val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} |
54 |
54 |
55 fun meta thm = thm RS eq_reflection |
55 fun meta thm = thm RS eq_reflection |
56 |
56 |
57 val sum_prod_conv = MetaSimplifier.rewrite true |
57 val sum_prod_conv = MetaSimplifier.rewrite true |
58 (map meta (@{thm split_conv} :: @{thms sum_cases})) |
58 (map meta (@{thm split_conv} :: @{thms sum.cases})) |
59 |
59 |
60 fun term_conv thy cv t = |
60 fun term_conv thy cv t = |
61 cv (cterm_of thy t) |
61 cv (cterm_of thy t) |
62 |> prop_of |> Logic.dest_equals |> snd |
62 |> prop_of |> Logic.dest_equals |> snd |
63 |
63 |
318 |> fold_rev (implies_intr o cprop_of) C_hyps |
318 |> fold_rev (implies_intr o cprop_of) C_hyps |
319 |> fold_rev (forall_intr o cert o Free) ws |
319 |> fold_rev (forall_intr o cert o Free) ws |
320 |
320 |
321 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |
321 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |
322 |> Goal.init |
322 |> Goal.init |
323 |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum_cases})) |
323 |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) |
324 THEN CONVERSION ind_rulify 1) |
324 THEN CONVERSION ind_rulify 1) |
325 |> Seq.hd |
325 |> Seq.hd |
326 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |
326 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |
327 |> Goal.finish |
327 |> Goal.finish |
328 |> implies_intr (cprop_of branch_hyp) |
328 |> implies_intr (cprop_of branch_hyp) |