597 val t = parse_patt thy "t_t is_polyexp"; |
597 val t = parse_patt thy "t_t is_polyexp"; |
598 val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^ |
598 val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^ |
599 " matchsub (?a + (?b - ?c)) t_t | " ^ |
599 " matchsub (?a + (?b - ?c)) t_t | " ^ |
600 " matchsub (?a - (?b + ?c)) t_t | " ^ |
600 " matchsub (?a - (?b + ?c)) t_t | " ^ |
601 " matchsub (?a + (?b - ?c)) t_t )"); |
601 " matchsub (?a + (?b - ?c)) t_t )"); |
|
602 show_types := true; |
602 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
603 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
603 then () else error "polyminus.sml type-structure of \"?a :: real\" changed"; |
604 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; |
604 show_types := false; |
|
605 |
|
606 "===== deconstruct datatype typ ==="; |
|
607 val str = "?a"; |
|
608 val t = (thy, str) |>> thy2ctxt |
|
609 |-> ProofContext.read_term_pattern |
|
610 |> numbers_to_string; |
|
611 val Var (("a", 0), ty) = t; |
|
612 val TVar ((str, i), srt) = ty; |
|
613 if str = "'a" andalso i = 1 andalso srt = [] then () |
|
614 else error "termC.sml type-structure of \"?a\" changed"; |
|
615 |
|
616 "----- real type in pattern ---"; |
|
617 val str = "?a :: real"; |
|
618 val t = (thy, str) |>> thy2ctxt |
|
619 |-> ProofContext.read_term_pattern |
|
620 |> numbers_to_string; |
|
621 val Var (("a", 0), ty) = t; |
|
622 val Type (str, tys) = ty; |
|
623 if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT then () |
|
624 else error "termC.sml type-structure of \"?a :: real\" changed"; |
|
625 |
|
626 "===== Not (matchsub (?a + (?b + ?c)) t_t |... ==="; |
|
627 val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^ |
|
628 " matchsub (?a + (?b - ?c)) t_t | " ^ |
|
629 " matchsub (?a - (?b + ?c)) t_t | " ^ |
|
630 " matchsub (?a + (?b - ?c)) t_t )"); |
|
631 "----- read_term_pattern ---"; |
|
632 val t = (thy, str) |>> thy2ctxt |
|
633 |-> ProofContext.read_term_pattern |
|
634 |> numbers_to_string; |
|
635 show_types := true; |
|
636 val t1 = typ_a2real t; |
|
637 if term2str t1 = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
|
638 then () else error "termC.sml type-structure of \"?a :: real\" changed expl"; |
|
639 show_types := false; |
605 show_types := false; |
640 |
606 |
641 (*========== inhibit exn ======================================================= |
607 (*========== inhibit exn ======================================================= |
642 ============ inhibit exn =====================================================*) |
608 ============ inhibit exn =====================================================*) |
643 |
609 |