22 "----------- 2011 thms with axclasses -------------------"; |
22 "----------- 2011 thms with axclasses -------------------"; |
23 "----------- repair NO asms from rls RatEq_eliminate ----"; |
23 "----------- repair NO asms from rls RatEq_eliminate ----"; |
24 "----------- fun assoc_thm' -----------------------------"; |
24 "----------- fun assoc_thm' -----------------------------"; |
25 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
25 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------"; |
26 "----------- fun mk_thm ------------------------------------------------------------------------"; |
26 "----------- fun mk_thm ------------------------------------------------------------------------"; |
|
27 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------"; |
27 "--------------------------------------------------------"; |
28 "--------------------------------------------------------"; |
28 "--------------------------------------------------------"; |
29 "--------------------------------------------------------"; |
29 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
30 |
31 |
31 |
32 |
652 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm |
653 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm |
653 gives another strange thm; but it is used and words with rewriting: *); |
654 gives another strange thm; but it is used and words with rewriting: *); |
654 |
655 |
655 val t1' = (#prop o Thm.rep_thm) (num_str thm_made); |
656 val t1' = (#prop o Thm.rep_thm) (num_str thm_made); |
656 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string"; |
657 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string"; |
|
658 |
|
659 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------"; |
|
660 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------"; |
|
661 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------"; |
|
662 (* norm_equation is defined in Test.thy, other rls see Knowledg/**) |
|
663 val thy = @{theory}; |
|
664 val rls = norm_equation; |
|
665 val term = str2term "x + 1 = 2"; |
|
666 |
|
667 val SOME (t, asm) = rewrite_set_ thy false rls term; |
|
668 if term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED"; |
|
669 |
|
670 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term); |
|
671 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term); |