equal
deleted
inserted
replaced
125 let |
125 let |
126 |
126 |
127 fun remove_suc thy thms = |
127 fun remove_suc thy thms = |
128 let |
128 let |
129 val vname = Name.variant (map fst |
129 val vname = Name.variant (map fst |
130 (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
130 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; |
131 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
131 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
132 fun lhs_of th = snd (Thm.dest_comb |
132 fun lhs_of th = snd (Thm.dest_comb |
133 (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); |
133 (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); |
134 fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); |
134 fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); |
135 fun find_vars ct = (case term_of ct of |
135 fun find_vars ct = (case term_of ct of |
178 end; |
178 end; |
179 |
179 |
180 fun remove_suc_clause thy thms = |
180 fun remove_suc_clause thy thms = |
181 let |
181 let |
182 val vname = Name.variant (map fst |
182 val vname = Name.variant (map fst |
183 (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
183 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; |
184 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) |
184 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) |
185 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) |
185 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) |
186 | find_var _ = NONE; |
186 | find_var _ = NONE; |
187 fun find_thm th = |
187 fun find_thm th = |
188 let val th' = Conv.fconv_rule ObjectLogic.atomize th |
188 let val th' = Conv.fconv_rule ObjectLogic.atomize th |