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')))))), |