# [isabelle] Using Simplifier.asm_rewrite

```I am trying to use asm_rewrite to simplify a term f(u,v,w) under some
assumptions p(u,v,w). p and f are given as a pair (p,f) and p and f have
the same domain type. For this I construct in ML the term
"p(u,v,w) ==> Aux_Var = f(u,v,w)".

In my test f(u,v,w) = ((if u + v < 10 then w else w + 1) + 2)
and p(u,v,w) = (u + v < 10), and the goal is to simplify
f to f(u,v,w) = w + 2 under the assumption p(u,v,w).

If I define in ML

val pair_a = @{term "(term for p, term for f)"};

and I apply the procedure described above all works well,
however if instead I define the pair as the right hand
side of a definition that contains the same term for the
pair, the simplification does not work. The "if" term stays
unsimplified

val pair_b =  Thm.term_of (Thm.rhs_of ( @{thm Test_Pair_def}));

The only difference between pair_a and pair_b seems to be the
types. In pair_a there are simple type variables, while in pair_b
there are schematic type variables.

Attached is the theory with the ML function implementing this
simplification. At the end it defines two variables simp_a_th
simp_b_th holding the simplifications of the two terms
pair_a and pair_b. In pair_a "if" is simplified, while in pair_b
"if" is not simplified. It works the same in Isabelle2015 and
also Isabelle2016-RC3.

Why is this difference? Is it possible to get the same simplification
result also on the pair_b term?

Best regards,

Viorel Preoteasa
```
```theory TestAsmRewrite imports Main
begin
ML{*
fun mk_funT t t' = (Type ("fun", [t, t']));
fun mk_prop t = (Const ("HOL.Trueprop", mk_funT HOLogic.boolT Term.propT)) \$ t;
fun mk_imp s t =  Const ("Pure.imp", mk_funT Term.propT (mk_funT Term.propT Term.propT)) \$ s \$ t;

fun change_type (Free (x, _)) typ = Free (x, typ)

fun is_tuple (Const ("Product_Type.Pair", _) \$ _ \$ _) = true
| is_tuple _ = false;

fun zip l1 l2 = case l1 of
[] => (case l2 of [] => [])
| h::t => case l2 of h1::t1 => (h,h1)::(zip t t1);

fun distribute_types (trm, typ) =
if (is_tuple trm) then
HOLogic.mk_tuple (List.map distribute_types (zip (HOLogic.strip_tuple trm) (HOLogic.strip_tupleT typ)))
else
change_type trm typ;

*}

definition "Test_Pair \<equiv> ((\<lambda> (x::'a::{numeral,ord}, y, z::'b) . x + y < 10), (\<lambda> (x::'a, y, z::'b::numeral) . (if x + y < 10 then z else z + 1) + 2))"

ML{*
val T = @{typ "'a \<Rightarrow> 'b"};
val ctxt = @{context};
val pair_a =  @{term "((\<lambda> (x::'a::{numeral,ord}, y, z::'b) . x + y < 10), (\<lambda> (x::'a, y, z::'b::numeral) . (if x + y < 10 then z else z + 1) + 2))"};
val pair_b =  Thm.term_of (Thm.rhs_of ( @{thm Test_Pair_def}));

fun simp_pair pair =
let
val _ \$ prec \$ func =  pair;
val input_type = fst (dest_funT (type_of prec))
val ouput_type = snd (dest_funT (type_of func))
val aux_var = (Free("Aux_Var", ouput_type));
val vars = @{term "(u,v,w)"};
val input_vars = distribute_types (vars, input_type);
val prec_simp = Simplifier.rewrite ctxt (Thm.cterm_of ctxt (prec \$ input_vars));
val T1 = Thm.term_of (Thm.rhs_of prec_simp);
val T2 = HOLogic.mk_eq(aux_var, func \$ input_vars);
val T3 = mk_imp (mk_prop T1) (mk_prop T2)
val simp_pair_th = Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt T3);
in
simp_pair_th
end

val simp_a_th = simp_pair pair_a;
val simp_b_th = simp_pair pair_b;
*}

end

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.