# Theory Refine_Imperative_HOL.User_Smashing

```theory User_Smashing
imports Pure
begin
(* Alternative flex-flex smasher by Simon Wimmer *)
ML ‹
fun enumerate xs = fold (fn x => fn (i, xs) => (i +1, (x, i) :: xs)) xs (0, []) |> snd
›

ML ‹
fun dummy_abs _ [] t = t
| dummy_abs n (T :: Ts) t = Abs ("x" ^ Int.toString n, T, dummy_abs (n + 1) Ts t)
›

ML ‹
fun common_prefix Ts (t1 as Abs (_, T, t)) (u1 as Abs (_, U, u)) =
if U = T then common_prefix (T :: Ts) t u else ([], t1, u1)
| common_prefix Ts t u = (Ts, t, u);

fun dest_app acc (t \$ u) = dest_app (u :: acc) t
| dest_app acc t = (t, acc);

fun add_bound (Bound i, n) bs = (i, n) :: bs
| add_bound _ bs = bs;
›

ML ‹
fun smash_pair ctxt thm (t, u) =
let
val idx = Thm.maxidx_of thm + 1;
val ctxt' = ctxt;
val (Ts, t1, _) = common_prefix [] t u;
val (tas, t2) = Term.strip_abs t;
val (uas, u2) = Term.strip_abs u;
val (tx as Var (_, T1), ts) = Term.strip_comb t2;
val (ux as Var (_, U1), us) = Term.strip_comb u2;
val Ts1 = Term.binder_types T1;
val Us1 = Term.binder_types U1;
val T = Term.fastype_of1 (Ts, t1);
val tshift = length tas - length Ts;
val ushift = length uas - length Ts;
val tbs = fold add_bound (enumerate (rev ts)) [] |> map (apfst (fn i => i - tshift));
val ubs = fold add_bound (enumerate (rev us)) [] |> map (apfst (fn i => i - ushift));
val bounds = inter (op =) (map fst tbs) (map fst ubs) |> distinct (=);
val T' = map (nth Ts) bounds ---> T;
val v = Var (("simon", idx), T');
val tbs' = map (fn i => find_first (fn (j, _) => i = j) tbs |> the |> snd |> Bound) bounds;
val t' = list_comb (v, tbs') |> dummy_abs 0 Ts1;
(* Need to add bounds for superfluous abstractions here *)
val ubs' = map (fn i => find_first (fn (j, _) => i = j) ubs |> the |> snd |> Bound) bounds;
val u' = list_comb (v, ubs') |> dummy_abs 0 Us1;
val subst = [(Term.dest_Var tx, Thm.cterm_of ctxt' t'), (Term.dest_Var ux, Thm.cterm_of ctxt' u')];
in
instantiate_normalize (TVars.empty, Vars.make subst) thm
end;
fun smash ctxt thm =
case (Thm.tpairs_of thm) of
[] => thm
| (p :: _) => smash_pair ctxt thm p;
fun smashed_attrib ctxt thm =
(NONE, SOME (smash ctxt thm));
›

ML ‹
val smash_new_rule = Seq.single oo smash;
›

end
```