1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 13 18:37:24 2020 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 14 12:39:26 2020 +0200
1.3 @@ -17,9 +17,7 @@
1.4 "----------- fun app_rev, Rrls, -------------------------";
1.5 "----------- 2011 thms with axclasses -------------------";
1.6 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.7 -"----------- fun assoc_thm' -----------------------------";
1.8 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.9 -"----------- fun mk_thm ------------------------------------------------------------------------";
1.10 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.11 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.12 "--------------------------------------------------------";
1.13 @@ -682,27 +680,6 @@
1.14 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
1.15
1.16
1.17 -"----------- fun assoc_thm' -----------------------------";
1.18 -"----------- fun assoc_thm' -----------------------------";
1.19 -"----------- fun assoc_thm' -----------------------------";
1.20 -val thy = @{theory ProgLang}
1.21 -
1.22 -val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
1.23 -if string_of_thm' thy tth = "6 = 2 * 3" then ()
1.24 -else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
1.25 -
1.26 -val tth = assoc_thm' thy ("add_0_left","");
1.27 -if string_of_thm' thy tth = "0 + ?a = ?a" then ()
1.28 -else error "assoc_thm' (add_0_left,\"\") changed";
1.29 -
1.30 -val tth = assoc_thm' thy ("sym_add_0_left","");
1.31 -if string_of_thm' thy tth = "?t = 0 + ?t" then ()
1.32 -else error "assoc_thm' (sym_add_0_left,\"\") changed";
1.33 -
1.34 -val tth = assoc_thm' thy ("add_commute","");
1.35 -if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
1.36 -else error "assoc_thm' (add_commute,\"\") changed"
1.37 -
1.38 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.39 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.40 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.41 @@ -723,72 +700,6 @@
1.42 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
1.43 else error "Pattern.match CHANGED";
1.44
1.45 -"----------- fun mk_thm ------------------------------------------------------------------------";
1.46 -"----------- fun mk_thm ------------------------------------------------------------------------";
1.47 -"----------- fun mk_thm ------------------------------------------------------------------------";
1.48 -val thy = @{theory Isac_Knowledge}
1.49 -
1.50 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.51 -val thm = @{thm realpow_twoI};
1.52 -val patt_str = "?r ^^^ 2 = ?r * ?r";
1.53 -val term_str = "r ^^^ 2 = r * r";
1.54 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.55 -case parse_patt thy patt_str of
1.56 - Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
1.57 - (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
1.58 -| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
1.59 -case parse thy term_str of
1.60 - NONE => ()
1.61 -| _ => writeln "parse does NOT take patterns with '?'";
1.62 -
1.63 -val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
1.64 -if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.65 -
1.66 -val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
1.67 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.68 -
1.69 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
1.70 -(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
1.71 - gives a strange thm*);
1.72 -(*while this..*)
1.73 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
1.74 - ..gives another strange thm; but it is used and works with rewriting: *);
1.75 -
1.76 -val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
1.77 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
1.78 -
1.79 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.80 -val thm = @{thm real_mult_div_cancel2};
1.81 -val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
1.82 -val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
1.83 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.84 -case parse_patt thy patt_str of
1.85 - Const ("Pure.imp", _) $
1.86 - (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
1.87 - (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
1.88 - (Const ("HOL.Trueprop", _) $
1.89 - (Const ("HOL.eq", _) $ _ $ _ )) => ()
1.90 -| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
1.91 -case parse thy term_str of
1.92 - NONE => ()
1.93 -| _ => writeln "parse does NOT take patterns with '?'";
1.94 -
1.95 -val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
1.96 -if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.97 -
1.98 -val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
1.99 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.100 -
1.101 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
1.102 -(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
1.103 - gives a strange thm*);
1.104 -(*while this*)
1.105 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
1.106 - gives another strange thm; but it is used and words with rewriting: *);
1.107 -
1.108 -val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
1.109 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
1.110 -
1.111 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.112 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.113 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";