equal
deleted
inserted
replaced
54 |
54 |
55 val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq}; |
55 val Suc_if_eq = Thm.incr_indexes 1 @{thm Suc_if_eq}; |
56 |
56 |
57 fun remove_suc ctxt thms = |
57 fun remove_suc ctxt thms = |
58 let |
58 let |
59 val thy = Proof_Context.theory_of ctxt; |
|
60 val vname = singleton (Name.variant_list (map fst |
59 val vname = singleton (Name.variant_list (map fst |
61 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
60 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
62 val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
61 val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT)); |
63 val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of; |
62 val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of; |
64 val rhs_of = snd o Thm.dest_comb o Thm.cprop_of; |
63 val rhs_of = snd o Thm.dest_comb o Thm.cprop_of; |
65 fun find_vars ct = (case Thm.term_of ct of |
64 fun find_vars ct = (case Thm.term_of ct of |
66 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
65 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
67 | _ $ _ => |
66 | _ $ _ => |