|
1 (* tests on Scripts/term_G.sml |
|
2 author: Walther Neuper |
|
3 051006, |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"../smltest/Scripts/term_G.sml"; |
|
7 use"term_G.sml"; |
|
8 *) |
|
9 "-----------------------------------------------------------------"; |
|
10 "table of contents -----------------------------------------------"; |
|
11 "-----------------------------------------------------------------"; |
|
12 "----------- inst_bdv --------------------------------------------"; |
|
13 "----------- subst_atomic_all ------------------------------------"; |
|
14 "----------- Pattern.match ---------------------------------------"; |
|
15 "-----------------------------------------------------------------"; |
|
16 "-----------------------------------------------------------------"; |
|
17 "-----------------------------------------------------------------"; |
|
18 |
|
19 |
|
20 "----------- inst_bdv --------------------------------------------"; |
|
21 "----------- inst_bdv --------------------------------------------"; |
|
22 "----------- inst_bdv --------------------------------------------"; |
|
23 if string_of_thm (num_str d1_isolate_add2) = |
|
24 "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then () |
|
25 else raise error "term_G.sml d1_isolate_add2"; |
|
26 val subst = [(str2term "bdv", str2term "x")]; |
|
27 val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2); |
|
28 val t' = inst_bdv subst t; |
|
29 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () |
|
30 else raise error "term_G.sml inst_bdv 1"; |
|
31 |
|
32 if string_of_thm (num_str separate_bdvs_add) = |
|
33 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\ |
|
34 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then () |
|
35 else raise error "term_G.sml separate_bdvs_add"; |
|
36 val subst = [(str2term"bdv_1",str2term"c"), |
|
37 (str2term"bdv_2",str2term"c_2"), |
|
38 (str2term"bdv_3",str2term"c_3"), |
|
39 (str2term"bdv_4",str2term"c_4")]; |
|
40 val t = (norm o #prop o rep_thm) (num_str separate_bdvs_add); |
|
41 val t' = inst_bdv subst t; |
|
42 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ |
|
43 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () |
|
44 else raise error "term_G.sml inst_bdv 2"; |
|
45 |
|
46 |
|
47 "----------- subst_atomic_all ------------------------------------"; |
|
48 "----------- subst_atomic_all ------------------------------------"; |
|
49 "----------- subst_atomic_all ------------------------------------"; |
|
50 val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))"; |
|
51 val env = [(str2term"vs_::real list",str2term"[c, c_2]"), |
|
52 (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")]; |
|
53 val (all_Free_subst, t') = subst_atomic_all env t; |
|
54 if all_Free_subst andalso |
|
55 term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
|
56 else raise error "term_G.sml subst_atomic_all should be 'true'"; |
|
57 |
|
58 |
|
59 val (all_Free_subst, t') = subst_atomic_all (tl env) t; |
|
60 if not all_Free_subst andalso |
|
61 term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
|
62 else raise error "term_G.sml subst_atomic_all should be 'false'"; |
|
63 |
|
64 |
|
65 "----------- Pattern.match ---------------------------------------"; |
|
66 "----------- Pattern.match ---------------------------------------"; |
|
67 "----------- Pattern.match ---------------------------------------"; |
|
68 val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1"; |
|
69 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c"; |
|
70 (* !^^^^^^^^!... necessary for Pattern.match*) |
|
71 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t); |
|
72 (*val insts = |
|
73 ([], |
|
74 [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")), |
|
75 (("a",0),Free ("3","RealDef.real"))]) |
|
76 : (indexname * typ) list * (indexname * term) list*) |
|
77 |
|
78 "----- throws exn MATCH..."; |
|
79 val t = str2term "x"; |
|
80 (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) |
|
81 handle MATCH => ([(* (Term.indexname * Term.typ) *)], |
|
82 [(* (Term.indexname * Term.term) *)]); |