1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  "----------- 2011 thms with axclasses -------------------";
     1.5  "----------- repair NO asms from rls RatEq_eliminate ----";
     1.6  "----------- fun assoc_thm' -----------------------------";
     1.7 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -566,3 +567,22 @@
    1.12  if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
    1.13  else error "assoc_thm' (add_commute,\"\") changed"
    1.14  
    1.15 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
    1.16 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
    1.17 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
    1.18 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
    1.19 +  (@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
    1.20 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
    1.21 +  (thy, 1, [], rew_ord, erls, bool, thm, term);
    1.22 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
    1.23 +  (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
    1.24 +     val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
    1.25 +     val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
    1.26 +     val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
    1.27 +     val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
    1.28 +;
    1.29 +if term2str lhss = "?a * (?b + ?c)" andalso term2str t = "x * (y + z)" then ()
    1.30 +else error "ARGS FOR Pattern.match CHANGED";
    1.31 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
    1.32 +if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
    1.33 +  else error "Pattern.match CHANGED";