[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.