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