src/HOL/Library/Efficient_Nat.thy
changeset 35625 9c818cab0dd0
parent 34944 970e1466028d
child 35689 c3bef0c972d7
equal deleted inserted replaced
35624:c4e29a0bb8c1 35625:9c818cab0dd0
   179       (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
   179       (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
   180     fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
   180     fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
   181       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   181       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   182       | find_var _ = NONE;
   182       | find_var _ = NONE;
   183     fun find_thm th =
   183     fun find_thm th =
   184       let val th' = Conv.fconv_rule ObjectLogic.atomize th
   184       let val th' = Conv.fconv_rule Object_Logic.atomize th
   185       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   185       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   186   in
   186   in
   187     case get_first find_thm thms of
   187     case get_first find_thm thms of
   188       NONE => thms
   188       NONE => thms
   189     | SOME ((th, th'), (Sucv, v)) =>
   189     | SOME ((th, th'), (Sucv, v)) =>
   190         let
   190         let
   191           val cert = cterm_of (Thm.theory_of_thm th);
   191           val cert = cterm_of (Thm.theory_of_thm th);
   192           val th'' = ObjectLogic.rulify (Thm.implies_elim
   192           val th'' = Object_Logic.rulify (Thm.implies_elim
   193             (Conv.fconv_rule (Thm.beta_conversion true)
   193             (Conv.fconv_rule (Thm.beta_conversion true)
   194               (Drule.instantiate' []
   194               (Drule.instantiate' []
   195                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   195                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   196                    abstract_over (Sucv,
   196                    abstract_over (Sucv,
   197                      HOLogic.dest_Trueprop (prop_of th')))))),
   197                      HOLogic.dest_Trueprop (prop_of th')))))),